doc: add tips about lake usage #510
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
joneugster
changed the title
grunweg
reviewed
Aug 5, 2024
Co-authored-by: grunweg <[email protected]>
|
Thank you @grunweg for the review! I completely forgot this PR, but now I've addressed all your suggestions |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adding some notes about custom setups that are possible with a
lakefile.lean, in particular how to use a single sharedmathlibin multiple projects.This might be useful for people with little disk space as well as for teaching setups where it might be reasonable to have a single
mathlibon a shared drive and then have students reference this instead of downloading their own copy.