You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
@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.
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.
The text was updated successfully, but these errors were encountered: