search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.78k stars 639 forks source link

Coq Universe meta issue #9232

Open ejgallego opened 5 years ago

ejgallego commented 5 years ago

The "Coq Universe" is the composed build of Coq with all known maintained Coq libraries.

The idea of having such a global build is not new, as for example outlined here https://dune.build/blog/new-computation-model/ , or in coq-contribs, and is convenient in order to perform global refactoring, incremental CI testing, etc...

This issue intends to discuss a possible implementation plan and goals.

It is assumed that building the Coq universe would take huge amounts of memory and CPU power, thus developers willing to use it should have accordingly powerful machines.

Currently, thanks to Dune, there is some global build support for plugins and their ML part. IMO using Dune and following the OCaml roadmap does make sense, thus the concrete list of actions is:

Related issues:

ejgallego commented 5 years ago

FYI a prototype replacing the CI scripts with OCaml written universe manager + composition of coq libs (locally) for Dune is about to work soon.

My model does assume that auto-code synchronization is kinda science fiction thus it is designed to work with upstream repositories by submitting PRs, rebasing, etc...