Silent sorry

Stream: lean4

[Yaël Dillies]

Is there any way to build a project without throwing warnings on sorry?

[Yaël Dillies]

Motivation: My projects are unfinished and I do not care about them using sorry, but I care about them not throwing other warnings

[Tomas Skrivan]

I'm doing it with a custom axiom and you can override existing notation with priority.

axiom silentSorryAxiom {P : Sort _} : P

macro (priority:=high) "sorry" : term => `(silentSorryAxiom)

macro (priority:=high) "sorry" : tactic => `(tactic| exact sorry)

[Yaël Dillies]

Good idea, but unfortunately that's an extra import to add to all files, and I use having no imports from my project as the signal that a file can be upstreamed

[Tomas Skrivan]

I see, then I'm afraid you need to ask core to change as there does not seem to be a option switch when printing warning about sorry. It happens here

[Tomas Skrivan]

I'm all for having an option for this!

[Adam Topaz]

What’s your application? Isn’t it possible to ask lake to spit out json, then pipe the output to jq and filter out warnings using the output of jq?

[Damiano Testa]

In the meantime, can you simply screen out warnings that come from sorrys, and keep everything else?

[Ruben Van de Velde]

That's the question, right? :)

[Damiano Testa]

Oh, sorry, I meant using a commandline filter like grep on the output of lake build.

[Adam Topaz]

Yeah that’s essentially what I had in mind too. I.e. one can say this is not a lean question.

[Yaël Dillies]

Adam Topaz said:

What’s your application? Isn’t it possible to ask lake to spit out json, then pipe the output to jq and filter out warnings using the output of jq?

The application is for me to find the relevant information in the output of lake build. Given how often I am running this operation, I would rather avoid any extra filtering

[Adam Topaz]

I would pass json output to jq, and process it that way.

[Kevin Buzzard]

I also type lake build a lot in FLT and am now always inundated with hundreds of warnings, meaning that it's much harder to look at what I was just typing seconds before. I've just got used to it now but it would be great to be able to switch it off by default when building. I know I can just write a script in 10 seconds but I've never cared enough to do so (so this must be filed as low prio in my head)

[Damiano Testa]

Here is what I would use:

