Try this with a sequence of commands

Stream: metaprogramming / tactics

[Damiano Testa]

In the snippet below, the Try these suggestions are two separate commands that can replace printMe.

How can I have a single Try this suggestion that prints both commands?

import Mathlib.Tactic

open Lean Elab in
elab "printMe" : command =>
  Command.liftTermElabM do
    let s1 ← `(command| def $(mkIdent `x1) := 1)
    let s2 ← `(command| def $(mkIdent `x2) := 2)
    let s := #[s1, s2]
    Std.Tactic.TryThis.addSuggestions (← getRef) (s.map (↑))

printMe

/-  would like to have this suggestion:
def x1 := 1
def x2 := 2
-/

[Jon Eugster]

I think I ran into this before too, and back then I settled with creating a tactic sequence and adding this:

let cmd ←`(tactic| · $x*)
addSuggestion (← getRef) cmd

Dont know if there is a better solution by now.

(edit: here x : Array (Syntax.Tactic))

[Damiano Testa]

I am not sure that I understand your suggestion: if I use `(tactic| ...) then I cannot put a command there.

[Jon Eugster]

my suggestion was to use the central dot \. as it bundles a tactic sequence into a single tactic. But I see you are working with command instead, and I dont know rn on the phone how to change that snipped from tactic to command, sry

[Damiano Testa]

Ok, no worries, and thanks anyways! I am indeed specifically interested in a command sequence, not a tactic sequence.

[Kyle Miller]

You can use mkNullNode to create a sequence of commands, but this doesn't seem to be pretty printable

[Thomas Murrills]

Could we create a new parser? E.g. syntax commandSeq := sepBy1IndentSemicolon(command)

[Damiano Testa]

Thomas, I had assumed that this was already available, since a lean file is exactly a sequence of commands, after all... but I am happy to try it out!

[Thomas Murrills]

Me too, but I couldn’t find it! :P Maybe I’m just missing it?

[Thomas Murrills]

There’s probably a better combinator than sepBy1Indent for pretty printing, as this seems to leave an indent before each def. (I just grabbed the first thing that came to mind)

[Kyle Miller]

There's a parser somehow, but it creates a null node.

