How deterministic are deterministic timeouts?

Stream: general

[Eric Wieser]

After merging in master, my PR at https://github.com/leanprover-community/mathlib/pull/4908 is now experiencing a deterministic timeout in a file I haven't touched. What worries me, is that I don't think any of the files I've touched are even imported by that file - so why am I getting a timeout?

[Johan Commelin]

The bad file is src/data/polynomial/monic.lean. This is a sufficiently basic file that it ought not cause timeouts. We should fix this.

[Eric Wieser]

These commits have identical file trees:

https://github.com/leanprover-community/mathlib/compare/5cf35e8501b74cc8391099c08c34ac504a30ccc0..e24736b251ebee44fcfb066ac5dfaa2e9c3b59d1

Yet one builds and one does not

[Johan Commelin]

You could just click the "Rerun jobs" button. Maybe the timeout came from cosmic background radiation interfering with CI.)

[Eric Wieser]

My hunch is that the the difference between those commits is they start with different caches

[Eric Wieser]

For merge commits, the mathlib CI only tries the first parent, which never includes origin/master

[Eric Wieser]

So maybe mathlib is now unbuildable with an empty cache?

[Eric Wieser]

Johan Commelin said:

You could just click the "Rerun jobs" button. Maybe the timeout came from cosmic background radiation interfering with CI.)

I'll push an empty commit instead - I don't want to discard the evidence of this happening

[Johan Commelin]

next_coeff_mul is very slow

[Eric Wieser]

Is there a way to up the timeout for a single lemma?

[Bryan Gin-ge Chen]

Uh oh, this build in the attempt to merge the totally unrelated #4915 is also failing at the same place.

[Eric Wieser]

It looks like pushing an empty commit to the same branch wa enough to fix the problem, based on the fact it didn't immediately fail - so the time _is_ non-deterministic, but it's at least not deterministically always a problem

[Gabriel Ebner]

Umm yeah, deterministic timeouts are only deterministic in the sense that they don't count how many seconds it takes to run something. But there's lots of other "hidden state" that can influence how long a proof takes. For example, caches, or the result of mk_fresh_name, etc.

[Sebastian Ullrich]

Silly Lean 3

[Johan Commelin]

I'm speeding up the lemma. There are a lot of calls to omega.

[Johan Commelin]

It's sad, because now I need to prove stupid trivialities about nats by hand

[Johan Commelin]

I wish omega would print 5-line unreadable proof certificates that are reasonably fast. But show_term { omega } is more like 50 lines and unreadable.

[Johan Commelin]

I've now got a speed up from 15.2s to 2.35s

[Johan Commelin]

#4920, 15 extra lines :sad: 36 insertions(+), 21 deletions(-)

[Reid Barton]

I wonder whether there's any work done on efficiently checkable proof formats for Presburger arithmetic

[Reid Barton]

I wouldn't be surprised if the answer is no

[Johan Commelin]

I didn't check whether the output of show_term { omega } allowed for fast checking...

[Johan Commelin]

If we could hide those 50 lines, then I wouldn't mind have 50 fast lines of garbage introduced by -- omega says:

[Johan Commelin]

Can we have VScode automatically hide lines. Something like

-- proof generated by omega
-- START HIDDEN BLOCK
complicated (proof term) (goes here)
-- END HIDDEN BLOCK

[Johan Commelin]

And only the first line would be shown in VScode, and the rest would be folded away

[Eric Wieser]

Johan Commelin said:

But show_term { omega } is more like 50 lines and unreadable.

Does its output even elaborate correctly? I find that a lot of the time when I use show_term, the result does not

[Johan Commelin]

https://marketplace.visualstudio.com/items?itemName=maptz.regionfolder looks promising!

[Johan Commelin]

Eric Wieser said:

Johan Commelin said:

But show_term { omega } is more like 50 lines and unreadable.

Does its output even elaborate correctly? I find that a lot of the time when I use show_term, the result does not

Bleh, you are right... it's more like 200 lines of non-elaborating crap.

[Johan Commelin]

It would be great if we can have omega? which prints a correct proof certificate.

[Eric Wieser]

Well, given squeeze_simp? sometimes gives incorrect output, I'm not too optimistic that getting omega to do that is propery is likely

[Johan Commelin]

The problems that I currently had was stuff like 0.succ_pos where projection notation is used but it shouldn't.

[Kevin Lacker]

why does lean have the quasi-deterministic timeouts? most programming languages, if compiling something is taking a long time, then it will just go ahead and take longer.

[Mario Carneiro]

because it's used in an editor

[Mario Carneiro]

no one likes when their editor hangs

[Mario Carneiro]

if you use lean on the console there are no timeouts

[Kevin Lacker]

your editor shouldn't hang, right? it should just take a while to check syntax

[Kevin Lacker]

and besides, the problem here is not in an editor - the CI system is failing with a timeout https://github.com/leanprover-community/mathlib/runs/1363431665

[Johan Commelin]

For CI we want the timeouts to make sure that our code is reasonably fast

[Bryan Gin-ge Chen]

By default, when you use Lean on the console there are no timeouts. In both the editor and CI, we use the -T100000 option to throw an error when a proof takes too long.

[Kevin Lacker]

I feel a vague unease but i guess I can't put my finger on quite why this seems wrong to me. I guess pretty soon mathlib will just hit the limits, they can always be increased but the status quo where compiling everything takes an hour isn't great, and hopefully lean 4 has much faster compilation?

[Bryan Gin-ge Chen]

GitHub Actions allows up to 6 hours for each run, so we should be OK for at least a few more months. Believe it or not, mathlib used to take even longer to build and lint, but then Gabriel went and improved a bunch of stuff in community Lean for us.

[Johan Commelin]

Johan Commelin said:

#4920, 15 extra lines :sad: 36 insertions(+), 21 deletions(-)

Thanks to tips and tricks from Eric and Bryan, this is now almost a 10x speedup, and only 3 lines longer than it used to be.

[Johan Commelin]

In fact, only 1 line longer: 30 insertions(+), 29 deletions(-)
(I forgot to disable the profile... doing that saves another 2 lines :grinning: )

[Mario Carneiro]

Kevin Lacker said:

I feel a vague unease but i guess I can't put my finger on quite why this seems wrong to me. I guess pretty soon mathlib will just hit the limits, they can always be increased but the status quo where compiling everything takes an hour isn't great, and hopefully lean 4 has much faster compilation?

Note that the time limit is on individual proofs, so this doesn't represent a global bound on mathlib, unless the growth of the typeclass hierarchy makes all our individual proofs unbearably slow, in which case we have a bigger problem

[Reid Barton]

Reid Barton said:

I wonder whether there's any work done on efficiently checkable proof formats for Presburger arithmetic

@Mario Carneiro this seems like the kind of thing that would exist in metamath if it exists anywhere?

[Mario Carneiro]

I don't have any particular suggestions beyond the usual. Omega consists of a bunch of logical steps, you just write those down

[Mario Carneiro]

I'm pretty sure it's not nearly as bad as the omega tactic makes it look because omega uses proof by reflection

[Mario Carneiro]

The only fundamental advantage an efficiently checkable proof format would have over the omega test is if there is an advantage in nondeterministic computation. Such a thing might exist in the SAT part of omega but I think the main line is pretty deterministic