merge: branch 'dev' into chore/cleanup

Pantograph/Frontend/InfoTree.lean

@@ -25,9 +25,9 @@ protected def Info.stx? : Info → Option Syntax
   | .ofCustomInfo         info => info.stx
   | .ofFVarAliasInfo      _    => none
   | .ofFieldRedeclInfo    info => info.stx
-  | .ofOmissionInfo       info => info.stx
   | .ofChoiceInfo         info => info.stx
   | .ofPartialTermInfo    info => info.stx
+  | .ofDelabTermInfo      info => info.stx
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 protected def Info.isOriginal (i : Info) : Bool :=
   match i.stx? with
@@ -142,9 +142,9 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
       | .ofCustomInfo _ => pure "[custom]"
       | .ofFVarAliasInfo _ => pure "[fvar]"
       | .ofFieldRedeclInfo _ => pure "[field_redecl]"
-      | .ofOmissionInfo _ => pure "[omission]"
       | .ofChoiceInfo _ => pure "[choice]"
       | .ofPartialTermInfo  _ => pure "[partial_term]"
+      | .ofDelabTermInfo _ => pure "[delab_term]"
       let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
       return s!"{node}\n{children}"
     else throw <| IO.userError "No `ContextInfo` available."

Pantograph/Tactic/Assign.lean

@@ -28,15 +28,16 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
   Elab.Tactic.replaceMainGoal nextGoals
 
 def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
-  Meta.transform src λ
+  Meta.transform src λ expr =>
-    | .app (.app (.const ``sorryAx ..) type) .. => do
+    if expr.isSorry then do
-      let type ← instantiateMVars type
+      let type ← instantiateMVars (expr.getArg! 0 |>.bindingBody!)
       if type.hasSorry then
         throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
       let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
       modify (mvar.mvarId! :: .)
       pure $ .done mvar
-    | _ => pure .continue
+    else
+      pure .continue
 
 -- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals.
 def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do

Pantograph/Version.lean

@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.2.25"
+def version := "0.3.0-rc.1"
 
 end Pantograph

Test/Metavar.lean

@@ -192,7 +192,7 @@ def test_proposition_generation: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "?m.29 x"])
+    #[.some "?m.30 x"])
   addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
   let assign := "Eq.refl x"

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1741352980,
+        "lastModified": 1738453229,
-        "narHash": "sha256-+u2UunDA4Cl5Fci3m7S643HzKmIDAe+fiXrLqYsR2fs=",
+        "narHash": "sha256-7H9XgNiGLKN1G1CgRh0vUL4AheZSYzPm+zmZ7vxbJdo=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "f4330d22f1c5d2ba72d3d22df5597d123fdb60a9",
+        "rev": "32ea77a06711b758da0ad9bd6a844c5740a87abd",
         "type": "github"
       },
       "original": {
@@ -44,11 +44,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1741472588,
+        "lastModified": 1739073990,
-        "narHash": "sha256-XnMeMZKuspEphP+fEq4soc3PY7Nz+gsMPjlsXbobyrA=",
+        "narHash": "sha256-VmLkZf4+1HWrIDB/JUlPOAmOlutR6XTFRhDzDYJcYZM=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "cffeb67d58e02b50ccb9acd51b0212dc653ed6ce",
+        "rev": "7a6faedc6c3ab35c42add15c354bf69542b9a6e6",
         "type": "github"
       },
       "original": {
@@ -75,17 +75,14 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1740877520,
+        "lastModified": 1738452942,
-        "narHash": "sha256-oiwv/ZK/2FhGxrCkQkB83i7GnWXPPLzoqFHpDD3uYpk=",
+        "narHash": "sha256-vJzFZGaCpnmo7I6i416HaBLpC+hvcURh/BQwROcGIp8=",
-        "owner": "nix-community",
+        "type": "tarball",
-        "repo": "nixpkgs.lib",
+        "url": "https://github.com/NixOS/nixpkgs/archive/072a6db25e947df2f31aab9eccd0ab75d5b2da11.tar.gz"
-        "rev": "147dee35aab2193b174e4c0868bd80ead5ce755c",
-        "type": "github"
       },
       "original": {
-        "owner": "nix-community",
+        "type": "tarball",
-        "repo": "nixpkgs.lib",
+        "url": "https://github.com/NixOS/nixpkgs/archive/072a6db25e947df2f31aab9eccd0ab75d5b2da11.tar.gz"
-        "type": "github"
       }
     },
     "nixpkgs-lib_2": {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0