Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

lake update does not always update #94

Closed
Kha opened this issue Jul 3, 2022 · 3 comments
Closed

lake update does not always update #94

Kha opened this issue Jul 3, 2022 · 3 comments
Labels
bug Something isn't working
Milestone

Comments

@Kha
Copy link
Member

Kha commented Jul 3, 2022

I was trying to move the LeanInk test suite to the new Lake format:

~/lean/LeanInk/test/dep $ cat lakefile.lean
import Lake
open Lake DSL

package dep

require mathlib from git "https://github.com/leanprover-community/mathlib4.git"

lean_lib dep

~/lean/LeanInk/test/dep $ lake update
error: ./lean_packages/mathlib/./lakefile.lean:9:18: error: unknown constant 'Lake.PackageFacet.oleans'
error: package configuration `./lean_packages/mathlib/./lakefile.lean` has errors

~/lean/LeanInk/test/dep $ git -C lean_packages/mathlib rev-parse @
84ca33e940678954dc146f732f447ddc8984cf39  # old!

~/lean/LeanInk/test/dep $ nix shell nixpkgs#elan -c lake --version
Lake version 3.2.0 (Lean version 4.0.0-nightly-2022-07-03)

~/lean/LeanInk/test/dep $ rm -rf lean_packages/

~/lean/LeanInk/test/dep $ lake update
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to ./lean_packages/mathlib

~/lean/LeanInk/test/dep $ git -C lean_packages/mathlib rev-parse @
ecd37441047e490ff2ad339e16f45bb8b58591bd

I'm not completely sure what's happening, does it decide not to update the dep or does it try to parse the dep's lakefile before deciding whether to update it?

@Kha
Copy link
Member Author

Kha commented Jul 3, 2022

The old lean_packages, before deleting it, probably did not have a manifest.json yet. If that's the problem, this issue can probably be ignored as the bug will fix itself with time.

@tydeu
Copy link
Member

tydeu commented Jul 4, 2022

@Kha, I'm confused -- is this or is this not a reproducible bug?

@Kha
Copy link
Member Author

Kha commented Jul 4, 2022

Yes, it should be reproducible by replaying LeanInk's history

$ git checkout 0a160d91458c1873937449a7c78d25b34b8686df
$ cd test/dep
$ lake build  # checks out old mathlib, does not create manifest.json
$ git checkout 4b5e606ea8cc54c2447ce48706f8ec1d133d19e9
$ git rm lean_packages/manifest.json  # restore state before successful `lake update`
$ lake update  # as above

Restoring the manifest.json leads to another unexpected error:

$ lake update
info: mathlib: updating ./lean_packages/mathlib
error: stdout:

stderr:
You are not currently on a branch.
Please specify which branch you want to rebase against.
See git-pull(1) for details.

    git pull <remote> <branch>
error: git exited with code 1

I don't think the branch state of the current checkout should matter. However, after switching to mathlib's master, everything works as expected, so it seems the issue really was the lack of manifest.json resulting from the Lake version transition.

@tydeu tydeu added the bug Something isn't working label Jul 4, 2022
@tydeu tydeu added this to the v3.2.1 milestone Jul 5, 2022
@tydeu tydeu closed this as completed in c4b1b93 Jul 5, 2022
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants