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

How long does it take to build, and how much ram?

Here is some information on the builds that are checked: https://github.com/coq/coq/blob/master/dev/ci/README-users.md

You are talking about this one right? https://github.com/jwiegley/category-theory

(On the side) you might also consider adding an opam file to https://github.com/coq/opam-coq-archive

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.

Ali Caglayan said:

You are talking about this one right? https://github.com/jwiegley/category-theory

Correct!

I've created https://github.com/coq/coq/pull/14744

Seems that native compilation takes more than 2G so I will turn it off for this job.

The file in question is: Theory/Metacategory/ArrowsOnly.vo

Looks like the CI job is working

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?

The entire job ended up taking 120 minutes 18 seconds

@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.

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).

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.

@John Wiegley you probably already noticed, but just in case: the CI of category_theory seems broken since a few days

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?

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...

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.

@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)

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.

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.

Thanks!

Last updated: Jul 24 2024 at 12:02 UTC