custom incremental tactic and commands

Stream: lean4

[Tomas Skrivan]

Having incrementality in the new Lean version is really nice!

I'm interested in writing my own incremental commands and tactics. Are there any simple examples of incremental commands? Also, I have noticed that conv is not incremental, how would I go about implementing an incremental elaborator for convSeq?

[Tomas Skrivan]

I'm trying to make sense of https://github.com/leanprover/lean4/blob/d5a45dfa8b2600e300bd1968e91f2b17951d5e98/src/Lean/Elab/Tactic/BuiltinTactic.lean#L280 and https://github.com/leanprover/lean4/blob/d5a45dfa8b2600e300bd1968e91f2b17951d5e98/src/Lean/Elab/Term.lean#L356
I'm a bit unsure if I'm digging too deep or not.

[Sebastian Ullrich]

You can take a look at the existing builtin_incremental tactics but it is very much not simple. There is some high-level documentation in the library note "Incremental Command Elaboration".

[Tomas Skrivan]

Here is a simple macro #def_strings a b c which just expands into

def a := "a"
def b := "b"
def c := "c"

How can I make this incremental?

code

import Lean

open Lean

syntax (name:=defStringsStx) "#def_strings" ident* : command

macro_rules (kind := defStringsStx)
| `(#def_strings $x:ident) =>
      let s := Syntax.mkStrLit x.getId.toString
      `(def $x : String := by sleep 1000; exact $s)
| `(#def_strings $x:ident $xs:ident*) =>
  `(#def_strings $x
    #def_strings $xs*)


#def_strings
  a
  b
  c
  d
  e
  f


#check a
#check b
#check c
#check d
#check e
#check f

[Tomas Skrivan]

I have a solution! The command #def_strings a b c ... defines def a := "a", def b := "b", ... incrementally. To see the effect I made sure that each new definition takes 1s to elaborate.

One big missing thing is to update the info tree, but I have no experience with that.

The solution is an extremely stripped down version of elabCommand

code

import Lean

open Lean Elab Command

@[incremental]
syntax (name:=defStringsStx) "#def_strings" ident* : command


structure CommandSeqSnapshot extends Language.Snapshot where
  data : Array (Syntax × Command.State)
deriving Nonempty, TypeName
instance : Language.ToSnapshotTree CommandSeqSnapshot where
  toSnapshotTree s := ⟨s.toSnapshot, #[]⟩


@[command_elab defStringsStx, incremental]
def defStringsElab : CommandElab := fun stx =>
match stx with
| `(#def_strings $xs*) => do
  withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do
    if let some snap := (←read).snap? then
      let oldSnap? := snap.old?.map (·.val.get.toTyped? CommandSeqSnapshot) |>.join
      let oldData := oldSnap?.map (fun old => old.data) |>.getD #[]

      let mut reuse := true
      let mut newData := #[]

      for x in xs, i in [0:xs.size] do

        -- reuse old state if possible
        if h : reuse ∧ i < oldData.size then
          let (x', oldState) := oldData[i]
          if x == x' then
            modify (fun _ => oldState)
            newData := newData.push (x, oldState)
            continue

        reuse := false

        let s := Syntax.mkStrLit x.getId.toString
        withoutCommandIncrementality true do
          elabCommand (← `(def $x : String := by sleep 1000; exact $s))
        newData := newData.push (x.raw, ← get)

      snap.new.resolve <| .ofTyped {
          diagnostics := .empty
          data := newData
          : CommandSeqSnapshot
      }
    else
      throwError "no snapshot"
| _ => throwUnsupportedSyntax



#def_strings a b c d e f


#check a
#check b
#check c
#check d
#check e
#check f