Merge pull request #1899 from goblint/github-actions-macos-13-deprecated

sim642 · web-flow · commit 272a0df4e00d · 2025-12-12T17:09:21.000+02:00
Update CI runner images
diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
@@ -16,7 +16,7 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+          - ubuntu-latest
         ocaml-compiler:
           - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
@@ -40,7 +40,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
-        if: ${{ matrix.os == 'ubuntu-22.04' }}
+        if: ${{ startsWith(matrix.os, 'ubuntu') }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -16,7 +16,7 @@ jobs:
     strategy:
       matrix:
         os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+          - ubuntu-latest
         ocaml-compiler:
           - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml
@@ -10,7 +10,7 @@ jobs:
     strategy:
       matrix:
         os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+          - ubuntu-latest
         ocaml-compiler:
           - 4.14.x
 
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
@@ -17,8 +17,8 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
-          - macos-13
+          - ubuntu-latest
+          - macos-latest
         ocaml-compiler:
           - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
@@ -42,7 +42,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
-        if: ${{ matrix.os == 'ubuntu-22.04' }}
+        if: ${{ startsWith(matrix.os, 'ubuntu') }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
@@ -73,7 +73,7 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+          - ubuntu-latest
         ocaml-compiler:
           - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
@@ -94,7 +94,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
-        if: ${{ matrix.os == 'ubuntu-22.04' }}
+        if: ${{ startsWith(matrix.os, 'ubuntu') }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install spin
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
@@ -14,27 +14,71 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
-          - macos-13
-        ocaml-compiler:
-          - 5.2.x
-          - 5.1.x
-          - 5.0.x
-          - ocaml-variants.4.14.2+options,ocaml-option-flambda
-          - 4.14.x
-        apron:
-          - false
-          - true
-        z3:
-          - false
-
+        # We don't want a full matrix because it is too slow, so we only have linear axes overriding these below.
         include:
-          - os: ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+          # Common configuration
+          - os: ubuntu-24.04
+            ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
+            apron: true
+            z3: false
+
+          # OCaml versions
+          - os: ubuntu-24.04
+            ocaml-compiler: 5.4.x
+            apron: true
+            z3: false
+          - os: ubuntu-24.04
+            ocaml-compiler: 5.3.x
+            apron: true
+            z3: false
+          - os: ubuntu-24.04
+            ocaml-compiler: 5.2.x
+            apron: true
+            z3: false
+          - os: ubuntu-24.04
+            ocaml-compiler: 5.1.x
+            apron: true
+            z3: false
+          - os: ubuntu-24.04
+            ocaml-compiler: 5.0.x
+            apron: true
+            z3: false
+          - os: ubuntu-24.04
             ocaml-compiler: 4.14.x
+            apron: true
+            z3: false
+
+          # OS-s
+          - os: ubuntu-22.04
+            ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
+            apron: true
+            z3: false
+          - os: macos-26
+            ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
+            apron: true
+            z3: false
+          - os: macos-15-intel
+            ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
+            apron: true
+            z3: false
+          - os: macos-15
+            ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
+            apron: true
+            z3: false
+          - os: macos-14
+            ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
+            apron: true
+            z3: false
+
+          # Optional dependencies
+          - os: ubuntu-24.04
+            ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
+            apron: false
+            z3: false
+          - os: ubuntu-24.04
+            ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
+            apron: true
             z3: true
-          - os: macos-latest
-            ocaml-compiler: 4.14.x
 
     # customize name to use readable string for apron instead of just a boolean
     # workaround for missing ternary operator: https://github.com/actions/runner/issues/409
@@ -52,7 +96,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
-        if: ${{ matrix.os == 'ubuntu-22.04' }}
+        if: ${{ startsWith(matrix.os, 'ubuntu') }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
@@ -63,7 +107,7 @@ jobs:
 
       - name: Install Apron dependencies
         if: ${{ matrix.apron }}
-        run: opam install apron mlgmpidl.1.2.15
+        run: opam install apron mlgmpidl
 
       - name: Install Z3 dependencies
         if: ${{ matrix.z3 }}
@@ -86,8 +130,8 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
-          - macos-13
+          - ubuntu-latest
+          - macos-latest
         ocaml-compiler:
           - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
 
@@ -105,7 +149,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
-        if: ${{ matrix.os == 'ubuntu-22.04' }}
+        if: ${{ startsWith(matrix.os, 'ubuntu') }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
@@ -115,7 +159,7 @@ jobs:
         run: sudo gem install os
 
       - name: Install Apron dependencies
-        run: opam install apron mlgmpidl.1.2.15
+        run: opam install apron mlgmpidl
 
       - name: Downgrade dependencies
         # without "+removed" in criteria, because it also removes optional apron
@@ -138,8 +182,8 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
-          - macos-13
+          - ubuntu-latest
+          - macos-latest
         ocaml-compiler:
           - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
 
@@ -155,14 +199,14 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
-        if: ${{ matrix.os == 'ubuntu-22.04' }}
+        if: ${{ startsWith(matrix.os, 'ubuntu') }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install Goblint with test
         run: opam install goblint --with-test
 
       - name: Install Apron dependencies
-        run: opam install apron mlgmpidl.1.2.15
+        run: opam install apron mlgmpidl
 
       - name: Symlink installed goblint to repository # because tests want to use locally built one
         run: ln -s $(opam exec -- which goblint) goblint
@@ -206,7 +250,7 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
+          - ubuntu-latest
         ocaml-compiler:
           - ocaml-variants.5.0.0+options,ocaml-option-flambda
         node-version:
diff --git a/dune-project b/dune-project
@@ -39,7 +39,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (ocaml (>= 4.14))
     (goblint-cil (>= 2.0.9)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.9.0))
-    (zarith (>= 1.10))
+    (zarith (>= 1.12))
     (yojson (and (>= 2.0.0) (< 3))) ; json-data-encoding has incompatible yojson representation for yojson 3
     (qcheck-core (>= 0.19))
     (ppx_deriving (>= 6.0.2))
@@ -80,6 +80,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (apron (< v0.9.15)) ; lower bounds for depopts seem to not properly constrain in builtin-0install lower-bounds job, so upper bounds for conflicts instead
     (camlidl (< 1.13)) ; for stability (https://github.com/goblint/analyzer/issues/1520)
     (ez-conf-lib (= 1)) ; https://github.com/nberth/ez-conf-lib/issues/3
+    (mlgmpidl (< 1.3.0)) ; to use conf-mpfr-paths to work on MacOS
   )
   (sites
     (share lib)
diff --git a/goblint.opam b/goblint.opam
@@ -41,7 +41,7 @@ depends: [
   "ocaml" {>= "4.14"}
   "goblint-cil" {>= "2.0.9"}
   "batteries" {>= "3.9.0"}
-  "zarith" {>= "1.10"}
+  "zarith" {>= "1.12"}
   "yojson" {>= "2.0.0" & < "3"}
   "qcheck-core" {>= "0.19"}
   "ppx_deriving" {>= "6.0.2"}
@@ -78,6 +78,7 @@ conflicts: [
   "apron" {< "v0.9.15"}
   "camlidl" {< "1.13"}
   "ez-conf-lib" {= "1"}
+  "mlgmpidl" {< "1.3.0"}
 ]
 build: [
   ["dune" "subst"] {dev}
diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -140,6 +140,7 @@ conflicts: [
   "apron" {< "v0.9.15"}
   "camlidl" {< "1.13"}
   "ez-conf-lib" {= "1"}
+  "mlgmpidl" {< "1.3.0"}
 ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}

Original file line number	Diff line number	Diff line change
`@@ -140,6 +140,7 @@ conflicts: [`
`140`	`140`	`"apron" {< "v0.9.15"}`
`141`	`141`	`"camlidl" {< "1.13"}`
`142`	`142`	`"ez-conf-lib" {= "1"}`
	`143`	`+ "mlgmpidl" {< "1.3.0"}`
`143`	`144`	`]`
`144`	`145`	`post-messages: [`
`145`	`146`	`"Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}`