diff --git a/tests/common.sh b/tests/common.sh index 04e5522453..a5759abe14 100644 --- a/tests/common.sh +++ b/tests/common.sh @@ -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 diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index c0e8a50dfb..effaec57c4 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -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}} diff --git a/tests/lean/interactive/hoverDot.lean.expected.out b/tests/lean/interactive/hoverDot.lean.expected.out index d9838408d4..7751666093 100644 --- a/tests/lean/interactive/hoverDot.lean.expected.out +++ b/tests/lean/interactive/hoverDot.lean.expected.out @@ -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"}}