mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
70 lines
1.9 KiB
Lean4
70 lines
1.9 KiB
Lean4
noncomputable def badPair : Nat × (Nat × Nat) := ⟨1, ⟨2, 3⟩⟩
|
||
noncomputable def badFun (a : Nat) : Nat := a
|
||
|
||
structure S (n : Nat)
|
||
structure T where
|
||
n : Nat
|
||
|
||
def test1 : S badPair.2.1 := {}
|
||
|
||
/--
|
||
error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'badPair', which is 'noncomputable'
|
||
-/
|
||
#guard_msgs in
|
||
def test2 : T := { n := badPair.2.1 }
|
||
|
||
def test3 (a : Nat) : S (badFun a) := {}
|
||
def test4 (a : Nat) : S ((badFun a) + 1) := {}
|
||
|
||
/--
|
||
error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'badFun', which is 'noncomputable'
|
||
-/
|
||
#guard_msgs in
|
||
def test5 (a : Nat) : T := { n := badFun a }
|
||
|
||
/--
|
||
error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'badFun', which is 'noncomputable'
|
||
-/
|
||
#guard_msgs in
|
||
def test6 (a : Nat) : T := { n := 2 * (badFun a) }
|
||
|
||
structure U (a : Nat × Nat)
|
||
structure V where
|
||
a : Nat × Nat
|
||
|
||
def test7 (a : Nat) : U (⟨badFun a, 0⟩) := {}
|
||
def test8 (a : Nat) : U ((V.mk ⟨badFun a, 1⟩).a) := {}
|
||
|
||
/--
|
||
error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'badFun', which is 'noncomputable'
|
||
-/
|
||
#guard_msgs in
|
||
def test9 (a : Nat) : V := ⟨a, badFun a⟩
|
||
|
||
universe u
|
||
|
||
def Erased (α : Sort u) : Sort max 1 u :=
|
||
{ s : α → Prop // ∃ a, (a = ·) = s }
|
||
|
||
@[macro_inline] def Erased.mk {α} (a : α) : Erased α :=
|
||
⟨fun b => a = b, a, rfl⟩
|
||
|
||
noncomputable def Erased.out {α} : Erased α → α
|
||
| ⟨_, h⟩ => Classical.choose h
|
||
|
||
structure Foo where
|
||
spec : Erased Nat
|
||
data : Nat
|
||
|
||
def test10 : Foo where
|
||
spec := Erased.mk (Erased.mk 0).out
|
||
data := 0
|
||
|
||
/--
|
||
error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Erased.out', which is 'noncomputable'
|
||
-/
|
||
#guard_msgs in
|
||
def test11 : Foo where
|
||
spec := Erased.mk 0
|
||
data := (Erased.mk 0).out
|