Created
October 2, 2025 01:05
-
-
Save algebraic-dev/f3e975234c100d051552529b54820106 to your computer and use it in GitHub Desktop.
HasCallstack weird thing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Std.Internal.UV | |
| import Lean | |
| import Lean.Attributes | |
| open Std.Internal.UV | |
| open Lean Elab Term | |
| -- Based on: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Introducing.20the.20nest/near/387447219 | |
| structure CallStack where | |
| list : Std.Queue (String × String × Nat × Nat) := .empty | |
| size : Nat := 0 | |
| private def CallStack.overLimit (stack: CallStack) : CallStack := | |
| if stack.size > 15 then | |
| { stack with list := stack.list.dequeue?.map Prod.snd |>.get!, size := 15 } | |
| else | |
| stack | |
| def CallStack.push (stack: CallStack) (name : String) (filename : String) (line col : Nat) : CallStack := | |
| { stack with list := stack.list.enqueue (name, filename, line, col), size := stack.size + 1 } | |
| |>.overLimit | |
| -- Macro | |
| syntax (name := posMa) "hasCallStack" : term | |
| @[term_elab posMa] | |
| def elabhasCallstack : TermElab := fun _stx _expectedType? => do | |
| let some pos := (← getRef).getPos? | |
| | throwError "no position info" | |
| let fm ← getFileMap | |
| let p := fm.toPosition pos | |
| let line := p.line | |
| let col := p.column | |
| let declName? ← getDeclName? | |
| let fnName := match declName? with | |
| | some name => name.toString | |
| | none => "<unknown>" | |
| let callstackType ← `(CallStack) | |
| let callstackTypeExpr ← elabTerm callstackType none | |
| let lctx ← getLCtx | |
| let mut stackFVarId? : Option FVarId := none | |
| for localDecl in lctx do | |
| if localDecl.isImplementationDetail then | |
| continue | |
| let declType := localDecl.type | |
| if (← Meta.isDefEq declType callstackTypeExpr) then | |
| stackFVarId? := some localDecl.fvarId | |
| break | |
| let filename ← getFileName | |
| let cwd ← System.cwd | |
| let filename := filename.stripPrefix cwd | |
| let stackExpr ← do | |
| if let some stackFVarId := stackFVarId? then | |
| exprToSyntax (mkFVar stackFVarId) | |
| else | |
| `({}) | |
| let result ← elabTerm (← `(CallStack.push $stackExpr $(quote fnName) $(quote filename) $(quote line) $(quote col))) none | |
| return result | |
| def err (s : String) (x : CallStack := by exact hasCallStack) : IO Unit := do | |
| let mut message := s!"error: {s}\n" | |
| for (name, filename, line, col) in x.list.toArray.reverse do | |
| message := message ++ s!" at {name} ({filename}:{line}:{col + 1})\n" | |
| throw (.userError message) | |
| def t (l : Nat) (x : CallStack := by exact hasCallStack) : IO Unit := | |
| match l with | |
| | 0 => err "failed" | |
| | n + 1 => t n | |
| def g (x : CallStack := by exact hasCallStack) : IO Unit := do | |
| t 5 | |
| /-- | |
| error: error: failed | |
| at t (/build/client.lean:78:10) | |
| at t (/build/client.lean:79:14) | |
| at t (/build/client.lean:79:14) | |
| at t (/build/client.lean:79:14) | |
| at t (/build/client.lean:79:14) | |
| at t (/build/client.lean:79:14) | |
| at g (/build/client.lean:82:3) | |
| at _eval (/build/client.lean:96:7) | |
| -/ | |
| #guard_msgs in | |
| #eval g |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment