unlocked #1939
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: unlocked | |
| on: | |
| # pull_request: # save CI time on PRs, run manually if needed (before merge) or find out failures from scheduled run (after merge) | |
| workflow_dispatch: | |
| schedule: | |
| # nightly | |
| - cron: '31 1 * * *' # 01:31 UTC, 02:31/03:31 Munich, 03:31/04:31 Tartu | |
| # GitHub Actions load is high at minute 0, so avoid that | |
| jobs: | |
| regression: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: | |
| - ubuntu-latest | |
| - 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 | |
| include: | |
| - os: ubuntu-latest | |
| ocaml-compiler: 4.14.x | |
| 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 | |
| name: regression (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}${{ matrix.apron && ', apron' || '' }}${{ matrix.z3 && ', z3' || '' }}) | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| - name: Set up OCaml ${{ matrix.ocaml-compiler }} | |
| uses: ocaml/setup-ocaml@v3 | |
| with: | |
| ocaml-compiler: ${{ matrix.ocaml-compiler }} | |
| - name: Install graph-easy # TODO: remove if depext --with-test works | |
| if: ${{ matrix.os == 'ubuntu-latest' }} | |
| run: sudo apt install -y libgraph-easy-perl | |
| - name: Install dependencies | |
| run: opam install . --deps-only --with-test | |
| - name: Install Apron dependencies | |
| if: ${{ matrix.apron }} | |
| run: | | |
| opam depext apron | |
| opam install apron mlgmpidl.1.2.15 | |
| - name: Install Z3 dependencies | |
| if: ${{ matrix.z3 }} | |
| run: | | |
| opam depext z3 | |
| opam install z3 | |
| - name: Build | |
| run: ./make.sh nat | |
| - name: Download Linux headers | |
| run: ./make.sh headers | |
| - name: Test | |
| run: opam exec -- dune runtest | |
| - name: Test marshal regression # not part of @runtest due to time | |
| run: ruby scripts/update_suite.rb -m | |
| lower-bounds-downgrade: | |
| # use external 0install solver to downgrade: https://github.com/ocaml-opam/opam-0install-solver | |
| # TODO: will be built in in opam 2.2: https://github.com/ocaml/opam/pull/4909 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: | |
| - ubuntu-latest | |
| - macos-13 | |
| ocaml-compiler: | |
| - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step | |
| name: lower-bounds (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}, downgrade) | |
| runs-on: ${{ matrix.os }} | |
| env: | |
| OPAMCONFIRMLEVEL: unsafe-yes # allow opam depext to yes package manager prompts | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| - name: Set up OCaml ${{ matrix.ocaml-compiler }} | |
| uses: ocaml/setup-ocaml@v2 | |
| with: | |
| ocaml-compiler: ${{ matrix.ocaml-compiler }} | |
| - name: Install graph-easy # TODO: remove if depext --with-test works | |
| if: ${{ matrix.os == 'ubuntu-latest' }} | |
| run: sudo apt install -y libgraph-easy-perl | |
| - name: Install dependencies | |
| run: opam install . --deps-only --with-test | |
| - name: Install Apron dependencies | |
| run: | | |
| opam depext apron | |
| opam install apron mlgmpidl.1.2.15 | |
| - name: Build | |
| if: ${{ false }} | |
| run: ./make.sh nat | |
| - name: Install opam-0install | |
| run: opam install opam-0install | |
| - name: Downgrade dependencies | |
| # must specify ocaml-base-compiler again to prevent it from being downgraded | |
| # prevent num downgrade to avoid dune/jbuilder error: https://github.com/ocaml/dune/issues/5280 | |
| run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.2+options ocaml-option-flambda num.1.5) | |
| - name: Build | |
| run: ./make.sh nat | |
| - name: Download Linux headers | |
| run: ./make.sh headers | |
| - name: Test | |
| run: opam exec -- dune runtest | |
| - name: Test marshal regression # not part of @runtest due to time | |
| run: ruby scripts/update_suite.rb -m | |
| lower-bounds-docker: | |
| # use builtin-0install solver to remove and downgrade, opam normally compiled without, Docker images have it compiled | |
| if: ${{ false }} | |
| name: lower-bounds (docker) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| - name: Set up Docker Buildx | |
| uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action | |
| - name: Build dev Docker image | |
| id: build | |
| uses: docker/build-push-action@v6 | |
| with: | |
| context: . | |
| target: dev | |
| load: true # load into docker instead of immediately pushing | |
| tags: dev | |
| cache-from: type=gha | |
| cache-to: type=gha,mode=max # max mode caches all layers for multi-stage image | |
| - name: Run opam downgrade and tests in dev Docker image | |
| uses: addnab/docker-run-action@v3 | |
| with: | |
| image: dev | |
| run: | | |
| OPAMCRITERIA=+removed,+count[version-lag,solution] OPAMEXTERNALSOLVER=builtin-0install opam-2.1 install . --deps-only --with-test --confirm-level=unsafe-yes | |
| opam exec -- dune runtest | |
| opam-install: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: | |
| - ubuntu-latest | |
| - macos-13 | |
| ocaml-compiler: | |
| - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| - name: Set up OCaml ${{ matrix.ocaml-compiler }} | |
| uses: ocaml/setup-ocaml@v3 | |
| with: | |
| ocaml-compiler: ${{ matrix.ocaml-compiler }} | |
| - name: Install graph-easy # TODO: remove if depext --with-test works | |
| if: ${{ matrix.os == 'ubuntu-latest' }} | |
| 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 depext apron | |
| opam install apron mlgmpidl.1.2.15 | |
| - name: Symlink installed goblint to repository # because tests want to use locally built one | |
| run: ln -s $(opam exec -- which goblint) goblint | |
| - name: Download Linux headers | |
| run: ./make.sh headers | |
| - name: Set gobopt with pre.kernel-root # because linux-headers are not installed | |
| run: echo "gobopt=--set pre.kernel-root $PWD/linux-headers" >> $GITHUB_ENV | |
| - name: Test regression | |
| run: ruby scripts/update_suite.rb -s | |
| - name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!) | |
| # if: ${{ matrix.apron }} | |
| run: | | |
| ruby scripts/update_suite.rb group apron -s | |
| ruby scripts/update_suite.rb group apron2 -s | |
| - name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!) | |
| run: ruby scripts/update_suite.rb group octagon -s | |
| - name: Test apron affeq regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!) | |
| run: ruby scripts/update_suite.rb group affeq -s | |
| - name: Test apron regression (Mukherjee et. al SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!) | |
| # if: ${{ matrix.apron }} | |
| run: ruby scripts/update_suite.rb group apron-mukherjee -s | |
| - name: Test marshal regression | |
| run: ruby scripts/update_suite.rb -m | |
| - name: Test incremental regression | |
| run: ruby scripts/update_suite.rb -i | |
| - name: Test incremental regression with cfg comparison | |
| run: ruby scripts/update_suite.rb -c |