Permalink
Browse files

Add appropriate Fail(s) to opened bugs

The contract is that a file in bugs/opened should not raise errors if
the bug is still open.

Some of them fail for different reasons than they used to; I'm not sure
what to do about these.
  • Loading branch information...
JasonGross authored and mattam82 committed Apr 8, 2014
1 parent c728441 commit 8cc25de5e1c07fe93bba85c3792e5c4153066e5c
Showing with 135 additions and 77 deletions.
  1. +9 −4 test-suite/bugs/opened/HoTT_coq_007.v
  2. +24 −3 test-suite/bugs/opened/HoTT_coq_014.v
  3. +15 −3 test-suite/bugs/opened/HoTT_coq_020.v
  4. +2 −1 test-suite/bugs/opened/HoTT_coq_027.v
  5. +5 −5 test-suite/bugs/opened/HoTT_coq_029.v
  6. +2 −1 test-suite/bugs/opened/HoTT_coq_030.v
  7. +2 −2 test-suite/bugs/opened/HoTT_coq_032.v
  8. +3 −1 test-suite/bugs/opened/HoTT_coq_033.v
  9. +5 −4 test-suite/bugs/opened/HoTT_coq_034.v
  10. +6 −3 test-suite/bugs/opened/HoTT_coq_036.v
  11. +4 −1 test-suite/bugs/opened/HoTT_coq_045.v
  12. +6 −3 test-suite/bugs/opened/HoTT_coq_052.v
  13. +2 −2 test-suite/bugs/opened/HoTT_coq_053.v
  14. +3 −3 test-suite/bugs/opened/HoTT_coq_054.v
  15. +1 −1 test-suite/bugs/opened/HoTT_coq_061.v
  16. +2 −2 test-suite/bugs/opened/HoTT_coq_062.v
  17. +2 −2 test-suite/bugs/opened/HoTT_coq_063.v
  18. +1 −1 test-suite/bugs/opened/HoTT_coq_064.v
  19. +1 −1 test-suite/bugs/opened/HoTT_coq_078.v
  20. +1 −1 test-suite/bugs/opened/HoTT_coq_080.v
  21. +1 −1 test-suite/bugs/opened/HoTT_coq_081.v
  22. +4 −4 test-suite/bugs/opened/HoTT_coq_082.v
  23. +1 −1 test-suite/bugs/opened/HoTT_coq_083.v
  24. +1 −1 test-suite/bugs/opened/HoTT_coq_084.v
  25. +1 −1 test-suite/bugs/opened/HoTT_coq_085.v
  26. +3 −2 test-suite/bugs/opened/HoTT_coq_089.v
  27. +2 −2 test-suite/bugs/opened/HoTT_coq_098.v
  28. +1 −1 test-suite/bugs/opened/HoTT_coq_101.v
  29. +5 −1 test-suite/bugs/opened/HoTT_coq_102.v
  30. +1 −1 test-suite/bugs/opened/HoTT_coq_103.v
  31. +1 −1 test-suite/bugs/opened/HoTT_coq_104.v
  32. +1 −1 test-suite/bugs/opened/HoTT_coq_105.v
  33. +1 −1 test-suite/bugs/opened/HoTT_coq_106.v
  34. +1 −1 test-suite/bugs/opened/HoTT_coq_107.v
  35. +2 −2 test-suite/bugs/opened/HoTT_coq_110.v
  36. +6 −5 test-suite/bugs/opened/HoTT_coq_111.v
  37. +1 −1 test-suite/bugs/opened/HoTT_coq_113.v
  38. +1 −1 test-suite/bugs/opened/HoTT_coq_115.v
  39. +2 −2 test-suite/bugs/opened/HoTT_coq_120.v
  40. +1 −1 test-suite/bugs/opened/HoTT_coq_122.v
  41. +2 −2 test-suite/bugs/opened/HoTT_coq_124.v
