Checkpointing subcommands

Stream: lean4

[Tomas Skrivan]

When I have a macro that generates multiple commands, would it be possible to have checkpointing between the generated commands?

Example

def foo (n : Nat) : IO Unit := do
  IO.sleep 1000
  IO.println s!"done {n}"

syntax "#foo" term,+ : command
macro_rules
| `(#foo $n) => `(#eval foo $n)
| `(#foo $n,$ns,*) =>
  `(#foo $n
    #foo $ns,*)

#foo 1,2,3,4

When I changes #foo 1,2,3,4 to #foo 1,2,3,4,5 I would like to wait only one second instead of five. Also I when I change #foo 1,2,3,4 to #foo 1,42,3,4 I want to see "done 42" in my Goal View after one seconds instead of four.

I'm expecting it is not possible for arbitrary macro. I guess this would require for example that #foo 1,2 generates the commands in the order i.e. #eval foo 1; #eval foo 2 instead of #eval foo 2; #eval foo 1

---

Here is a concrete example of what I'm dealing with. I'm defining a function conv1d doing one dimensional convolution and I want to derive gradients in all its arguments. The whole definition with the annotations def conv1d ... := ... argument x ... argument w ... is a single big command. There is a sub command adjDiff by <convSeq> that symbolically computes the gradien. The problem is that the Goal View response is fairly poor as each time I change the tactic the whole command needs to be re-elaborated.

  def conv1d {N n} (x : Fin N → ℝ) (w : Fin n → ℝ) (b : ℝ) : Fin N → ℝ :=
     λ i => ∑ i', w i' * x (i.shift i') + b
  argument x [Fact (N≠0)] [Fact (n≠0)]
    hasAdjDiff,
    adjDiff by
      simp only [adjointDifferential, conv1d]
      simp[hold, sum_into_lambda]
      enter[x];
      rw [sum_swap]
      simp only [kron_smul_assoc, sum_of_kron_2]
      simp
  argument w [Fact (N≠0)] [Fact (n≠0)]
    hasAdjDiff,
    adjDiff by
      simp only [adjointDifferential, conv1d]
      simp[hold, sum_into_lambda]
      simp only [kron_smul_assoc, sum_of_kron_2]
      simp
  argument b [Fact (N≠0)] [Fact (n≠0)]
    hasAdjDiff,
    adjDiff by
      simp only [adjointDifferential]
      unfold conv1d; simp

Each of hasAdjDiff or adjDiff by <convSeq> generates a new instance or simp theorem.

[Tomas Skrivan]

Effectively I want a syntactic family commands which would allow me to define a command that has access to the syntax of the previous commands but not the later ones. With this restriction, I believe that the checkpointing can be done.