Comments (7)
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 [email protected] 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.
from coq.
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).
from coq.
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!
from coq.
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.
from coq.
Thanks, this is very useful to have. I wonder if coq has reached complexity at pushes it past "mature software".
from coq.
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.
from coq.
I do not think this is relevant any more.
from coq.
Related Issues (20)
- abstract creates duplicate theorems / Anomaly: Backtrack.backto 55: a state with no vcs_backup. Please report. (polyproj)
- Most recent version of trunk-polyproj will not build HOT 1
- Anomaly: Uncaught exception Not_found(_). Please report. (polyproj)
- [abstract] duplicates fresh lemmas in universe polymorphic mode (polyproj) HOT 1
- Application Error: The 1st term has type "Univalence (* Top.934 Top.935 Top.936 Top.937 *)" which should be coercible to "Univalence (* Top.1003 Top.1003 Top.1001 Top.997 *)". (polyproj)
- [change ... in *] picks universes once, which unifies universes too eagerly (polyproj)
- "Unable to handle arbitrary u+k <= v constraints" should probably be an Error, not an Anomaly (polyproj)
- Anomaly: not an arity. Please report. (polyproj)
- Error: No such section variable or assumption: U' at section end (HoTT/coq)
- Anomaly: unknown meta ?190. Please report. (HoTT/coq)
- Error: Unable to satisfy the following constraints (bug in typeclass resolution?) (polyproj)
- Sometimes, universe polymorphic definitions aren't polymorphic enough (but making them more polymorphic might break other things) (polyproj)
- HoTT/coq's universe inconsistencies do not respect delta (polyproj) (maybe?) HOT 13
- Error: Unsatisfied constraints: <universe constraints> (polyproj)
- Stack overflow on "Hint Rewrite @<primitive projection>" (polyproj)
- Stack overflow on [Defined] (polyproj)
- Universe polymorphism breaks record eta (polyproj)
- Syntax for explicit universe levels HOT 2
- Anomaly: variable n unbound. (using [transparent assert])
- Multiple definition of the extension constructor name Found. HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coq.