From e2e6a2e64fb0040c0b354b2bf267bf60b0ccd3f5 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 12 Aug 2026 18:39:55 +0200 Subject: [PATCH 1/5] Clean up the lock file The lock file contains several dependencies that are not related to the package `alt-ergo-lib.opam`. In particular, it contains dependencies related to the JavaScript package and they cannot be installed in a switch with OCaml 5.6.0. This commit removes them, upgrades the locked dune version to 3.24.2 and improves the filter performed by `make lock`. The `findlib` cannot be locked because it may contrain the OCaml version. --- Makefile | 12 +++++++++++- alt-ergo-lib.opam.locked | 41 +++++++++++++--------------------------- 2 files changed, 24 insertions(+), 29 deletions(-) diff --git a/Makefile b/Makefile index 41fa2ccc0..d1cd76566 100644 --- a/Makefile +++ b/Makefile @@ -205,7 +205,17 @@ lock: opam lock ./alt-ergo-lib.opam -w # Remove OCaml compiler constraints sed -i \ - '/"ocaml"\|"ocaml-base-compiler"\|"ocaml-system"\|"ocaml-config"\|"base-domains"\|"base-nnp"/d' \ + -e '/"ocaml"/d' \ + -e '/"ocaml-base-compiler"/d' \ + -e '/"ocaml-compiler-lib"/d' \ + -e '/"ocaml-system"/d' \ + -e '/"ocaml-config"/d' \ + -e '/"ocaml-variants"/d' \ + -e '/"base-domains"/d' \ + -e '/"base-effects"/d' \ + -e '/"base-nnp"/d' \ + -e '/"ocamlfind"/d' \ + -e '/"host-.*"/d' \ ./alt-ergo-lib.opam.locked dev-switch: diff --git a/alt-ergo-lib.opam.locked b/alt-ergo-lib.opam.locked index 8cabfc383..3bd07ffea 100644 --- a/alt-ergo-lib.opam.locked +++ b/alt-ergo-lib.opam.locked @@ -1,3 +1,4 @@ + opam-version: "2.0" name: "alt-ergo-lib" version: "dev" @@ -17,7 +18,6 @@ doc: "https://ocamlpro.github.io/alt-ergo" bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" depends: [ "base-bigarray" {= "base"} - "base-bytes" {= "base"} "base-threads" {= "base"} "base-unix" {= "base"} "camlzip" {= "1.14"} @@ -25,56 +25,44 @@ depends: [ "conf-gmp" {= "5"} "conf-pkg-config" {= "4"} "conf-zlib" {= "1"} - "cppo" {= "1.8.0"} "crunch" {= "4.0.0"} "csexp" {= "1.5.2"} "dolmen" {= "dev"} "dolmen_loop" {= "dev"} "dolmen_type" {= "dev"} - "dune" {= "3.22.0"} - "dune-build-info" {= "3.22.0"} - "dune-configurator" {= "3.22.0"} - "dune-private-libs" {= "3.22.0"} - "dune-site" {= "3.22.0"} - "dyn" {= "3.22.0"} + "dune" {= "3.24.2"} + "dune-build-info" {= "3.24.2"} + "dune-private-libs" {= "3.24.2"} + "dune-site" {= "3.24.2"} + "dyn" {= "3.24.2"} "fmt" {= "0.11.0"} - "fs-io" {= "3.22.0"} + "fs-io" {= "3.24.2"} "gen" {= "1.1"} "hmap" {= "0.8.1"} - "js_of_ocaml-compiler" {= "6.2.0"} "logs" {= "0.10.0"} - "lwt" {= "5.9.2"} "menhir" {= "20260209"} "menhirCST" {= "20260209"} "menhirGLR" {= "20260209"} "menhirLib" {= "20260209"} "menhirSdk" {= "20260209"} - "ocaml-compiler-libs" {= "v0.12.4"} - "ocaml-options-vanilla" {= "1"} "ocamlbuild" {= "0.16.1"} - "ocamlfind" {= "1.9.8"} - "ocplib-endian" {= "1.2"} "ocplib-simplex" {= "0.5.1"} - "ordering" {= "3.22.0"} - "ounit2" {= "2.2.7" & with-test} + "ordering" {= "3.24.2"} "pp" {= "2.0.0"} "pp_loc" {= "2.1.0"} "ptime" {= "1.2.0"} - "qcheck" {= "0.25" & with-test} - "qcheck-core" {= "0.25" & with-test} - "qcheck-ounit" {= "0.25" & with-test} - "sedlex" {= "3.7"} "seq" {= "base"} - "sexplib0" {= "v0.16.0"} "spelll" {= "0.4"} "stdlib-shims" {= "0.3.0"} - "stdune" {= "3.22.0"} - "top-closure" {= "3.22.0"} + "stdune" {= "3.24.2"} + "top-closure" {= "3.24.2"} "topkg" {= "1.1.1"} "uutf" {= "1.0.4"} - "yojson" {= "2.2.2"} "zarith" {= "1.14"} ] +conflicts: [ + "result" {< "1.5"} +] build: [ ["dune" "subst"] {dev} [ @@ -92,9 +80,6 @@ build: [ ["dune" "install" "-p" name "--create-install-files" name] ] dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git" -conflicts: [ - "result" {< "1.5"} -] pin-depends: [ [ "dolmen.dev" From 2aa995764eba60466912f6162957fc9bd2264137 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 14 Aug 2026 01:53:15 +0200 Subject: [PATCH 2/5] Generate lock files in a fresh switch Generating lock files in an existing switch is risky as they could included undesired optional dependencies by transitivity. This commit introduces a new strategy to generate lock files in order to mitigate this issue: - We don't generate a lock file for alt-ergo-js package, - For alt-ergo and alt-ergo-lib packages, the script installs them in a fresh switch, generates lock files and removes all the dependencies related to the OCaml compiler itself with opam-ed. --- Makefile | 18 +------ alt-ergo-lib.opam.locked | 10 ++-- alt-ergo.opam.locked | 91 +++++++++++++++++++++++++++++++++ rsc/extra/filter_depends.sh | 29 +++++++++++ rsc/extra/generate_lock_file.sh | 27 ++++++++++ 5 files changed, 156 insertions(+), 19 deletions(-) create mode 100644 alt-ergo.opam.locked create mode 100755 rsc/extra/filter_depends.sh create mode 100755 rsc/extra/generate_lock_file.sh diff --git a/Makefile b/Makefile index d1cd76566..629135a01 100644 --- a/Makefile +++ b/Makefile @@ -9,6 +9,7 @@ BIN_DIR := $(SRC_DIR)/bin LIB_DIR := $(SRC_DIR)/lib PLUGINS_DIR := $(SRC_DIR)/plugins PARSERS_DIR := $(SRC_DIR)/parsers +LOCK_SWITCH := alt-ergo-lock COMMON_DIR := $(BIN_DIR)/common BTEXT_DIR := $(BIN_DIR)/text @@ -201,22 +202,7 @@ archi: $(EXTRA_DIR)/ocamldot/ocamldot dot -Tpdf archi.dot > archi.pdf lock: - dune build ./alt-ergo-lib.opam - opam lock ./alt-ergo-lib.opam -w - # Remove OCaml compiler constraints - sed -i \ - -e '/"ocaml"/d' \ - -e '/"ocaml-base-compiler"/d' \ - -e '/"ocaml-compiler-lib"/d' \ - -e '/"ocaml-system"/d' \ - -e '/"ocaml-config"/d' \ - -e '/"ocaml-variants"/d' \ - -e '/"base-domains"/d' \ - -e '/"base-effects"/d' \ - -e '/"base-nnp"/d' \ - -e '/"ocamlfind"/d' \ - -e '/"host-.*"/d' \ - ./alt-ergo-lib.opam.locked + LOCK_SWITCH="$(LOCK_SWITCH)" ./rsc/extra/generate_lock_file.sh dev-switch: opam switch create . --deps-only --ignore-constraints-on alt-ergo-lib diff --git a/alt-ergo-lib.opam.locked b/alt-ergo-lib.opam.locked index 3bd07ffea..e84e938d6 100644 --- a/alt-ergo-lib.opam.locked +++ b/alt-ergo-lib.opam.locked @@ -21,11 +21,11 @@ depends: [ "base-threads" {= "base"} "base-unix" {= "base"} "camlzip" {= "1.14"} - "cmdliner" {= "2.1.0"} + "cmdliner" {= "2.1.1"} "conf-gmp" {= "5"} - "conf-pkg-config" {= "4"} + "conf-pkg-config" {= "5"} "conf-zlib" {= "1"} - "crunch" {= "4.0.0"} + "crunch" {= "4.1.0"} "csexp" {= "1.5.2"} "dolmen" {= "dev"} "dolmen_loop" {= "dev"} @@ -48,9 +48,13 @@ depends: [ "ocamlbuild" {= "0.16.1"} "ocplib-simplex" {= "0.5.1"} "ordering" {= "3.24.2"} + "ounit2" {= "2.2.7" & with-test} "pp" {= "2.0.0"} "pp_loc" {= "2.1.0"} "ptime" {= "1.2.0"} + "qcheck" {= "0.25" & with-test} + "qcheck-core" {= "0.25" & with-test} + "qcheck-ounit" {= "0.25" & with-test} "seq" {= "base"} "spelll" {= "0.4"} "stdlib-shims" {= "0.3.0"} diff --git a/alt-ergo.opam.locked b/alt-ergo.opam.locked new file mode 100644 index 000000000..70dbb574b --- /dev/null +++ b/alt-ergo.opam.locked @@ -0,0 +1,91 @@ +opam-version: "2.0" +name: "alt-ergo" +version: "dev" +synopsis: "The Alt-Ergo SMT prover" +description: """\ +Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro. + +See more details on https://alt-ergo.ocamlpro.com/""" +maintainer: "Alt-Ergo developers " +authors: "Alt-Ergo developers " +license: ["LicenseRef-OCamlpro-Non-Commercial" "Apache-2.0"] +tags: "org:OCamlPro" +homepage: "https://alt-ergo.ocamlpro.com/" +doc: "https://ocamlpro.github.io/alt-ergo" +bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" +depends: [ + "alt-ergo-lib" {= "dev"} + "base-bigarray" {= "base"} + "base-threads" {= "base"} + "base-unix" {= "base"} + "camlzip" {= "1.14"} + "cmdliner" {= "2.1.1"} + "conf-gmp" {= "5"} + "conf-pkg-config" {= "5"} + "conf-zlib" {= "1"} + "crunch" {= "4.1.0"} + "csexp" {= "1.5.2"} + "dolmen" {= "dev"} + "dolmen_loop" {= "dev"} + "dolmen_type" {= "dev"} + "dune" {= "3.24.2"} + "dune-build-info" {= "3.24.2"} + "dune-private-libs" {= "3.24.2"} + "dune-site" {= "3.24.2"} + "dyn" {= "3.24.2"} + "fmt" {= "0.11.0"} + "fs-io" {= "3.24.2"} + "gen" {= "1.1"} + "hmap" {= "0.8.1"} + "logs" {= "0.10.0"} + "menhir" {= "20260209"} + "menhirCST" {= "20260209"} + "menhirGLR" {= "20260209"} + "menhirLib" {= "20260209"} + "menhirSdk" {= "20260209"} + "ocamlbuild" {= "0.16.1"} + "ocplib-simplex" {= "0.5.1"} + "ordering" {= "3.24.2"} + "pp" {= "2.0.0"} + "pp_loc" {= "2.1.0"} + "ptime" {= "1.2.0"} + "seq" {= "base"} + "spelll" {= "0.4"} + "stdlib-shims" {= "0.3.0"} + "stdune" {= "3.24.2"} + "top-closure" {= "3.24.2"} + "topkg" {= "1.1.1"} + "uutf" {= "1.0.4"} + "zarith" {= "1.14"} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git" +pin-depends: [ + [ + "dolmen.dev" + "git+https://github.com/Gbury/dolmen.git#a0f1bc66e7256fff1068ac0df525a2d23c1f3ea7" + ] + [ + "dolmen_loop.dev" + "git+https://github.com/Gbury/dolmen.git#a0f1bc66e7256fff1068ac0df525a2d23c1f3ea7" + ] + [ + "dolmen_type.dev" + "git+https://github.com/Gbury/dolmen.git#a0f1bc66e7256fff1068ac0df525a2d23c1f3ea7" + ] +] diff --git a/rsc/extra/filter_depends.sh b/rsc/extra/filter_depends.sh new file mode 100755 index 000000000..d71800c8b --- /dev/null +++ b/rsc/extra/filter_depends.sh @@ -0,0 +1,29 @@ +#!/usr/bin/env bash +set -e + +forbidden_fields=( + "\"ocaml\"" + "\"ocaml-base-compiler\"" + "\"ocaml-system\"" + "\"ocaml-config\"" + "\"ocaml-variants\"" + "\"ocaml-compiler\"" + "\"ocaml-compiler-libs\"" + "\"ocaml-options-vanilla\"" + "\"base-domains\"" + "\"base-effects\"" + "\"base-nnp\"" + "\"ocamlfind\"" + "\"host" +) + +read input || true + +for key in "${forbidden_fields[@]}" +do + if [[ "$input" =~ "$key" ]] then + exit 1 + fi +done + +exit 0 diff --git a/rsc/extra/generate_lock_file.sh b/rsc/extra/generate_lock_file.sh new file mode 100755 index 000000000..5020ae10d --- /dev/null +++ b/rsc/extra/generate_lock_file.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash +set -e +trap cleanup EXIT +export OPAMYES=true +export OPAMSWITCH="$LOCK_SWITCH" + +function cleanup() { + opam switch remove "$LOCK_SWITCH" +} + +opam switch create "$LOCK_SWITCH" 5.4.1 --no-switch + +opam install --deps-only --with-test --assume-depexts \ + ./alt-ergo-lib.opam \ + ./alt-ergo.opam + +opam exec -- dune build @install @runtest -p \ + alt-ergo-lib,alt-ergo + +opam lock -w \ + ./alt-ergo-lib.opam \ + ./alt-ergo.opam + +opam-ed -i \ + "filter depends ./rsc/extra/filter_depends.sh" \ + -f ./alt-ergo-lib.opam.locked \ + -f ./alt-ergo.opam.locked From 30522c520570b95d1e988a05287cc4ea5edae82d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 14 Aug 2026 08:54:40 +0200 Subject: [PATCH 3/5] Add opam-ed package in the nix shell --- nix/default.nix | 1 + nix/opam-ed.nix | 25 +++++++++++++++++++++++++ nix/sources.json | 13 +++++++++++++ shell.nix | 1 + 4 files changed, 40 insertions(+) create mode 100644 nix/opam-ed.nix diff --git a/nix/default.nix b/nix/default.nix index 869559bce..1a0d62c7f 100644 --- a/nix/default.nix +++ b/nix/default.nix @@ -20,6 +20,7 @@ import sources.nixpkgs { }; }); zarith_stubs_js = self.callPackage ./zarith_stubs_js.nix { }; + opam-ed = self.callPackage ./opam-ed.nix { }; }); }) ]; diff --git a/nix/opam-ed.nix b/nix/opam-ed.nix new file mode 100644 index 000000000..4c5342def --- /dev/null +++ b/nix/opam-ed.nix @@ -0,0 +1,25 @@ +{ sources, lib, ocamlPackages, cmdliner_2, opam-file-format }: + +let + opam-ed = sources.opam-ed; +in + +ocamlPackages.buildDunePackage { + strictDeps = true; + pname = "opam-ed"; + inherit (opam-ed) version; + + minimalOCamlVersion = "4.08"; + duneVersion = "3"; + + propagatedBuildInputs = with ocamlPackages; [ + cmdliner_2 + opam-file-format + ]; + + src = opam-ed; + + meta = with lib; { + inherit (opam-ed) homepage description; + }; +} diff --git a/nix/sources.json b/nix/sources.json index 5fadf06b4..3c0b2d4eb 100644 --- a/nix/sources.json +++ b/nix/sources.json @@ -50,6 +50,19 @@ "url_template": "https://github.com///archive/.tar.gz", "version": "0.5.1" }, + "opam-ed": { + "branch": "master", + "description": "A small command-line tool to help with mechanical edition of opam files", + "homepage": null, + "owner": "ocaml-opam", + "repo": "opam-ed", + "rev": "ac93c41d99987f598dffa012f73794cafdc0e487", + "sha256": "1fm38mr439pm1yndskk484z4b7l20bdp7r14ygjxfc7rdny0w31a", + "type": "tarball", + "url": "https://github.com/ocaml-opam/opam-ed/archive/ac93c41d99987f598dffa012f73794cafdc0e487.tar.gz", + "url_template": "https://github.com///archive/.tar.gz", + "version": "0.5" + }, "pp_loc": { "branch": "v2.1.0", "description": "Pretty-printing for error source locations", diff --git a/shell.nix b/shell.nix index 5919fcfe7..fd316f3b0 100644 --- a/shell.nix +++ b/shell.nix @@ -42,5 +42,6 @@ pkgs.mkShell { landmarks-ppx qcheck utop + opam-ed ]); } From dbf5b16a716b98beb24fb4064ea7ba61f0fff055 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 14 Aug 2026 12:58:59 +0200 Subject: [PATCH 4/5] Do not erase the locked switch at end of the script --- Makefile | 3 +-- rsc/extra/generate_lock_file.sh | 20 ++++++++++++++------ 2 files changed, 15 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile index 629135a01..377e80e65 100644 --- a/Makefile +++ b/Makefile @@ -9,7 +9,6 @@ BIN_DIR := $(SRC_DIR)/bin LIB_DIR := $(SRC_DIR)/lib PLUGINS_DIR := $(SRC_DIR)/plugins PARSERS_DIR := $(SRC_DIR)/parsers -LOCK_SWITCH := alt-ergo-lock COMMON_DIR := $(BIN_DIR)/common BTEXT_DIR := $(BIN_DIR)/text @@ -202,7 +201,7 @@ archi: $(EXTRA_DIR)/ocamldot/ocamldot dot -Tpdf archi.dot > archi.pdf lock: - LOCK_SWITCH="$(LOCK_SWITCH)" ./rsc/extra/generate_lock_file.sh + ./rsc/extra/generate_lock_file.sh dev-switch: opam switch create . --deps-only --ignore-constraints-on alt-ergo-lib diff --git a/rsc/extra/generate_lock_file.sh b/rsc/extra/generate_lock_file.sh index 5020ae10d..2c39d14bb 100755 --- a/rsc/extra/generate_lock_file.sh +++ b/rsc/extra/generate_lock_file.sh @@ -1,14 +1,22 @@ #!/usr/bin/env bash -set -e -trap cleanup EXIT +set -euo pipefail +export LOCKED_SWITCH="alt-ergo-locked" export OPAMYES=true -export OPAMSWITCH="$LOCK_SWITCH" +export OPAMSWITCH="$LOCKED_SWITCH" -function cleanup() { - opam switch remove "$LOCK_SWITCH" +function check_switch_available() { + opam list >/dev/null 2>&1 } -opam switch create "$LOCK_SWITCH" 5.4.1 --no-switch +if check_switch_available; then + cat << EOF +The switch $LOCKED_SWITCH already exists. Please remove it to run the script +or override the value of the environment variable \$LOCKED_SWITCH. +EOF + exit 1 +fi + +opam switch create "$LOCKED_SWITCH" 5.4.1 --no-switch opam install --deps-only --with-test --assume-depexts \ ./alt-ergo-lib.opam \ From 0274cd6fd6d92c33cba350021e25f0576d23622d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 14 Aug 2026 14:14:21 +0200 Subject: [PATCH 5/5] Clean up the switch if it is a fresh one --- rsc/extra/generate_lock_file.sh | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/rsc/extra/generate_lock_file.sh b/rsc/extra/generate_lock_file.sh index 2c39d14bb..88e9432b0 100755 --- a/rsc/extra/generate_lock_file.sh +++ b/rsc/extra/generate_lock_file.sh @@ -1,9 +1,13 @@ #!/usr/bin/env bash set -euo pipefail -export LOCKED_SWITCH="alt-ergo-locked" +export LOCKED_SWITCH="${LOCKED_SWITCH:=alt-ergo-locked}" export OPAMYES=true export OPAMSWITCH="$LOCKED_SWITCH" +function cleanup() { + opam switch remove "$LOCKED_SWITCH" +} + function check_switch_available() { opam list >/dev/null 2>&1 } @@ -16,6 +20,7 @@ EOF exit 1 fi +trap cleanup EXIT opam switch create "$LOCKED_SWITCH" 5.4.1 --no-switch opam install --deps-only --with-test --assume-depexts \