use decl_name%

Auto/Embedding/LamTermInterp.lean

@@ -268,10 +268,10 @@ abbrev InterpM := StateRefT State MetaState.MetaStateM
 def getLCtxTy! (idx : Nat) : InterpM LamSort := do
   let lctxTyRev ← getLctxTyRev
   if idx ≥ lctxTyRev.size then
-    throwError "getLCtxTy! :: Index out of bound"
+    throwError "{decl_name%} :: Index out of bound"
   match lctxTyRev[idx]? with
   | .some s => return s
-  | .none => throwError "getLCtxTy! :: Unexpected error"
+  | .none => throwError "{decl_name%} :: Unexpected error"
 
 /--
   Turning a sort into `fvar` in a hash-consing manner
@@ -303,7 +303,7 @@ def collectSortFor (ltv : LamTyVal) : LamTerm → InterpM LamSort
 | .atom n => do
   let _ ← sort2FVarId (ltv.lamVarTy n)
   return ltv.lamVarTy n
-| .etom _ => throwError "collectSortFor :: etoms should not occur here"
+| .etom _ => throwError "{decl_name%} :: etoms should not occur here"
 | .base b => do
   let s := b.lamCheck ltv
   let _ ← sort2FVarId s
@@ -325,8 +325,8 @@ def collectSortFor (ltv : LamTyVal) : LamTerm → InterpM LamSort
     if argTy' == argTy && argTy' == s then
       return resTy
     else
-      throwError "collectSortFor :: Application type mismatch"
-  | _ => throwError "collectSortFor :: Malformed application"
+      throwError "{decl_name%} :: Application type mismatch"
+  | _ => throwError "{decl_name%} :: Malformed application"
 where withLCtxTy {α : Type} (s : LamSort) (k : InterpM α) : InterpM α := do
   let lctxTyRev ← getLctxTyRev
   setLctxTyRev (lctxTyRev.push s)

Auto/IR/SMT.lean

@@ -472,7 +472,7 @@ section
     if let .some name := h2lMap.get? cstr then
       return name
     let .some nameSuggestion := nameSuggestion
-      | throwError "IR.SMT.h2Symb :: Fresh high-level constraint {cstr} without name suggestion"
+      | throwError "{decl_name%} :: Fresh high-level constraint {cstr} without name suggestion"
     let name ← processSuggestedName nameSuggestion
     setL2hMap (l2hMap.insert name cstr)
     setH2lMap (h2lMap.insert cstr name)

Auto/LemDB.lean

@@ -42,7 +42,7 @@ partial def LemDB.toHashSet : LemDB → AttrM (Std.HashSet Name)
     let mut ret := Std.HashSet.empty
     for hdb in hdbs do
       let some hdb := state.get? hdb
-        | throwError "LemDB.toHashSet :: Unknown lemma database {hdb}"
+        | throwError "{decl_name%} :: Unknown lemma database {hdb}"
       let hset ← hdb.toHashSet
       ret := ret.insertMany hset
     return ret

Auto/Lib/DeCompile.lean

@@ -86,7 +86,7 @@ private partial def exprDeCompileAux (final : Bool) (e : Expr) : ExprDeCompM Str
     | .natVal l => return toString l
     | .strVal s => return toString s
   | Expr.sort l => return s!"Sort ({l})"
-  | Expr.mvar .. => throwError "exprDeCompile :: Metavariable is not supported"
+  | Expr.mvar .. => throwError "{decl_name%} :: Metavariable is not supported"
   | Expr.fvar f =>
     let some decl := (← getLCtx).find? f
       | throwError "Unknown free variable {e}"
@@ -103,9 +103,9 @@ where
         String.intercalate ", " (us.map toString) ++ "}"
   etaExpandConst (cst : Expr) (appliedArgs : Nat) := do
     if !cst.isConst then
-      throwError s!"exprDeCompile :: etaExpandConst received non-const {cst}"
+      throwError s!"{decl_name%} :: etaExpandConst received non-const {cst}"
     let some val := (← getEnv).find? cst.constName!
-      | throwError s!"exprDeCompile :: Unknown identifier {cst.constName!}"
+      | throwError s!"{decl_name%} :: Unknown identifier {cst.constName!}"
     let ty := val.type
     let lparams := val.levelParams
     let bs := Expr.forallBinders ty
