Zulip Chat Archive
Stream: new members
Topic: emacs lean mathlib
Marijn Stollenga (Oct 13 2019 at 20:23):
I want to play with parts of the mathlib, try to follow some proofs in there. I have lean mode in emacs installed and the mathlib cloned. Can I somehow open all of mathlib and evaluate things there?
Just opening the files doesn't seem to work too well.
Marijn Stollenga (Oct 13 2019 at 20:24):
Hi, can I somehow load mathlib in lean and evaluate expressions in there / follow some proof? I have leanpkg / lean mode installed for emacs. But not sure how to open the source dir of mathlib after cloning.
Nicolás Ojeda Bär (Oct 13 2019 at 20:31):
It should work; make sure to compile everything before starting browsing them: leanpkg build.
Afterwards, you should be able to browse the files in emacs and play with them.
Marijn Stollenga (Oct 13 2019 at 20:32):
Ok I'll try that. Do you also know how to let emacs 'expand' #print commands etc? Now I keep having to move the cursor on them
Nicolás Ojeda Bär (Oct 13 2019 at 20:34):
I think you can try with C-c C-b
Nicolás Ojeda Bär (Oct 13 2019 at 20:34):
M-x lean-message-boxes-toggle
Marijn Stollenga (Oct 13 2019 at 20:45):
Building mathlib takes some time! Is the default build of lean in release? Can I optimize it some more?
Patrick Massot (Oct 13 2019 at 20:46):
https://github.com/leanprover-community/mathlib-nightly/releases
Patrick Massot (Oct 13 2019 at 20:47):
Note that if you followed mathlib installation instructions at https://github.com/leanprover/mathlib then you got the update-mathlib script whose job is to download those pre-compiled mathlib in your projects
Marijn Stollenga (Oct 13 2019 at 20:47):
https://github.com/leanprover-community/mathlib-nightly/releases
Thanks! I was wondering for a local build though! Right now I just cmake - G Ninja the lean/src dir and that seems to work. But I wonder if there are some optimizations
Patrick Massot (Oct 13 2019 at 20:48):
Oh, you mean compiling Lean, not mathlib!
Marijn Stollenga (Oct 13 2019 at 20:48):
Note that if you followed mathlib installation instructions at https://github.com/leanprover/mathlib then you got the
update-mathlibscript whose job is to download those pre-compiled mathlib in your projects
Hmm, I did that so I might have the prebuild ones. Still it seems to take lean quite some time to start evaluating expressions. Like it needs some bootup time
Patrick Massot (Oct 13 2019 at 20:48):
mathlib is the math library, compiled by Lean.
Patrick Massot (Oct 13 2019 at 20:49):
Did you create a project using leanpkg as described in https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md?
Marijn Stollenga (Oct 13 2019 at 20:49):
Oh, you mean compiling Lean, not mathlib!
Yeah I built lean, but also have mathlib and am building it now. I just wanna run through some proofs, see if it helps me make sense of them.
Patrick Massot (Oct 13 2019 at 20:50):
You are really choosing the hard way if you build Lean.
Patrick Massot (Oct 13 2019 at 20:50):
Maybe we already had that conversation, there are so many new people those days...
Patrick Massot (Oct 13 2019 at 20:51):
The supported way described in mathlib install docs does not involve building Lean from source (neither mathlib for that matter).
Marijn Stollenga (Oct 13 2019 at 20:52):
The supported way described in mathlib install docs does not involve building Lean from source (neither mathlib for that matter).
Yeah I tried that first, but it didn't seem to setup lean for my system. No lean / leanpkg anywhere.
Patrick Massot (Oct 13 2019 at 20:52):
OS?
Marijn Stollenga (Oct 13 2019 at 20:54):
OS?
OpenSuse. The mathlib building is done and it seems to work! I can evaluate expressions. Do you know an interesting proof to start with in the mathlib?
Patrick Massot (Oct 13 2019 at 20:55):
There shouldn't be any issue with OpenSuse. Do you have anything like $HOME/.elan and $HOME/.mathlib?
Patrick Massot (Oct 13 2019 at 20:56):
About interesting parts of mathlib, it depends on things you like. Do you come from maths or computer science?
Marijn Stollenga (Oct 13 2019 at 20:57):
About interesting parts of mathlib, it depends on things you like. Do you come from maths or computer science?
Computer science more, but have some slight math background. Maybe the fundamental theory of arithmetic?
Patrick Massot (Oct 13 2019 at 20:59):
Maybe https://github.com/leanprover-community/mathlib/tree/master/src/data/int then?
Marijn Stollenga (Oct 13 2019 at 21:04):
Thanks, will have a look. So it seems easiest to set C-c C-g to see the goals and step through them. Though some proofs seem to be complex single line constructions, in which case you can't really go through the steps? Any tips there?
Patrick Massot (Oct 13 2019 at 21:08):
Very simple proofs are directly given as proof terms, so there is nothing to step through.
Patrick Massot (Oct 13 2019 at 21:08):
And I know nothing about emacs.
Marijn Stollenga (Oct 13 2019 at 21:09):
Very simple proofs are directly given as proof terms, so there is nothing to step through.
Ah makes sense
Patrick Massot (Oct 13 2019 at 21:11):
Note: the recommended path is to read https://leanprover.github.io/theorem_proving_in_lean/, but that's a lot of reading. If you prefer to see code first, and don't fear maths I recommend cloning https://github.com/PatrickMassot/lean-tutorials and stepping through proofs there.
Patrick Massot (Oct 13 2019 at 21:12):
This story of proof terms vs stepable proofs is explained there.
Marijn Stollenga (Oct 13 2019 at 21:13):
Note: the recommended path is to read https://leanprover.github.io/theorem_proving_in_lean/, but that's a lot of reading. If you prefer to see code first, and don't fear maths I recommend cloning https://github.com/PatrickMassot/lean-tutorials and stepping through proofs there.
Thanks! Good pointers.
Alex J. Best (Oct 13 2019 at 21:20):
I think the idea is that if something is a small lemma that is not-so-interesting proof wise it's often given as a term-mode 1-liner sort of thing (but thats not so much of a rule). You can always declare the assumptions of such a lemma/theorem as variables, and then take subterms starting from the innermost and #check them and build up the main term to get a sense of what is happening within the proof. But probably looking through the longer tactic proofs is better to get a sense of things.
Rob Lewis (Oct 13 2019 at 21:22):
I think the idea is that if something is a small lemma that is not-so-interesting proof wise it's often given as a term-mode 1-liner sort of thing (but thats not so much of a rule). You can always declare the assumptions of such a lemma/theorem as variables, and then take subterms starting from the innermost and
#checkthem and build up the main term to get a sense of what is happening within the proof. But probably looking through the longer tactic proofs is better to get a sense of things.
You can also enclose subterms in {! !} and use the hole command that displays the type of a subterm. Afraid I don't know the key to trigger a hole command in emacs though.
Alex J. Best (Oct 13 2019 at 21:24):
Wow, didn't know this, this is much easier, thanks!
Jesse Michael Han (Oct 13 2019 at 21:29):
hole command in emacs is C-c SPC
Floris van Doorn (Oct 13 2019 at 23:57):
Do you know an interesting proof to start with in the mathlib?
This list has some pointers of nice theorems: https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md
Simon Hudon (Oct 14 2019 at 00:44):
It might be interesting to keep a sort of wish list for projects that contributors don't have time to start but that undergraduates, new grad students or simply newcomers could undertake
Scott Morrison (Oct 14 2019 at 01:06):
Yes, I think this would be really great. Partly we can do this via the issues list. I think it would also be pretty reasonable to record these in the code itself, for example in comments marked with TODO and PROJECT.
Simon Hudon (Oct 14 2019 at 01:15):
Yeah, that would work! We would need to make them easy to find.
Mario Carneiro (Oct 14 2019 at 01:22):
I thought we were already doing this?
Mario Carneiro (Oct 14 2019 at 01:23):
Not inline PROJECT tags, but a page of potential project ideas has been proposed (and I think implemented) before
Mario Carneiro (Oct 14 2019 at 01:25):
I can't find it in the mathlib docs any more. Were they removed because they got out of date? @Johan Commelin
Bryan Gin-ge Chen (Oct 14 2019 at 01:26):
There's this on the Github wiki.
Scott Morrison (Oct 14 2019 at 02:13):
The page on the wiki is pretty out of date, which I think is the inevitable fate of any standalone “projects” page.
Scott Morrison (Oct 14 2019 at 02:13):
This was why I suggested that embedding them in mathlib itself might be possible.
Mario Carneiro (Oct 14 2019 at 02:15):
Most new projects will need to be located in their own files though, so they may not fit well with inline comments. Issues seems like a better way to track projects, although it's a bit open ended - there is a near-infinite list of things that have not yet been done in mathlib.
Simon Hudon (Oct 14 2019 at 02:18):
How does one find that page?
Mario Carneiro (Oct 14 2019 at 02:19):
we don't use the wiki much, so I didn't think to look there
Simon Hudon (Oct 14 2019 at 02:20):
We could reference it in the README.md file or move it to the docs directory
Scott Morrison (Oct 14 2019 at 02:33):
I did manage to sneak some TODOs in the file on surreal numbers: https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/surreal.lean#L346
Scott Morrison (Oct 14 2019 at 02:35):
I think these are actually pretty good: someone filling them in would probably be editing that same file, and the TODOs in some sense form part of the documentation.
Scott Morrison (Oct 14 2019 at 02:36):
I think that wiki page should basically be given up for dead; lots has been done!
Last updated: Dec 20 2023 at 11:08 UTC