diff --git a/Makefile b/Makefile index 41fa2ccc0..377e80e65 100644 --- a/Makefile +++ b/Makefile @@ -201,12 +201,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 \ - '/"ocaml"\|"ocaml-base-compiler"\|"ocaml-system"\|"ocaml-config"\|"base-domains"\|"base-nnp"/d' \ - ./alt-ergo-lib.opam.locked + ./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 8cabfc383..e84e938d6 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,45 +18,36 @@ 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"} - "cmdliner" {= "2.1.0"} + "cmdliner" {= "2.1.1"} "conf-gmp" {= "5"} - "conf-pkg-config" {= "4"} + "conf-pkg-config" {= "5"} "conf-zlib" {= "1"} - "cppo" {= "1.8.0"} - "crunch" {= "4.0.0"} + "crunch" {= "4.1.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"} + "ordering" {= "3.24.2"} "ounit2" {= "2.2.7" & with-test} "pp" {= "2.0.0"} "pp_loc" {= "2.1.0"} @@ -63,18 +55,18 @@ depends: [ "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 +84,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" 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/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/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..88e9432b0 --- /dev/null +++ b/rsc/extra/generate_lock_file.sh @@ -0,0 +1,40 @@ +#!/usr/bin/env bash +set -euo pipefail +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 +} + +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 + +trap cleanup EXIT +opam switch create "$LOCKED_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 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 ]); }