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

fix: catch exception at elabMutualDef

Browse source 
closes #1301
This commit is contained in:
Leonardo de Moura 2022-07-12 18:39:30 -07:00
parent fdef55339f
commit b6860968ff
5 changed files with 79 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Elab/MutualDef.lean
View file

@ -777,9 +777,14 @@ where
withFunLocalDecls headers fun funFVars => do
for view in views, funFVar in funFVars do
addLocalVarInfo view.declId funFVar
let values ← elabFunValues headers
Term.synthesizeSyntheticMVarsNoPostponing
let values ← values.mapM (instantiateMVars ·)
let values ←
try
let values ← elabFunValues headers
Term.synthesizeSyntheticMVarsNoPostponing
values.mapM (instantiateMVars ·)
catch ex =>
logException ex
headers.mapM fun header => mkSorry header.type (synthetic := true)
let headers ← headers.mapM instantiateMVarsAtHeader
let letRecsToLift ← getLetRecsToLift
let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift

6
tests/lean/343.lean.expected.out
View file

@ -5,3 +5,9 @@ while trying to unify
Catish.Obj Catish.Obj
with
CatIsh.{max ?u ?u, max (?u + 1) (?u + 1)}
343.lean:30:0-30:54: error: failed to solve universe constraint
max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
while trying to unify
Catish.Obj : Type (max ((max (u_1 + 1) (u_2 + 1)) + 1) ((max u_3 u_4) + 1))
with
CatIsh : Type (max ((max u_4 u_3) + 1) ((max (u_4 + 1) (u_3 + 1)) + 1))

118
tests/lean/infoTree.lean.expected.out
View file

