Skip to content

Add boundary proofs to dfold and smap #3258

Add boundary proofs to dfold and smap

Add boundary proofs to dfold and smap #3258

Workflow file for this run

name: CI
on:
push:
branches:
# PRs can only use caches from their target branch. We therefore need to
# make sure we run on 'master' too.
- master
pull_request:
concurrency:
group: ${{ github.head_ref || github.run_id }}
cancel-in-progress: true
jobs:
build_mac_windows:
name: Build and run limited tests
runs-on: ${{ matrix.os }}
strategy:
fail-fast: false
matrix:
os: ["macOS-13", "windows-latest"]
ghc: ["8.10", "9.0", "9.2", "9.4", "9.6", "9.8"]
exclude:
# Some tests fail with a mysterious -11 error code.
- os: macOS-13
ghc: 8.10
# GHC 9.0 fails to compile clash-cores due to a template haskell
# failure
- os: windows-latest
ghc: 9.0
# GHC/Clash starts extremely slowly, see
# https://github.com/clash-lang/clash-compiler/issues/2684
- os: windows-latest
ghc: 9.6
steps:
- uses: actions/checkout@v4
- uses: haskell-actions/setup@v2
id: setup-haskell
with:
enable-stack: true
stack-no-global: true
- name: Install IVerilog (macOS)
if: ${{ startsWith(matrix.os, 'macOS') }}
run: brew install icarus-verilog
- name: Install IVerilog (Windows)
if: ${{ startsWith(matrix.os, 'windows') }}
run: choco install --no-progress iverilog
- name: General Setup
shell: bash
run: |
cp .ci/stack-${{ matrix.ghc }}.yaml stack.yaml
# Print out stack.yaml for debugging purposes
cat stack.yaml
- name: Restore cache (Windows)
if: ${{ startsWith(matrix.os, 'windows') }}
uses: actions/cache/restore@v4
id: cache-win
with:
# On windows we have to use "\" as a path separator, otherwise caching fails
path: |
${{ steps.setup-haskell.outputs.stack-root }}\snapshots
key: ${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles('stack.yaml', '**/*.cabal', '.github/workflows/ci.yml') }}
restore-keys: ${{ matrix.os }}-${{ matrix.ghc }}-
- name: Restore cache (non-Windows)
if: ${{ !startsWith(matrix.os, 'windows') }}
uses: actions/cache/restore@v4
id: cache-other
with:
path: |
${{ steps.setup-haskell.outputs.stack-root }}/snapshots
key: ${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles('stack.yaml', '**/*.cabal', '.github/workflows/ci.yml') }}
restore-keys: ${{ matrix.os }}-${{ matrix.ghc }}-
# https://gitlab.haskell.org/haskell/ghcup-hs/-/issues/188
# https://github.com/commercialhaskell/stack/issues/4937
# - name: Use system GHC
# run: stack config set system-ghc --global true
# Retry Stack initialization, see:
# https://github.com/commercialhaskell/stack/issues/5770
- name: Initialize Stack
shell: bash
run: ./.ci/retry.sh stack build base
# Building 'happy' sometimes fails on Windows for some obscure reason
- name: Build happy with Stack
shell: bash
run: ./.ci/retry.sh stack build happy
- name: Build dependencies
run: stack build --only-dependencies
- name: Save cache (Windows)
uses: actions/cache/save@v4
# Trying to save over an existing cache gives distracting
# "Warning: Cache save failed." since they are immutable
if: ${{ startsWith(matrix.os, 'windows') && steps.cache-win.outputs.cache-hit != 'true' }}
with:
# On windows we have to use "\" as a path separator, otherwise caching fails
path: |
${{ steps.setup-haskell.outputs.stack-root }}\snapshots
key: ${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles('stack.yaml', '**/*.cabal', '.github/workflows/ci.yml') }}
- name: Save cache (non-Windows)
uses: actions/cache/save@v4
# Trying to save over an existing cache gives distracting
# "Warning: Cache save failed." since they are immutable
if: ${{ !startsWith(matrix.os, 'windows') && steps.cache-other.outputs.cache-hit != 'true' }}
with:
path: |
${{ steps.setup-haskell.outputs.stack-root }}/snapshots
key: ${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles('stack.yaml', '**/*.cabal', '.github/workflows/ci.yml') }}
# Note: the --pedantic switch adds -Wall -Werror to the options passed to
# GHC. Options specified in stack.yaml (like -Wcompat) are still passed;
# it is cumulative. Future versions of Stack might add behavior to
# --pedantic.
- name: Build with Stack
run: stack build --pedantic
- name: Run Vector testsuite
if: github.ref != 'refs/heads/master'
run: stack run -- clash-testsuite --hide-successes -p .Vector. --no-ghdl --no-verilator --no-modelsim --no-vivado
build_and_test:
# Only run for external PRs
if: github.event.pull_request.head.repo.full_name != github.repository
runs-on: ubuntu-latest
name: Build and Test
strategy:
fail-fast: false
matrix:
ghc: [ "8.10.7", "9.0.2", "9.6.4" ]
include:
- multiple_hidden: yes
- ghc: 8.10.7
multiple_hidden: no
workaround_ghc_mmap_crash: yes
- ghc: 9.0.2
workaround_ghc_mmap_crash: yes
# Run steps inside the clash CI docker image
container:
image: ghcr.io/clash-lang/clash-ci:${{ matrix.ghc }}-20240721
env:
THREADS: 2
CABAL_JOBS: 2
CI_COMMIT_BRANCH: ${{ github.base_ref }}
WORKAROUND_GHC_MMAP_CRASH: ${{ matrix.workaround_ghc_mmap_crash }}
steps:
- name: Checkout
uses: actions/checkout@v4
with:
submodules: true
ref: ${{ github.event.pull_request.head.ref }}
repository: ${{ github.event.pull_request.head.repo.full_name }}
- name: Setup CI
run: |
# Work around dubious owner error
git config --global --add safe.directory "$(pwd)"
export CABAL_DIR=$HOME/.cabal
./.ci/setup.sh
cabal v2-freeze
# We only want this for caching, and it makes the CI scripts way
# more brittle than is ideal.
mv cabal.project.freeze frozen
- name: Restore Cache
uses: actions/cache/restore@v4
id: cache
with:
path: |
dist-newstyle
~/.cabal/store
key: ${{ matrix.ghc }}-${{ hashFiles('frozen', 'cabal.project', '**/*.cabal', '.github/workflows/ci.yml') }}
restore-keys: ${{ matrix.ghc }}-
- name: Build Clash
run: |
export CABAL_DIR=$HOME/.cabal
./.ci/build.sh
- name: Save Cache
# Trying to save over an existing cache gives distracting
# "Warning: Cache save failed." since they are immutable
if: ${{ !cancelled() && steps.cache.outputs.cache-hit != 'true' }}
uses: actions/cache/save@v4
with:
path: |
dist-newstyle
~/.cabal/store
key: ${{ matrix.ghc }}-${{ hashFiles('frozen', 'cabal.project', '**/*.cabal', '.github/workflows/ci.yml') }}
- name: Unit Tests
if: github.ref != 'refs/heads/master'
run: |
export CABAL_DIR=$HOME/.cabal
cabal v2-run clash-prelude:doctests
cabal v2-run clash-prelude:unittests -- --hide-successes
cabal v2-run clash-lib:doctests
cabal v2-run clash-lib:unittests -- --hide-successes
cabal v2-run clash-cores:doctests
cabal v2-run clash-cores:unittests -- --hide-successes
cabal v2-run clash-cosim:test -- --hide-successes
- name: Testsuite (VHDL)
if: github.ref != 'refs/heads/master'
run: |
export CABAL_DIR=$HOME/.cabal
cabal v2-run clash-testsuite -- -j$THREADS --hide-successes -p .VHDL --no-vivado
- name: Testsuite (Verilog)
if: github.ref != 'refs/heads/master'
run: |
export CABAL_DIR=$HOME/.cabal
cabal v2-run clash-testsuite -- -j$THREADS --hide-successes -p .Verilog --no-vivado
- name: Testsuite (SystemVerilog)
if: github.ref != 'refs/heads/master'
run: |
export CABAL_DIR=$HOME/.cabal
cabal v2-run clash-testsuite -- -j$THREADS --hide-successes -p .SystemVerilog --no-modelsim --no-vivado
all:
name: All jobs finished
if: ${{ !cancelled() }}
needs: [
build_mac_windows,
build_and_test,
]
runs-on: ubuntu-22.04
steps:
- name: Checkout
uses: actions/checkout@v4
- name: Check dependencies for failures
run: |
# Test all dependencies for success/failure
set -x
success="${{ contains(needs.*.result, 'success') }}"
fail="${{ contains(needs.*.result, 'failure') }}"
set +x
# Test whether success/fail variables contain sane values
if [[ "${success}" != "true" && "${success}" != "false" ]]; then exit 1; fi
if [[ "${fail}" != "true" && "${fail}" != "false" ]]; then exit 1; fi
# We want to fail if one or more dependencies fail. For safety, we introduce
# a second check: if no dependencies succeeded something weird is going on.
if [[ "${fail}" == "true" || "${success}" == "false" ]]; then
echo "One or more dependency failed, or no dependency succeeded."
exit 1
fi
- name: Install dependencies
run: |
sudo apt-get update
sudo apt-get -y install python3-yaml
- name: Check that the 'all' job depends on all other jobs
run: |
.ci/all_check.py