mathlib workflow

Stream: new members

[Ashley Blacquiere]

I keep running into excessive memory consumption errors, and I've been unable to find a fix after scrolling through ZulipChat for a while, so I think maybe something about my workflow is incorrect: In short, I'm working on a mathlib project with some minor edits to algebra/groups/defs.lean. Is the following correct?

1. I cloned mathlib using leanproject get mathlib - is this the right approach?
2. After making some edits to algebra/group/defs.lean I shut down VS Code and rebuilt the olean using lean --make src/alegbra/group.defs.lean - is this the right approach?

I've done the above and a number of other trouble-shooting steps I found in ZulipChat, but I still get an orange bar, then eventually a lot of "excessive memory consumption detected at 'expression traversal'" errors. For reference, git status and leanproject check look fine. What am I doing wrong? :thinking:

[Kevin Buzzard]

The file you're editing is really high up in the import heirarchy, so the moment you edit it, hundreds of later files which import this file either directly or indirectly need to be recompiled. Chaos hence ensues (it would take about 2 hours on a regular machine to recompile all the files).

[Kevin Buzzard]

If you're absolutely sure you want to be editing this file (e.g. you want to make a PR to this file) then I would recommend closing all other files and then closing and re-opening VS Code.

[Kevin Buzzard]

A1: yes it's correct. A2: the command you posted seems to have a typo but if you meant lean --make src/algebra/group/defs.lean then this will only recompile that one file, and not all of the hundreds of files which depend on it and also need to be recompiled.

[Kevin Buzzard]

You might want to un- #xy by explaining why you want to edit such a fundamental file. Can you get away with leaving the file alone and just adding the things you want to add in a different file?

[Ashley Blacquiere]

Fair points. Probably there is a way to edit a different file to get a similar result. I've been working on learning meta programming, and in particular for a project that involves creating a term rewriter for commutative groups. As part of this I've been exploring abel, but learned recently that there have been some bugs reported. So as part of trying to better understand both abel and metaprogramming I've been debugging issue 8456. I've made some progress, but wanted to test some potential ideas I had for fixes, which seemed to necessitate editing algebra/group/defs.lean.

[Ashley Blacquiere]

But, ya, the small changes that I've made could probably be added elsewhere. I'm basically just adding a typeclass instance to the file, so that could probably be handled in another way.

[Kevin Buzzard]

Oh if you're only adding a typeclass as opposed to deleting or changing stuff then your life would be a lot easier if you just added it in another file. I should say I don't know much at all about tactics. Another possibility is to be very clear about which files you're using (maybe just tactic.abel and algebra.group.defs?) and then make sure that on the blue line at the bottom of VS Code it says "checking visible files" rather than "checking project files" , and make sure you have no other mathlib files open, and then edit algebra.group.defs, and then close VS Code and on the command line just recompile those two files with lean --make, and you will hopefully be able to get away with it.

[Kevin Buzzard]

PS it has oft been pointed out that abel doesn't work for abelian multiplicative groups! I don't have a clue how easy this would be to implement though, I'm a mathematician.

[Ashley Blacquiere]

Kevin Buzzard said:

Another possibility is to be very clear about which files you're using (maybe just tactic.abel and algebra.group.defs?) and then make sure that on the blue line at the bottom of VS Code it says "checking visible files" rather than "checking project files"

Yup, just have 'checking visible files' on.

and make sure you have no other mathlib files open, and then edit algebra.group.defs, and then close VS Code and on the command line just recompile those two files with lean --make, and you will hopefully be able to get away with it.

Is that any different from what I said about about using lean --make src/algebra/group/defs.lean? Just for clarity - in case I'm missing something...

[Kevin Buzzard]

You also need to compile src/tactic/abel.lean. I have no idea how long this will take but I am cautiously optimistic that it won't be too long.

[Kevin Buzzard]

Hmm I dunno though, tactic.abel imports tactic.norm_num which imports stuff from data.rat which imports loads of data.int which imports algebra.char_zero which imports...

[Kevin Buzzard]

This is probably your problem.

[Ashley Blacquiere]

Yes, that seems likely...

[Ashley Blacquiere]

Will try adding the typeclass elsewhere and see if that gets me anywhere. Thanks for the help!

[Kevin Buzzard]

Yeah, abel is importing all of field theory which will all need to be recompiled if you edit the file containing the definition of a group.

[Kevin Buzzard]

Of course one might also ask why this is! But I'm not the person to answer this.

[Yakov Pechersky]

If you're just testing new lemmas and defs and instances, I'd do them in a new file like Kevin suggested. If you're editing abel, you can then add your new file to the list of imports.

[Eric Rodriguez]

Yeah, what I often do is work on a new file until the very last moment possible, and pile everything in there. Working within mathlib files directly can be fairly frustrating... one thing that is helpful is just keeping on restarting the server, or turning off checking whilst typing

[Eric Rodriguez]

it'd be nice if we had a feature like Coq where you can turn on a mode that only runs Lean when you press a specific keybind

[Arthur Paulino]

Eric Rodriguez said:

it'd be nice if we had a feature like Coq where you can turn on a mode that only runs Lean when you press a specific keybind

The Coq IDE also has a feature that allows you to have full control over the code you want to process. It's very useful when I'm trying to prove something in the beginning of a module that was already fully verified (and correct)

[Kevin Buzzard]

I just dump an #exit under my work when I'm goofing around at the top of a large file

[Eric Rodriguez]

ooh, that's a nice tip