Minimally commenting out a branch of a proof

Stream: lean4

[Geoffrey Irving]

If I put a sorry at the beginning of a block of a proof, any following tactic statements produce errors. Is there a variant of sorry that would be silent, to allow quickly commenting out a branch (in particular to save time during proving)?

Example that I would like to work

import Mathlib

lemma simple : 7 = 7 := by
  sorryVariant
  norm_num  -- I'd like this not to produce an error

[Johan Commelin]

In Lean 3 you could do sorry { tac1, tac2 }. We should get that to work again.

[Geoffrey Irving]

Having to add the { } doesn't look as nice alongside Lean 4's indentation style, though.

[Ruben Van de Velde]

Use stop instead

[Geoffrey Irving]

Perfect, terrific that it already exists!

[Patrick Massot]

I didn't know either, and the implementation looks like a miraculous hack to me.

[Patrick Massot]

But it makes sense when you think of it.

[Patrick Massot]

The miracle clears up with https://github.com/leanprover/std4/blob/main/Std/Linter/UnreachableTactic.lean#L35-L38. This stop tactic is actually special-cased by the unreachable tactic linter.

[Patrick Massot]

Now it completely makes sense.

[Patrick Massot]

For people who are curious but not curious enough to track it down, the implementation of stop is in core Lean, it says:

macro "stop" tacticSeq : tactic => `(tactic| repeat sorry)

[Patrick Massot]

So stop consumes a sequence of tactics (this is the tacticSeq) so the parser eats up every following tactics (without triggering the unreachable tactic linter, this was the confusing part until I looked at the linter implementation) and replaces them with repeat sorry.

[Patrick Massot]

@Marc Huisinga It would be nice to get stop syntax-highlighted the same way sorry is.

[Alex J. Best]

stop is already marked as leanSorryLike semantically https://github.com/leanprover/lean4/blob/cc1dcf804359276f0f7e8a673c04b2a2b7d69951/src/Lean/Server/FileWorker/RequestHandling.lean#L424. So I have

    "editor.semanticTokenColorCustomizations": {
        "enabled": true,
        "rules": {"leanSorryLike": "#FF0000"},
    },

in my vscode settings to acheive this

[Patrick Massot]

And indeed it works!

[Geoffrey Irving]

Hmm, it doesn't work like I was hoping, though. If I do

lemma simple : 7 = 7 ∧ 5 = 5 := by
  constructor
  · stop
  ·

and put my cursor after the second ·, it says No goals. Though it also says

unsolved goals
case right
⊢ 5 = 5

[Patrick Massot]

Maybe a better implementation would be macro "stop" (colGe tacticSeq)? : tactic => `(tactic| repeat sorry)? @Sebastian Ullrich

[Alex J. Best]

I think you'd need to use sorry for that example? but stop if there are other following tactics indeed

[Geoffrey Irving]

Hmm, so stop requires a nonzero number of following tactics?

[Alex J. Best]

Well it always eats a tacticSeq, which could be empty, but in this case I think it's matching your second . as the following tacticSeq, which Patrick's version should avoid

[Ruben Van de Velde]

That's a little odd. stop; done works as intended