Pantograph/Frontend/Elab.lean

@@ -122,6 +122,13 @@ protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
 protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
   t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
 
+protected def usedConstants (t: TacticInvocation) : NameSet :=
+  let info := t.info
+  info.goalsBefore
+    |>.filterMap info.mctxAfter.getExprAssignmentCore?
+    |>.map Expr.getUsedConstantsAsSet
+    |>.foldl .union .empty
+
 end TacticInvocation
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
@@ -158,7 +165,13 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
     let tactic ← invocation.ctx.runMetaM {} do
       let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
       return t.pretty
-    return { goalBefore, goalAfter, tactic }
+    let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
+    return {
+      goalBefore,
+      goalAfter,
+      tactic,
+      usedConstants,
+    }
 
 structure InfoWithContext where
   info: Elab.Info

Pantograph/Protocol.lean

@@ -298,6 +298,9 @@ structure InvokedTactic where
   goalBefore: String
   goalAfter: String
   tactic: String
+
+  -- List of used constants
+  usedConstants: Array String
   deriving Lean.ToJson
 
 structure CompilationUnit where

Test/Integration.lean

@@ -167,8 +167,8 @@ example : ∀ (p: Prop), p → p := by
 
 def test_frontend_process : Test :=
   [
-    let file := "example : ∀ (p: Prop), p → p := by\n  intro p h\n  exact h"
-    let goal1 := "p : Prop\nh : p\n⊢ p"
+    let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
+    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
     step "frontend.process"
       [
         ("file", .str file),
@@ -180,14 +180,16 @@ def test_frontend_process : Test :=
          boundary := (0, file.utf8ByteSize),
          invocations? := .some [
            {
-             goalBefore := "⊢ ∀ (p : Prop), p → p",
+             goalBefore := "⊢ ∀ (p q : Prop), p → p ∨ q",
              goalAfter := goal1,
-             tactic := "intro p h",
+             tactic := "intro p q h",
+             usedConstants := #[],
            },
            {
              goalBefore := goal1 ,
              goalAfter := "",
-             tactic := "exact h",
+             tactic := "exact Or.inl h",
+             usedConstants := #["Or.inl"],
            },
          ]
        }],