[new release] catt (3 packages) (1.0)

[thibautbenjamin]

An infinity-categorical coherence typechecker

• Project page: https:/thibautbenjamin/catt

CHANGES:

Coq catt plugin

• Working export of catt term into coq

Catt

• Computation of 1-naturality
• Computation of functorialisation
• Computation of inverses and cancellation witnesses
• Computation of opposites
• Builtin identities and compositions
• Computation of suspension and implicit suspension
• Inference of implicit variables
• Basic type checker

[thibautbenjamin]

Hi, apologies for the delay for the reply, and thank you for the suggestion. This is the first time I am publishing a package, so forgive me if some things are not optimal. Here is my situation:

• I have used dune-release to create this merge request. As it happens, dune-release added the opam file for the catt-web package. This package does not install anything, it just generates javascript code, and we are using internally, but I do not believe it should be on opam.
• We have some dependency problem with the landmarks library, that we use for profiling. I do not want to add landmarks as a mandatory dependency, as it is not necessary for the code to run smoothly. I thought I found a way to have landmarks be an optional dependency with dune, but evidently I failed in doing so.
• Since I submitted this pull request, I have been informed that the parsing we are doing fails on windows generated files. We now have a fix.

I will try to solve all those three problems and update this merge request accordingly

[mseri]

Thanks!

[thibautbenjamin]

I made the changes that I wanted. Hopefully it passes the CI. Please let me know if there is anything else I should do

[thibautbenjamin]

I am seeing there is still a compilation issue. One of the issues might be that one of the package is a coq plugin. I just find out that there was a separate repository for these. Should I remove the coq-plugin from this MR to only have the base package, and open an MR on the dedicated coq-plugins repo?