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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-30 17:52:30 -08:00
parent 0db02c3911
commit 5a151ca64c
16 changed files with 121 additions and 124 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/compiler/expr.lean.expected.out
View file

@ -1,3 +1,3 @@
f a b
hash: 4194966675
hash: 3375555335
#[a, b]

2
tests/lean/450.lean.expected.out
View file

@ -1,4 +1,4 @@
450.lean:2:6-2:7: error: failed to infer 'let' declaration type
450.lean:2:11-2:12: error: don't know how to synthesize placeholder
context:
⊢ ?m
450.lean:2:6-2:7: error: failed to infer 'let' declaration type

3
tests/lean/906.lean.expected.out
View file

@ -1,3 +1,2 @@
906.lean:2:4-2:15: warning: declaration uses 'sorry'
906.lean:12:2-12:28: error: tactic 'simp' failed, nested error:
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
906.lean:12:2-12:28: error: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

31
tests/lean/CompilerElimDeadBranches.lean.expected.out
View file

@ -1,9 +1,9 @@
[Compiler.elimDeadBranches] Eliminating addSomeVal._redArg with #[("_x.37",
[Compiler.elimDeadBranches] Eliminating addSomeVal._redArg with #[("val.20", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
("val.16", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
("_x.37",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor
`Option.some
#[Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]]),
("val.20", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
("val.16", Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Nat.zero #[]),
("_x.35", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.36",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
@ -47,22 +47,21 @@
let _x.5 := some _ _x.4;
return _x.5
[Compiler.result] size: 1 def addSomeVal x : Option Nat := let _x.1 := addSomeVal._redArg; return _x.1
[Compiler.elimDeadBranches] Eliminating monadic with #[("_x.207",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
[Compiler.elimDeadBranches] Eliminating monadic with #[("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.91",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.ok #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("_x.88", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.205",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.211",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.212",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("_x.91",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.ok #[Lean.Compiler.LCNF.UnreachableBranches.Value.top])]
("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.211",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.207",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("_x.205",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top)]
[Compiler.elimDeadBranches] Threw away cases _x.211 branch Option.none
[Compiler.elimDeadBranches] Threw away cases _x.212 branch Option.none
[Compiler.elimDeadBranches] Threw away cases _x.205 branch Except.ok

8
tests/lean/argNameAtPlaceholderError.lean.expected.out
View file

@ -1,11 +1,11 @@
argNameAtPlaceholderError.lean:8:13-8:14: error: don't know how to synthesize placeholder for argument 'expectedType?'
context:
stx : Syntax
⊢ Option Expr
argNameAtPlaceholderError.lean:8:15-8:16: error: don't know how to synthesize placeholder for argument 'catchExPostpone'
context:
stx : Syntax
⊢ Bool
argNameAtPlaceholderError.lean:8:13-8:14: error: don't know how to synthesize placeholder for argument 'expectedType?'
context:
stx : Syntax
⊢ Option Expr
argNameAtPlaceholderError.lean:8:11-8:12: error: don't know how to synthesize placeholder for argument 'stx'
context:
stx : Syntax

8
tests/lean/derivingHashable.lean.expected.out
View file

@ -1,4 +1,4 @@
1182690223427565068
4993501213146294156
21469593610
6073217436820174634
10047522373567521337
18299533346889728271
5501096720095961210
6693367456468911342

8
tests/lean/evalNone.lean.expected.out
View file

@ -2,11 +2,11 @@ evalNone.lean:1:6-1:10: error: don't know how to synthesize implicit argument
@none ?m
context:
⊢ Type ?u
evalNone.lean:3:6-3:14: error: don't know how to synthesize implicit argument
@List.head? ?m []
context:
⊢ Type ?u
evalNone.lean:3:6-3:8: error: don't know how to synthesize implicit argument
@List.nil ?m
context:
⊢ Type ?u
evalNone.lean:3:6-3:14: error: don't know how to synthesize implicit argument
@List.head? ?m []
context:
⊢ Type ?u

10
tests/lean/hidingInaccessibleNames.lean.expected.out
View file

@ -14,11 +14,6 @@ context:
x✝¹ : Nat
x✝ : [] ≠ []
⊢ Nat
hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
context:
a b x✝¹ : Nat
x✝ : [a, b] ≠ []
⊢ Nat
hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder
context:
x✝¹ : Nat
@ -30,6 +25,11 @@ x✝² : List Nat
x✝¹ : Nat
x✝ : x✝² ≠ []
⊢ Nat
hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
context:
a b x✝¹ : Nat
x✝ : [a, b] ≠ []
⊢ Nat
case inl
p q : Prop
h✝ : p

10
tests/lean/holeErrors.lean.expected.out
View file

@ -1,22 +1,22 @@
holeErrors.lean:3:11-3:20: error: failed to infer definition type
holeErrors.lean:3:14-3:20: error: don't know how to synthesize implicit argument
@id ?m
context:
⊢ Sort u
holeErrors.lean:3:11-3:20: error: failed to infer definition type
holeErrors.lean:5:9-5:10: error: failed to infer definition type
when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
holeErrors.lean:7:11-9:1: error: failed to infer definition type
holeErrors.lean:8:9-8:15: error: don't know how to synthesize implicit argument
@id ?m
context:
⊢ Sort u
holeErrors.lean:7:11-9:1: error: failed to infer definition type
holeErrors.lean:11:11-11:15: error: failed to infer definition type
holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
holeErrors.lean:11:8-11:9: error: failed to infer binder type
holeErrors.lean:11:11-11:15: error: failed to infer definition type
holeErrors.lean:13:12-13:13: error: failed to infer binder type
holeErrors.lean:13:15-13:19: error: failed to infer definition type
holeErrors.lean:16:4-16:5: error: failed to infer binder type
holeErrors.lean:15:7-16:10: error: failed to infer definition type
holeErrors.lean:16:4-16:5: error: failed to infer binder type
holeErrors.lean:19:13-19:19: error: don't know how to synthesize implicit argument
@id ?m
context:

12
tests/lean/holes.lean.expected.out
View file

@ -4,17 +4,17 @@ holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument
context:
x : Nat
⊢ Type
holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
@g Nat (?m x) x
context:
x : Nat
⊢ Type
holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
context:
case hole
x : Nat
y : Nat := g x + g x
⊢ Nat
holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
@g Nat (?m x) x
context:
x : Nat
⊢ Type
holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
context:
x : Nat
@ -22,12 +22,12 @@ y : Nat := g x + g x
⊢ Nat
holes.lean:13:10-13:11: error: failed to infer binder type
holes.lean:15:16-15:17: error: failed to infer binder type
holes.lean:18:9-18:10: error: failed to infer binder type
holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument
@f Nat (?m a) a
context:
a : Nat
f : {α : Type} → {β : ?m a} → α → α := fun {α} {β} a => a
⊢ ?m a
holes.lean:18:9-18:10: error: failed to infer binder type
holes.lean:21:25-22:4: error: failed to infer definition type
holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type

2
tests/lean/implicitTypePos.lean.expected.out
View file

@ -1,5 +1,5 @@
implicitTypePos.lean:1:6-1:7: error: failed to infer binder type
implicitTypePos.lean:1:8-1:9: error: failed to infer binder type
implicitTypePos.lean:1:6-1:7: error: failed to infer binder type
implicitTypePos.lean:3:9-3:10: error: failed to infer binder type
implicitTypePos.lean:5:9-5:10: error: failed to infer binder type
implicitTypePos.lean:7:10-7:11: error: failed to infer binder type

132
tests/lean/jason1.lean.expected.out
View file

@ -1,53 +1,3 @@
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
@TySyntaxLayer.arrow G T EG getCtx
(getCtx
@ -80,22 +30,12 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
context:
G T Tm : Type
EG : G → G → Type
@ -122,3 +62,63 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G

8
tests/lean/jason2.lean.expected.out
View file

@ -1,8 +1,8 @@
jason2.lean:4:30-4:37: error: don't know how to synthesize implicit argument
@Foo.foo ?m
context:
⊢ Nat
jason2.lean:4:20-4:23: error: don't know how to synthesize implicit argument
@Foo ?m
context:
⊢ Nat
jason2.lean:4:30-4:37: error: don't know how to synthesize implicit argument
@Foo.foo ?m
context:
⊢ Nat

4
tests/lean/multiConstantError.lean.expected.out
View file

@ -1,6 +1,6 @@
multiConstantError.lean:1:9-1:10: error: failed to infer binder type
recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
multiConstantError.lean:1:11-1:12: error: failed to infer binder type
recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
multiConstantError.lean:1:9-1:10: error: failed to infer binder type
recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
multiConstantError.lean:3:9-3:10: error: failed to infer binder type
recall that you cannot declare multiple constants in a single declaration. The identifier(s) `α`, `β` are being interpreted as parameters `(α : _)`, `(β : _)`

3
tests/lean/run/match1.lean
View file

@ -48,7 +48,6 @@ theorem ex3 {p q r : Prop} : p ∨ q → r → (q ∧ r) ∨ (p ∧ r) :=
by intro
| Or.inl hp, h => { apply Or.inr; apply And.intro; assumption; assumption }
| Or.inr hq, h => { apply Or.inl; exact ⟨hq, h⟩ }
#eval checkWithMkMatcherInput ``ex3.match_1
inductive C
| mk₁ : Nat → C
@ -91,7 +90,7 @@ inductive Vec.{u} (α : Type u) : Nat → Type u
def Vec.mapHead1 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
| _, nil, nil, f => none
| _, cons a as, cons b bs, f => some (f a b)
#eval checkWithMkMatcherInput ``Vec.mapHead1.match_1
def Vec.mapHead2 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
| _, nil, nil, f => none

2
tests/pkg/user_ext/test.sh
View file

@ -1,4 +1,4 @@
#!/usr/bin/env bash
rm -rf build
lake build -v 2>&1 | grep 'world, hello, test'
lake build -v 2>&1 | grep 'hello, world, test'