From c40a8abf40a471632ffca949bc0f85742fe0bf24 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 13 Apr 2026 15:24:25 +0200 Subject: [PATCH 1/2] Prepare for https://github.com/rocq-prover/stdlib/pull/251 --- .gitlab-ci.yml | 98 +++++++++++++++++++++++-- Makefile.ci | 3 + dev/ci/ci-basic-overlay.sh | 6 ++ dev/ci/docker/old_ubuntu_lts/Dockerfile | 2 +- doc/sphinx/addendum/micromega.rst | 8 +- 5 files changed, 105 insertions(+), 12 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index bd5fc9890774..c37eb7e7e54d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -40,7 +40,7 @@ variables: # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g. # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10) # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10) - BASE_CACHEKEY: "old_ubuntu_lts-V2025-11-14-69405188ee" + BASE_CACHEKEY: "old_ubuntu_lts-V2026-04-13-df80ac3f8b" EDGE_CACHEKEY: "edge_ubuntu-V2026-05-22-20228d7d42" BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY" EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY" @@ -591,6 +591,7 @@ validate:base: CI_TARGETS: "stdlib" needs: - build:base + - plugin:ci-micromega - library:ci-stdlib only: *full-ci @@ -610,6 +611,7 @@ validate:edge+flambda: CI_TARGETS: "stdlib" needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda variables: OPAM_VARIANT: "+flambda" @@ -622,18 +624,21 @@ library:ci-argosy: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib library:ci-autosubst: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda library:ci-bbv: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib library:ci-bedrock2: @@ -643,6 +648,7 @@ library:ci-bedrock2: SAVE_BUILD_CI: "1" # for bedrock2_examples needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-coqutil - library:ci-kami @@ -655,6 +661,7 @@ library:ci-bedrock2_examples: NJOBS: "1" needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-coqutil - library:ci-kami @@ -667,6 +674,7 @@ library:ci-category_theory: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-equations stage: build-2 @@ -675,6 +683,7 @@ library:ci-color: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-bignums stage: build-2 @@ -683,6 +692,7 @@ library:ci-compcert: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-flocq - library:ci-menhir @@ -692,18 +702,21 @@ library:ci-coq_performance_tests: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib library:ci-coq_tools: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib library:ci-coqprime: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-bignums stage: build-2 @@ -715,6 +728,7 @@ library:ci-coquelicot: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb - plugin:ci-micromega @@ -725,12 +739,14 @@ library:ci-coqutil: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda library:ci-cross_crypto: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib variables: SAVE_BUILD_CI: "1" # for the minimizer (no install target available) @@ -739,18 +755,21 @@ library:ci-engine_bench: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib library:ci-ext_lib: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda library:ci-fcsl_pcm: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb - plugin:ci-micromega @@ -764,6 +783,7 @@ library:ci-fiat_crypto: SAVE_BUILD_CI: "1" # for fiat_crypto_ocaml needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-coqutil - library:ci-kami @@ -779,6 +799,7 @@ library:ci-fiat_crypto_legacy: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-coqprime stage: build-3+ @@ -791,6 +812,7 @@ library:ci-fiat_crypto_ocaml: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-coqutil - library:ci-kami @@ -808,18 +830,21 @@ library:ci-flocq: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda library:ci-kami: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda library:ci-menhir: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda library:ci-oddorder: @@ -844,6 +869,7 @@ library:ci-corn: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-bignums - plugin:ci-elpi_hb # CoRN uses elpi only (not HB) - depending on ci-elpi_hb reduces CI package count @@ -857,6 +883,7 @@ library:ci-iris: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-autosubst stage: build-2 @@ -865,6 +892,7 @@ library:ci-math_classes: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-bignums stage: build-2 @@ -874,7 +902,7 @@ library:ci-mathcomp: needs: - build:edge+flambda - plugin:ci-elpi_hb # for Hierarchy Builder - - plugin:ci-micromega + - plugin:ci-micromega+flambda stage: build-2 variables: SAVE_BUILD_CI: "1" # for mathcomp_test @@ -884,7 +912,7 @@ library:ci-mathcomp_test: needs: - build:edge+flambda - plugin:ci-elpi_hb - - plugin:ci-micromega + - plugin:ci-micromega+flambda - library:ci-mathcomp stage: build-3+ @@ -892,6 +920,7 @@ library:ci-mczify: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb - plugin:ci-micromega @@ -924,7 +953,7 @@ library:ci-analysis: - library:ci-finmap - library:ci-bigenough - plugin:ci-elpi_hb # for Hierarchy Builder - - plugin:ci-micromega + - plugin:ci-micromega+flambda stage: build-3+ variables: SAVE_BUILD_CI: "1" # for analysis_stdlib @@ -938,7 +967,7 @@ library:ci-analysis_stdlib: - library:ci-bigenough - library:ci-analysis - plugin:ci-elpi_hb # for Hierarchy Builder - - plugin:ci-micromega + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda stage: build-3+ @@ -946,18 +975,21 @@ library:ci-neural_net_interp: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib library:ci-paco: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda library:ci-itree: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-ext_lib - library:ci-paco @@ -967,6 +999,7 @@ library:ci-itree_io: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-ext_lib - library:ci-paco @@ -978,6 +1011,7 @@ library:ci-simple_io: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-ext_lib stage: build-2 @@ -986,15 +1020,22 @@ library:ci-simple_io: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib library:ci-stdlib: extends: .ci-template + needs: + - build:base + - plugin:ci-micromega variables: SAVE_BUILD_CI: "1" # for test suite library:ci-stdlib+flambda: extends: .ci-template-flambda + needs: + - build:edge+flambda + - plugin:ci-micromega+flambda variables: CI_TARGETS: "stdlib" SAVE_BUILD_CI: "1" # for test suite @@ -1003,6 +1044,7 @@ library:ci-stdlib_test: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib stage: build-2 @@ -1010,6 +1052,7 @@ library:ci-stdlib_doc: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda stage: build-2 variables: @@ -1019,6 +1062,7 @@ library:ci-tlc: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib library:ci-unimath: @@ -1028,6 +1072,7 @@ library:ci-verdi_raft: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda library:ci-vst: @@ -1036,6 +1081,7 @@ library:ci-vst: NJOBS: "1" needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-flocq - library:ci-menhir @@ -1047,6 +1093,7 @@ library:ci-deriving: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb - plugin:ci-micromega @@ -1057,6 +1104,7 @@ library:ci-mathcomp_word: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb - plugin:ci-micromega @@ -1067,6 +1115,7 @@ library:ci-jasmin: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb - plugin:ci-micromega @@ -1082,6 +1131,7 @@ library:ci-http: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb - plugin:ci-micromega @@ -1103,12 +1153,14 @@ plugin:ci-aac_tactics: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda plugin:ci-atbr: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda plugin:ci-autosubst_ocaml: @@ -1118,6 +1170,7 @@ plugin:ci-itauto: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda allow_failure: true @@ -1125,24 +1178,28 @@ plugin:ci-bignums: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda plugin:ci-coinduction: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda plugin:ci-coq_dpdgraph: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda plugin:ci-coqhammer: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda plugin:ci-elpi_hb: @@ -1157,6 +1214,7 @@ plugin:ci-elpi_test: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb stage: build-2 @@ -1165,6 +1223,7 @@ plugin:ci-hb_test: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb stage: build-2 @@ -1173,6 +1232,7 @@ plugin:ci-equations: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda variables: SAVE_BUILD_CI: "1" # for equations_test @@ -1181,6 +1241,7 @@ plugin:ci-equations_test: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-equations stage: build-2 @@ -1189,12 +1250,14 @@ plugin:ci-fiat_parsers: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib plugin:ci-lean_importer: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib plugin:ci-ltac2_compiler: @@ -1204,6 +1267,7 @@ plugin:ci-metarocq: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-equations - library:ci-ext_lib @@ -1211,14 +1275,21 @@ plugin:ci-metarocq: timeout: 1h 30min plugin:ci-micromega: + extends: .ci-template + variables: + SAVE_BUILD_CI: "1" # for test suite + +plugin:ci-micromega+flambda: extends: .ci-template-flambda - needs: - - build:edge+flambda + variables: + CI_TARGETS: "micromega" + SAVE_BUILD_CI: "1" # for test suite plugin:ci-mtac2: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda variables: CI_TARGETS: "unicoq mtac2" @@ -1227,12 +1298,14 @@ plugin:ci-paramcoq: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda plugin:ci-perennial: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda plugin:plugin-tutorial: @@ -1247,6 +1320,7 @@ plugin:ci-quickchick: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-ext_lib - library:ci-simple_io @@ -1261,6 +1335,7 @@ plugin:ci-quickchick_test: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-ext_lib - library:ci-simple_io @@ -1277,6 +1352,7 @@ plugin:ci-relation_algebra: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb - plugin:ci-micromega @@ -1288,12 +1364,14 @@ plugin:ci-rewriter: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda library:ci-riscv_coq: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-coqutil stage: build-2 @@ -1302,6 +1380,7 @@ library:ci-rupicola: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - library:ci-coqutil - library:ci-kami @@ -1313,6 +1392,7 @@ plugin:ci-rocq_lsp: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda plugin:ci-vsrocq: @@ -1322,12 +1402,14 @@ plugin:ci-smtcoq: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib plugin:ci-stalmarck: extends: .ci-template needs: - build:base + - plugin:ci-micromega - library:ci-stdlib plugin:ci-tactician: @@ -1337,12 +1419,14 @@ plugin:ci-waterproof: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda doc:ci-refman: extends: .ci-template-flambda needs: - build:edge+flambda + - plugin:ci-micromega+flambda - library:ci-stdlib+flambda - plugin:ci-elpi_hb - plugin:ci-micromega diff --git a/Makefile.ci b/Makefile.ci index 70708e47a530..e3cd986da3d2 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -28,6 +28,7 @@ CI_PLATFORM_FULL= \ ci-mathcomp \ ci-mathcomp_word \ ci-mczify \ + ci-micromega \ ci-finmap \ ci-bigenough \ ci-analysis \ @@ -178,6 +179,8 @@ ci-smtcoq_trakt: ci-stdlib ci-trakt ci-stalmarck: ci-stdlib +ci-stdlib: ci-micromega + ci-stdlib_test: ci-stdlib ci-stdlib_doc: ci-stdlib diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index b97e041df281..ef31e64b172f 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -392,6 +392,12 @@ project async_test "https://github.com/liyishuai/coq-async-test" "master" project http "https://github.com/liyishuai/coq-http" "master" # Contact @liyishuai on github +######################################################################## +# micromega-plugin +######################################################################## +project micromega "https://github.com/rocq-community/micromega-plugin" "master" +# Contact @fajb, @proux01 on github + ######################################################################## # paramcoq ######################################################################## diff --git a/dev/ci/docker/old_ubuntu_lts/Dockerfile b/dev/ci/docker/old_ubuntu_lts/Dockerfile index ee78cfc0a945..9daf9663fb83 100644 --- a/dev/ci/docker/old_ubuntu_lts/Dockerfile +++ b/dev/ci/docker/old_ubuntu_lts/Dockerfile @@ -52,7 +52,7 @@ ENV COMPILER="4.14.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.11 ounit2.2.2.6 yojson.1.7.0 camlzip.1.10" \ CI_OPAM="ocamlgraph.2.0.0 cppo.1.6.9" \ - BASE_ONLY_OPAM="dune.3.8.3 stdlib-shims.0.1.0 ocamlfind.1.9.1 odoc.2.0.2 num.1.4" + BASE_ONLY_OPAM="dune.3.8.3 stdlib-shims.0.1.0 ocamlfind.1.9.1 odoc.2.0.2 num.1.4 ppx_optcomp.v0.15.0" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.2" diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 759ae31aa552..c1f082509541 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -477,22 +477,22 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz `, the goal is valid. Proof. pose (ff := IMPL (A isProp - {| Flhs := PEadd (PEX 1) (PEmul (PEc 2) (PEX 2)); + {| Flhs := PEadd (@PEX _ 1) (PEmul (PEc 2) (@PEX _ 2)); Fop := OpLe; Frhs := PEc 4 |} tt) None (IMPL (A isProp - {| Flhs := PEadd (PEmul (PEc 2) (PEX 1)) (PEX 2); + {| Flhs := PEadd (PEmul (PEc 2) (@PEX _ 1)) (@PEX _ 2); Fop := OpLe; Frhs := PEc 4 |} tt) None (A isProp - {| Flhs := PEadd (PEX 1) (PEX 2); + {| Flhs := PEadd (@PEX _ 1) (@PEX _ 2); Fop := OpLt; Frhs := PEc 3 |} tt)) : BFormula (Formula Q) isProp). .. rocqtop:: all extra-stdlib pose (varmap := VarMap.Branch (VarMap.Elt y) x VarMap.Empty). - let ff' := eval unfold ff in ff in wlra_Q wit ff'. + let ff' := eval unfold ff in ff in mp_wlra_Q wit ff'. change (eval_bf (Qeval_formula (@VarMap.find Q 0 varmap)) ff). apply (QTautoChecker_sound ff wit). From 0d6af778e06d5aefda9c0eb3098aaeba146e9a90 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 10 Jun 2026 08:30:36 +0200 Subject: [PATCH 2/2] Add overlays --- dev/ci/user-overlays/21842-fajb-tify.sh | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 dev/ci/user-overlays/21842-fajb-tify.sh diff --git a/dev/ci/user-overlays/21842-fajb-tify.sh b/dev/ci/user-overlays/21842-fajb-tify.sh new file mode 100644 index 000000000000..7bf4ac1970d4 --- /dev/null +++ b/dev/ci/user-overlays/21842-fajb-tify.sh @@ -0,0 +1,10 @@ +overlay bedrock2 https://github.com/proux01/bedrock2 stdlib251 21842 +overlay coqutil https://github.com/proux01/coqutil stdlib251 21842 +overlay elpi https://github.com/proux01/coq-elpi stdlib251 21842 +overlay equations https://github.com/proux01/Coq-Equations stdlib251 21842 +overlay itauto https://github.com/proux01/itauto stdlib251 21842 +overlay metarocq https://github.com/proux01/metarocq stdlib251 21842 +overlay micromega https://github.com/rocq-community/micromega-plugin tify 21842 +overlay stdlib https://github.com/fajb/stdlib tify 21842 +overlay smtcoq https://github.com/proux01/smtcoq stdlib251 21842 +overlay waterproof https://github.com/proux01/coq-waterproof stdlib251 21842