From 7ecb79975df5536a82842ff99fbd0bb24124116d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 11 Sep 2023 10:59:31 +0200 Subject: [PATCH 1/6] Test AE on 4.08.0 and 4.14.2 --- .github/workflows/build.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 3484cf81b..0cac8b1b3 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -8,7 +8,7 @@ on: permissions: {} env: - OCAML_DEFAULT_VERSION: 4.10.1 + OCAML_DEFAULT_VERSION: 4.08.0 # Add OPAMYES=true to the environment, this is usefill to replace `-y` option # in any opam call OPAMYES: true @@ -26,7 +26,8 @@ jobs: - macos-latest - ubuntu-latest ocaml-compiler: - - 4.10.1 + - 4.08.0 + - 4.14.2 runs-on: ${{ matrix.os }} From f2ea8a818dfa044de25ba0f0b8032816e064fe44 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 11 Sep 2023 11:07:52 +0200 Subject: [PATCH 2/6] Use 4.14.1 --- .github/workflows/build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 0cac8b1b3..4b9b1d865 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -27,7 +27,7 @@ jobs: - ubuntu-latest ocaml-compiler: - 4.08.0 - - 4.14.2 + - 4.14.1 runs-on: ${{ matrix.os }} From 8386e0797ba13cf3230b3c82813b1eaf2ced296d Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 11 Sep 2023 14:42:21 +0200 Subject: [PATCH 3/6] Use 4.08.1 as the lower bound --- .github/workflows/build.yml | 4 ++-- alt-ergo-lib.opam | 2 +- alt-ergo-parsers.opam | 2 +- alt-ergo.opam | 2 +- dune-project | 6 +++--- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 4b9b1d865..f4df18ba2 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -8,7 +8,7 @@ on: permissions: {} env: - OCAML_DEFAULT_VERSION: 4.08.0 + OCAML_DEFAULT_VERSION: 4.08.1 # Add OPAMYES=true to the environment, this is usefill to replace `-y` option # in any opam call OPAMYES: true @@ -26,7 +26,7 @@ jobs: - macos-latest - ubuntu-latest ocaml-compiler: - - 4.08.0 + - 4.08.1 - 4.14.1 runs-on: ${{ matrix.os }} diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index e9ee9c2a8..e7959f9ba 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -14,7 +14,7 @@ homepage: "https://alt-ergo.ocamlpro.com/" doc: "https://ocamlpro.github.io/alt-ergo" bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" depends: [ - "ocaml" {>= "4.08.0"} + "ocaml" {>= "4.08.1"} "dune" {>= "3.0"} "dune-build-info" "dolmen" {>= "0.9"} diff --git a/alt-ergo-parsers.opam b/alt-ergo-parsers.opam index 3349ef9f8..708a41a0d 100644 --- a/alt-ergo-parsers.opam +++ b/alt-ergo-parsers.opam @@ -14,7 +14,7 @@ homepage: "https://alt-ergo.ocamlpro.com/" doc: "https://ocamlpro.github.io/alt-ergo" bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" depends: [ - "ocaml" {>= "4.08.0"} + "ocaml" {>= "4.08.1"} "dune" {>= "3.0"} "alt-ergo-lib" {= version} "psmt2-frontend" {>= "0.4"} diff --git a/alt-ergo.opam b/alt-ergo.opam index cab36cf82..c8fd35ac0 100644 --- a/alt-ergo.opam +++ b/alt-ergo.opam @@ -12,7 +12,7 @@ homepage: "https://alt-ergo.ocamlpro.com/" doc: "https://ocamlpro.github.io/alt-ergo" bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" depends: [ - "ocaml" {>= "4.08.0"} + "ocaml" {>= "4.08.1"} "dune" {>= "3.0"} "alt-ergo-lib" {= version} "alt-ergo-parsers" {= version} diff --git a/dune-project b/dune-project index 4df02c309..db62ff3dc 100644 --- a/dune-project +++ b/dune-project @@ -25,7 +25,7 @@ Alt-Ergo is an automatic theorem prover of mathematical formulas. It was develop See more details on https://alt-ergo.ocamlpro.com/") (depends - (ocaml (>= 4.08.0)) + (ocaml (>= 4.08.1)) dune (alt-ergo-lib (= :version)) (alt-ergo-parsers (= :version)) @@ -51,7 +51,7 @@ See more details on http://alt-ergo.ocamlpro.com/" (license "LicenseRef-OcamlPro-Non-Commercial") (depends - (ocaml (>= 4.08.0)) + (ocaml (>= 4.08.1)) dune (alt-ergo-lib (= :version)) (psmt2-frontend (>= 0.4)) @@ -74,7 +74,7 @@ See more details on http://alt-ergo.ocamlpro.com/" (license "LicenseRef-OcamlPro-Non-Commercial") (depends - (ocaml (>= 4.08.0)) + (ocaml (>= 4.08.1)) dune dune-build-info (dolmen (>= 0.9)) From 1420dafaf515dcc63fd1e3acaf0481949569efda Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 11 Sep 2023 16:39:23 +0200 Subject: [PATCH 4/6] Update the changes log --- CHANGES.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index b4629b521..4a2dd37a6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,9 @@ ## unreleased -### deprecated -* printing underscore instead of fresh value in model +### Deprecated +* printing underscore instead of fresh value in model (PR #805) + +### Build +* use OCaml 4.08.1 as the minimal supported version (PR #803) ## v2.5.0 From f7270f4faf73684905b301ceb775acfa3f78b131 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 11 Sep 2023 16:39:51 +0200 Subject: [PATCH 5/6] Add OCaml 5.0.0 --- .github/workflows/build.yml | 1 + test.smt2 | 5 +++++ 2 files changed, 6 insertions(+) create mode 100644 test.smt2 diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index f4df18ba2..70f236177 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -28,6 +28,7 @@ jobs: ocaml-compiler: - 4.08.1 - 4.14.1 + - 5.0.0 runs-on: ${{ matrix.os }} diff --git a/test.smt2 b/test.smt2 new file mode 100644 index 000000000..7bcb70d3c --- /dev/null +++ b/test.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-fun a (Int) Int) +(check-sat) +(get-model) From d4964d9afdd139c87d6e47777b0947880621476c Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 11 Sep 2023 16:41:44 +0200 Subject: [PATCH 6/6] Remove artefact --- test.smt2 | 5 ----- 1 file changed, 5 deletions(-) delete mode 100644 test.smt2 diff --git a/test.smt2 b/test.smt2 deleted file mode 100644 index 7bcb70d3c..000000000 --- a/test.smt2 +++ /dev/null @@ -1,5 +0,0 @@ -(set-logic ALL) -(set-option :produce-models true) -(declare-fun a (Int) Int) -(check-sat) -(get-model)