Skip to content

Concretization

Concretization #1004

Workflow file for this run

name: What4 CI
on:
- push
- pull_request
# This CI configuration uses nix tooling to obtain the needed GHC and
# cabal-install packages, as well as the external dependencies
# (solvers, libz, libgmp, etc.). The cabal + cabal project files
# handle Haskell-level dependencies within the nix shell used for the
# build.
#
# Variable aspects of this CI configuration:
#
# * GHC versions
# - specified in the strategy matrix
# - provided via nix: ensure the nix base and NIXPKGS used provide the requested GHC version
# * nix tool version 2.11.0
# - all nix operations use new tool suite and cmdline interface (available in 2.4+) instead of older format
# The CACHE_VERSION can be updated to force the use of a new cache if
# the current cache contents become corrupted/invalid. This can
# sometimes happen when (for example) the OS version is changed but
# older .so files are cached, which can have various effects
# (e.g. cabal complains it can't find a valid version of the "happy"
# tool).
env:
CACHE_VERSION: 3
jobs:
genmatrix:
runs-on: ubuntu-latest
outputs:
matrix: ${{ steps.gen-matrix.outputs.matrix }}
steps:
- uses: actions/checkout@v2
with:
submodules: true
- name: Install Nix
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixos-21.11
install_url: https://releases.nixos.org/nix/nix-2.11.0/install
extra_nix_config: |
access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
- uses: cachix/cachix-action@v10
with:
name: galois
authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
- id: gen-matrix
run: |
echo ::set-output name=matrix::$(nix run nixpkgs#swiProlog -- .github/workflows/gen_matrix.pl)
linux:
name: GHC-${{ matrix.ghc }} Z3-${{ matrix.z3 }} Yices-${{ matrix.yices }} CVC4-${{ matrix.cvc4 }} CVC5-${{ matrix.cvc5 }} STP-${{ matrix.stp }} Bitwuzla-${{ matrix.bitwuzla }} Boolector-${{ matrix.boolector }} ABC-${{ matrix.abc }} ${{ matrix.os }}
runs-on: ${{ matrix.os }}
needs: genmatrix
continue-on-error: false
env:
CI_TEST_LEVEL: "1"
strategy:
matrix: ${{fromJSON(needs.genmatrix.outputs.matrix)}}
fail-fast: false
steps:
- uses: actions/checkout@v2
with:
submodules: true
- name: Install Nix
uses: cachix/install-nix-action@v16
with:
nix_path: nixpkgs=channel:nixos-21.11
install_url: https://releases.nixos.org/nix/nix-2.11.0/install
extra_nix_config: |
access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
- uses: cachix/cachix-action@v10
with:
name: galois
authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
- uses: actions/cache/restore@v3
name: Restore cabal store cache
with:
path: |
${{ steps.setup-haskell.outputs.cabal-store }}
~/.cabal/packages
~/.cabal/store
dist-newstyle
key: |
${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-ghc${{ matrix.ghc }}-${{ github.ref }}
restore-keys: |
${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-ghc${{ matrix.ghc }}-
- name: Setup Environment Vars
# Setup a nix shell environment command that will supply the
# appropriate GHC version as well as dependent libraries (and
# includes for zlib) as well as the cabal-install tool.
run: |
GHC=haskell.compiler.ghc$(echo ${{ matrix.ghc }} | sed -e s,\\.,,g)
case ${{ matrix.ghc }} in
8.6.5) GHC_NIXPKGS=github:nixos/nixpkgs/20.09 ;;
9.0.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-22.05 ;;
9.2.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-22.05 ;;
9.4.4) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.05 ;;
9.6.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.05 ;;
9.8.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.11 ;;
*) GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;;
esac
echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV
- name: Cabal update
shell: bash
run: $NS -c cabal update
- name: Package's Cabal/GHC compatibility
shell: bash
# Using setup will use the cabal library installed with GHC
# instead of the cabal library of the Cabal-install tool to
# verify the cabal file is compatible with the associated
# GHC cabal library version. Cannot run configure or build,
# because dependencies aren't present, but a clean is
# sufficient to cause parsing/validation of the cabal file.
run: |
defsetup() { echo import Distribution.Simple; echo main = defaultMain; }
setup_src() { if [ ! -f Setup.hs ] ; then defsetup > DefSetup.hs; fi; ls *Setup.hs; }
setup_bin() { echo setup.${{ matrix.ghc }}; }
with_ghc() { $NS -c ${@}; }
(cd what4; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
(cd what4-abc; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
(cd what4-blt; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
- name: Cabal check
shell: bash
run: |
(cd what4; $NS -c cabal check)
(cd what4-abc; $NS -c cabal check)
(cd what4-blt; $NS -c cabal check)
- name: Cabal configure what4
shell: bash
# Note: the extra-lib-dirs and extra-include-dirs specified on
# the command-line are placed at the top-level of the
# generated cabal.project.local, but only apply to the primary
# package. The zlib dependency also needs these flags, so the
# following adds a zlib package-specific stanza for these.
run: |
cd what4
$NS -c cabal configure --enable-tests -fdRealTestDisable -fsolverTests --extra-lib-dirs=$(nix eval --raw nixpkgs#zlib)/lib --extra-include-dirs=$(nix eval --raw nixpkgs#zlib.dev)/include
echo "" >> ../cabal.project.local
echo package zlib >> ../cabal.project.local
echo " extra-lib-dirs: $(nix eval --raw nixpkgs#zlib)/lib" >> ../cabal.project.local
echo " extra-include-dirs: $(nix eval --raw nixpkgs#zlib.dev)/include" >> ../cabal.project.local
cp ../cabal.project.local ./
- name: Build
shell: bash
run: |
cd what4
$NS -c cabal build
- name: Test
shell: bash
run: |
cd what4
echo ABC version $(nix eval github:GaloisInc/flakes#abc.v${{ matrix.abc }}.version)
echo Bitwuzla version $(nix run github:GaloisInc/flakes#bitwuzla.v${{ matrix.bitwuzla }} -- --version | head -n1)
echo Boolector version $(nix run github:GaloisInc/flakes#boolector.v${{ matrix.boolector }} -- --version | head -n1)
echo CVC4 version $(nix run github:GaloisInc/flakes#cvc4.v${{ matrix.cvc4 }} -- --version | head -n1)
echo CVC5 version $(nix run github:GaloisInc/flakes#cvc5.v${{ matrix.cvc5 }} -- --version | head -n1)
echo STP version $(nix run github:GaloisInc/flakes#stp.v${{ matrix.stp }} -- --version | head -n1)
echo Yices version $(nix run github:GaloisInc/flakes#yices.v${{ matrix.yices }} -- --version | head -n1)
echo Z3 version $(nix run github:GaloisInc/flakes#z3.v${{ matrix.z3 }} -- --version | head -n1)
$NS \
github:GaloisInc/flakes#abc.v${{ matrix.abc }} \
github:GaloisInc/flakes#bitwuzla.v${{ matrix.bitwuzla }} \
github:GaloisInc/flakes#boolector.v${{ matrix.boolector }} \
github:GaloisInc/flakes#cvc4.v${{ matrix.cvc4 }} \
github:GaloisInc/flakes#cvc5.v${{ matrix.cvc5 }} \
github:GaloisInc/flakes#stp.v${{ matrix.stp }} \
github:GaloisInc/flakes#yices.v${{ matrix.yices }} \
github:GaloisInc/flakes#z3.v${{ matrix.z3 }} \
-c cabal test
- name: Documentation
shell: bash
run: |
cd what4
$NS -c cabal haddock what4
- uses: actions/cache/save@v3
name: Save cabal store cache
if: always()
with:
path: |
${{ steps.setup-haskell.outputs.cabal-store }}
~/.cabal/packages
~/.cabal/store
dist-newstyle
key: |
${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-ghc${{ matrix.ghc }}-${{ github.ref }}