Speeding up Geometry/

Stream: PR reviews

[Michael Rothgang]

#13454, #13456, #13458, #13459 and #13497 each apply a few presumably-standard tricks to speed up the files in Geometry/Manifolds. Review is welcome.
One particular question: When making these improvements, I commented these declarations (and also ones which I could not speed up, though I wanted to): is some form of these (if any) worth preserving? I'll happily take these out if desired.

[Patrick Massot]

Thanks Michael. @Heather Macbeth did you see the sphere instance file in particular? I think it is a serious issue that those calculation-heavy file are so slow or so ugly depending on how much automation we use.

[Patrick Massot]

There are also lots of short-cut instances that hide issues we should probably work on. @Matthew Ballard did you see that?

[Patrick Massot]

Michael, could you make sure to create issues and clear annotations in the Lean code referring to those issues?

[Heather Macbeth]

I am a bit sad to see this (especially since the sphere file already got somewhat de-automated in the port). Is there a consensus that speedup is an intrinsic good? I think that there is real content conveyed by the statement that "this problem can be solved by simp with the standard simp-set" and this is lost when a simp is squeezed.

I'd also flag the field_simps and the convert .. using 1s in particular -- I don't really understand why these should be slow, we should have fast tactics for these tasks!

[Kevin Buzzard]

I think "field_simp is slow" is a known phenomenon but as far as I know nobody is working on it, even though we know some ways to speed it up (eg "don't just multiply by the product of all terms occurring to the right of a / sign, especially if several of them are powers or multiples of other ones")

[Kim Morrison]

I don't think it's even what field_simp is doing that is bad, it's the implementation that is bad. It is doing bad things with the simp discharger.

[Michael Rothgang]

Thanks for the comments! Let me respond to a few points:
First of all: I agree that ideally, adding short-cut instances, squeezing simps or avoid field_simp should not be necessary. I would also prefer living in a world where none of these were needed. That said, particularly Sphere and ContDiff/NormedSpace are really slow: that's beyond the point at which I can work on them nicely. I don't think this is a satisfactory state of affairs. I consider a temporary improvement which can be reverted once tactics have improved worth it.

I will happily file tracking issues for all these problems: slow nlinarith, slow field_simps and also the short-cut instances. (These are not close to all, by the way. There are enough remaining issues to be debugged :-))

[Michael Rothgang]

For field_simp in particular: the root fix is improving this tactic! (In fact, I was wondering how much effort this would be, and if I have a moment in the summer to work on this.) When this happens, my band-aid fixes should be taken out again.
In the mean-time, I personally think we should rather save the CI (and/or local development) time from not taking ages for a slow field_simp call.

[Michael Rothgang]

I was wondering: would using simp? says for all the changes help? At least, this documents the intent (which I agree is nice to preserve).

[Michael Stoll]

If I'm not mistaken, the simp? says syntax will be as slow as the original simp, so this would not help with speeding up things. I would think a comment to the effect "simp [minimal set of lemmas] can do this, but is slow" at the relevant points would allow to revert to the un-squeezed version whenever desired.

[Johan Commelin]

simp? says is only slow in CI, but not locally. tac1 says tac2 will run tac2 locally, but in CI it will run tac1 and check that it prints Try this: tac2.

[Michael Stoll]

So it's OK when working on a file, but misses the goal of speeding up CI.

[Mauricio Collares]

Michael Rothgang said:

That said, particularly Sphere and ContDiff/NormedSpace are really slow: that's beyond the point at which I can work on them nicely. I don't think this is a satisfactory state of affairs.

Did you test the bump/v4.9.0 branch? lean4#3636 might help, and 4.9.0-rc1 will probably be released in a few days.

[Michael Rothgang]

Mauricio Collares said:

Michael Rothgang said:

That said, particularly Sphere and ContDiff/NormedSpace are really slow: that's beyond the point at which I can work on them nicely. I don't think this is a satisfactory state of affairs.

Did you test the bump/v4.9.0 branch? lean4#3636 might help, and 4.9.0-rc1 will probably be released in a few days.

Not yet - I'll do so. Thanks for the pointer!

[Matthew Ballard]

Patrick Massot said:

There are also lots of short-cut instances that hide issues we should probably work on. Matthew Ballard did you see that?

Can someone point to a precise line and I can try to take a look?

[Michael Rothgang]

I guess the diff view in #13458 is a good start. Another option is line 81 in Instances/Sphere in #13456. (I cannot seem to permalink these, sorry.)
Also: thanks a lot for taking a look!

[Matthew Ballard]

The first local instance in #13458 is almost surely tripping synthPendingDepth

[Matthew Ballard]

Maybe the second also

[Matthew Ballard]

For #13456, making Submodule.span return a type a'la #12386 might help

[Michael Rothgang]

#13497 (squeezing very really slow field_simps in Geometry/Euclidean) is ready for review again
#15488 is a reduced version of #13456, and hopefully not controversial

[Yaël Dillies]

Could we put this energy into fixing field_simp itself, maybe?

[Yaël Dillies]

Oh sorry, I guess this was already discussed at length above

[Michael Rothgang]

This is just fixing up existing PRs; I agree to prioritise a field_simp rewrite over new PRs like this.