feat: use sepBy1Indent for tactic and conv blocks

[gebner]

This is the first step towards using colEq in tactic/conv blocks, addressing #1606.

The main user-visible change is that by simp rfl (without newline or semicolon) is no longer supported.

[gebner]

I had to do a slightly ugly bootstrapping hack in 4657b74.

The issue is that parser aliases (such as tacticSeq) are always taken from the previous stage (because they're defined using builtin_initialize). With other syntax, you can use parseQuotWithCurrentStage to use the current stage. But from what I can tell this does not affect parser aliases.

[digama0]

It seems the formatter regressed here?

[gebner]

This is fun. It turns out that tacticSeq now parses the trailing newline (after trivial) as a separator. And the formatter then prints this final newline-separator. We might want to change the formatter to drop the final separator if it's a newline.

[gebner]

Final newline tweak implemented.

[leodemoura]

The main user-visible change is that by simp rfl (without newline or semicolon) is no longer supported.

I suspect many will view this change as an extra plus :)

[gebner]

After this PR, it will be a very small change to enforce uniform start columns in tactic blocks (and sepByIndent generally): https://github.com/gebner/lean4/compare/sepbyindenttac...gebner:lean4:coleq?expand=1

[leodemoura]

Could you please explain the "HACK"?

[gebner]

It's a hack because it creates invalid syntax (see pretty-printer issues in the Zulip thread):

import Lean open Lean Elab Command PrettyPrinter

elab "run" : command => do
  let tac ← `(tactic| simp)
  let tac : TSyntax `tactic := ⟨mkNullNode #[tac]⟩ -- HACK: produces invalid tactic
  let term ← `(by $tac:tactic)
  logInfo (← liftCoreM do ppTerm term)

run -- unknown constant 'null'

[leodemoura]

You are converting here to Array Syntax.Tactic. It is not clear to me why.

[gebner]

(Note: I have rewritten this function one more time since your comment.)

The general reason is that the AST of tactic sequences has changed from many1 (group (tactic >> optional ";")) to sepBy1Indent tactic, i.e. from [(group (skip) [])] to [(skip) []]. Having explicit types available (Array Syntax.Tactic instead of Syntax) makes the refactoring easier because the type system tells you what is a list of tactics, what is a tactic, etc., and you don't have to guess yourself what the Syntax means.

At first it seemed like it was not necessary to keep the separators, making Array Syntax.Tactic a natural choice.

I have now changed it back to untyped Syntax because we need to preserve the separators. Ideally we'd have a TSepIndentArray for this because the manual index calculations are not particularly pretty. (However that doesn't solve all problems either. Even the TSepArray API is pretty bare-bones---and it doesn't preserve the separators either.)

[gebner]

TSepIndentArray

Oh I completely forgot we had this already. It's called TSepArray `tactic "".

[leodemoura]

It is not clear to me why we don't need this anymore.

[leodemoura]

"this" here is the line saveTacticInfoForToken seqElem[1]

[gebner]

Yes, I understand. I thought this was subsumed by Sebastian's other tactic position tweaks. And the tests passed (including the ones checking tactic states at semicolons), so this was plausible.

But it turns out this was indeed necessary, but only for the space after the semicolon... I'm adding a test.

  tac1; tac2
     --^

[leodemoura]

Adding more tests is great. I am frequently worried about changes that affect the infoview because of the lack of tests.

[gebner]

Re: saving tactic info at separators.

This prevents the regression with tac1; tac2 noted above, but it is extremely fragile because the separators can be easily lost:

syntax "mytac" tacticSeq : tactic
macro_rules
  | `(tactic| mytac $[$tacs]*) => `(tactic| { $tacs* })

example : True ∨ True := by
  mytac constructor; constructor
-- still has the issue with the space after the semicolon

We should probably fix this somewhere else.

[leodemoura]

Thanks for the changes. I will go over the code tomorrow, and try to merge it. If I am still confused, we can discuss during the dev meeting.