Linear arithmetic tactic

Stream: general

[Rob Dockins]

I'm trying to do some basic proofs/programming involving an abstract syntax for a language that requires some mutual inductive types and indirect recursion. In order to work with these effectively, I need to use well-founded recursion. As a consequence, I really need a tactic for discharging some pretty straightforward theorems of linear arithmetic that arise from reasoning about sizeof-based measure functions.

Up until now, I've been using tactic.linarith from mathlib. However, when including mathlib in my project, I run into persistent problems with lean reporting excessive memory usage errors and the flycheck emacs mode crapping out and disabling itself, and making the editor rather unresponsive. It's unpredictable, but I typically get less than an hour's worth of work done before I have to shutdown my emacs and restart, which is intensely annoying. I haven't found a feasible workaround yet. Running leanpkg build from the command line seems to help for a time, but the problem eventually resurfaces for reasons I don't understand.

So, the questions: is there an alternate linear arithmetic tactic I can use that has a smaller footprint than mathlib? Do other people experience similar problems to the ones I'm describing? How do you deal with them?

[Simon Hudon]

Hi Rob! Right now, every contribution that I know of goes into mathlib. The good news is that there is now a nightly build of mathlib that you can fetch using a script called update-mathlib which you can get by following the instructions here: https://github.com/leanprover-community/mathlib#obtaining-binaries

[Simon Hudon]

It is still a new feature of mathlib so please let us know if you find any issue or if there's a better way it could function.

[Simon Hudon]

Also, a tactic like Coq's omega (also called omega) is in the process of being merged to mathlib so you might be happier with it than with linarith.

[Rob Lewis]

@Simon Hudon I'm not sure that's related. leanpkg build will achieve everything that update-mathlib does (except saving time). If it doesn't fix this issue then update-mathlib won't help.

[Rob Lewis]

@Rob Dockins can you tell if the problem is linarith-specific, or do you think it's more general to mathlib? Just having mathlib loaded/importing files from there shouldn't cause memory issues. If that's what's happening then there's something odd with your setup.

[Simon Hudon]

That is a common issue that building too much of mathlib because of a new import will cause emacs to misbehave. After calling leanpkg build, the issue might resurface if you import a module that hasn't been compiled yet.

[Rob Dockins]

It's really hard to tell, honestly. I get the impression that it is more related to lean going off and doing background recompiles and such, rather than being related to the tactic itself, but that's just a guess...

[Rob Dockins]

So, leanpkg build doesn't just build the entire mathlib tree? Would using the binaries as you suggested prevent recompilation?

[Rob Lewis]

Ah. I haven't used emacs for Lean in a long time, so I'm not sure of the details there. Rather than restarting emacs, you should be able to restart the Lean server, which could at least make debugging smoother.

[Rob Lewis]

Running lean --make in the root directory should build all of mathlib, if you don't want to fetch the prebuilt binaries.

[Simon Hudon]

leanpkg build will only build as much of mathlib as you import in your project.

[Rob Dockins]

Unfortunately, restarting lean doesn't seem to help for long, it will pretty much immediately go back to doing whatever it was doing before and run out of memory again. And once emacs gets into it's weird state, it's very hard to get it to clean itself up again.

OK, I'll try to build it all first, see if that helps.

[Johan Commelin]

We've recently started using update-mathlib on our project, and it saves us a lot of headaches and wasted time.

[Kevin Buzzard]

Yeah I never have issues with anything compiling lean or mathlib any more. Elan takes care of lean and update-mathlib takes care of mathlib

[Simon Hudon]

@Kevin Buzzard and @Johan Commelin Do you often have to invoke update-mathlib explicitly or does it mostly get called by git hooks?

[Johan Commelin]

So far I've been calling it explicitly.

[Johan Commelin]

Since when ought it be called by git hooks?

[Johan Commelin]

If that is recent, maybe we just haven't given it the chance yet.

[Patrick Massot]

It won't be called by git hooks if you don't ask for it. You need to call https://github.com/leanprover-community/mathlib/blob/master/scripts/setup-lean-git-hooks.sh

[Patrick Massot]

After using https://github.com/leanprover-community/mathlib/blob/master/scripts/setup-dev-scripts.sh of course

[Rob Dockins]

FWIW, things seem to be more stable for me after doing a complete build using lean --make.

I have also learned what might be an important lesson, which is to be very careful not to input stray characters in buffers of the lean standard library source after using M-. to follow a definition, as this will kick off a whole bunch of useless work.

[Simon Hudon]

Yes that’s true. For that reason, I have directory local variables for that directory to put lean buffers in view mode

[Kevin Buzzard]

Yes, you have to be super-super-careful once you have compiled .olean files. The moment you change the timestamp for some file low down in the hierarachy, Lean notices that the timestamp of the olean file is too old and this triggers recompilation of everything (and the olean files don't get rewritten, so you are in a far more borked situation than before the edit, you're forever recompiling).

[Rob Dockins]

@Simon Hudon Can you say a bit more about how to set up those directory local variables? I'd like to do the same.

[Simon Hudon]

at the root of my projects, I add a .dir-locals.el file in which I have the line:

(("_target/" . ((lean-mode . ((eval . (view-mode)))))))

It seems I no longer have the same for the core library but you can make a similar file at the root of ~/.elan/toolchains/3.4.2/lib/lean/library/ (if you use elan). The code should be:

(("./" . ((lean-mode . ((eval . (view-mode)))))))