Zulip Chat Archive

Stream: general

Topic: Linear arithmetic tactic


view this post on Zulip Rob Dockins (Mar 28 2019 at 17:10):

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?

view this post on Zulip Simon Hudon (Mar 28 2019 at 17:14):

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

view this post on Zulip Simon Hudon (Mar 28 2019 at 17:14):

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.

view this post on Zulip Simon Hudon (Mar 28 2019 at 17:17):

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.

view this post on Zulip Rob Lewis (Mar 28 2019 at 17:17):

@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.

view this post on Zulip Rob Lewis (Mar 28 2019 at 17:19):

@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.

view this post on Zulip Simon Hudon (Mar 28 2019 at 17:20):

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.

view this post on Zulip Rob Dockins (Mar 28 2019 at 17:21):

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...

view this post on Zulip Rob Dockins (Mar 28 2019 at 17:23):

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

view this post on Zulip Rob Lewis (Mar 28 2019 at 17:23):

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.

view this post on Zulip Rob Lewis (Mar 28 2019 at 17:24):

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

view this post on Zulip Simon Hudon (Mar 28 2019 at 17:25):

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

view this post on Zulip Rob Dockins (Mar 28 2019 at 17:26):

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.

view this post on Zulip Johan Commelin (Mar 28 2019 at 17:30):

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

view this post on Zulip Kevin Buzzard (Mar 28 2019 at 19:51):

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

view this post on Zulip Simon Hudon (Mar 28 2019 at 20:02):

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

view this post on Zulip Johan Commelin (Mar 28 2019 at 21:07):

So far I've been calling it explicitly.

view this post on Zulip Johan Commelin (Mar 28 2019 at 21:07):

Since when ought it be called by git hooks?

view this post on Zulip Johan Commelin (Mar 28 2019 at 21:07):

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

view this post on Zulip Patrick Massot (Mar 28 2019 at 21:11):

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

view this post on Zulip Patrick Massot (Mar 28 2019 at 21:12):

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

view this post on Zulip Rob Dockins (Mar 28 2019 at 21:35):

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.

view this post on Zulip Simon Hudon (Mar 28 2019 at 23:01):

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

view this post on Zulip Kevin Buzzard (Mar 28 2019 at 23:27):

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).

view this post on Zulip Rob Dockins (Mar 29 2019 at 00:46):

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

view this post on Zulip Simon Hudon (Mar 29 2019 at 01:40):

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)))))))

Last updated: May 13 2021 at 16:25 UTC