Skip to content

Latest commit

 

History

History
 
 

ci

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
docker
docker
 
 
gitlab-modes
gitlab-modes
 
 
nix
nix
 
 
platform
platform
 
 
user-overlays
user-overlays
 
 
README-developers.md
README-developers.md
 
 
README-users.md
README-users.md
 
 
README.md
README.md
 
 
ci-aac_tactics.sh
ci-aac_tactics.sh
 
 
ci-analysis.sh
ci-analysis.sh
 
 
ci-argosy.sh
ci-argosy.sh
 
 
ci-async_test.sh
ci-async_test.sh
 
 
ci-atbr.sh
ci-atbr.sh
 
 
ci-autosubst.sh
ci-autosubst.sh
 
 
ci-autosubst_ocaml.sh
ci-autosubst_ocaml.sh
 
 
ci-basic-overlay.sh
ci-basic-overlay.sh
 
 
ci-bbv.sh
ci-bbv.sh
 
 
ci-bedrock2.sh
ci-bedrock2.sh
 
 
ci-bedrock2_examples.sh
ci-bedrock2_examples.sh
 
 
ci-bigenough.sh
ci-bigenough.sh
 
 
ci-bignums.sh
ci-bignums.sh
 
 
ci-category_theory.sh
ci-category_theory.sh
 
 
ci-ceres.sh
ci-ceres.sh
 
 
ci-coinduction.sh
ci-coinduction.sh
 
 
ci-color.sh
ci-color.sh
 
 
ci-common.sh
ci-common.sh
 
 
ci-compcert.sh
ci-compcert.sh
 
 
ci-coq_dpdgraph.sh
ci-coq_dpdgraph.sh
 
 
ci-coq_lsp.sh
ci-coq_lsp.sh
 
 
ci-coq_performance_tests.sh
ci-coq_performance_tests.sh
 
 
ci-coq_tools.sh
ci-coq_tools.sh
 
 
ci-coqhammer.sh
ci-coqhammer.sh
 
 
ci-coqprime.sh
ci-coqprime.sh
 
 
ci-coqtail.sh
ci-coqtail.sh
 
 
ci-coquelicot.sh
ci-coquelicot.sh
 
 
ci-coqutil.sh
ci-coqutil.sh
 
 
ci-corn.sh
ci-corn.sh
 
 
ci-cross_crypto.sh
ci-cross_crypto.sh
 
 
ci-deriving.sh
ci-deriving.sh
 
 
ci-elpi.sh
ci-elpi.sh
 
 
ci-elpi_test.sh
ci-elpi_test.sh
 
 
ci-engine_bench.sh
ci-engine_bench.sh
 
 
ci-equations.sh
ci-equations.sh
 
 
ci-equations_test.sh
ci-equations_test.sh
 
 
ci-ext_lib.sh
ci-ext_lib.sh
 
 
ci-fcsl_pcm.sh
ci-fcsl_pcm.sh
 
 
ci-fiat_crypto.sh
ci-fiat_crypto.sh
 
 
ci-fiat_crypto_legacy.sh
ci-fiat_crypto_legacy.sh
 
 
ci-fiat_crypto_ocaml.sh
ci-fiat_crypto_ocaml.sh
 
 
ci-fiat_parsers.sh
ci-fiat_parsers.sh
 
 
ci-finmap.sh
ci-finmap.sh
 
 
ci-flocq.sh
ci-flocq.sh
 
 
ci-fourcolor.sh
ci-fourcolor.sh
 
 
ci-hb.sh
ci-hb.sh
 
 
ci-hb_test.sh
ci-hb_test.sh
 
 
ci-hott.sh
ci-hott.sh
 
 
ci-http.sh
ci-http.sh
 
 
ci-iris.sh
ci-iris.sh
 
 
ci-itauto.sh
ci-itauto.sh
 
 
ci-itree.sh
ci-itree.sh
 
 
ci-itree_io.sh
ci-itree_io.sh
 
 
ci-jasmin.sh
ci-jasmin.sh
 
 
ci-json.sh
ci-json.sh
 
 
ci-kami.sh
ci-kami.sh
 
 
ci-lean_importer.sh
ci-lean_importer.sh
 
 
ci-ltac2_compiler.sh
ci-ltac2_compiler.sh
 
 
ci-math_classes.sh
ci-math_classes.sh
 
 
ci-mathcomp.sh
ci-mathcomp.sh
 
 
ci-mathcomp_test.sh
ci-mathcomp_test.sh
 
 
ci-mathcomp_word.sh
ci-mathcomp_word.sh
 
 
ci-mczify.sh
ci-mczify.sh
 
 
ci-menhir.sh
ci-menhir.sh
 
 
ci-metacoq.sh
ci-metacoq.sh
 
 
ci-mtac2.sh
ci-mtac2.sh
 
 
ci-neural_net_interp.sh
ci-neural_net_interp.sh
 
 
ci-oddorder.sh
ci-oddorder.sh
 
 
ci-paco.sh
ci-paco.sh
 
 
ci-paramcoq.sh
ci-paramcoq.sh
 
 
ci-parsec.sh
ci-parsec.sh
 
 
ci-perennial.sh
ci-perennial.sh
 
 
ci-quickchick.sh
ci-quickchick.sh
 
 
ci-quickchick_test.sh
ci-quickchick_test.sh
 
 
ci-reduction_effects.sh
ci-reduction_effects.sh
 
 
ci-refman.sh
ci-refman.sh
 
 
ci-relation_algebra.sh
ci-relation_algebra.sh
 
 
ci-rewriter.sh
ci-rewriter.sh
 
 
ci-riscv_coq.sh
ci-riscv_coq.sh
 
 
ci-rupicola.sh
ci-rupicola.sh
 
 
ci-sf.sh
ci-sf.sh
 
 
ci-simple_io.sh
ci-simple_io.sh
 
 
ci-smtcoq.sh
ci-smtcoq.sh
 
 
ci-smtcoq_trakt.sh
ci-smtcoq_trakt.sh
 
 
ci-stalmarck.sh
ci-stalmarck.sh
 
 
ci-stdlib.sh
ci-stdlib.sh
 
 
ci-stdlib_doc.sh
ci-stdlib_doc.sh
 
 
ci-stdlib_test.sh
ci-stdlib_test.sh
 
 
ci-tactician.sh
ci-tactician.sh
 
 
ci-tlc.sh
ci-tlc.sh
 
 
ci-trakt.sh
ci-trakt.sh
 
 
ci-unicoq.sh
ci-unicoq.sh
 
 

README.md

Continuous Integration for the Rocq Prover

Changes to Rocq are systematically tested for regression and compatibility breakage on our Continuous Integration (CI) platforms before integration, so as to ensure better robustness and catch problems as early as possible. These tests include the compilation of several external libraries / plugins.

This README is split into two specific documents:

  • README-users.md which contains information for authors of external libraries and plugins who might be interested in having their development tested in our CI system.

  • README-developers.md for Rocq developers / contributors, who must ensure that they don't break these external developments accidentally.

Remark: the CI policy outlined in these documents is susceptible to evolve and specific accommodations are of course possible.