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

lake build modifies manifest #137

Closed
gebner opened this issue Nov 21, 2022 · 3 comments
Closed

lake build modifies manifest #137

gebner opened this issue Nov 21, 2022 · 3 comments
Labels
bug Something isn't working
Milestone

Comments

@gebner
Copy link
Member

gebner commented Nov 21, 2022

This causes a build failure in mathport:

git clone https://github.com/leanprover-community/mathport
cd mathport
git checkout f071992a732b95d49b75111dfbdd9cdd9cd371dc
lake print-paths  # lake build works too but takes longer and fails
git diff          # shows modified manifest.json!
@gebner
Copy link
Member Author

gebner commented Nov 21, 2022

I think this happens because aesop and mathlib4 reference different revisions of std4 in their manifests.

@tydeu tydeu added the bug Something isn't working label Nov 21, 2022
@tydeu
Copy link
Member

tydeu commented Nov 21, 2022

Yeah, I think your interpretation is correct. I believe this is thus the same root problem as #70.

@tydeu
Copy link
Member

tydeu commented Nov 25, 2022

Fixed by #138 (not sure why GitHub did not automatically close it already).

@tydeu tydeu closed this as completed Nov 25, 2022
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