@ -388,94 +388,102 @@ bitwise bne
xor : Nat → Nat → Nat @ ⟨38, 7⟩-⟨38, 10⟩
command @ ⟨37, 0⟩†-⟨38, 10⟩† @ Lean.Elab.Command.elabEnd
infoTree.lean:41:0: error: expected identifier or term
[Elab.info] command @ ⟨39, 0⟩-⟨39, 30⟩ @ no_elab
[Elab.info] command @ ⟨39, 0⟩-⟨39, 30⟩ @ Lean.Elab.Command.elabDeclaration
Inhabited Nat : Type @ ⟨39, 11⟩-⟨39, 24⟩ @ Lean.Elab.Term.elabApp
[.] `Inhabited : some Sort.{?_uniq.1173} @ ⟨39, 11⟩-⟨39, 20⟩
Inhabited : Type → Type @ ⟨39, 11⟩-⟨39, 20⟩
Nat : Type @ ⟨39, 21⟩-⟨39, 24⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.1174} @ ⟨39, 21⟩-⟨39, 24⟩
Nat : Type @ ⟨39, 21⟩-⟨39, 24⟩
instInhabitedNat_1 (isBinder := true) : Inhabited Nat @ ⟨39, 0⟩†-⟨39, 30⟩†
instInhabitedNat_1 (isBinder := true) : Inhabited Nat @ ⟨39, 0⟩-⟨39, 8⟩
infoTree.lean:44:0: error: expected stx
[Elab.info] command @ ⟨41, 0⟩-⟨41, 5⟩ @ no_elab
[Elab.info] command @ ⟨44, 0⟩-⟨44, 22⟩ @ Lean.Elab.Command.elabSetOption
[.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩
[Elab.info] command @ ⟨45, 0⟩-⟨47, 8⟩ @ Lean.Elab.Command.elabDeclaration
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.1173} @ ⟨45, 14⟩-⟨45, 17⟩
[.] `Nat : some Sort.{?_uniq.1177} @ ⟨45, 14⟩-⟨45, 17⟩
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
_uniq.1174 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
_uniq.1178 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.1175} @ ⟨45, 14⟩-⟨45, 17⟩
[.] `Nat : some Sort.{?_uniq.1179} @ ⟨45, 14⟩-⟨45, 17⟩
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
_uniq.1176 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
Eq.{1} Nat _uniq.1174 _uniq.1174 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
_uniq.1180 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
Eq.{1} Nat _uniq.1178 _uniq.1178 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
Macro expansion
(«term_=_» `x "=" `x)
===>
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.180 `x `x)
Eq.{1} Nat _uniq.1174 _uniq.1174 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel
[.] `Eq._@.infoTree._hyg.180 : none @ ⟨45, 21⟩†-⟨45, 26⟩†
_uniq.1174 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.182 `x `x)
Eq.{1} Nat _uniq.1178 _uniq.1178 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.BinOp.elabBinRel
[.] `Eq._@.infoTree._hyg.182 : none @ ⟨45, 21⟩†-⟨45, 26⟩†
_uniq.1178 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨45, 21⟩-⟨45, 22⟩
_uniq.1174 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
_uniq.1174 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
_uniq.1178 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
_uniq.1178 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨45, 25⟩-⟨45, 26⟩
_uniq.1174 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
_uniq.1180 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
_uniq.1181 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
_uniq.1182 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1181 _uniq.1182]) f6.f7 : Eq.{1} Nat _uniq.1181 _uniq.1181 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
_uniq.1178 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
_uniq.1184 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
_uniq.1185 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
_uniq.1186 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.1185 _uniq.1186]) f6.f7 : Eq.{1} Nat _uniq.1185 _uniq.1185 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.1183} @ ⟨46, 20⟩-⟨46, 23⟩
[.] `Nat : some Sort.{?_uniq.1187} @ ⟨46, 20⟩-⟨46, 23⟩
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
_uniq.1184 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
_uniq.1188 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.1185} @ ⟨46, 20⟩-⟨46, 23⟩
[.] `Nat : some Sort.{?_uniq.1189} @ ⟨46, 20⟩-⟨46, 23⟩
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
_uniq.1186 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.{1} Nat _uniq.1184 _uniq.1184 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
_uniq.1190 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.{1} Nat _uniq.1188 _uniq.1188 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
Macro expansion
(«term_=_» `x "=" `x)
===>
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.188 `x `x)
Eq.{1} Nat _uniq.1184 _uniq.1184 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel
[.] `Eq._@.infoTree._hyg.188 : none @ ⟨46, 27⟩†-⟨46, 32⟩†
_uniq.1184 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.190 `x `x)
Eq.{1} Nat _uniq.1188 _uniq.1188 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.BinOp.elabBinRel
[.] `Eq._@.infoTree._hyg.190 : none @ ⟨46, 27⟩†-⟨46, 32⟩†
_uniq.1188 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨46, 27⟩-⟨46, 28⟩
_uniq.1184 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
_uniq.1184 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
_uniq.1188 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
_uniq.1188 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨46, 31⟩-⟨46, 32⟩
_uniq.1184 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
_uniq.1191 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
_uniq.1192 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
_uniq.1193 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.refl.{1} Nat _uniq.1192 : Eq.{1} Nat _uniq.1192 _uniq.1192 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
[.] `Eq.refl : some Eq.{?_uniq.1188} Nat _uniq.1192 _uniq.1192 @ ⟨46, 36⟩-⟨46, 43⟩
_uniq.1188 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
_uniq.1195 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
_uniq.1196 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
_uniq.1197 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.refl.{1} Nat _uniq.1196 : Eq.{1} Nat _uniq.1196 _uniq.1196 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
[.] `Eq.refl : some Eq.{?_uniq.1192} Nat _uniq.1196 _uniq.1196 @ ⟨46, 36⟩-⟨46, 43⟩
Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩
_uniq.1192 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
[.] `x : some ?_uniq.1195 @ ⟨46, 44⟩-⟨46, 45⟩
_uniq.1192 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
[mdata _recApp: _uniq.1191 _uniq.1181 _uniq.1182] : Eq.{1} Nat _uniq.1181 _uniq.1181 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
[.] `f7 : some Eq.{1} Nat _uniq.1181 _uniq.1181 @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.1191 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.1181 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
_uniq.1196 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
[.] `x : some ?_uniq.1199 @ ⟨46, 44⟩-⟨46, 45⟩
_uniq.1196 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
[mdata _recApp: _uniq.1195 _uniq.1185 _uniq.1186] : Eq.{1} Nat _uniq.1185 _uniq.1185 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
[.] `f7 : some Eq.{1} Nat _uniq.1185 _uniq.1185 @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.1195 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.1185 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
[.] `x : some Nat @ ⟨47, 5⟩-⟨47, 6⟩
_uniq.1181 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
_uniq.1182 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
_uniq.1185 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
_uniq.1186 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
[.] `y : some Nat @ ⟨47, 7⟩-⟨47, 8⟩
_uniq.1182 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
_uniq.1186 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
f6 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
[Elab.info] command @ ⟨50, 0⟩-⟨50, 32⟩ @ Lean.Elab.Command.elabDeclaration
B : Type @ ⟨50, 12⟩-⟨50, 13⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq.1215} @ ⟨50, 12⟩-⟨50, 13⟩
[.] `B : some Sort.{?_uniq.1219} @ ⟨50, 12⟩-⟨50, 13⟩
B : Type @ ⟨50, 12⟩-⟨50, 13⟩
_uniq.1216 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
_uniq.1220 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq.1217} @ ⟨50, 17⟩-⟨50, 18⟩
[.] `B : some Sort.{?_uniq.1221} @ ⟨50, 17⟩-⟨50, 18⟩
B : Type @ ⟨50, 17⟩-⟨50, 18⟩
_uniq.1218 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
_uniq.1219 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
B.mk (B.pair _uniq.1219) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
_uniq.1219 : B @ ⟨50, 24⟩-⟨50, 25⟩
B.pair _uniq.1219 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
_uniq.1222 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
_uniq.1223 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
B.mk (B.pair _uniq.1223) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
_uniq.1223 : B @ ⟨50, 24⟩-⟨50, 25⟩
B.pair _uniq.1223 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
[.] `b : some Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩
_uniq.1219 : B @ ⟨50, 24⟩-⟨50, 25⟩
[.] _uniq.1219 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
_uniq.1223 : B @ ⟨50, 24⟩-⟨50, 25⟩
[.] _uniq.1223 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
B.pair : B -> (Prod.{0 0} A A) @ ⟨50, 24⟩†-⟨50, 25⟩†
pair : Prod.{0 0} A A := B.pair _uniq.1219 @ ⟨50, 22⟩†-⟨50, 32⟩
pair : Prod.{0 0} A A := B.pair _uniq.1223 @ ⟨50, 22⟩†-⟨50, 32⟩
f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩

2
tests/lean/rewrite.lean
View file

@ -14,7 +14,7 @@ done
axiom zeroAdd (x : Nat) : 0 + x = x
theorem ex2 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
theorem ex2a (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
rewrite [zeroAdd] at h₁ h₂;
trace_state;
subst x;

2
tests/lean/typeMismatch.lean
View file

@ -8,5 +8,5 @@ IO.println ""
open Lean
def test (x : Expr) : MetaM Unit :=
def test2 (x : Expr) : MetaM Unit :=
Meta.isDefEq x x