Some bugs: slowness, universe inconsistencies, and anomalies

[JasonGross]

The new version has fixed most of the problems I was having with my category theory library. Great work!

There still seem to be a few bugs, though. When I apply the patch at https://gist.github.com/JasonGross/5308008 to the tip (ede8193) of https://bitbucket.org/JasonGross/catdb, I get the following output. Some of these are probably just minor incompatibilities (for example, Build_Equivalence now takes one fewer explicit argument than it did in Coq 8.4) that I haven't gotten around to tracking down yet. However, the anomaly and the error on case H are probably actual bugs. The problem in Grothendieck.v seems to be related to Identity Coercions; do these coercions fix universe levels which don't need to be fixed? The universe inconsistencies are also worrying, given that I've Set Universe Polymorphism in all of my files. Additionally, InducedLimitFunctors is much slower to compile (from 2.5 minutes to 32 minutes), as is CommaCategoryFunctors (from 8.5 minutes to more than 19 minutes). I'll be creating individual issues with small reproducing cases for these bugs as I have time over the next few days, but I figured I'd put them all here in case you want to tackle them before I get a chance to make smaller test cases.

"coqc"  -q  -I .  -dont-load-proofs  EnrichedCategory
"coqc"  -q  -I .  -dont-load-proofs  CommaCategoryFunctors
"coqc"  -q  -I .  -dont-load-proofs  DecidableDiscreteCategoryFunctors
"coqc"  -q  -I .  -dont-load-proofs  InducedLimitFunctors
"coqc"  -q  -I .  -dont-load-proofs  CoendFunctor
"coqc"  -q  -I .  -dont-load-proofs  Grothendieck
"coqc"  -q  -I .  -dont-load-proofs  Yoneda
"coqc"  -q  -I .  -dont-load-proofs  Examples
File "./EnrichedCategory.v", line 24, characters 2-34:
Anomaly: apply_coercion_args: mismatch between arguments and coercion.
Please report.
make[1]: *** [EnrichedCategory.vo] Error 1
File "./Grothendieck.v", line 114, characters 2-193:
Error: Illegal application:
The term "ObjectOf" of type
 "forall (objC : Type) (C : SpecializedCategory objC)
    (objD : Type) (D : SpecializedCategory objD),
  SpecializedFunctor C D -> objC -> objD"
cannot be applied to the terms
 "objC" : "Type"
 "C" : "SpecializedCategory objC"
 "Type" : "Type"
 "TypeCat" : "SpecializedCategory Set"
 "F'" : "SpecializedFunctorToType C"
 "SetGrothendieckC' G" : "objC"