@@ -36,9 +36,14 @@ Module Comment1.
Set Printing All.
Set Printing Universes.
- Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x).
- intro. (* Illegal application (Type Error) *)
- Abort.
+ Fail Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). (** ??? The term "y" has type
+ "@Functor (* Top.448 Top.449 Top.450 Top.451 *)
+ (@Functor (* Set Top.441 Top.442 Top.336 *) Empty_set Cat0 objC C) C0
+ Empty_set Cat0" while it is expected to have type
+ "@Functor (* Top.295 Top.296 Top.295 Top.296 *) ?46 ?47 ?48 ?49"
+(Universe inconsistency: Cannot enforce Set = Top.295)). *)
+ Fail intro. (* Illegal application (Type Error) *)
+ Fail Abort.
End Comment1.
Module Comment2.
@@ -106,5 +111,5 @@ Module Comment3.
Polymorphic Hint Resolve foo. (* success *)
Polymorphic Hint Rewrite @foo. (* Success *)
Polymorphic Hint Resolve @foo. (* Error: @foo is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints. *)
- Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *)
+ Fail Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *)
End Comment3.
@@ -158,7 +158,28 @@ Section GraphObj.
Defined.
End GraphObj.
-
-Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
+Set Printing Universes.
+Set Printing All.
+Fail Polymorphic Definition UnderlyingGraphFunctor_MorphismOf' (C D : SmallCategory) (F : SpecializedFunctor C D) :
+ Morphism (FunctorCategory TypeCat GraphIndexingCategory) (@UnderlyingGraph (SObject C) (C:SpecializedCategory (SObject C))) (UnderlyingGraph D). (* Toplevel input, characters 216-249:
+Error:
+In environment
+C : SmallCategory (* Top.594 *)
+D : SmallCategory (* Top.595 *)
+F :
+@SpecializedFunctor (* Top.25 Set Top.25 Set *) (SObject (* Top.25 *) C)
+ (SUnderlyingCategory (* Top.25 *) C) (SObject (* Top.25 *) D)
+ (SUnderlyingCategory (* Top.25 *) D)
+The term
+ "SUnderlyingCategory (* Top.25 *) C
+ :SpecializedCategory (* Top.25 Set *) (SObject (* Top.25 *) C)" has type
+ "SpecializedCategory (* Top.618 Top.619 *) (SObject (* Top.25 *) C)"
+while it is expected to have type
+ "SpecializedCategory (* Top.224 Top.225 *) (SObject (* Top.617 *) C)"
+(Universe inconsistency: Cannot enforce Set = Top.225)).
+ *)
+Fail Admitted.
+
+Fail Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
Morphism (FunctorCategory TypeCat GraphIndexingCategory) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*)
-Admitted.
+Fail Admitted.
@@ -65,9 +65,18 @@ Section Law0.
Set Printing Universes.
Set Printing Existential Instances.
- Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
- hnf.
- refine (@FunctorFrom0 _ _).
+ Fail Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf' : Object (@FunctorCategory Empty_set Cat0 objC C).
+ (* In environment
+objC : Type (* Top.154 *)
+C : Category (* Top.155 Top.154 *) objC
+The term "objC" has type "Type (* Top.154 *)"
+while it is expected to have type "Type (* Top.184 *)"
+(Universe inconsistency: Cannot enforce Top.154 <= Set)). *)
+ Fail Admitted.
+
+ Fail Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
+ Fail hnf.
+ Fail refine (@FunctorFrom0 _ _).
(* Toplevel input, characters 23-40:
Error:
In environment
@@ -81,3 +90,6 @@ The term
while it is expected to have type
"@Functor (* Set Prop Set Prop *) Empty_set Cat0 objC C".
*)
+ Fail admit.
+ Fail Defined.
+End Law0.
@@ -20,9 +20,10 @@ Identity Coercion FunctorToType_Id : FunctorToType >-> Functor.
Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C)
: FunctorToType C.
- refine (@Build_Functor _ C _ TypeCat
+ Fail refine (@Build_Functor _ C _ TypeCat
(fun x => F.(ObjectOf) x)
(fun s d m => F.(MorphismOf) _ _ m)).
+ admit.
Defined. (* Toplevel input, characters 0-8:
Error:
The term
@@ -140,9 +140,9 @@ Module FirstComment.
Section MonoidalCategory.
Variable objC : Type.
- Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.
+ Fail Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.
- Record MonoidalCategory :=
+ Fail Record MonoidalCategory :=
{
MonoidalUnderlyingCategory :> @Category objC;
TensorProduct : Functor (MonoidalUnderlyingCategory * MonoidalUnderlyingCategory) MonoidalUnderlyingCategory;
@@ -153,8 +153,8 @@ Module FirstComment.
End MonoidalCategory.
Section EnrichedCategory.
- Context `(M : @MonoidalCategory objM).
- Let x : M := IdentityObject M.
+ Fail Context `(M : @MonoidalCategory objM).
+ Fail Let x : M := IdentityObject M.
(* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report. *)
End EnrichedCategory.
End FirstComment.
@@ -301,7 +301,7 @@ Module SecondComment.
Definition CommaCategoryProjection : Functor (CommaCategory S T) (ProductCategory A B).
Admitted.
- Definition CommaCategoryProjectionFunctor_ObjectOf
+ Fail Definition CommaCategoryProjectionFunctor_ObjectOf
: @SliceCategoryOver _ LocallySmallCat (ProductCategory A B : Category _)
:=
existT _
@@ -235,6 +235,7 @@ Section FullyFaithful.
Context `(C : @SpecializedCategory objC).
Set Printing Universes.
- Check InducedHomNaturalTransformation (Yoneda C).
+ Fail Check InducedHomNaturalTransformation (Yoneda C).
(* Error: Universe inconsistency (cannot enforce Top.865 = Top.851 because
Top.851 < Top.869 <= Top.864 <= Top.865). *)
+End FullyFaithful.
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-xml") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *)
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
@@ -11,7 +11,7 @@ Delimit Scope functor_scope with functor.
Local Open Scope category_scope.
-Record SpecializedCategory (obj : Type) :=
+Fail Record SpecializedCategory (obj : Type) :=
{
Object :> _ := obj;
Morphism : obj -> obj -> Type;
@@ -7,6 +7,8 @@ Monomorphic Inductive JMeq' (A : Type) (x : A)
: forall B : Type, B -> Prop :=
JMeq'_refl : JMeq' x x.
+(* Note: This should fail (the [Fail] should be present in the final file, even when in bugs/closed) *)
Fail Monomorphic Definition foo := @JMeq' _ (@JMeq').
-Monomorphic Definition bar := @JMeq _ (@JMeq).
+(* Note: This should not fail *)
+Fail Monomorphic Definition bar := @JMeq _ (@JMeq).
@@ -14,7 +14,7 @@ Module Short.
Set Printing Universes.
Check bar nat Set : Set. (* success *)
- Check foo nat Set : Set. (* Toplevel input, characters 6-17:
+ Fail Check foo nat Set : Set. (* Toplevel input, characters 6-17:
Error:
The term "foo (* Top.303 Top.304 *) nat Set" has type
"Type (* Top.304 *)" while it is expected to have type
@@ -97,8 +97,8 @@ SpecializedFunctor C D.] gets rid of the universe inconsistency. *)
Let TypeCatC := FunctorCategory C TypeCat.
Let YC := (Yoneda C).
Set Printing Universes.
- Check @FunctorProduct' C TypeCatC (Yoneda C).
- (* Toplevel input, characters 35-43:
+ Fail Check @FunctorProduct' C TypeCatC (Yoneda C).
+ (* Toplevel input, characters 35-43:
Error:
In environment
objC : Type (* Top.186 *)
@@ -123,5 +123,6 @@ while it is expected to have type
"Functor (* Top.216 Top.219 Top.217 Top.220 *) C TypeCatC"
(Universe inconsistency: Cannot enforce Top.230 = Top.217 because Top.217
<= Top.227 < Top.225 <= Top.231 <= Top.230)).
- *)
+ *)
+ End FullyFaithful.
End Long.
@@ -27,7 +27,10 @@ Module Version1.
Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
assert (Hf : focus ((S tt) = (S tt))) by constructor.
- progress change CObject with (fun C => @Object (CObject C) C) in *.
+ let C1 := constr:(CObject) in
+ let C2 := constr:(fun C => @Object (CObject C) C) in
+ unify C1 C2.
+ Fail progress change CObject with (fun C => @Object (CObject C) C) in *.
simpl in *.
match type of Hf with
| focus ?V => exact V
@@ -74,7 +77,7 @@ Module Version2.
(objD : Type) (D : SpecializedCategory objD), Prop.
Definition CommaCategory_Object (A : Category) : Type.
assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
- progress change CObject with (fun C => @Object (CObject C) C) in *;
+ Fail progress change CObject with (fun C => @Object (CObject C) C) in *;
simpl in *.
match type of Hf with
| focus ?V => exact V
@@ -111,7 +114,7 @@ Module OtherBug.
(objD : Type) (D : SpecializedCategory objD), Prop.
Definition CommaCategory_Object (A : Category) : Type.
assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
- progress change CObject with (fun C => @Object (CObject C) C) in *;
+ Fail progress change CObject with (fun C => @Object (CObject C) C) in *;
simpl in *.
match type of Hf with
| focus ?V => exact V
@@ -26,7 +26,10 @@ Definition focus A (_ : A) := True.
Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
assert (Hf : focus ((S tt) = (S tt))) by constructor.
- progress change CObject with (fun C => @Object (CObject C) C) in *.
+ let C1 := constr:(CObject) in
+ let C2 := constr:(fun C => @Object (CObject C) C) in
+ unify C1 C2.
+ Fail progress change CObject with (fun C => @Object (CObject C) C) in *.
simpl in *.
let V := match type of Hf with
| focus ?V => constr:(V)
@@ -7,13 +7,16 @@ Goal Prop.
Abort.
Goal Prop = Set.
- Fail match goal with |- ?x = ?x => idtac end.
+ (* This should fail *)
+ Fail Fail match goal with |- ?x = ?x => idtac end.
Abort.
Goal Type = Prop.
- Fail match goal with |- ?x = ?x => idtac end.
+ (* This should fail *)
+ Fail Fail match goal with |- ?x = ?x => idtac end.
Abort.
Goal Type = Set.
- Fail match goal with |- ?x = ?x => idtac end.
+ (* This should fail *)
+ Fail Fail match goal with |- ?x = ?x => idtac end.
Abort.
@@ -29,7 +29,7 @@ Definition IndiscreteCategory X : PreCategory
:= @Build_PreCategory X
(fun _ _ => Unit).
-Definition NatCategory (n : nat) :=
+Fail Definition NatCategory (n : nat) :=
match n with
| 0 => IndiscreteCategory Unit
| _ => DiscreteCategory Bool
@@ -43,7 +43,7 @@ Definition NatCategory' (n : nat) :=
| _ => DiscreteCategory Bool
end.
-Definition NatCategory'' (n : nat) :=
+Fail Definition NatCategory'' (n : nat) :=
match n with
| 0 => IndiscreteCategory Unit
| _ => DiscreteCategory Bool
@@ -24,7 +24,7 @@ Defined.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with idpath => idpath end.
-Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
+Fail Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
(* Fortunately, this unifies properly *)
(pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
@@ -57,8 +57,8 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
| inr y' => ap h
end
end) pq).
- destruct x; destruct y; destruct pq; reflexivity.
-Qed.
+ Fail destruct x; destruct y; destruct pq; reflexivity.
+Fail Qed.
(* Toplevel input, characters 1367-1374:
Error:
In environment
@@ -116,7 +116,7 @@ Notation "[ C , D ]" := (FunctorCategory C D) : category_scope.
Variable C : PreCategory.
Variable D : PreCategory.
Variable E : PreCategory.
-Definition NTWhiskerR_Functorial (G : [C, D]%category)
+Fail Definition NTWhiskerR_Functorial (G : [C, D]%category)
: [[D, E], [C, E]]%category
:= Build_Functor
[C, D] [C, E]
@@ -70,8 +70,8 @@ Theorem thm `{Univalence} : (forall A, ((A -> False) -> False) -> A) -> False.
intro f.
Set Printing Universes.
Set Printing All.
- pose proof (apD f (path_universe e)).
- pose proof (apD f p).
+ Fail pose proof (apD f (path_universe e)).
+ Fail pose proof (apD f p).
(* Toplevel input, characters 18-19:
Error:
In environment
@@ -8,7 +8,7 @@ Module A.
| BuildContr : forall A (center : A) (contr : forall y, center = y), IsTrunc 0 A
| trunc_S : forall A n, (forall x y : A, IsTrunc n (x = y)) -> IsTrunc (S n) A.
- Existing Class IsTrunc.
+ Fail Existing Class IsTrunc.
(* Anomaly: Mismatched instance and context when building universe substitution.
Please report. *)
End A.
@@ -20,7 +20,7 @@ Module B.
| S _ => False
end.
- Existing Class IsTrunc.
+ Fail Existing Class IsTrunc.
(* Anomaly: Mismatched instance and context when building universe substitution.
Please report. *)
End B.
@@ -180,7 +180,7 @@ Section bar.
Variable D : PreCategory.
- Context `(has_colimits
+ Fail Context `(has_colimits
: forall F : Functor D C,
@IsColimit _ C D F (colimits F)).
(* Error: Unsatisfied constraints: Top.3773 <= Set
@@ -35,7 +35,7 @@ Definition transport_prod' {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
| idpath => idpath
end. (* success *)
-Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
+Fail Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
(z : P a * Q a)
: transport (fun a => P a * Q a) p z = (transport _ p (fst z), transport _ p (snd z))
:= match p with
@@ -23,7 +23,7 @@ Definition sum_category (C D : category) : category :=
Goal forall C D (x y : ob (sum_category C D)), Type.
intros C D x y.
hnf in x, y.
-exact (hom x y). (* Toplevel input, characters 26-27:
+Fail exact (hom x y). (* Toplevel input, characters 26-27:
Error:
In environment
C : category
@@ -7,6 +7,6 @@ Record category :=
hom : ob -> ob -> Type
}.
-Record foo := { C : category; x :> ob C }.
+Fail Record foo := { C : category; x :> ob C }.
(* Toplevel input, characters 0-42:
Error: Cannot find the target class. *)
@@ -4,16 +4,16 @@ Set Universe Polymorphism.
Record category :=
{ ob : Type }.
-Existing Class category. (*
+Fail Existing Class category. (*
Toplevel input, characters 0-24:
Anomaly: Mismatched instance and context when building universe substitution.
Please report. *)
Record category' :=
- { ob : Type;
- hom : ob -> ob -> Type }.
+ { ob' : Type;
+ hom' : ob' -> ob' -> Type }.
-Existing Class category'. (*
+Fail Existing Class category'. (*
Toplevel input, characters 0-24:
Anomaly: Mismatched instance and context when building universe substitution.
Please report. *)
@@ -24,6 +24,6 @@ generalize dependent (@ob C).
============================
Type -> ob C
(dependent evars:) *)
-intros T t.
+Fail intros T t.
(* Toplevel input, characters 9-10:
Error: No product even after head-reduction. *)
Oops, something went wrong.

0 comments on commit 8cc25de

Please sign in to comment.