unlocked #1600
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-latest | |
| ocaml-compiler: | |
| - 5.0.x | |
| - ocaml-variants.4.14.0+options,ocaml-option-flambda | |
| - 4.14.x | |
| - 4.13.x | |
| - 4.12.x | |
| - 4.10.x | |
| apron: | |
| - false | |
| - true | |
| z3: | |
| - false | |
| include: | |
| - os: ubuntu-latest | |
| ocaml-compiler: 4.14.x | |
| z3: true | |
| - os: ubuntu-latest | |
| ocaml-compiler: 5.0.0 | |
| apron: false | |
| # 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@v2 | |
| with: | |
| ocaml-compiler: ${{ matrix.ocaml-compiler }} | |
| - name: Install dependencies | |
| run: opam install . --deps-only --with-test | |
| - name: Install Apron dependencies | |
| if: ${{ matrix.apron }} | |
| run: | | |
| opam depext apron | |
| opam install apron | |
| - name: Install Z3 dependencies | |
| if: ${{ matrix.z3 }} | |
| run: | | |
| opam depext z3 | |
| opam install z3 | |
| - name: Build | |
| run: ./make.sh nat | |
| - name: Test regression | |
| run: ./make.sh headers testci | |
| - 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!) | |
| if: ${{ matrix.apron }} | |
| 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!) | |
| if: ${{ matrix.apron }} | |
| 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 apron termination 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 termination -s | |
| - name: Test regression cram | |
| run: opam exec -- dune runtest tests/regression | |
| - name: Test incremental cram | |
| run: opam exec -- dune runtest tests/incremental | |
| - name: Test unit | |
| run: opam exec -- dune runtest unittest | |
| - 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 | |
| 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-latest | |
| ocaml-compiler: | |
| - ocaml-variants.4.14.0+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 dependencies | |
| run: opam install . --deps-only --with-test | |
| - name: Install Apron dependencies | |
| run: | | |
| opam depext apron | |
| opam install apron | |
| - 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 | |
| run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda) | |
| - name: Build | |
| run: ./make.sh nat | |
| - name: Test regression | |
| run: ./make.sh headers testci | |
| - 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 regression cram | |
| run: opam exec -- dune runtest tests/regression | |
| - name: Test incremental cram | |
| run: opam exec -- dune runtest tests/incremental | |
| - name: Test unit | |
| run: opam exec -- dune runtest unittest | |
| - 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 | |
| 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@v5 | |
| 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-latest | |
| ocaml-compiler: | |
| - ocaml-variants.4.14.0+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@v2 | |
| with: | |
| ocaml-compiler: ${{ matrix.ocaml-compiler }} | |
| - name: Install Goblint with test | |
| run: opam install goblint --with-test | |
| - name: Install Apron dependencies | |
| run: | | |
| opam depext apron | |
| opam install apron | |
| - name: Symlink installed goblint to repository # because tests want to use locally built one | |
| run: ln -s $(opam exec -- which goblint) goblint | |
| - 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: ./make.sh headers testci | |
| - 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 |