The 5th term has type "SpecializedFunctorToType C"
which should be coercible to "SpecializedFunctor C TypeCat".
make[1]: *** [Grothendieck.vo] Error 1
File "./Yoneda.v", line 161, characters 2-63:
Error: Universe inconsistency.
make[1]: *** [Yoneda.vo] Error 1
File "./DecidableDiscreteCategoryFunctors.v", line 112, characters 4-5:
In nested Ltac calls to "t" and "case H", last call failed.
Error: Cannot instantiate metavariable P of type
"forall a : O, x = a -> Prop" with abstraction
"fun (x : O) (e : x = x) =>
 match eq_sym e in (_ = y) return (Morphism O' (f y) (f x)) with
 | eq_refl => Identity (f x)
 end = Identity (f x)" of incompatible type "forall x : O, x = x -> Prop".
make[1]: *** [DecidableDiscreteCategoryFunctors.vo] Error 1
File "./Examples.v", line 236, characters 2-138:
Error: Proof is not complete.
make[1]: *** [Examples.vo] Error 1
File "./CoendFunctor.v", line 108, characters 4-830:
Error: Proof is not complete.
make[1]: *** [CoendFunctor.vo] Error 1
Finished transaction in 280.631 secs (280.629u,0.016s)
File "./CommaCategoryFunctors.v", line 364, characters 2-6:
Error: Universe inconsistency.
make[1]: *** [CommaCategoryFunctors.vo] Error 1

[mattam82]

Hi Jason,

thanks for trying this, I'll be looking at the bugs. There clearly remains bug in inference that engender the inconsistencies, and there is an issue with first-order unification which sets universes too eagerly, I'm working on that. Regarding slowness, I think it can be attributed to the use of records and projections, which repeat universe instances needlessly, I have the same problem in one of my libraries. I'm working on a patch in parallel to this that makes projections primitive and avoids this exponential blowup of type annotations (compilation went from 20minutes to seconds on that library :).

Best,
-- Matthieu

Le 4 avr. 2013 à 02:07, Jason Gross notifications@github.com a écrit :

The new version has fixed most of the problems I was having with my category theory library. Great work!

There still seem to be a few bugs, though. When I apply the patch at https://gist.github.com/JasonGross/5308008 to the tip (ede8193) of https://bitbucket.org/JasonGross/catdb, I get the following output. Some of these are probably just minor incompatibilities (for example, Build_Equivalence now takes one fewer explicit argument than it did in Coq 8.4) that I haven't gotten around to tracking down yet. However, the anomaly and the error on case H are probably actual bugs. The problem in Grothendieck.v seems to be related to Identity Coercions; do these coercions fix universe levels which don't need to be fixed? The universe inconsistencies are also worrying, given that I've Set Universe Polymorphism in all of my files. Additionally, InducedLimitFunctors is much slower to compile (from 2.5 minutes to 32 minute s), as is CommaCategoryFunctors (from 8.5 minutes to more than 19 minutes). I'll be creating individual issues with small reproducing cases for these bugs as I have time over the next few days, but I figured I'd put them all here in case you want to tackle them before I get a chance to make smaller test cases.

"coqc" -q -I . -dont-load-proofs EnrichedCategory
"coqc" -q -I . -dont-load-proofs CommaCategoryFunctors
"coqc" -q -I . -dont-load-proofs DecidableDiscreteCategoryFunctors
"coqc" -q -I . -dont-load-proofs InducedLimitFunctors
"coqc" -q -I . -dont-load-proofs CoendFunctor
"coqc" -q -I . -dont-load-proofs Grothendieck
"coqc" -q -I . -dont-load-proofs Yoneda
"coqc" -q -I . -dont-load-proofs Examples
File "./EnrichedCategory.v", line 24, characters 2-34:
Anomaly: apply_coercion_args: mismatch between arguments and coercion.
Please report.
make[1]: *** [EnrichedCategory.vo] Error 1
File "./Grothendieck.v", line 114, characters 2-193:
Error: Illegal application:
The term "ObjectOf" of type
"forall (objC : Type) (C : SpecializedCategory objC)
(objD : Type) (D : SpecializedCategory objD),
SpecializedFunctor C D -> objC -> objD"
cannot be applied to the terms
"objC" : "Type"
"C" : "SpecializedCategory objC"
"Type" : "Type"
"TypeCat" : "SpecializedCategory Set"
"F'" : "SpecializedFunctorToType C"
"SetGrothendieckC' G" : "objC"
The 5th term has type "SpecializedFunctorToType C"
which should be coercible to "SpecializedFunctor C TypeCat".
make[1]: *** [Grothendieck.vo] Error 1
File "./Yoneda.v", line 161, characters 2-63:
Error: Universe inconsistency.
make[1]: *** [Yoneda.vo] Error 1
File "./DecidableDiscreteCategoryFunctors.v", line 112, characters 4-5:
In nested Ltac calls to "t" and "case H", last call failed.
Error: Cannot instantiate metavariable P of type
"forall a : O, x = a -> Prop" with abstraction
"fun (x : O) (e : x = x) =>
match eq_sym e in (_ = y) return (Morphism O' (f y) (f x)) with
| eq_refl => Identity (f x)
end = Identity (f x)" of incompatible type "forall x : O, x = x -> Prop".
make[1]: *** [DecidableDiscreteCategoryFunctors.vo] Error 1
File "./Examples.v", line 236, characters 2-138:
Error: Proof is not complete.
make[1]: *** [Examples.vo] Error 1
File "./CoendFunctor.v", line 108, characters 4-830:
Error: Proof is not complete.
make[1]: *** [CoendFunctor.vo] Error 1
Finished transaction in 280.631 secs (280.629u,0.016s)
File "./CommaCategoryFunctors.v", line 364, characters 2-6:
Error: Universe inconsistency.
make[1]: *** [CommaCategoryFunctors.vo] Error 1
—
Reply to this email directly or view it on GitHub.

[JasonGross]

Update at the status of the compilation: The "Proof is not complete" error messages were a result of tactics not behaving the same in v8.4 vs HoTT/coq / trunk. For example, the one in CoendFunctor.v is a result of discriminate becoming more powerful and being able to destruct sum hypotheses.

The two universe inconsistencies remain, as does the anomaly. I'm probably going to wait until the universe inconsistency in Yoneda.v is solved to try to track down the one in CommaCategoryFunctors.v; that file is very slow to compile, and depends on a very large number of other files in the development. The fix I mentioned for #30 (replacing auto with assumption) doesn't seem to work on the non-minimized Yoneda.v universe inconsistency (rather, the analogous change of replacing Record Category ... with Record > Category ... and removing the coercions all together doesn't seem to work).

[JasonGross]

Update on the status of compilation: I've found work-arounds for all of the issues I've reported; using the work-arounds (there are many commits at https://bitbucket.org/JasonGross/catdb/commits/all labeled "work around a bug in HoTT/coq"), my code fully compiles with both Coq 8.4 and HoTT/coq.
Great work!

[JasonGross]

If you want something to stress-test the speed of any changes you make, the file CommaCategoryProjectionFunctors.v at https://bitbucket.org/JasonGross/catdb/commits/4eb6407c6ca3200bebefaa3a1834d05c49b01846 takes about 4m50s to compile with Coq 8.4, and about 57m to compile with the tip of HoTT/coq. The entire catdb repository takes about 20 minutes with Coq 8.4, and 143m with HoTT/coq. (Removing the object argument to my category record cuts the time down to 42 minutes for CommaCategoryProjectionFunctors.v, and 105 minutes total; this was impossible to do with Coq 8.4. I have some other changes that should cut down the time now that I have polymorphic definitions, though I hope that the algorithm gets quicker, too. You said that you were hoping to get an improved version pushed in the next few months, right?)

If you want to test the timing of the catdb repository, there's the make timed and make pretty-timed targets.

[andrejbauer]

Thanks, this is very useful to have. I wonder if coq has reached complexity at pushes it past "mature software".

[JasonGross]

I've just pushed a commit (https://bitbucket.org/JasonGross/catdb/commits/1bc8cd4caddcc6489f3f3ac7a648e783b612d06c) that cuts the compile time of CommaCategoryProjectionFunctors.v down to 3m46s. The commit consisted of replacing slightly sig and sigT and prod with records, which permitted me to clean up some proof scripts to be more selective about the order in which they unfold and destruct things. I suspect that the drastic change in speed is a result of the proof terms being smaller (because destruct no longer needs to list out all of the arguments of the sig and sigT types). I'm not sure how much it speeds things up in the original branch; I wrote it for the version with the object argument of SpecializedCategory removed.

[JasonGross]

I do not think this is relevant any more.