open Lean Elab Command in
elab "printMe" : command =>
  Command.liftTermElabM do
    let s ← `(
        def $(mkIdent `x1) := 1
        def $(mkIdent `x2) := 2)
    Std.Tactic.TryThis.addSuggestion (← getRef) (↑s)

printMe -- fails

[Damiano Testa]

This works, but with improvable prettyprinting:

import Std.Tactic.TryThis

syntax commandSeq := sepBy1IndentSemicolon(command)

open Lean Elab in
elab "printMe" ppLine : command =>
  Command.liftTermElabM do
    let s1 ← `(command| def $(mkIdent `x1) := 1)
    let s2 ← `(commandSeq|
$s1
def $(mkIdent `x2) := 2)
    Std.Tactic.TryThis.addSuggestion (← getRef) (s2) --(s.map (↑))

/-
Try this:
  def x1 :=
    1
  def x2 :=
    2
-/
printMe

[Damiano Testa]

(I am not sure that the previous message conveys that I am very happy with the suggestions! Even if they still require some work!)

[Thomas Murrills]

`(commandSeq|
  def x1 := 0
  def x2 := 1)

gets rid of the semicolon, but not the lack of newline before the first def!

[Thomas Murrills]

It would also be nice to not have 1 on a newline, but that seems to be just how command prettyprints anyway.

[Damiano Testa]

I guess that I would like a "line-break separated sequence".

[Damiano Testa]

Well, my intended case would have more likely a lemma rather than a def, so the line break after := is not so bad.

[Damiano Testa]

I updated the snippet above using Kyle's line breaks. Now, the formatting nit-pick is the indentation of all the lines.

[Thomas Murrills]

Maybe the solution is creating a custom pretty printer for commandSeq—or better, a pretty printer for a sepBy1Linebreak combinator.

[Thomas Murrills]

(By the way, the way to create a newline after "Try this" is to use addSuggestion (header := "Try this:\n")!)

[Thomas Murrills]

(Unrelated: It seems the coercions from TSyntax to Suggestion aren't working as I had hoped—I'd also like Array (TSyntax _) to coerce to Array Suggestion. I'll see if I can fix this...)

[Damiano Testa]

Thanks!

Thomas Murrills said:

(Unrelated: It seems the coercions from TSyntax to Suggestion aren't working as I had hoped—I'd also like Array (TSyntax _) to coerce to Array Suggestion. I'll see if I can fix this...)

Btw, how can I go from a Array (TSyntax command) to a TSyntax commandSeq? I would like a fold-like operation, but I cannot make it work...

[Thomas Murrills]

Given as : Array (TSyntax `command), `(commandSeq|$as*)seems to work! :)

[Damiano Testa]

Wow, awesome!

Syntax is such a foreign concept for me...

[Thomas Murrills]

Thomas Murrills said:

(Unrelated: It seems the coercions from TSyntax to Suggestion aren't working as I had hoped—I'd also like Array (TSyntax _) to coerce to Array Suggestion. I'll see if I can fix this...)

Oh wait, they seem fine now. I wonder what was going wrong on my end; a second ago I was getting a red squiggle.

[Damiano Testa]

I found that they are very susceptible to imports.

[Thomas Murrills]

Oh, really! What imports mess it up?

[Damiano Testa]

I could not figure it out...

[Damiano Testa]

But I also had the up-arrow give a squiggle and suddenly not give it anymore after messing with the imports.

[Thomas Murrills]

Ideally no up-arrow should be required (I'm not sure if this changes things?); what's odd is that I don't think I changed the imports between my red squiggle and the lack of it. But I did restart lean and mess with the lake folder...hmm.

[Damiano Testa]

Well, maybe the imports were not the cause for me either -- I simply did not understand what changed and assumed that it was the imports, where some coercion suddenly was available.

[Thomas Murrills]

It could very well be! I could also be forgetting something I did to the imports. :P

[Damiano Testa]

Ok, I was messing around with this, since I wanted to have a "deprecation helper". This is what I can achieve so far:

deprecate to good_mul good_add
/-- I also have a doc-string -/
@[to_additive "As do I"]
theorem aDeprecatable_mul : True := .intro

/-
Try this:
/-- I also have a doc-string -/
  @[to_additive "As do I"]
  theorem aDeprecatable_mul : True :=
    .intro
  @[deprecated]
  alias aDeprecatable_add := good_mul
  @[deprecated]
  alias aDeprecatable_mul := good_add
-/

[Damiano Testa]

The idea is that you write deprecate to you then provide the new names, and then the command to deprecate. The "tool" then prints for you the same command (ideally it would rename the declaration, but I have not gotten there yet) and also prints the aliases deprecating the old names in favor of the new ones.

[Damiano Testa]

What is still missing:

• rename the old declarations with the new names;
• add a comment with today's date to the deprecations;
• improve the formatting of the Try this suggestion.

[Thomas Murrills]

Oh, handling the indentation might be easy:

syntax commandSeq := ppDedent(sepBy1IndentSemicolon(command))

It looks like that also obviates the need for header := "Try this:\n"—I'm not totally sure why. Nevermind, I was using syntax with a line break. :P

[Thomas Murrills]

(That probably suffices (re: indentation) for testing and such—but I think if this were to eventually be PR'd, we really should come up with the "right" combinator for a command sequence, which should not be so general as to allow ;.)

[Damiano Testa]

I pushed what I have to branch#adomani/deprecation_tool. Feel free to adapt: I'm done for the day!

[Kyle Miller]

By the way, I found why it is that ` (...) supports a sequence of commands (like in my code block). It's docs#Lean.Parser.Command.quot

I wonder if core should get a commandSeq parser and have this `(...) syntax return something with that kind rather than a null node?