Skip to content
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.

Sign up for GitHub

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

Jump to bottom

README: clarify line about .olean files #129

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

README: clarify line about .olean files #129

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion readme.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,8 @@ rm -rf _target
leanproject up
```

Make sure that olean files are generated for mathlib in `_target`, otherwise this will be extremely slow.
Make sure that [`.olean` files](https://github.com/leanprover/tutorial/blob/master/05_Interacting_with_Lean.org#projects)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We most likely don't want to link to that tutorial which is very out of date. It's better to link to the community webpage on leanproject.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, I can remove the link — just changing from "olean files" to ".olean files" already helps making things a little clearer, IMO. I could replace the link with https://leanprover-community.github.io/leanproject.html instead, but I don't think that page (in its current state) provides the information one would expect when clicking on the expression ".olean files" (i.e. additional details on what .olean files are).

That said, depending on the outcome of the conversation at leanprover-community/leanprover-community.github.io#180, it could make sense to add the link here. I'd suggest holding this PR until that one is resolved, so we can decide what makes the most sense here.

are generated for mathlib in `_target`, otherwise this will be extremely slow.

## Usage

Expand Down