sorry a tactic block

Stream: mathlib4

[Kyle Miller]

In Lean 3 we added the feature that you could sorry out subproofs by putting sorry in front of them. It worked particularly well because subproofs were wrapped in curly braces, so you could just put the sorry in front of the leading {. For example, you could replace { intro, expensive_tactic, } with sorry { intro, expensive_tactic, }, even if the subproof spanned multiple lines. https://github.com/leanprover-community/lean/pull/689

I've been wondering what a Lean 4 version could look like for a while.

This seems like a design:

• "with_sorry" tactic evaluates as sorry (ignoring the tactic)
• "with_sorry" " => " tacticSeq evaluates as sorry (ignoring the tactic sequence)

This way you can "comment out" the rest of a block by inserting with_sorry => (you can also adjust the indentation for that if needed).

You can also "comment out" subproofs with with_sorry, for example, the with_sorry would consume the existing · block in the following:

theorem perm_factors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
    (a * b).factors ~ a.factors ++ b.factors := by
  refine' (factors_unique _ _).symm
  · rw [List.prod_append, prod_factors ha, prod_factors hb]
  with_sorry
  · intro p hp
    rw [List.mem_append] at hp
    cases' hp with hp' hp' <;> exact prime_of_mem_factors hp'

The main goal with this design for with_sorry is that it is easy to insert without adjusting the formatting of the rest of the proof.

[Yaël Dillies]

Can it be similar to how classical works?

[Kyle Miller]

Sure, it could, but I'm not sure that classical is how we would want this to work.

[Kyle Miller]

I think often you want to comment out a single sub-proof, rather than comment out the rest of the proof.

[Mario Carneiro]

Kyle Miller said:

In Lean 3 we added the feature that you could sorry out subproofs by putting sorry in front of them. It worked particularly well because subproofs were wrapped in curly braces, so you could just put the sorry in front of the leading {. For example, you could replace { intro, expensive_tactic, } with sorry { intro, expensive_tactic, }, even if the subproof spanned multiple lines. https://github.com/leanprover-community/lean/pull/689

I've been wondering what a Lean 4 version could look like for a while.

Are you familiar with the stop tactic? In mathport I originally used sorry => as the spelling of lean 3 sorry { ... } but later switched it to stop which is not different enough to matter

[Mario Carneiro]

(More generally, if you are thinking "what happened to that old lean 3 feature?" then mathport has probably already considered it and come up with an answer)

[Mario Carneiro]

stop is a complete drop-in replacement for with_sorry in your examples

[Thomas Murrills]

Kyle Miller said:

I think often you want to comment out a single sub-proof, rather than comment out the rest of the proof.

I’m not sure how stop works, but it certainly sounds like it doesn’t do this; if it does, maybe it could use a better name

[Kyle Miller]

I'd seen (but forgotten) about it, but I think it's worth thinking about how the user experience should work.

It's a "drop-in replacement" functionally, but not experience-wise. It doesn't solve the problem of "how do I conveniently sorry-out this single focus block". The stop tactic comments out the entire rest of the proof.

[Mario Carneiro]

that's the "not quite the same" part, related to the way that block tactics parse in lean 4. In this example stop will consume both subproofs:

example : True ∧ True ∧ True := by
  refine ⟨?_, ?_, ?_⟩
  · trivial
  stop
  · trivial
  · trivial

[Mario Carneiro]

this is also why stop is defined as repeat sorry instead of just sorry, because otherwise it would bracket both subproofs but only close the first goal

[Kyle Miller]

Exactly, so with what I was proposing, there would be a way to consume just the next tactic, which I think is a very important feature as a replacement for sorry { ... }

[Mario Carneiro]

You need some indentation if you want to only consume the one goal

[Mario Carneiro]

But actually it's not that bad, you can always kill individual subproofs by just moving the stop:

example : True ∧ True ∧ True := by
  refine ⟨?_, ?_, ?_⟩
  · trivial
  · stop
    trivial
  · trivial

[Kyle Miller]

Is there some mistake with this design that I proposed that would make it so that you need some indentation to consume one goal?
Kyle Miller said:

This seems like a design:

• "with_sorry" tactic evaluates as sorry (ignoring the tactic)
• "with_sorry" " => " tacticSeq evaluates as sorry (ignoring the tactic sequence)

[Kyle Miller]

Mario Carneiro said:

But actually it's not that bad, you can always kill individual subproofs by just moving the stop:

I discarded this idea myself, because you have to alter that subproof by inserting the right amount of whitespace

[Mario Carneiro]

like I said, that's exactly how the sorry => tactic worked. We could bring it back but it has a lot of overlap with stop

[Mario Carneiro]

Also with_sorry foo; bar will have some weird parsing in your example

[Kyle Miller]

At least you can do with_sorry => foo; bar if you notice the weird parsing.

[Thomas Murrills]

sorry => does look like it demands indentation after it, though, even if it doesn’t.

[Mario Carneiro]

The idea is that it really should have indentation

[Mario Carneiro]

if you want the unindented block version you should probably be using stop

[Thomas Murrills]

I think Kyle’s idea is that you should be able to insert it in a proof easily for good UX

[Kyle Miller]

And there's the consideration that these are never meant to be permanent parts of the proofs, so you want to be able to insert/delete them quickly and accurately

[Mario Carneiro]

If the whitespace handling around the dots is annoying you can always just put an extra newline there

[Mario Carneiro]

I agree that this is an issue, although it's true in general and not just with stop

[Mario Carneiro]

it would be great if vscode autoindent played better with the dots

[Kyle Miller]

Are you saying that we could "just" make all of mathlib look like this?

theorem perm_factors_mul_of_coprime {a b : ℕ} (hab : Coprime a b) :
    (a * b).factors ~ a.factors ++ b.factors := by
  rcases a.eq_zero_or_pos with (rfl | ha)
  ·
    simp [(coprime_zero_left _).mp hab]
  rcases b.eq_zero_or_pos with (rfl | hb)
  ·
    simp [(coprime_zero_right _).mp hab]
  exact perm_factors_mul ha.ne' hb.ne'

[Kyle Miller]

Just to support being able to insert stop?

[Mario Carneiro]

no, I'm saying that you would reformat into that style on an ad-hoc basis when messing about

[Mario Carneiro]

vscode doesn't have the same issues with markdown lists, so maybe there is a way to fix it in the editor

[Kyle Miller]

I agree that is something that we could do, but I think you have to agree that as a user experience, that's a non-starter, unless we want to rely on editor support.

[Thomas Murrills]

Mario Carneiro said:

it would be great if vscode autoindent played better with the dots

I think the extension PR I made for this a while ago recently got merged

[Mario Carneiro]

I mean it's not that bad to type stop + enter + tab but I get what you mean

[Kyle Miller]

I would rather not rely on editor support. There are solutions where you can "just" insert some tactics (like the ones I proposed) and get the behavior that you want.

[Yaël Dillies]

My muscles expect

sorry · tactic_that_does_not_run
  another_tactic_not_running

to work

[Kyle Miller]

("Just" is in quotes because I usually consider it to be a banned word for design discussions. It always hides too much about what the underlying constraints are, and what we each think is important to design for.)

[Mario Carneiro]

stop would almost work with that, but you broke the whitespace sensitive tacticSeq there

[Yaël Dillies]

I think that's easy enough to be user-friendly, and ugly enough that nobody will want to leave that in final code?

[Yaël Dillies]

Yeah; that breaks the tacticSeq expectation, but I would claim that's a feature?

[Kyle Miller]

I'd want your idea to work @Yaël Dillies, but I think it's not technically possible because of indentation sensitivity (what Mario said). What if you want to comment out a tactic that itself is multi-line and indentation sensitive?

[Thomas Murrills]

Half-serious proposal for an alternate name for with_sorry if Yaël’s sorry doesn’t work (but I like that one best): sorry_about (pros: initial sorry so you can easily see when a line starts with it, makes “linguistic sense”; cons: not idiomatic/consistent with other withs)

[Kyle Miller]

(I do want to mention that I think stop is a good design for stopping a proof partway through.)

[Mario Carneiro]

For the case of stubbing out a single subgoal from the outside, kyle's with_sorry would work. I wouldn't recommend using it in any other situation though

example : True ∧ True ∧ True := by
  refine ⟨?_, ?_, ?_⟩
  · trivial
  with_sorry
  · trivial
  · trivial

[Yaël Dillies]

Can't macros handle multiline things somehow? I mean if we have a macro that literally replaces

sorry · tac1
  tac2

with

· stop
  tac1
  tac2

then we win, right?

[Kyle Miller]

Maybe the solution is add with_sorry for commenting out a single tactic, and keep stop as-is?

[Mario Carneiro]

it's already a parse error though @Yaël Dillies

[Thomas Murrills]

What if we had "sorry" "." <followed by appropriate tactics> parse?

[Mario Carneiro]

but you could have a code action that changes

· tac1
  tac2

to

· stop
  tac1
  tac2

[Mario Carneiro]

maybe just "insert tactic here"

[Yaël Dillies]

Hmm, I thought we could have macro-like objects getting replaced at several points, including possibly before parsing?

[Mario Carneiro]

In fact, the tactic code actions infrastructure was designed specifically to support code actions of this form

[Mario Carneiro]

Yaël Dillies said:

Hmm, I thought we could have macro-like objects getting replaced at several points, including possibly before parsing?

The trouble is that if it doesn't parse then either you have no parse information or garbage parse information, so either way it's difficult to make a very intelligent suggestion about the code

[Thomas Murrills]

(On the code action route, there also ought to be a code action to remove stop, which could also be annoying to do)

[Mario Carneiro]

ditto for done

[Mario Carneiro]

this probably overlaps with (the code action for) @Damiano Testa 's useless tactic linter

[Kyle Miller]

Hey, his tactic linter is useful :upside_down:

[Damiano Testa]

The useless tactic linter does not have a code action... at least not yet! I think that finding a way to formatting the output might be the biggest blocker, though.

[Thomas Murrills]

By the way, can you still see the tactic state at a tactic that comes after stop? Say, if you wanted to consider whether to keep working on it?

[Mario Carneiro]

rust-analyzer has a code action for remove dbg!() where you can just select a whole code block and it will delete all these temporary debugging things. We could do the same for stop / done removal

[Mario Carneiro]

@Thomas Murrills No? I mean the code doesn't run at all

[Kyle Miller]

I'm liking this design for "how to sorry out proofs":

• keep stop exactly as it is, to sorry out the rest of a proof
• with_sorry (or whatever the name) for a single tactic, to support sorrying out blocks without relying on editor support
• create a code action for inserting and removing other tactics, including stop

[Kyle Miller]

Maybe inserting skip before/after would be a good code action to have?

[Mario Carneiro]

@Thomas Murrills I'm not sure how that could work

[Yaël Dillies]

How do code actions display? Are they "noisy", as in add an info message to the infoview?

[Mario Carneiro]

they are the lightbulb

[Thomas Murrills]

It could work if syntax like sorry . <tacs> worked (I.e. if sorry . was like .)

[Yaël Dillies]

Thomas, you can see the tactic state by putting your cursor here: |stop

[Thomas Murrills]

I mean at the end of the block, not the beginning!

[Mario Carneiro]

Thomas Murrills said:

It could work if syntax like sorry . <tacs> worked (I.e. if sorry . was like .)

This already works, exactly as Yael described (for stop). The trouble is that you have to match indentation for the rest of the block

[Thomas Murrills]

Oh, so the code does run!

[Mario Carneiro]

i.e.

stop · tac1
  tac2

is a parse error but

stop · tac1
       tac2

parses as intended (although actually you wouldn't want to use stop for this because it does repeat sorry instead of sorry)

[Mario Carneiro]

it's just that aligning the rest of the block is way too much work to ask for

[Damiano Testa]

You could do this and maybe get Yaël's behaviour:

syntax "sorrys " tactic (colGt tacticSeq) : tactic

open Lean Elab Command Tactic
elab_rules : tactic
  | `(tactic| sorrys $_
                $_) => do evalTactic (← `(tactic| sorry))


example (n : Nat) : True := by
  rcases n with _|_|_|_|_
  sorrys · have := 0
    have := 1
  repeat exact .intro

[Thomas Murrills]

I just want to be clear: if you write

. stop
  tac1
  tac2

then placing your cursor before stop shows the tactic state after tac2? That’s what I’m asking about.

[Mario Carneiro]

No, it shows the tactic state before tac1

[Mario Carneiro]

and there is no tactic state after tac1 because tac1 was never run

[Mario Carneiro]

if you put your cursor inside or after the stop token or anywhere in the block I expect you to see No goals because stop closes all goals

[Thomas Murrills]

Mario Carneiro said:

Thomas Murrills said:

It could work if syntax like sorry . <tacs> worked (I.e. if sorry . was like .)

This already works, exactly as Yael described (for stop). The trouble is that you have to match indentation for the rest of the block

Ok, I got confused by “this already works”—I thought you were talking about the behavior I’m asking about

[Mario Carneiro]

? I am?

[Mario Carneiro]

if <tacs> was on one line it would work

[Mario Carneiro]

@Damiano Testa that fails if the first line has more than one tactic in it (separated by ;)

[Damiano Testa]

I'm not sure it does: this seems to work for me

example (n : Nat) : True := by
  rcases n with _|_|_|_|_
  sorrys· have := 0; have := 1
    exact .intro
  repeat exact .intro

[Mario Carneiro]

I wonder what would happen if you use "sorrys " tacticSeq (colGt tacticSeq)? though

[Mario Carneiro]

it's because you used a dot after sorrys

[Mario Carneiro]

  sorrys have := 0; have := 0
    have := 1

doesn't parse

[Damiano Testa]

Mario Carneiro said:

it's because you used a dot after sorrys

Right, but this was Yaël's suggestion. In the situation that you are describing, wouldn't stop already work?

[Thomas Murrills]

stop . tac1
       tac2

runs tac1, tac2 on the goal after stop, does it not?

[Thomas Murrills]

(Sorry, this is a reply to Mario.)

[Mario Carneiro]

No

[Damiano Testa]

You are right, but your suggestion works, I think.

Mario Carneiro said:

I wonder what would happen if you use "sorrys " tacticSeq (colGt tacticSeq)? though

[Mario Carneiro]

it does not run tac1 or tac2, but if there is a tac3 after it then it would be run

stop . tac1
       tac2
. tac3
  tac4

this runs tac3 and tac4 but not tac1 and tac2 (and fails at the second dot because of the semantics of stop)

[Damiano Testa]

So, this is what might work:

syntax "sorrys " tacticSeq (colGt tacticSeq)? : tactic

open Lean Elab Command Tactic
elab_rules : tactic
  | `(tactic| sorrys $_
               $_) => do evalTactic (← `(tactic| sorry))


example (n : Nat) : True := by
  rcases n with _|_|_|_|_
  sorrys have := 0; have := 1
    exact .intro
  sorrys have := 0
    have := 1
    exact .intro
  repeat exact .intro

[Thomas Murrills]

Mario Carneiro said:

No

Ok, so it must not produce the behavior I’m talking about, right? Because it doesn’t run tac1/tac2? I’m specifically looking to get the tactic state at tac2.

[Yaël Dillies]

Yeah, Mario is misunderstanding what behavior you were talking about

[Notification Bot]

95 messages were moved here from #mathlib4 > haves with blanks by Mario Carneiro.

[Yaël Dillies]

The point of stop is to not run the tactics that are in the same indentation block, because they are expensive, throw a lot of error, etc...

[Mario Carneiro]

Thomas Murrills said:

Mario Carneiro said:

No

Ok, so it must not produce the behavior I’m talking about, right? Because it doesn’t run tac1/tac2? I’m specifically looking to get the tactic state at tac2.

It's impossible to get the tactic state at tac2 without running tac1

[Mario Carneiro]

It would be great if there was a "sorry mode" one could set in the tactic state so that tactics only do structural stuff and sorry everything they can...

[Mario Carneiro]

then you could get the state of tac2 without "fully" running tac1

[Mario Carneiro]

this would be especially useful for simp

[Thomas Murrills]

Yaël Dillies said:

The point of stop is to not run the tactics that are in the same indentation block, because they are expensive, throw a lot of error, etc...

Hmm, yeah, makes sense...thinking about it more, waiting for a stopped proof to elaborate when it has expensive tactics just to have the option of seeing how far you've gotten seems like it would be too annoying...

[Thomas Murrills]

I suppose second-best to being able to see the tactic state after tac2 is to be able to activate the stop-removing code action from anywhere after stop! :) (Which is maybe already what you had in mind, Mario?)

[Thomas Murrills]

Mario Carneiro said:

it would be great if vscode autoindent played better with the dots

(Just to record this here now that I’m at my computer, this was vscode-lean4#328, merged 4 days ago)

[Matthew Ballard]

(deleted)

[Matthew Ballard]

:peach: post