Skip to content

Commit ddcaed4

Browse files
KhaKha
committed
chore: register test files in lakefile for consistent privacy mangling
1 parent 6fd84dc commit ddcaed4

10 files changed

+37
-28
lines changed

‎tests/lakefile.toml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,3 +3,7 @@ name = "tests"
33
# Allow `module` in tests when opened in the language server.
44
# Enabled during actual test runs in the respective test_single.sh.
55
moreGlobalServerArgs = ["-Dexperimental.module=true"]
6+
7+
[[lean_lib]]
8+
name = "Tests"
9+
globs = ["lean.*"]

‎tests/lean/binopInfoTree.lean.expected.out‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int
6060
• [Term] n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent
6161
• [Completion-Id] n : none @ ⟨7, 29⟩-⟨7, 30⟩
6262
• [Term] n : Nat @ ⟨7, 29⟩-⟨7, 30⟩
63-
• [Term] ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1»
63+
• [Term] ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_lean_binopInfoTree___macroRules_term_+'__1»
6464
• [MacroExpansion]
6565
m +' l
6666
===>

‎tests/lean/dbgMacros.lean.expected.out‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
PANIC at f dbgMacros:2:14: unexpected zero
1+
PANIC at f lean.dbgMacros:2:14: unexpected zero
22
0
33
9
4-
PANIC at g dbgMacros:10:14: unreachable code has been reached
4+
PANIC at g lean.dbgMacros:10:14: unreachable code has been reached
55
0
66
0
7-
PANIC at h dbgMacros:16:0: assertion violation: x != 0
7+
PANIC at h lean.dbgMacros:16:0: assertion violation: x != 0
88
0
99
f2, x: 10
1010
11