## builds the input module/filename removing `sorry` warnings from the output
nosorry () {
  local module=${1//\//.}
  lake build "${module/%.lean/}" | grep -v "^warning: .*: declaration uses 'sorry'"
}

# both work
nosorry Mathlib/Data/Nat/Basic.lean
nosorry Mathlib.Data.Nat.Basic

It is not especially high-tech, but will probably mostly work.

[Kevin Buzzard]

how do I do lake build? (edit: looks like nosorry works)

[Kevin Buzzard]

It's still noisy but it's far less noisy:

buzzard@buster:~/lean-projects/FLT$ nosorry
⚠ [1318/6290] Replayed FLT.Mathlib.Topology.Algebra.Module.ModuleTopology
⚠ [6228/6290] Replayed FLT.DedekindDomain.FiniteAdeleRing.BaseChange
⚠ [6243/6290] Replayed FLT.NumberField.InfiniteAdeleRing
⚠ [6244/6290] Replayed FLT.NumberField.AdeleRing
⚠ [6245/6290] Replayed FLT.DivisionAlgebra.Finiteness
⚠ [6247/6290] Replayed FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional
⚠ [6249/6290] Replayed FLT.AutomorphicRepresentation.Example
⚠ [6250/6290] Replayed FLT.EllipticCurve.Torsion
⚠ [6251/6290] Replayed FLT.Basic.Reductions
⚠ [6259/6290] Replayed FLT.GlobalLanglandsConjectures.GLnDefs
⚠ [6260/6290] Replayed FLT.GlobalLanglandsConjectures.GLzero
warning: ././././FLT/GlobalLanglandsConjectures/GLzero.lean:73:28: `Complex.abs` has been deprecated: use the norm instead
⚠ [6267/6290] Replayed FLT.Mathlib.MeasureTheory.Group.Action
⚠ [6268/6290] Replayed FLT.Mathlib.NumberTheory.Padics.PadicIntegers
⚠ [6269/6290] Replayed FLT.HaarMeasure.MeasurableSpacePadics
⚠ [6274/6290] Replayed FLT.Junk.Algebra
warning: ././././FLT/Junk/Algebra.lean:1:0: using 'exit' to interrupt Lean
⚠ [6275/6290] Replayed FLT.Junk.Algebra2
warning: ././././FLT/Junk/Algebra2.lean:1:0: using 'exit' to interrupt Lean
⚠ [6276/6290] Replayed FLT.Mathlib.Algebra.IsQuaternionAlgebra
⚠ [6286/6290] Replayed FLT.QuaternionAlgebra.NumberField
ℹ [6289/6290] Replayed FermatsLastTheorem
info: ././././FermatsLastTheorem.lean:30:0: 'PNat.pow_add_pow_ne_pow' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
Build completed successfully.
buzzard@buster:~/lean-projects/FLT$

[Sébastien Gouëzel]

Worth filtering out also the Replayed lines?

[Damiano Testa]

Oh, you want it to be completely silent?

[Damiano Testa]

I thought that you only wanted to silence warnings arising from sorry.

[Yaël Dillies]

Sébastien is saying that there are some replaying lines that do not correspond to any warning anymore

[Damiano Testa]

Ah, so filtering should also omit a Replayed if the consecutive line is also Replayed.

[Damiano Testa]

I'm not at a computer now, but that is also easy.

[Kevin Buzzard]

I personally want it to not print out all the things I don't care about. I already know that my repo has many sorrys and I don't care about that. I also don't care about replaying (whatever that means), but I definitely care about everything else in that output.

[Damiano Testa]

If no Replayed is wanted with no extra condition, that is even easier.

[Damiano Testa]

I actually have another script that already extracts the code fileLocation for each warning.

[Damiano Testa]

Is the goal to just print outin the lines that begin with warning:, error: and maybe info: and filter out everything else?

[Damiano Testa]

Here is a version that only keeps the warning, error and info lines:

## builds the input module/filename keeping only `warning`/`error`/`info`
## but ignoring `sorry`s
short_nosorry () {
  local module=${1//\//.}
  lake build "${module/%.lean/}" | grep "^\(warning:\|error:\|info:\|Build completed\)" | grep -v "^warning: .*: declaration uses 'sorry'"
}

# both work
short_nosorry Mathlib/Data/Nat/Basic.lean
short_nosorry Mathlib.Data.Nat.Basic

[Kevin Buzzard]

Oh this gives the desired output on FLT, thanks! What do I do with the code though? Right now I'm just cutting and pasting it. I was expecting a shell script nosorry which I could put in ~/.local/bin.

[Yaël Dillies]

Thank you Damiano for the effort, but I would like us to stop writing scripts as bandages to issues that should be fixed at their source. This leads to fragmentation between repositories and reduces maintainability: I am currently spending literal days of my life making the ten or so projects I manage align.

[Damiano Testa]

If you add the definition of short_sorry to .bash_aliases on your computer, then you can use it on your computer directly as short_nosorry.

[Damiano Testa]

Yaël, I agree with you: I was not expecting the command above to become a script in the repository, but just a script in a personal .bash_aliases file that you can run on your computer.

[Adam Topaz]

I don’t quite agree with this point of view. I think the output of lake build should include all the messages that are generated in the code itself, and it should be the responsibility of the user to process those messages as they require.

[Adam Topaz]

sorry generates a warning, which is one kind of a message. I don’t see why it should get special treatment in the lake source over other warnings (e.g. linter warnings) or other messages (e.g. those coming from #check commands)

[Adam Topaz]

One thing that I do think should be an option is to have the option for lake build to give its output in json form. I thought this was already available, but it seems that it is not? (it is available for lake query.)

[Yaël Dillies]

What is the downside of having a flag --no-warning-on-sorry or similar to lake build?

[Yaël Dillies]

Having an unfinished project is a common use case, and wanting to check whether you have any errors/warnings besides sorries is a common subuse case

[Adam Topaz]

Claude told me that the following should work:

lake build | grep -v -E 'warning.*sorry|sorry.*warning'

[Kevin Buzzard]

Did Claude not read the bit about the replaying?

[Kyle Miller]

I think it might be possible to have a core Lean option (unapologetic or sorry.notSorry?) to turn off sorry warnings.

One detail is that it should only filter out warnings that come from user-defined sorries, rather than synthetic sorries (sorries due to invalid code or tactic failures).

It's possible to pass Lean options on the command line to Lake, right?

Are there any issues where people's grading scripts might break because they didn't anticipate students being able to turn off the warning?

[Yaël Dillies]

I like the unapologetic option!

[Asei Inoue]

I like the unapologetic option, too!
I really want this!

[Damiano Testa]

In some test files, mathlib also uses custom sorrys to avoid warnings. Those could also be replaced by "actual" and setting the unapologetic option.

[Floris van Doorn]

lean already has a command-line option -q or --quiet that doesn't do anything, but maybe could turn Lean quiet for anything but errors.

[Yaël Dillies]

I do want other warnings to show though (I am currently turning on the mathlib linters in my projects)

[Kim Morrison]

Hopefully someone can write an RFC? It seems like there's not quite consensus on what this should even do.

[Damiano Testa]

My view is as follows.

[Damiano Testa]

Except for sorry, all other axioms are used "silently".

[Damiano Testa]

I certainly understand that sorry is the only axiom that is known to be inconsistent (ignoring ofReduceBool), so it is great that the default is to flag it.

[Damiano Testa]

However, I also can see that in the development phase of a project, sorryed out statements have a different status than other errors/linter messages, so it seems reasonable to want to have an option to silence sorry as opposed to any other kind of warning/error/info.

[Joachim Breitner]

When writing test cases often a mwe is full of sorries. A quckt way to disable the warning about such explicit worries (set_option warning.sorry false or so) would be useful. Although I have started to define a local testSorry axiom and used that with exact, so a workaround exists

[Asei Inoue]

@Kim Morrison said:

Hopefully someone can write an RFC?

Has the RFC been created yet? Shall I do it?

[Julian Berman]

What's the attractiveness of creating a sorry-specific mechanism for this rather than a warnings-wide one?

[Julian Berman]

Is it "simply" that the latter seems more likely to be more effort and discussion?

[Julian Berman]

Also :bike: while "unapologetic" is cute it is very undiscoverable? Hopefully if that really is what ends up happening that's addressed in some other way.

[Kyle Miller]

Joachim's warning.sorry is much more serious of a contender. You could see it as being part of a warnings-wide solution to the problem too: we might have a way to register warnings and have a macro like trace[...] that conditionally outputs a given warning.