Zulip Chat Archive

Stream: new members

Topic: emacs lean mathlib


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Nicolás Ojeda Bär (Oct 13 2019 at 20:34):

I think you can try with C-c C-b

view this post on Zulip Nicolás Ojeda Bär (Oct 13 2019 at 20:34):

M-x lean-message-boxes-toggle

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Oct 13 2019 at 20:46):

https://github.com/leanprover-community/mathlib-nightly/releases

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Oct 13 2019 at 20:48):

Oh, you mean compiling Lean, not mathlib!

view this post on Zulip 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-mathlib script 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

view this post on Zulip Patrick Massot (Oct 13 2019 at 20:48):

mathlib is the math library, compiled by Lean.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 13 2019 at 20:50):

You are really choosing the hard way if you build Lean.

view this post on Zulip Patrick Massot (Oct 13 2019 at 20:50):

Maybe we already had that conversation, there are so many new people those days...

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 13 2019 at 20:52):

OS?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Oct 13 2019 at 20:59):

Maybe https://github.com/leanprover-community/mathlib/tree/master/src/data/int then?

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Oct 13 2019 at 21:08):

Very simple proofs are directly given as proof terms, so there is nothing to step through.

view this post on Zulip Patrick Massot (Oct 13 2019 at 21:08):

And I know nothing about emacs.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 13 2019 at 21:12):

This story of proof terms vs stepable proofs is explained there.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 #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.

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.

view this post on Zulip Alex J. Best (Oct 13 2019 at 21:24):

Wow, didn't know this, this is much easier, thanks!

view this post on Zulip Jesse Michael Han (Oct 13 2019 at 21:29):

hole command in emacs is C-c SPC

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Oct 14 2019 at 01:15):

Yeah, that would work! We would need to make them easy to find.

view this post on Zulip Mario Carneiro (Oct 14 2019 at 01:22):

I thought we were already doing this?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Oct 14 2019 at 01:26):

There's this on the Github wiki.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Oct 14 2019 at 02:13):

This was why I suggested that embedding them in mathlib itself might be possible.

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Oct 14 2019 at 02:18):

How does one find that page?

view this post on Zulip Mario Carneiro (Oct 14 2019 at 02:19):

we don't use the wiki much, so I didn't think to look there

view this post on Zulip Simon Hudon (Oct 14 2019 at 02:20):

We could reference it in the README.md file or move it to the docs directory

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: May 09 2021 at 18:17 UTC