-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
doc(*): switch from update-mathlib to leanproject #2093
Conversation
Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
This PR should only be merged once @PatrickMassot has pushed the mathlibtools release to pypi. |
docs/install/project.md
Outdated
@@ -11,10 +11,10 @@ terminal. | |||
* Then go to a folder where you want to create a project in a subfolder | |||
`my_project`, and type: | |||
```bash | |||
leanpkg new my_project | |||
leanpkg +leanprover-community/lean:3.6.1 new my_project |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is outdated. The new workflow is leanproject new my_project
, nothing else.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sweet.
- You can do this by running the following commands (anywhere in the `mathlib` repository). | ||
5. You can use `leanproject get-cache` to fetch `.olean` binaries. | ||
The `.olean` binaries take two hours to generate, so they might not yet be available if you're on the master branch. | ||
If you checkout the remote branch `lean-3.6.1` then you can always get olean binaries: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Unfortunately this is not yet true, this is why I didn't want to merge.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The oleans should always be available for lean-3.6.1
because we first push them to azure before updating the branch. It's only master
and feature branches that lag behind.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
They are now available within ~30 seconds, unless the most recent commit came from a PR from a fork.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The part about using an existing project is outdated. The new workflow is leanproject get tutorials
. You can replace tutorials with github_user/project or even a full git url.
Sweet. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Now that leanproject
has landed, we should get this finished and merged!
- You can do this by running the following commands (anywhere in the `mathlib` repository). | ||
5. You can use `leanproject get-cache` to fetch `.olean` binaries. | ||
The `.olean` binaries take two hours to generate, so they might not yet be available if you're on the master branch. | ||
If you checkout the remote branch `lean-3.6.1` then you can always get olean binaries: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
They are now available within ~30 seconds, unless the most recent commit came from a PR from a fork.
@robertylewis I'm confused. Does this mean we don't have to wait 1hr for the linter to complete? |
I think this is good to go, but I won't merge since I've done the latest commit. |
oleans are pushed to the server before the linter runs. |
…ty#2093) * doc(*): switch from update-mathlib to leanproject * Apply suggestions from code review Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Use shiny new `leanproject new` and `leanproject get` * documentation tweaks * project.md tweaks Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…ty#2093) * doc(*): switch from update-mathlib to leanproject * Apply suggestions from code review Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Use shiny new `leanproject new` and `leanproject get` * documentation tweaks * project.md tweaks Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list