Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 6 commits into from
Oct 15, 2024

Conversation

thibautbenjamin
Copy link
Contributor

An infinity-categorical coherence typechecker

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

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
Copy link
Contributor Author

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
Copy link
Member

mseri commented Oct 11, 2024

Thanks!

@thibautbenjamin
Copy link
Contributor Author

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
Copy link
Contributor Author

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?

@mseri
Copy link
Member

mseri commented Oct 14, 2024

No, don't worry, it looks all right. The windows failure is coq-core that is not building properly in our CI and the other failure is due to a strict lint that is there for our own sake (to avoid certain package names collisions).

Would it be possible, however, to have one of the maintainers email in the opam file?

@thibautbenjamin
Copy link
Contributor Author

I just added our emails! Let me know if there is anything else I should do

@mseri
Copy link
Member

mseri commented Oct 15, 2024

Thanks a lot!

@mseri mseri merged commit cdc6ae9 into ocaml:master Oct 15, 2024
0 of 2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants