max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: normalize URLs to the language reference in test results (#7782)

Browse source 
Links to the language reference include a version slug, either `latest`
or `v4.X.0`. These are included in hovers, which then get tested. To
avoid test breakages, in the testing framework we normalize all such URL
prefixes back to `REFERENCE`.
This commit is contained in:
Kim Morrison 2025-04-02 17:17:31 +11:00 • committed by GitHub
parent 85f94abe19
commit 1ee7e1a9d8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 15 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/common.sh
View file

@ -48,9 +48,13 @@ function exec_capture_raw {
function exec_capture {
# backtraces are system-specific, strip them
# mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g' > "$f.produced.out"
# similarly, links to the language reference may have URL components depending on the toolchain, so normalize those
LEAN_BACKTRACE=0 "$@" 2>&1 \
| perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g' \
| perl -pe 's/https:\/\/lean-lang\.org\/doc\/reference\/(v?[0-9.]+(-rc[0-9]+)?|latest)/REFERENCE/g' > "$f.produced.out"
}
# Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise.
function check_ret {
[ -n "${expected_ret+x}" ] || expected_ret=0

12
tests/lean/interactive/hover.lean.expected.out
View file

@ -20,7 +20,7 @@
{"start": {"line": 12, "character": 4}, "end": {"line": 12, "character": 12}},
"contents":
{"value":
"```lean\nNat.zero : Nat\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.zero : Nat\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 21, "character": 2}}
@ -521,7 +521,7 @@
{"start": {"line": 257, "character": 4}, "end": {"line": 257, "character": 9}},
"contents":
{"value":
"```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 257, "character": 15}}
@ -530,7 +530,7 @@
"end": {"line": 257, "character": 18}},
"contents":
{"value":
"```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 260, "character": 6}}
@ -538,7 +538,7 @@
{"start": {"line": 260, "character": 4}, "end": {"line": 260, "character": 9}},
"contents":
{"value":
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 260, "character": 17}}
@ -547,7 +547,7 @@
"end": {"line": 260, "character": 20}},
"contents":
{"value":
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 263, "character": 27}}
@ -565,7 +565,7 @@
"end": {"line": 263, "character": 36}},
"contents":
{"value":
"```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hover.lean"},
"position": {"line": 269, "character": 2}}

8
tests/lean/interactive/hoverDot.lean.expected.out
View file

@ -20,7 +20,7 @@
{"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 18}},
"contents":
{"value":
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hoverDot.lean"},
"position": {"line": 16, "character": 11}}
@ -34,7 +34,7 @@
{"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}},
"contents":
{"value":
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hoverDot.lean"},
"position": {"line": 19, "character": 13}}
@ -48,7 +48,7 @@
{"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}},
"contents":
{"value":
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}
{"textDocument": {"uri": "file:///hoverDot.lean"},
"position": {"line": 22, "character": 14}}
@ -62,5 +62,5 @@
{"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}},
"contents":
{"value":
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](REFERENCE/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*",
"kind": "markdown"}}