@@ -145,7 +145,7 @@ def exprCollectNames (e : Expr) : StateT (Std.HashSet String) MetaM Unit := do
   | Expr.mvar .. => return
   | Expr.fvar f =>
     let some decl := (← getLCtx).find? f
-      | throwError "Unknown free variable {e}"
+      | throwError "{decl_name%} :: Unknown free variable {e}"
     let name := decl.userName.toString
     modify (fun s => s.insert name)
   | Expr.bvar .. => return

Auto/Lib/ExprExtra.lean

@@ -203,7 +203,7 @@ def Expr.depArgs (e : Expr) : Array Nat := ⟨Expr.depArgsIdx e 0⟩
 -/
 def Expr.constDepArgs (c : Name) : CoreM (Array Nat) := do
   let .some decl := (← getEnv).find? c
-    | throwError "Expr.constDepArgs :: Unknown constant {c}"
+    | throwError "{decl_name%} :: Unknown constant {c}"
   return Expr.depArgs decl.type
 
 def Expr.numLeadingDepArgs : Expr → Nat
@@ -234,14 +234,14 @@ def Expr.formatWithUsername (e : Expr) : MetaM Format := do
   let names ← fvarIds.mapM (fun fid => do
     match ← fid.findDecl? with
     | .some decl => return decl.userName
-    | .none => throwError "Expr.formatWithUsername :: Unknown free variable {(Expr.fvar fid).dbgToString}")
+    | .none => throwError "{decl_name%}e :: Unknown free variable {(Expr.fvar fid).dbgToString}")
   let e := e.replaceFVars (fvarIds.map Expr.fvar) (names.map (Expr.const · []))
   let e ← instantiateMVars e
   let mvarIds := (Expr.collectMVars {} e).result
   let names ← mvarIds.mapM (fun mid => do
     match ← mid.findDecl? with
     | .some decl => return decl.userName
-    | .none => throwError "xpr.formatWithUsername :: Unknown metavariable {(Expr.mvar mid).dbgToString}")
+    | .none => throwError "{decl_name%} :: Unknown metavariable {(Expr.mvar mid).dbgToString}")
   let e := (e.abstract (mvarIds.map Expr.mvar)).instantiateRev (names.map (Expr.const · []))
   return f!"{e}"
 
@@ -257,14 +257,14 @@ unsafe def elabGetExprAndApply : CommandElab := fun stx =>
     match stx with
     | `(command | #getExprAndApply[ $t:term | $i:ident ]) => withRef stx <| do
       let some iexpr ← Term.resolveId? i
-        | throwError "elabGetExprAndApply :: Unknown identifier {i}"
+        | throwError "{decl_name%} :: Unknown identifier {i}"
       let e ← Term.elabTerm t none
       Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
       let e ← Term.levelMVarToParam (← instantiateMVars e)
       let fname := iexpr.constName!
       match (← getEnv).evalConst (Expr → TermElabM Unit) (← getOptions) fname with
       | Except.ok f => f e
-      | Except.error err => throwError "elabGetExprAndApply :: Failed to evaluate {fname} to a term of type (Expr → TermElabM Unit), error : {err}"
+      | Except.error err => throwError "{decl_name%} :: Failed to evaluate {fname} to a term of type (Expr → TermElabM Unit), error : {err}"
     | _ => throwUnsupportedSyntax
 
 /--
@@ -274,7 +274,7 @@ unsafe def elabGetExprAndApply : CommandElab := fun stx =>
 unsafe def exprFromExpr (eToExpr : Expr) : TermElabM Expr := do
   let ty ← Meta.inferType eToExpr
   if ! (← Meta.isDefEq ty (.const ``Expr [])) then
-    throwError "exprFromExpr :: Type `{ty}` of input is not definitionally equal to `Expr`"
+    throwError "{decl_name%} :: Type `{ty}` of input is not definitionally equal to `Expr`"
   let declName := `_exprFromExpr
   let addAndCompile (value : Expr) : TermElabM Unit := do
     let value ← Term.levelMVarToParam (← instantiateMVars value)
@@ -359,7 +359,7 @@ section EvalAtTermElabM
           let α ← reduce (skipTypes := false) α
           synthInstance (mkApp (Lean.mkConst evalClassName [u]) α)
         catch _ =>
