intentional `sorry`

Stream: general

[Asei Inoue]

I often use sorry intentionally for illustrative purposes. In such cases, the warning that sorry is being used is obtrusive and should be removed.

This can be done using the #guard_msgs (drop warning) in command, but all warnings will disappear and I do not want to write them every time.

You could solve this by creating a new tactic that does the same thing instead of sorry, but there is no such tactic in the standard library, so you would have to define it yourself, which is not a desirable solution.

1. Is there a good solution?

2. Also, can it be solved by tactic, but also by (creating) an attribute?

[Eric Wieser]

set_option linter.sorry false might be a nice way to spell this

[Asei Inoue]

set_option linter.sorry false might be a nice way to spell this

Nice idea!!

[Damiano Testa]

Do you get a warning also if you define your own "copy" of sorry and use that instead?

[Damiano Testa]

Some of the test files do that.

[Damiano Testa]

E.g. https://github.com/leanprover-community/mathlib4/blob/b00c9dba4d70ab0ba583936391d41c5d5df86681/MathlibTest/ring.lean#L5

[Asei Inoue]

I see no warning

axiom anotherSorryAx {P} : P

macro "intensional_sorry" : tactic => `(tactic| exact anotherSorryAx)

example : ∀ (P Q : Prop), P → (P → Q) → Q := by
  intensional_sorry

[Edward van de Meent]

Would a #with_sorry command be more ergonomic?

[Asei Inoue]

It seems strange that they have to make their own tactic every time just for this. This is because we often want to use sorry intentionally.

[Asei Inoue]

Would a #with_sorry command be more ergonomic?

option would be more suitable. We already frequently use option when we want to temporarily change the behaviour of a tactic.

[Edward van de Meent]

So something like sorry +intentional?

[Mauricio Collares]

sorry +not_sorry

[Asei Inoue]

Does anyone else want this feature?

[Kyle Miller]

Lean and mathlib tests add this to the top of files that want silent sorries:

private axiom test_sorry : ∀ {α}, α

then you write exact test_sorry. (Edit: I see Damiano already mentioned this.)

[Kyle Miller]

Asei Inoue said:

It seems strange that they have to make their own tactic every time just for this. This is because we often want to use sorry intentionally.

You'll have to justify why making it so that people can insert silent sorries into proofs is desirable in general, since writing examples with silent sorries is the uncommon case. Think about the case of mathlib: if this feature existed, we would have to have an additional linter to make sure this new kind of sorry does not exist. Currently, we can rely on sorry raising a warning and the linter that disallows new axioms.

[Eric Wieser]

I think it would be useful to have a way to filter the warnings from a build to exclude the sorrys; if you're working on a project full of sorries, it's much harder to keep on top of deprecations if they're mixed in with hundreds of sorry warnings.

[Eric Wieser]

linter.sorry=false passed on the command line in CI seems like a reasonable way to address this

[Mario Carneiro]

Is there a way to get lake to give a warning if you use that setting? (But only once per build)

[Mario Carneiro]

I think the real issue is the "hundreds of sorry warnings" part, not the existence of the warnings themselves. If there was some kind of satiation where you don't get any more warnings of a specific kind once you have seen enough then that would solve this issue. (I have pitched this to Mac in the past but I don't think he took me up on it)

[Mario Carneiro]

one of the things that is missing here is to get more structured communication from lean to lake, so that lake can identify which warning is which so it can only make the noisy ones be quiet so that you can spot the others

[Kyle Miller]

I think the intention of lean4#5945 is to help with this last point @Mario Carneiro

[Mario Carneiro]

ah so maybe this is on his agenda after all

[Eric Wieser]

lean4#5194 is also perhaps related here

[Eric Wieser]

(one of the bullets in the RFC is "tag the sorry warnings", another is the PR that Kyle just linked)

[Asei Inoue]

@Kyle Miller

if this feature existed, we would have to have an additional linter to make sure this new kind of sorry does not exist.

I wasn't aware of that. Thanks.
I think there was already a linter that warned against the use of set_option, so why not set_option linter.sorry to switch?

[Asei Inoue]

I think it would be useful to have a way to filter the warnings from a build to exclude the sorrys; if you're working on a project full of sorries, it's much harder to keep on top of deprecations if they're mixed in with hundreds of sorry warning

This is close to my original motivation. I wanted to run the lake build with --wfail to make sure there were no warnings, but I was running into the problem of lots of deliberately filled in sorrys.

However, aesop may use sorryAx without notice, e.g. due to aesop updates. So we don't want CI to ignore all sorry-related warnings.

So for me it would be ideal if I could switch with set_option linter.sorry.

[Asei Inoue]

@Eric Wieser

now https://github.com/leanprover/lean4/issues/5194 has been completed.

Have I found a new, better way to suppress warnings caused by "sorry" without having to use "#guard_msgs" every time?