Skip to content

Commit

Permalink
removing lake-manifest should be superfluous
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Dec 7, 2023
1 parent 3689486 commit ef2f1b7
Showing 1 changed file with 1 addition and 5 deletions.
6 changes: 1 addition & 5 deletions server/build.sh
Original file line number Diff line number Diff line change
Expand Up @@ -10,17 +10,13 @@ cd $(dirname $0)
# https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4
# Additionally, we had once problems with the `lake-manifest` when a new dependency got added
# to `mathlib`, therefore we now delete it every time for good measure.
(cd LeanProject &&
rm -f ./lake-manifest.json &&
( cd LeanProject &&
lake update -R &&
lake build)

# note: mathlib has now a post-update hook that modifies the `lean-toolchain`
# and calls `lake exe cache get`. Therefore these two steps are currently superfluous.

# Copy info about new versions to the client.
# ./copy_versions.sh

duration=$SECONDS
echo "Finished in $(($duration / 60)):$(($duration % 60)) min."
echo "Finished in $(($duration / 60)):$(($duration % 60)) min." | logger -t lean4web

0 comments on commit ef2f1b7

Please sign in to comment.