Skip to content

Commit

Permalink
fix: redundant line breaks in trace messages (#571)
Browse files Browse the repository at this point in the history
This PR ensures that there are no redundant line breaks when the trace
formatter is including a newline at the end of a trace line.

Example (from `whnfProj.lean`):
```lean
import Lean

def h (x : Nat) := x
def f (x : Nat) := x + 1
def g (x : Nat) := (x, x+1).fst


open Lean
open Lean.Meta

def tst (declName : Name) : MetaM Unit := do
  let c ← getConstInfo declName
  lambdaTelescope c.value! fun _ b => do
    trace[Meta.debug] "1. {b}"
    trace[Meta.debug] "2. {← withReducible <| whnf b}"
    trace[Meta.debug] "3. {← withReducibleAndInstances <| whnf b}"
    trace[Meta.debug] "4. {← withDefault <| whnf b}"
    pure ()

set_option trace.Meta.debug true
#eval tst `f
#eval tst `g
```
  • Loading branch information
mhuisi authored Jan 30, 2025
1 parent 3f499d0 commit d13d83e
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 3 deletions.
2 changes: 1 addition & 1 deletion lean4-infoview/package.json
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"name": "@leanprover/infoview",
"version": "0.8.0",
"version": "0.8.1",
"description": "An interactive display for the Lean 4 theorem prover.",
"scripts": {
"watch": "rollup --config --environment NODE_ENV:development --watch",
Expand Down
3 changes: 3 additions & 0 deletions lean4-infoview/src/infoview/index.css
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,9 @@ body {
}

/* Interactive traces */
.trace-line {
display: inline-block;
}
.trace-line:hover {
background-color: #dbeeff;
}
Expand Down
4 changes: 2 additions & 2 deletions package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

0 comments on commit d13d83e

Please sign in to comment.