-          throwError "expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class"
+          throwError "{decl_name%} :: expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class"
 
   private def mkRunMetaEval (e : Expr) : MetaM Expr :=
     withLocalDeclD `env (mkConst ``Lean.Environment) fun env =>

Auto/Lib/MetaExtra.lean

@@ -40,7 +40,7 @@ def Meta.inspectMVarAssignments : MetaM Unit := do
 def Meta.trySynthInhabited (e : Expr) : MetaM (Option Expr) := do
   let eSort ← Expr.normalizeType (← instantiateMVars (← Meta.inferType e))
   let .sort lvl := eSort
-    | throwError "trySynthInhabited :: {e} is not a type"
+    | throwError "{decl_name%} :: {e} is not a type"
   try
     if let .some inh ← Meta.synthInstance? e then
       return .some inh
@@ -58,10 +58,10 @@ syntax (name := fromMetaTactic) "fromMetaTactic" "[" ident "]" : tactic
 unsafe def evalFromMetaTactic : Tactic.Tactic
 | `(fromMetaTactic | fromMetaTactic [ $i ]) => do
   let some iexpr ← Term.resolveId? i
-    | throwError "evalFromMetaTactic :: Unknown identifier {i}"
+    | throwError "{decl_name%} :: Unknown identifier {i}"
   let mtname := iexpr.constName!
   let Except.ok mt := (← getEnv).evalConst (MVarId → MetaM (List MVarId)) (← getOptions) mtname
-    | throwError "evalFromMetaTactic :: Failed to evaluate {mtname} to a term of type (Expr → TermElabM Unit)"
+    | throwError "{decl_name%} :: Failed to evaluate {mtname} to a term of type (Expr → TermElabM Unit)"
   Tactic.liftMetaTactic mt
 | _ => Elab.throwUnsupportedSyntax
 

Auto/Lib/MetaState.lean

@@ -75,7 +75,7 @@ private def runWithFVars (lctx : LocalContext) (fvarids : Array FVarId) (k : Met
         newlctx := newlctx.mkLocalDecl fvarId userName type bi kind
       | .ldecl _ fvarId userName type value nonDep kind =>
         newlctx := newlctx.mkLetDecl fvarId userName type value nonDep kind
-    | .none => throwError "runWithFVars :: Unknown free variable {Expr.fvar fid}"
+    | .none => throwError "{decl_name%} :: Unknown free variable {Expr.fvar fid}"
   withReader (fun ctx => {ctx with lctx := newlctx}) k
 
 private def runWithIntroducedFVarsImp (m : MetaStateM (Array FVarId × α)) (k : α → MetaM β) : MetaM β := do

Auto/Lib/MonadUtils.lean

@@ -53,13 +53,13 @@ syntax (name := genMonadState) "#genMonadState" term : command
 -/
 def structureProjs (structTy : Expr) : CoreM (Name × Expr × Array (Name × Expr)) := do
   let .const structName lvls := structTy.getAppFn
-    | throwError s!"structureProjs :: Head symbol of {structTy} is not a constant"
+    | throwError s!"{decl_name%} :: Head symbol of {structTy} is not a constant"
   let some structInfo := getStructureInfo? (← getEnv) structName
-    | throwError s!"structureProjs :: {structName} is not a structure"
+    | throwError s!"{decl_name%} :: {structName} is not a structure"
   let .some (.inductInfo structi) := (← getEnv).find? structName
-    | throwError s!"structureProjs :: Unknown identifier {structName}"
+    | throwError s!"{decl_name%} :: Unknown identifier {structName}"
   let [structDotMk] := structi.ctors
-    | throwError s!"structureProjs :: {structName} is not a structure"
+    | throwError s!"{decl_name%} :: {structName} is not a structure"
   let structMkExpr := mkAppN (Expr.const structDotMk lvls) structTy.getAppArgs
   let tyArgs := structTy.getAppArgs
   let nameMap : Std.HashMap Name StructureFieldInfo := Std.HashMap.ofList
@@ -75,7 +75,7 @@ private def elabStx (stx : Term) : TermElabM Expr := do
   Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
   let e ← instantiateMVars expr
   if e.hasMVar then
-    throwError "elabStx :: {e} contains metavariables"
+    throwError "{decl_name%} :: {e} contains metavariables"
   return e
 
 private def addDefnitionValFromExpr (e : Expr) (name : Name) : MetaM Unit := do
@@ -91,9 +91,9 @@ private def addDefnitionValFromExpr (e : Expr) (name : Name) : MetaM Unit := do
 private def elabGenMonadContextAux (m : Term) (stx : Syntax) : CommandElabM Unit := runTermElabM <| fun xs => do
   let mexpr ← elabStx m
   let .const mname _ := mexpr.getAppFn
-    | throwError "elabGenMonadContext :: Unknown monad"
+    | throwError "{decl_name%} :: Unknown monad"
   let .str pre _ := mname
-    | throwError "elabGenMonadContext :: {mname} is not a valid constant name"
+    | throwError "{decl_name%} :: {mname} is not a valid constant name"
   let pureInst ← elabStx (← `(inferInstanceAs (Pure $m)))
   let mctxInst ← elabStx (← `(inferInstanceAs (MonadReader _ $m)))
   let mctxInstTy ← Meta.inferType mctxInst
@@ -122,9 +122,9 @@ where
 private def elabGenMonadStateAux (m : Term) (stx : Syntax) : CommandElabM Unit := runTermElabM <| fun xs => do
   let mexpr ← elabStx m
   let .const mname _ := mexpr.getAppFn
-    | throwError "elabGenMonadState :: Unknown monad"
+    | throwError "{decl_name%} :: Unknown monad"
   let .str pre _ := mname
-    | throwError "elabGenMonadState :: {mname} is not a valid constant name"
+    | throwError "{decl_name%} :: {mname} is not a valid constant name"
   let pureInst ← elabStx (← `(inferInstanceAs (Pure $m)))
   let mstateInst ← elabStx (← `(inferInstanceAs (MonadState _ $m)))
   let mstateInstTy ← Meta.inferType mstateInst

Auto/Parser/TPTP.lean

@@ -854,22 +854,22 @@ def getProof (lamVarTy lamEVarTy : Array LamSort) (cmds : Array Command) : MetaM
           match term2LamTerm pi val with
           | .term (.base .prop) t =>
             ret := ret.push t
-          | .error e => throwError ("getProof :: " ++ e)
-          | lc => throwError "getProof :: Unexpected LamConstr {lc}, expected term"
+          | .error e => throwError (decl_name% ++ " :: " ++ e)
+          | lc => throwError "{decl_name%} :: Unexpected LamConstr {lc}, expected term"
         else
           match val with
           | ⟨.ident name, [ty]⟩ =>
             -- In zipperposition, skolems start with `sk_`
             if name.take 3 == "sk_" then
               match term2LamTerm pi ty with
               | .sort s => pi := pi.addSkolem name s
-              | lc => throwError "getProof :: Unexpected LamConstr {lc}, expected sort"
+              | lc => throwError "{decl_name%} :: Unexpected LamConstr {lc}, expected sort"
             else
               continue
           | _ => continue
       | _ => continue
-    | "include" => throwError "getProof :: `include` should not occur in proof output of TPTP solvers"
-    | _ => throwError "getProof :: Unknown command {cmd}"
+    | "include" => throwError "{decl_name%} :: `include` should not occur in proof output of TPTP solvers"
+    | _ => throwError "{decl_name%} :: Unknown command {cmd}"
   return ret
 
 /-- Returns the unsat core of an array of TSTP steps -/

Auto/Solver/Native.lean

@@ -42,7 +42,7 @@ opaque queryNative : Array Lemma → Array Lemma → MetaM Expr
 def emulateNative (lemmas : Array Lemma) (_ : Array Lemma) : MetaM Expr := do
   let _ ← lemmas.mapM (fun lem => do
     if lem.params.size != 0 then
-      throwError "Solver.emulateNative :: Universe levels parameters are not supported")
+      throwError "{decl_name%} :: Universe levels parameters are not supported")
   let descrs := lemmas.zipWithIndex.map (fun (lem, i) => (Name.mkSimple s!"lem{i}", lem.type, .default))
   let sty := Expr.mkForallFromBinderDescrs descrs (.const ``False [])
   let sorryExpr := Lean.mkApp2 (.const ``sorryAx [.zero]) sty (.const ``Bool.false [])

Auto/Solver/SMT.lean

@@ -97,7 +97,7 @@ private def emitCommands (p : SolverProc) (c : Array IR.SMT.Command) : IO Unit :
 def createSolver (name : SolverName) : MetaM SolverProc := do
   let tlim := auto.smt.timeout.get (← getOptions)
   match name with
