John Wiegley (Aug 03 2021 at 04:46): John Wiegley (Aug 03 2021 at 04:46):I've been maintaining a category-theory library since 8.5 days, and have found that I'm using enough different features that there is a non-trivial amount of porting work needed with every version update (after last weekend, I now support 8.13 and HEAD). Some of the issues I find are anamolies and exceptions that require workarounds for the library to keep building. Several bugs have been logged in the past while doing these ports.
I was wondering if the Coq development team would be interested in adding this library to their build pool, since perhaps some of the things I'm doing may help discover problems in type class resolution, and universe polymorphism, for example. These are often the areas that require the greatest changes. In the move from 8.12 to 8.13, for example, a certain type class resolution stopped working that had been going strong for many versions, and the replacement needed involved explicit universe annotations which I had never needed to do before. Is it a bug, or a new restriction? I cannot tell.
I'm willing to stay on top of issues with the team and help resolve any problems in my library. What would the next steps be if there is interest?
Thank you, John Wiegley
Gaëtan Gilbert (Aug 03 2021 at 08:03):How long does it take to build, and how much ram?
Ali Caglayan (Aug 03 2021 at 08:22):Here is some information on the builds that are checked: https://github.com/coq/coq/blob/master/dev/ci/README-users.md
Ali Caglayan (Aug 03 2021 at 08:24):You are talking about this one right? https://github.com/jwiegley/category-theory
Ali Caglayan (Aug 03 2021 at 08:26):(On the side) you might also consider adding an opam file to https://github.com/coq/opam-coq-archive
John Wiegley (Aug 03 2021 at 16:05):Gaëtan Gilbert said:
How long does it take to build, and how much ram?
On my iMac Pro, the whole build using 1 CPU takes 35 minutes, and each compilation process uses between 129M to 1.5G, with an average around 500.
John Wiegley (Aug 03 2021 at 16:06):Ali Caglayan said:
You are talking about this one right? https://github.com/jwiegley/category-theory
Correct!
Ali Caglayan (Aug 04 2021 at 16:09):I've created https://github.com/coq/coq/pull/14744
Ali Caglayan (Aug 05 2021 at 11:47):Seems that native compilation takes more than 2G so I will turn it off for this job.
Ali Caglayan (Aug 05 2021 at 11:47):The file in question is: Theory/Metacategory/ArrowsOnly.vo
Ali Caglayan (Aug 05 2021 at 14:41):Looks like the CI job is working
Ali Caglayan (Aug 05 2021 at 14:41):These are some chunky files!
Aggregating timing log...
Time | Peak Mem | File Name
-----------------------------------------------------------------------
46m55.82s | 1345784 ko | Total Time / Peak Mem
-----------------------------------------------------------------------
13m30.70s | 849040 ko | Construction/Comma/Adjunction.vo
6m18.34s | 1345784 ko | Functor/Construction/Product/Monoidal.vo
3m36.04s | 965308 ko | Functor/Strong/Product.vo
2m41.11s | 725656 ko | Construction/Comma/Natural/Transformation.vo
1m24.94s | 951060 ko | Construction/Comma/Isomorphism.vo
1m18.76s | 809132 ko | Structure/Monoid.vo
1m09.40s | 592560 ko | Instance/Adjoints.vo
1m08.06s | 585556 ko | Structure/Monoidal/Cartesian/Proofs.vo
1m04.67s | 861772 ko | Structure/Monoidal/Internal/Product.vo
0m54.72s | 614724 ko | Functor/Structure/Monoidal/Compose.
@John Wiegley do these times look right to you?
Ali Caglayan (Aug 05 2021 at 14:42):The entire job ended up taking 120 minutes 18 seconds
John Wiegley (Aug 05 2021 at 18:47):@Ali Caglayan Yes, those numbers are right. ArrowsOnly.v uses computational reflection, so I'm not entirely surprised that native compilation might be memory intensive in that case. The Comma/Adjunction.v is the most complex proof in the whole library, so yes, it takes a very long time to build.
Pierre Roux (Aug 06 2021 at 06:09):What makes native compilation expensive is not "computational reflection" per se (that could even speed it up when using native_compute) but rather the presence of very large terms. Anyway, deactivating native compilation is fine if you don't use it and not any (even indirect) user of your library ever want to use it (that's why turning off native compilation for MathComp, for instance, would be bad, even if MathComp itself is not doing any computational reflection).
John Wiegley (Aug 08 2021 at 21:39):Pierre Roux said:
What makes native compilation expensive is not "computational reflection" per se (that could even speed it up when using
native_compute) but rather the presence of very large terms.
Thank you for that clarification, you are quite right.
Pierre Roux (Sep 01 2021 at 13:08):@John Wiegley you probably already noticed, but just in case: the CI of category_theory seems broken since a few days
John Wiegley (Sep 01 2021 at 21:03):Pierre Roux said:
John Wiegley you probably already noticed, but just in case: the CI of category_theory seems broken since a few days
Thanks for pointing that out, Pierre. Local builds with Nix pass, but apparently the coq-equations dependency is not being installed via Opam. Still trying to get this working locally; do you know of any examples of projects that use this and whose CI builds via GitHub Actions?
John Wiegley (Sep 01 2021 at 22:10):Pierre Roux said:
John Wiegley you probably already noticed, but just in case: the CI of category_theory seems broken since a few days
I've fixed all the targets except for "dev". Apparently the dev version of coq-equations has moved a top-level module...
John Wiegley (Sep 01 2021 at 23:45):I'm going to disable the "dev" build on CI, since I myself don't have a way to reproduce those errors locally so it's difficult to resolve them. My development is done using Coq 8.13 and equations 1.2.4, so this is the highest I can support just now. Once I get back from vacation I can look at adding the current dev version back into my regular development work.
Théo Zimmermann (Sep 02 2021 at 08:31):@John Wiegley I think that you are missing the point raised by Pierre here. Coq's CI is failing because of the category-theory library being broken (by Equations AFAIU). So it's important to resolve this ASAP.
I think the best way for you to be able to locally test compatibility with dev versions of Coq and Equations is probably to rely on the Coq Nix Toolbox. I'll try to open a PR setting things up for you. (Done in: https://github.com/jwiegley/category-theory/pull/21)
John Wiegley (Sep 02 2021 at 22:46):Théo Zimmermann said:
John Wiegley I think that you are missing the point raised by Pierre here. Coq's CI is failing because of the category-theory library being broken (by Equations AFAIU). So it's important to resolve this ASAP.
I think the best way for you to be able to locally test compatibility with dev versions of Coq and Equations is probably to rely on the Coq Nix Toolbox. I'll try to open a PR setting things up for you. (Done in: https://github.com/jwiegley/category-theory/pull/21)
Ah, I see! I will disable building of the code that is breaking things for now, then, since I am headed on vacation for the next several weeks.
John Wiegley (Sep 02 2021 at 23:57):All is green again. And now that I know I'm linked to Coq's CI, I'll be certain to verify that CI in this repository does not break again.
Théo Zimmermann (Sep 03 2021 at 08:16):Thanks!
Last updated: Jun 05 2023 at 10:01 UTC