search

coq-community / manifesto

Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
Other
68 stars 6 forks source link

Proposal to move coq-primitive to Coq-community #151

Open palmskog opened 8 months ago

palmskog commented 8 months ago

Project name: coq-primitive

Initial author(s): The Coq development team, INRIA, CNRS, and contributors

Current URL: https://github.com/palmskog/coq-primitive

Kind: OCaml library

License: LGPL-2.1-only

Description: This library provides modules for primitive objects from the Coq repo as a standalone OCaml library built using Dune. It should be useful in Coq projects that perform extraction to OCaml, but needs testing and validation to ensure this is the case.

Status: Possibly co-maintained by myself and @yforster, hopefully eventually included as a package in Coq itself.

The background here is that we would like to prevent everyone who wants to use uint63.ml/float64.ml/parray.ml from copying (bundling) the code from Coq, and instead use this standalone library/package, which should be released for each major Coq version, preferably into the regular OCaml repository. Once we have ensured it works, we can begin the process of migrating the packaging boilerplate into the Coq GitHub repo and archive this repo.

@yforster do you agree this is a good idea? Could you do some quick smoke test to ensure the current code is not completely broken? I have a stake in this stuff since I maintain several extraction-based projects, e.g., this one.

palmskog commented 7 months ago

@yforster so are you fine with being co-maintainer here? I think our main goal would be to ensure this project is not needed at all by integrating packages into the Coq repo, but it seems unlikely this would happen for 8.19. Integration in time for 8.20 is probably more realistic.