‎tests/lean/ppNotationCode.lean.expected.out‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
[Elab.definition.body] «term_+++_» : Lean.TrailingParserDescr :=
22
Lean.ParserDescr.trailingNode `«term_+++_» 45 46
33
(Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46))
4-
[Elab.definition.body] «_aux_ppNotationCode___macroRules_term_+++__1» : Lean.Macro :=
4+
[Elab.definition.body] «_aux_lean_ppNotationCode___macroRules_term_+++__1» : Lean.Macro :=
55
fun x =>
66
have __discr := x;
77
if __discr.isOfKind `«term_+++_» = true then
@@ -24,7 +24,7 @@
2424
else
2525
have __discr := x;
2626
throw Lean.Macro.Exception.unsupportedSyntax
27-
[Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
27+
[Elab.definition.body] _aux_lean_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
2828
fun x =>
2929
have __discr := x;
3030
if __discr.isOfKind `Lean.Parser.Term.app = true then

‎tests/lean/root.lean.expected.out‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ root.lean:35:14-35:22: error: protected declarations must be in a namespace
77
root.lean:41:7-41:8: error(lean.unknownIdentifier): Unknown identifier `h`
88
root.lean:43:7-43:8: error(lean.unknownIdentifier): Unknown identifier `f`
99
Bla.f (x : Nat) : Nat
10-
_private.root.0.prv : Nat -> Nat
10+
_private.lean.root.0.prv : Nat -> Nat
1111
root.lean:90:89-90:93: error: unsolved goals
1212
x : Nat
1313
⊢ isEven (x + 1 + 1) = isEven x

‎tests/lean/run/decideNative.lean‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -126,5 +126,7 @@ instance : Decidable ItsTrue2 :=
126126
panic! "oh no"
127127

128128
-- Note: this test fails within VS Code
129-
/-- info: output: PANIC at instDecidableItsTrue2 decideNative:126:2: oh no -/
129+
/--
130+
info: output: PANIC at instDecidableItsTrue2 lean.run.decideNative:126:2: oh no
131+
-/
130132
#guard_msgs in example : ItsTrue2 := by collect_stdout native_decide

‎tests/lean/run/sorry.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -70,9 +70,9 @@ Showing source position when surfacing differences.
7070
error: Type mismatch
7171
sorry
7272
has type
73-
sorry `«sorry:77:43»
73+
sorry `«lean.run.sorry:77:43»
7474
but is expected to have type
75-
sorry `«sorry:77:25»
75+
sorry `«lean.run.sorry:77:25»
7676
-/
7777
#guard_msgs in example : sorry := (sorry : sorry)
7878

@@ -98,7 +98,7 @@ error: Unknown identifier `a`
9898
---
9999
error: Unknown identifier `b`
100100
---
101-
trace: ⊢ sorry `«sorry:106:10» = sorry `«sorry:106:14»
101+
trace: ⊢ sorry `«lean.run.sorry:106:10» = sorry `«lean.run.sorry:106:14»
102102
-/
103103
#guard_msgs in
104104
set_option autoImplicit false in

‎tests/lean/run/test_single.sh‎

100644100755
Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
#!/usr/bin/env bash
22
source ../../common.sh
33

4+
# `--root` to infer same private names as in the server
45
# Elab.inServer to allow for arbitrary `#eval`
5-
exec_check_raw lean -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f"
6+
exec_check_raw lean --root=../.. -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f"

‎tests/lean/sint_basic.lean.expected.out‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -73,11 +73,11 @@ true
7373
true
7474
true
7575
[Compiler.IR] [result]
76-
def _private.sint_basic.0.myId8 (x_1 : u8) : u8 :=
76+
def _private.lean.sint_basic.0.myId8 (x_1 : u8) : u8 :=
7777
ret x_1
78-
def _private.sint_basic.0.myId8._boxed (x_1 : tagged) : tagged :=
78+
def _private.lean.sint_basic.0.myId8._boxed (x_1 : tagged) : tagged :=
7979
let x_2 : u8 := unbox x_1;
80-
let x_3 : u8 := _private.sint_basic.0.myId8 x_2;
80+
let x_3 : u8 := _private.lean.sint_basic.0.myId8 x_2;
8181
let x_4 : tobj := box x_3;
8282
ret x_4
8383
Int16 : Type
@@ -155,11 +155,11 @@ true
155155
true
156156
true
157157
[Compiler.IR] [result]
158-
def _private.sint_basic.0.myId16 (x_1 : u16) : u16 :=
158+
def _private.lean.sint_basic.0.myId16 (x_1 : u16) : u16 :=
159159
ret x_1
160-
def _private.sint_basic.0.myId16._boxed (x_1 : tagged) : tagged :=
160+
def _private.lean.sint_basic.0.myId16._boxed (x_1 : tagged) : tagged :=
161161
let x_2 : u16 := unbox x_1;
162-
let x_3 : u16 := _private.sint_basic.0.myId16 x_2;
162+
let x_3 : u16 := _private.lean.sint_basic.0.myId16 x_2;
163163
let x_4 : tobj := box x_3;
164164
ret x_4
165165
Int32 : Type
@@ -237,12 +237,12 @@ true
237237
true
238238
true
239239
[Compiler.IR] [result]
240-
def _private.sint_basic.0.myId32 (x_1 : u32) : u32 :=
240+
def _private.lean.sint_basic.0.myId32 (x_1 : u32) : u32 :=
241241
ret x_1
242-
def _private.sint_basic.0.myId32._boxed (x_1 : tobj) : tobj :=
242+
def _private.lean.sint_basic.0.myId32._boxed (x_1 : tobj) : tobj :=
243243
let x_2 : u32 := unbox x_1;
244244
dec x_1;
245-
let x_3 : u32 := _private.sint_basic.0.myId32 x_2;
245+
let x_3 : u32 := _private.lean.sint_basic.0.myId32 x_2;
246246
let x_4 : tobj := box x_3;
247247
ret x_4
248248
Int64 : Type
@@ -320,12 +320,12 @@ true
320320
true
321321
true
322322
[Compiler.IR] [result]
323-
def _private.sint_basic.0.myId64 (x_1 : u64) : u64 :=
323+
def _private.lean.sint_basic.0.myId64 (x_1 : u64) : u64 :=
324324
ret x_1
325-
def _private.sint_basic.0.myId64._boxed (x_1 : tobj) : tobj :=
325+
def _private.lean.sint_basic.0.myId64._boxed (x_1 : tobj) : tobj :=
326326
let x_2 : u64 := unbox x_1;
327327
dec x_1;
328-
let x_3 : u64 := _private.sint_basic.0.myId64 x_2;
328+
let x_3 : u64 := _private.lean.sint_basic.0.myId64 x_2;
329329
let x_4 : tobj := box x_3;
330330
ret x_4
331331
ISize : Type
@@ -403,11 +403,11 @@ true
403403
true
404404
true
405405
[Compiler.IR] [result]
406-
def _private.sint_basic.0.myIdSize (x_1 : usize) : usize :=
406+
def _private.lean.sint_basic.0.myIdSize (x_1 : usize) : usize :=
407407
ret x_1
408-
def _private.sint_basic.0.myIdSize._boxed (x_1 : tobj) : tobj :=
408+
def _private.lean.sint_basic.0.myIdSize._boxed (x_1 : tobj) : tobj :=
409409
let x_2 : usize := unbox x_1;
410410
dec x_1;
411-
let x_3 : usize := _private.sint_basic.0.myIdSize x_2;
411+
let x_3 : usize := _private.lean.sint_basic.0.myIdSize x_2;
412412
let x_4 : tobj := box x_3;
413413
ret x_4

‎tests/lean/test_single.sh‎

100644100755
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,7 @@
22
source ../common.sh
33

44
# these tests don't have to succeed
5-
exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f" || true
5+
# `--root` to infer same private names as in the server
6+
# Elab.inServer to allow for arbitrary `#eval`
7+
exec_capture lean --root=.. -DprintMessageEndPos=true -Dlinter.all=false -Dexperimental.module=true -DElab.inServer=true "$f" || true
68
diff_produced

0 commit comments

Comments
 (0)