-  | .none => throwError "createSolver :: Unexpected error"
+  | .none => throwError "{decl_name%} :: Unexpected error"
   | .z3   => createAux "z3" #["-in", "-smt2", s!"-T:{tlim}"]
   | .cvc4 => throwError "cvc4 is not supported"
   | .cvc5 => createAux "cvc5" #[s!"--tlimit={tlim * 1000}", "--produce-models"]
@@ -111,31 +111,31 @@ axiom autoSMTSorry.{u} (α : Sort u) : α
 def getSexp (s : String) : MetaM (Sexp × String) :=
   match parseSexp s ⟨0⟩ {} with
   | .complete se p => return (se, Substring.toString ⟨s, p, s.endPos⟩)
-  | .incomplete _ _ => throwError s!"getSexp :: Incomplete input {s}"
-  | .malformed => throwError s!"getSexp :: Malformed (prefix of) input {s}"
+  | .incomplete _ _ => throwError s!"{decl_name%} :: Incomplete input {s}"
+  | .malformed => throwError s!"{decl_name%} :: Malformed (prefix of) input {s}"
 
 /--
   Recover id of valid facts from unsat core. Refer to `lamFOL2SMT`
 -/
 def validFactOfUnsatCore (unsatCore : Sexp) : MetaM (Array Nat) := do
   let .app unsatCore := unsatCore
-    | throwError "validFactOfUnsatCore :: Malformed unsat core `{unsatCore}`"
+    | throwError "{decl_name%} :: Malformed unsat core `{unsatCore}`"
   let mut ret := #[]
   for sexp in unsatCore do
     let .atom (.symb name) := sexp
       | continue
     if name.take 11 == "valid_fact_" then
       let .some n := (name.drop 11).toNat?
-        | throwError "validFactOfUnsatCore :: The id {name.drop 11} of {name} is invalid"
+        | throwError "{decl_name%} :: The id {name.drop 11} of {name} is invalid"
       ret := ret.push n
   return ret
 
 /-- Only put declarations in the query -/
 def querySolver (query : Array IR.SMT.Command) : MetaM (Option (Sexp × String)) := do
   if !(auto.smt.get (← getOptions)) then
-    throwError "querySolver :: Unexpected error"
+    throwError "{decl_name%} :: Unexpected error"
   if (auto.smt.solver.name.get (← getOptions) == .none) then
-    logInfo "querySolver :: Skipped"
+    logInfo s!"{decl_name%} :: Skipped"
     return .none
   let name := auto.smt.solver.name.get (← getOptions)
   let solver ← createSolver name
@@ -175,7 +175,7 @@ def querySolver (query : Array IR.SMT.Command) : MetaM (Option (Sexp × String))
 
 def saveQuery (query : Array IR.SMT.Command) : MetaM Unit := do
   if !(auto.smt.save.get (← getOptions)) then
-    throwError "querySolver :: Unexpected error"
+    throwError "{decl_name%} :: Unexpected error"
   let path := auto.smt.savepath.get (← getOptions)
   IO.FS.withFile path IO.FS.Mode.write fun fd =>
     for cmd in query do

Auto/Solver/TPTP.lean

@@ -114,7 +114,7 @@ def queryZEPort (zept : ZEPortType) (query : String) : MetaM String := do
     catch e =>
       let estr := toString (← (Exception.toMessageData e).format)
       if estr.extract ⟨0⟩ ⟨44⟩ != "already exists (error code: 17, file exists)" then
-        throwError "queryZEPort :: Unexpected error"
+        throwError "{decl_name%} :: Unexpected error"
       idx := idx + (← IO.rand 0 100)
   IO.FS.withFile s!"./.zeport_ignore/problem{idx}.p" .writeNew (fun stream => stream.putStr query)
   let solver ← createSolver path idx
@@ -149,7 +149,7 @@ def queryE (query : String) : MetaM String := do
 
 def querySolver (query : String) : MetaM (Array Parser.TPTP.Command) := do
   if !(auto.tptp.get (← getOptions)) then
-    throwError "querySolver :: Unexpected error"
+    throwError "{decl_name%} :: Unexpected error"
   let stdout ← (do
     match auto.tptp.solver.name.get (← getOptions) with
     | .zipperposition => queryZipperposition query