Running Mathlib under `set_option debug.byAsSorry`

Stream: mathlib4

[Kim Morrison]

I've been trying to get Mathlib to run under set_option debug.byAsSorry, which turns all by blocks into sorry.

[Kim Morrison]

The purpose of this is to enable very fast benchmarking builds of subsets of Mathlib. (e.g. one might turn it on globally, and then turn it off for select files, and then rebuild while making changes to Lean itself)

[Kim Morrison]

This causes some problems! Sometimes implicit arguments in term mode aren't determined until we run a tactic block. Other times variables are not pulled in when the tactic block is omitted.

[Kim Morrison]

Nearly all the changes required, however, seem positive. I've made 5 PRs so far backporting changes. #14993 #15119 #15120 #15125 #15126

[Kim Morrison]

Moreover, some of these changes are independently going to be helpful as we change the variable inclusion mechanism (as requested at lean#2452 with work in flight at lean#4814).

[Kim Morrison]

If anyone would like to help out with this effort, here's how you can assist:

• Checkout branch#byAsSorry
• lake build
• This will fail at a bunch of files, the current frontier of work.
• Look at these files
  • if you can fix them via the types of changes in the PRs above, please do so!
  • if you can't fix them, just as set_option debug.byAsSorry false, either to individual declarations or the whole file
• Commit any of the set_option changes direct to branch#byAsSorry
• But for all the other changes, please don't commit them directly: instead git stash them, create a branch off master, and PR them, then merge that branch in byAsSorry.

[Kim Morrison]

It's probably a good idea to "claim" and "unclaim" branch#byAsSorry here, via comment or emoji, so we don't have any collisions. I'm done for the night.

[Notification Bot]

9 messages were moved from this topic to #Zulip meta > fixing the mathlib#n linkifier by Kim Morrison.

[Michael Rothgang]

Let me "claim" this branch for perhaps an hour (I'll write another message once I'm done)

[Michael Rothgang]

Follow-up request: can you disable the linter.unusedTactic linter on that branch? (I won't do that now, to not bust my cache locally. But it seems useful to avoid warning spew.)

[Eric Wieser]

Are the semantics of byAsSorry "don't run any by blocks" or "don't run any Prop-typed by blocks"?

[Eric Wieser]

If the former, this seems to be leaning towards "by should not be used for data" as a hard rule, rather than the general guideline it used to be

[Sebastian Ullrich]

the latter

[Edward van de Meent]

assuming this gets adapted, i suppose mathlib would need another CI step where mathlib gets built with this option, to enforce this kind of benchmarking is possible? or maybe this can be enforced with some kind of linter?

[Edward van de Meent]

Michael Rothgang said:

Follow-up request: can you disable the linter.unusedTactic linter on that branch? (I won't do that now, to not bust my cache locally. But it seems useful to avoid warning spew.)

maybe you could just hide warnings?

[Edward van de Meent]

i imagine there might be an option for that?

[Michael Rothgang]

Sure, I can disable these warnings locally. I'm asking to globally disable these warnings (on that branch only) because

• with that option, "unreachable tactics" are bound to happen by design
• right now, runninglake build or opening a new file means waiting for what feels a minute, for lake to replay all the warnings produced by previous files --- which are not useful

[Michael Rothgang]

I filed #15133 with the fixes I have so far (for a few other files, I couldn't find an easy find, but set_option debug.byAsSorry at the top of the file did not work either; I left these alone.

[Edward van de Meent]

is it just me or do the changes to the lakefile you made at branch#MR-debugAsSorry make lake build throw errors saying invalid -D parameter, unknown configuration option 'linter.unreachableTactic'?

[Edward van de Meent]

or are you still working on that?

[Edward van de Meent]

i'd like to claim the branch for a bit

[Michael Rothgang]

Edward van de Meent said:

is it just me or do the changes to the lakefile you made at branch#MR-debugAsSorry make lake build throw errors saying invalid -D parameter, unknown configuration option 'linter.unreachableTactic'?

No, both tactics are mathlib tactics, and that branch apparently doesn't have the Lean change allowing to set mathlib options in lakefile.lean.

[Michael Rothgang]

I'm not working on this branch.

[Edward van de Meent]

(deleted)

[Edward van de Meent]

i've created a pr, is it the intention that the entirety of (current master + your changes) gets merged into branch#byAsSorry ? or just (your changes)?

[Edward van de Meent]

(the pr is #15137 for those interested)

[Edward van de Meent]

i suppose i will do the first option.

[Edward van de Meent]

once CI completes, that is

[Edward van de Meent]

ok, i'm done

[Kim Morrison]

Michael Rothgang said:

I filed #15133 with the fixes I have so far (for a few other files, I couldn't find an easy find, but set_option debug.byAsSorry at the top of the file did not work either; I left these alone.

Made one change, and 'd

[Kim Morrison]

Edward van de Meent said:

(the pr is #15137 for those interested)

Thank you! 'd

[Kim Morrison]

Oh: I should have said earlier, a good technique for debugging when Lean can't synthesize an implicit argument to is locally set_option debug.byAsSorry false, and then use #print to inspect the proof term, and fill things in from that.

[Kim Morrison]

Another: robustifying for debug.byAsSorry (part 8) #15149

[Kim Morrison]

And: robustifying for debug.byAsSorry (part 9) #15150

[Kim Morrison]

I'll fix the errors in those two, but otherwise branch#byAsSorry is available if anyone would like to hack on this.

[Kim Morrison]

We are definitely "getting there" now. We have been adding set_option debug.byAsSorry false in places, and these will have to be revisited, but the current frontier is now:

- Mathlib.Algebra.Algebra.Subalgebra.Directed
- Mathlib.Algebra.Category.Grp.Kernels
- Mathlib.Algebra.Exact
- Mathlib.Algebra.Homology.CommSq
- Mathlib.Algebra.Homology.ShortComplex.Exact
- Mathlib.Algebra.Polynomial.Basic
- Mathlib.CategoryTheory.Abelian.Transfer
- Mathlib.CategoryTheory.Galois.Decomposition
- Mathlib.CategoryTheory.Limits.EpiMono
- Mathlib.CategoryTheory.Quotient.Linear
- Mathlib.CategoryTheory.Quotient.Preadditive
- Mathlib.CategoryTheory.Sites.CoverLifting
- Mathlib.CategoryTheory.Sites.Preserves
- Mathlib.Combinatorics.Young.YoungDiagram
- Mathlib.Data.DFinsupp.WellFounded
- Mathlib.Geometry.Manifold.LocalInvariantProperties
- Mathlib.GroupTheory.OrderOfElement
- Mathlib.LinearAlgebra.TensorProduct.Tower
- Mathlib.RingTheory.Ideal.Quotient
- Mathlib.RingTheory.Localization.Basic
- Mathlib.RingTheory.Valuation.Integers
- Mathlib.SetTheory.Ordinal.Arithmetic
- Mathlib.Topology.Algebra.Module.Star
- Mathlib.Topology.Algebra.OpenSubgroup
- Mathlib.Topology.Order.Basic
- Mathlib.Topology.Order.ScottTopology
- Mathlib.Topology.SeparatedMap
- Mathlib.Topology.StoneCech

[Kim Morrison]

I couldn't work out how to fix

- Mathlib.Combinatorics.Young.YoungDiagram
- Mathlib.LinearAlgebra.TensorProduct.Tower

nicely at all.

Perhaps on these it is better to wait for lean#4814 to be ready, and to use include.

[Mario Carneiro]

Can we get some kind of by! which says "don't stub me under debug.byAsSorry"?

[Mario Carneiro]

this will be useful in particular for defs defined using tactics

[Mario Carneiro]

in fact, I think it can be implemented in user space, as set_option debug.byAsSorry false in by

[Mario Carneiro]

it is a uniform solution to migrate code to work with this option enabled

[Kim Morrison]

I'd like to do a first pass without this, and see where we land. With the changes required for the new variables I think there might not be a huge amount remaining, and by! would be a fine solution.

[Eric Wieser]

Mario Carneiro said:

this will be useful in particular for defs defined using tactics

I thought @Sebastian Ullrich's comment above means that such by blocks are run anyway?

[Mario Carneiro]

yes, but part of the reason for that was that it was just infeasible because the breakage was too much

[Mario Carneiro]

having a low cost syntax for opting out would make it a lot more feasible

[Edward van de Meent]

i'm claiming the branch again

[Michael Rothgang]

Kim Morrison said:

Another: robustifying for debug.byAsSorry (part 8) #15149

Do we have a standard emoji for "maintainer merge"'d? Anyway, I just did so this PR and its sequel.

[Edward van de Meent]

i think it would be useful for this effort to have a linter checking if toggling the option changes the type of a statement. currently, the only way to see if that is the case is hoping and waiting for an error to occur somewhere down the line when tactic-mode isn't used, but that seems a bit short-sighted to me...

[Damiano Testa]

As far as I understand a linter would be able to check that each individual declaration that is parsed would parse with "by replaced by sorry" (filtering out non-Prop-valued ones and whatever else). However, to recreate the full sorry-bearing environment and checking that a new declaration compiles with the previous ones sorryed out would mean basically that the linter would have to re-parse a big chunk of each file.

[Damiano Testa]

This looks more like a CI step: CI build mathlib as is and also mathlib-as-sorry.

[Edward van de Meent]

doesn't it suffice to check locally?

[Edward van de Meent]

because assuming that somehow a statement compiles differently when replacing by with sorry, there is a first such statement where that is the case.

[Damiano Testa]

I am not sure that it suffices to check locally: something sorryed may parse, but may not have the "same" meaning as the un-sorryed one in subtle ways.

[Damiano Testa]

A simple way in which this can happen is because a variable is not pulled in, since it was used in the proof (but not in the statement), but there are certainly more ways in which this can happen.

[Edward van de Meent]

so you can't compare the type of two versions of the term?

[Damiano Testa]

I'm not saying that the linter would be useless, just that you would still need to depend on more resources.

[Damiano Testa]

Yes, that could be done, but making it work for auto-generated declarations would be hard.

[Edward van de Meent]

maybe i'm not explaining it well...
take this example:

variable {a b :Nat} (h:a = b)

lemma heq : a = b := by exact h

with set_option debug.byAsSorry false, the type of heq is heq {a b : Nat} (h : a = b) : a = b while with set_option debug.byAsSorry true, it is heq {a b : Nat} : a = b. can't a linter tell this difference?

[Damiano Testa]

Yes, I think that this you could detect.

[Damiano Testa]

Let me try to write a linter that does that and see how it performs.

[Damiano Testa]

I agree that it will be useful, but I am not sure that it would flag everything that it should.

[Damiano Testa]

#15162

This is very preliminary, but I am not sure that I will have more time to work on this soon.

[Damiano Testa]

As you can probably see, the PR has just two new files: Mathlib.Tactic.Linter.CheckAsSorry and a test file. If you copy over Mathlib.Tactic.Linter.CheckAsSorry to your "other" PR, adding

import Mathlib.Tactic.Linter.CheckAsSorry

at the beginning should make the linter parse the file. The tests that I ran are basically exactly the ones contained in the test file, so I expect a lot of issues, since this is quite delicate, but hopefully it is useful.

[Damiano Testa]

If you accumulate the problems that you come across with the linter, I can try to fix them, though that would in all likelyhood not happen before Monday.

[Edward van de Meent]

right, thanks!

[Edward van de Meent]

#15164 is part 9 part 10 in the series

[Michael Rothgang]

Edward van de Meent said:

#15164 is part 9 in the series

Part 9 already landed on master, so this is even part 10. :-)

[Edward van de Meent]

ah oops :upside_down:

[Edward van de Meent]

forgot how to count

[Edward van de Meent]

#15169 is part 11 in the series

[Edward van de Meent]

@Kim Morrison i've taken a look at Mathlib.LinearAlgebra.TensorProduct.Tower, and it seems to be the case that removing [Module B P] as well as [IsScalarTower R B P] [SMulCommClass A B P] at lines 303-304 fixes the errors... it seems to have something to do with AlgebraTensorModule.assoc pulling in more variables for some reason? i'm not really sure exactly how it works. I'll create a PR for my current changes minus this tensorproduct stuff, and then free the branch

[Edward van de Meent]

a quick look at the docs for the file using ctrl+f makes it seem like the assumption [Module B P] occurs in 0 of the declarations in the file? nvm, that's just my browser not handling searching for italics

[Edward van de Meent]

it's at the very least not used in section CommSemiring, where the variable is declared

[Edward van de Meent]

ok, #15178 is number 12! i'm done for today

[Damiano Testa]

In case anyone tries the linter, I forgot to specify what I intended it to do:

• it only inspects lemmas and theorems whose proof begins with := (as opposed to |),
• protected confuses the linter,
• if it fails, it should produce a message saying what expressions the sorried version produced,
• it does not replace any other proof by sorry, just the "main" one.

[Edward van de Meent]

it would seem that i accidentally merged a batteries bump into the branch, which causes some issues i don't know how to fix. (it complained that some declarations like List.pmap and List.attach were already present.) For now, i'll undo the bump

[Kim Morrison]

@Edward van de Meent, I've merged your PRs, except for a few minor comments on #15178, which I've delegated ( :peace_sign:)

[Edward van de Meent]

i'm working on it again

[Edward van de Meent]

#15197 is part 13

[Edward van de Meent]

i'll stop there for today

[Damiano Testa]

Out of curiosity, did you try the linter? Was it in any way useful? :smile:

[Edward van de Meent]

i forgot :melting_face:

[Kim Morrison]

One more for now at "robustifying for debug.byAsSorry (part 14) #15247"

[Kim Morrison]

I propose, however, that we now pause on getting branch#byAsSorry working, as we are more and more often running into problems that are better solved by first updating Mathlib for the new variables inclusion mechanism from lean#4814.

[Kim Morrison]

I will started a separate thread describing the work that needs to be done there. We'll definitely need some help to get it pushed through. As soon as that is done we can return to byAsSorry. (Although, if anyone would like to continue here nevertheless, I'm not going to stop them!)

[Kim Morrison]

#15247 still awaiting review

[Shuhao Song]

I implemented a similar option many years ago. I used notation $\mathcal{S}$ to wrap around a by-block, and when the option checking_mode is true, it will be a usual by-tactic, when false it is elaborated as sorry.

[Mr Proof]

Hi, this sounds really useful what you're doing here. Can I just add my use case which is to basically have a small Mathlib library with propositions only without proofs included, which can be used offline, using REPL. In this use case we are not really interested in having things proved from the basic axioms, but are fine to "trust" the propositions in Mathlib are correct.