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

fix: use the correct toolchain in the math template #152

Merged
merged 1 commit into from
Feb 3, 2023

Conversation

arthurpaulino
Copy link
Contributor

Some users might end up with incompatible Lean toolchains when using the math template.

This PR prevents that by cloning mathlib4 and then reading the correct toolchain from lake-packages/mathlib4/lean-toolchain instead of using the default toolchain.

@tydeu tydeu added the enhancement New feature or request label Feb 2, 2023
@tydeu
Copy link
Member

tydeu commented Feb 2, 2023

Thanks for the contribution! While this will get the right lean-toolchain version -- which is great -- it does not properly setup the mathlib package (i.e., write the package to the manifest). Thus, clones of the package will not have the right mathlib pinned and subsequent run of lake build will not properly include mathlib. I would advise taking a look at Load.Main and Load.Materialize and using/adapting the definitions their to build a proper manifest. Does that make sense?

@arthurpaulino
Copy link
Contributor Author

it does properly setup the mathlib package

Did you mean it doesn't?

@tydeu
Copy link
Member

tydeu commented Feb 2, 2023

Did you mean it doesn't?

Oops, yeah that was a typo. I fixed it.

@tydeu
Copy link
Member

tydeu commented Feb 3, 2023

LGTM! Thanks!

@tydeu tydeu merged commit bee120a into leanprover:master Feb 3, 2023
@tydeu tydeu added this to the v4.1.0 milestone Feb 3, 2023
@arthurpaulino arthurpaulino deleted the ap/fix-math-template branch February 3, 2023 09:51
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants