Unify Coq CI into a single .yml file #637
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: CI (Coq) | ||
| on: | ||
| push: | ||
| branches: [ master , sp2019latest , v8.6 , v8.8 , v8.10 ] | ||
| pull_request: | ||
| merge_group: | ||
| workflow_dispatch: | ||
| release: | ||
| types: [published] | ||
| schedule: | ||
| - cron: '0 0 1 * *' | ||
| jobs: | ||
| build: | ||
| strategy: | ||
| fail-fast: false | ||
| matrix: | ||
| include: | ||
| - name: 'docker-master' | ||
| container: {name: 'coqorg/coq', image: 'coqorg/coq:dev'} | ||
| env: { ALLOW_DIFF: "1" } | ||
| make: 'etc/ci/github-actions-make.sh --warnings' | ||
| raw-make: 'make' | ||
| sudo-make: 'sudo make' | ||
| coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"' | ||
| os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'} | ||
| - name: 'alpine-edge' | ||
| container: {name: 'alpine', image: 'alpine:edge'} | ||
| env: { CAMLEXTRAFLAGS="-ccopt -static" } | ||
| make: 'etc/ci/github-actions-make.sh' | ||
| raw-make: 'make' | ||
| sudo-make: 'sudo make' | ||
| coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"' | ||
| os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'} | ||
| - name: 'archlinux' | ||
| container: {name: 'archlinux', image: 'archlinux'} | ||
| make: 'etc/ci/github-actions-make.sh' | ||
| raw-make: 'make' | ||
| sudo-make: 'sudo make' | ||
| coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"' | ||
| os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'} | ||
| - name: 'debian-sid' | ||
| container: {name: 'debian', image: 'debian:sid'} | ||
| make: 'etc/ci/github-actions-make.sh' | ||
| raw-make: 'make' | ||
| sudo-make: 'sudo make' | ||
| coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"' | ||
| os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'} | ||
| - name: 'windows' | ||
| coq-version: '8.17.0' # minimal major version required for bedrock2 components | ||
| os: {name: 'Windows', runs-on: 'windows-latest'} | ||
| env: { COQEXTRAFLAGS: "-async-proofs-j 1", COQCHKEXTRAFLAGS: "", OPAMYES: "true", OPAMCONFIRMLEVEL: "unsafe-yes" } | ||
| extra-ocaml-repositories: 'opam-repository-mingw: https://github.com/ocaml-opam/opam-repository-mingw.git#sunset' | ||
| make: 'opam exec -- etc/ci/github-actions-make.sh' | ||
| raw-make: 'opam exec -- make' | ||
| sudo-make: 'opam exec -- make' | ||
| container: {name: '', image: '', ocaml-compiler: '4.11.1'} | ||
| - name: 'macos' | ||
| coq-version: '8.18.0' # pick a version not tested on other platforms | ||
| os: {name: 'macOS', runs-on: 'macos-latest'} | ||
| env: { COQCHKEXTRAFLAGS: "", SKIP_BEDROCK2: "0", OPAMYES: "true", OPAMCONFIRMLEVEL: "unsafe-yes" } | ||
| make: 'etc/ci/github-actions-make.sh' | ||
| raw-make: 'make' | ||
| sudo-make: 'make' | ||
| container: {name: '', image: '', ocaml-compiler: '4.11.1'} | ||
| runs-on: ${{ matrix.os.runs-on }} | ||
| env: ${{ matrix.env }} | ||
| name: ${{ matrix.name }} | ||
| container: ${{ matrix.container.image }} | ||
| concurrency: | ||
| group: ${{ github.workflow }}-${{ matrix.name }}-${{ matrix.os }}-${{ github.head_ref || github.run_id }} | ||
| cancel-in-progress: true | ||
| steps: | ||
| - run: echo ::add-matcher::.github/make.json | ||
| - name: Install System Dependencies (Alpine) | ||
| run: apk add git make jq gcc musl-dev python3 ocaml ocaml-findlib ghc cabal coq ocaml-zarith bash sudo | ||
| if: matrix.container.name == 'alpine' | ||
| - name: Install System Dependencies (Debian) | ||
| run: | | ||
| apt-get -o Acquire::Retries=30 update -y | ||
| apt-get -q -y --allow-unauthenticated -o Acquire::Retries=30 install sudo git make time jq python3 python-is-python3 ocaml coq libcoq-core-ocaml-dev libfindlib-ocaml-dev ocaml-findlib cabal-install js-of-ocaml | ||
| if: matrix.container.name == 'debian' | ||
| - name: Install System Dependencies (Arch Linux) | ||
| run: | | ||
| pacman --noconfirm -Syu base-devel git make python3 which jq ghc ghc-static time diffutils coq ocaml-zarith --needed | ||
| if: matrix.container.name == 'archlinux' | ||
| - uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
| - name: Set up OCaml | ||
| uses: ocaml/setup-ocaml@v2 | ||
| with: | ||
| ocaml-compiler: ${{ matrix.container.ocaml-compiler }} | ||
| opam-repositories: |- | ||
| ${{ matrix.os.extra-ocaml-repositories }} | ||
| default: https://github.com/ocaml/opam-repository.git | ||
| if: matrix.container.name == '' | ||
| - run: eval $(opam env) | ||
| if: matrix.container.name == '' || matrix.container.name == 'coqorg/coq' | ||
| - run: opam update | ||
| if: matrix.container.name == '' | ||
| - run: opam depext coq.${{ matrix.coq-version }} | ||
| if: matrix.container.name == '' | ||
| - run: opam pin add --kind=version coq ${{ matrix.coq-version }} | ||
| if: matrix.container.name == '' | ||
| - run: opam install js_of_ocaml | ||
| if: matrix.container.name == '' || matrix.container.name == 'coqorg/coq' | ||
| - name: Install System Dependencies (Windows) | ||
| run: | | ||
| %CYGWIN_ROOT%\setup-x86_64.exe -qnNdO -P time,zip | ||
| shell: cmd | ||
| if: matrix.os.name == 'Windows' | ||
| - name: Install System Dependencies (coqorg/coq) | ||
| run: | | ||
| sudo apt-get -o Acquire::Retries=30 update -y | ||
| sudo apt-get -o Acquire::Retries=30 install -y --allow-unauthenticated python python3 bsdmainutils | ||
| if: matrix.container.name == 'coqorg/coq' | ||
| - name: Install system dependencies (MacOS) | ||
| run: | | ||
| set -e | ||
| brew install gnu-time coreutils | ||
| if: matrix.os.name == 'macOS' | ||
| - name: Work around https://github.com/actions/checkout/issues/766 (Windows) | ||
| run: %CYGWIN_ROOT%\bin\bash.exe -l -c 'git config --global --add safe.directory "*"' | ||
| shell: cmd | ||
| if: matrix.os.name == 'Windows' | ||
| - name: Work around https://github.com/actions/checkout/issues/766 (Linux) | ||
| run: git config --global --add safe.directory "*" | ||
| if: matrix.container.name != '' | ||
| - name: Update permissions (coqorg/coq) | ||
| run: sudo chmod -R a=u . | ||
| if: matrix.container.name == 'coqorg/coq' | ||
| - name: work around coq issue 15663 (Alpine & Arch Linux) | ||
| run: | | ||
| ln -s /usr/lib/coq /usr/lib/ocaml/coq | ||
| ln -s /usr/lib/coq-core /usr/lib/ocaml/coq-core | ||
| ln -s /usr/lib/coqide-server /usr/lib/ocaml/coqide-server | ||
| if: matrix.container.name == 'alpine' || matrix.container.name == 'archlinux' | ||
| - name: echo build params (Linux) | ||
| run: etc/ci/describe-system-config.sh | ||
| if: matrix.os.name == 'Ubuntu' | ||
| - name: echo build params (Windows) | ||
| run: %cd%\etc\ci\describe-system-config-win.bat | ||
| shell: cmd | ||
| if: matrix.os.name == 'Windows' | ||
| - name: echo build params (MacOS) | ||
| run: | | ||
| eval $(opam env) | ||
| etc/ci/describe-system-config-macos.sh | ||
| if: matrix.os.name == 'macOS' | ||
| - name: deps | ||
| run: ${{ matrix.make }} -j2 ${{ matrix.coqbin-arg }} deps | ||
| - name: all-except-generated-and-js-of-ocaml | ||
| run: ${{ matrix.make }} -j2 all-except-generated-and-js-of-ocaml | ||
| - name: pre-standalone-extracted | ||
| run: ${{ matrix.make }} -j2 pre-standalone-extracted | ||
| - name: upload OCaml files | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: ExtractionOCaml-${{ matrix.name }} | ||
| path: src/ExtractionOCaml | ||
| if: always () | ||
| - name: upload js_of_ocaml source files | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: ExtractionJsOfOCaml-source-${{ matrix.name }} | ||
| path: src/ExtractionJsOfOCaml | ||
| if: always () | ||
| - name: upload Haskell source files | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: ExtractionHaskell-source-${{ matrix.name }} | ||
| path: src/ExtractionHaskell | ||
| if: always () | ||
| - name: install-standalone-unified-ocaml | ||
| run: ${{ matrix.raw-make }} -f Makefile.standalone install-standalone-unified-ocaml BINDIR=dist | ||
| - name: upload standalone files | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: standalone-${{ matrix.name }} | ||
| path: dist/fiat_crypto | ||
| - run: git config --file .gitmodules --get-regexp path | awk '{ print $2 }' | xargs tar -czvf fiat-crypto-build.tar.gz src | ||
| if: matrix.os.name != 'Windows' | ||
| - name: Upload built files | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: build-outputs-${{ matrix.name }} | ||
| path: fiat-crypto-build.tar.gz | ||
| if: matrix.os.name != 'Windows' | ||
| - name: install | ||
| run: ${{ matrix.sudo-make }} ${{ matrix.coqbin-arg }} EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml | ||
| - name: install-without-bedrock2 | ||
| run: ${{ matrix.sudo-make }} ${{ matrix.coqbin-arg }} EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml | ||
| - name: install-dev | ||
| run: ${{ matrix.sudo-make }} ${{ matrix.coqbin-arg }} EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml | ||
| - name: display timing info | ||
| run: cat time-of-build-pretty.log | ||
| if: matrix.os.name != 'Windows' | ||
| - name: display timing info | ||
| run: type time-of-build-pretty.log | ||
| shell: cmd | ||
| if: matrix.os.name == 'Windows' | ||
| - name: display per-line timing info | ||
| run: etc/ci/github-actions-display-per-line-timing.sh | ||
| if: matrix.os.name != 'Windows' | ||
| - name: display per-line timing info | ||
| run: opam exec -- etc/ci/github-actions-display-per-line-timing.sh | ||
| if: matrix.os.name == 'Windows' | ||
| validate: | ||
| runs-on: ubuntu-latest | ||
| env: { COQCHKEXTRAFLAGS: "-bytecode-compiler yes" , ALLOW_DIFF: "1" } | ||
| name: validate-docker-master | ||
| container: 'coqorg/coq:dev' | ||
| concurrency: | ||
| group: ${{ github.workflow }}-validate-docker-master-${{ github.head_ref || github.run_id }} | ||
| cancel-in-progress: true | ||
| needs: build | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
| - name: Download a Build Artifact | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: build-outputs-docker-master | ||
| path: . | ||
| - name: Unpack build artifact | ||
| run: tar --overwrite -xzvf fiat-crypto-build.tar.gz | ||
| - name: validate | ||
| run: etc/ci/github-actions-docker-make.sh --warnings TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}" | ||
| if: github.event_name != 'pull_request' | ||
| build-js-of-ocaml: | ||
| needs: build | ||
| runs-on: ubuntu-latest | ||
| strategy: | ||
| fail-fast: false | ||
| matrix: | ||
| coq-version: [ 'docker-master' ] | ||
| ocaml-compiler: [ '4.11.1' ] | ||
| concurrency: | ||
| group: ${{ github.workflow }}-build-js-of-ocaml-${{ matrix.coq-version }}-${{ matrix.ocaml-compiler }}-${{ github.head_ref || github.run_id }} | ||
| cancel-in-progress: true | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
| - name: Set up OCaml | ||
| uses: ocaml/setup-ocaml@v2 | ||
| with: | ||
| ocaml-compiler: ${{ matrix.ocaml-compiler }} | ||
| - name: opam install deps | ||
| run: | | ||
| eval $(opam env) | ||
| opam update -y | ||
| opam install -y js_of_ocaml ocamlfind | ||
| - name: echo build params | ||
| run: etc/ci/describe-system-config.sh | ||
| - name: Download a Build Artifact | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: ExtractionJsOfOCaml-source-${{ matrix.coq-version }} | ||
| path: src/ExtractionJsOfOCaml | ||
| - name: standalone-js-of-ocaml | ||
| run: | | ||
| eval $(opam env) | ||
| etc/ci/github-actions-make.sh --warnings -f Makefile.standalone -j2 standalone-js-of-ocaml | ||
| - name: install-standalone-js-of-ocaml | ||
| run: make -f Makefile.standalone install-standalone-js-of-ocaml | ||
| - name: upload js_of_ocaml build files | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: ExtractionJsOfOCaml-${{ matrix.coq-version }}-ocaml-${{ matrix.ocaml-compiler }} | ||
| path: src/ExtractionJsOfOCaml | ||
| if: always () | ||
| - name: Upload js_of_ocaml outputs | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: fiat-html-js-of-ocaml | ||
| path: fiat-html | ||
| build-wasm-of-ocaml: | ||
| needs: build | ||
| runs-on: ubuntu-latest | ||
| strategy: | ||
| fail-fast: false | ||
| matrix: | ||
| coq-version: [ 'docker-master' ] | ||
| ocaml-compiler: [ '4.14.1' ] | ||
| concurrency: | ||
| group: ${{ github.workflow }}-build-wasm-of-ocaml-${{ matrix.coq-version }}-${{ matrix.ocaml-compiler }}-${{ github.head_ref || github.run_id }} | ||
| cancel-in-progress: true | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
| - name: Set up OCaml | ||
| uses: ocaml/setup-ocaml@v2 | ||
| with: | ||
| ocaml-compiler: ${{ matrix.ocaml-compiler }} | ||
| - name: echo build params | ||
| run: etc/ci/describe-system-config.sh | ||
| - name: Set up binaryen >= 116 | ||
| uses: acifani/setup-tinygo@v2 | ||
| with: | ||
| tinygo-version: '0.30.0' | ||
| binaryen-version: '116' | ||
| - name: set up custom dune and wasm_of_ocaml | ||
| run: | | ||
| eval $(opam env) | ||
| opam update -y | ||
| opam pin add -y 'https://github.com/ocaml-wasm/dune.git#wasm' | ||
| opam pin add -y --no-action --cli=2.1 --with-version 5.3.0 https://github.com/ocaml-wasm/wasm_of_ocaml.git | ||
| - name: install wasm_of_ocaml | ||
| run: | | ||
| eval $(opam env) | ||
| opam install -y wasm_of_ocaml-compiler ocamlfind | ||
| - name: echo build params | ||
| run: etc/ci/describe-system-config.sh | ||
| - name: Download a Build Artifact | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: ExtractionJsOfOCaml-source-${{ matrix.coq-version }} | ||
| path: src/ExtractionJsOfOCaml | ||
| - name: standalone-wasm-of-ocaml | ||
| run: | | ||
| eval $(opam env) | ||
| etc/ci/github-actions-make.sh --warnings -f Makefile.standalone -j2 standalone-wasm-of-ocaml | ||
| - name: install-standalone-wasm-of-ocaml | ||
| run: make -f Makefile.standalone install-standalone-wasm-of-ocaml | ||
| - name: upload wasm_of_ocaml build files | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: ExtractionJsOfOCaml-${{ matrix.coq-version }}-ocaml-${{ matrix.ocaml-compiler }}+wasm | ||
| path: src/ExtractionJsOfOCaml | ||
| if: always () | ||
| - name: Upload wasm_of_ocaml outputs | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: fiat-html-wasm-of-ocaml | ||
| path: fiat-html | ||
| deploy-js-wasm-of-ocaml: | ||
| needs: [build-js-of-ocaml, build-wasm-of-ocaml] | ||
| runs-on: ubuntu-latest | ||
| concurrency: | ||
| group: ${{ github.workflow }}-deploy-js-wasm-of-ocaml-${{ github.head_ref || github.run_id }} | ||
| cancel-in-progress: true | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
| fetch-depth: 0 # Fetch all history for all tags and branches, for fiat-html/version.js | ||
| tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version | ||
| - name: Download a Build Artifact | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: fiat-html-js-of-ocaml | ||
| path: fiat-html | ||
| - run: find fiat-html | ||
| - run: ls -la fiat-html | ||
| - name: Download a Build Artifact | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: fiat-html-wasm-of-ocaml | ||
| path: fiat-html | ||
| - run: find fiat-html | ||
| - run: ls -la fiat-html | ||
| - run: make -f Makefile.js-html fiat-html/version.js | ||
| - run: find fiat-html | ||
| - run: ls -la fiat-html | ||
| - name: backup .gitignore | ||
| run: mv .gitignore{,.bak} | ||
| - name: Deploy js_of_ocaml and wasm_of_ocaml 🚀 ${{ ( github.ref != 'refs/heads/master' && '(dry run)' ) || '' }} | ||
| uses: JamesIves/github-pages-deploy-action@v4.5.0 | ||
| with: | ||
| branch: gh-pages # The branch the action should deploy to. | ||
| folder: fiat-html # The folder the action should deploy. | ||
| git-config-email: actions@users.noreply.github.com | ||
| target-folder: . | ||
| single-commit: true # otherwise the repo will get too big | ||
| dry-run: ${{ github.ref != 'refs/heads/master' }} | ||
| - name: restore .gitignore | ||
| run: mv .gitignore{.bak,} | ||
| generated-files: | ||
| needs: build | ||
| runs-on: ubuntu-latest | ||
| strategy: | ||
| fail-fast: false | ||
| matrix: | ||
| coq-version: [ 'docker-master' ] | ||
| concurrency: | ||
| group: ${{ github.workflow }}-generated-files-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }} | ||
| cancel-in-progress: true | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
| - name: Download a Build Artifact | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: ExtractionOCaml-${{ matrix.coq-version }} | ||
| path: src/ExtractionOCaml | ||
| - name: make binaries executable | ||
| run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x | ||
| - name: touch binaries to prevent rebuilding | ||
| run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs touch | ||
| - name: generated-files | ||
| run: etc/ci/github-actions-make.sh --warnings -f Makefile.examples -j2 generated-files | ||
| if: github.event_name == 'pull_request' | ||
| - run: tar -czvf generated-files.tgz fiat-*/ | ||
| if: ${{ failure() }} | ||
| - name: upload generated files | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: generated-files-${{ matrix.coq-version }} | ||
| path: generated-files.tgz | ||
| if: ${{ failure() }} | ||
| standalone-haskell: | ||
| needs: build | ||
| runs-on: ubuntu-latest | ||
| strategy: | ||
| fail-fast: false | ||
| matrix: | ||
| coq-version: [ 'docker-master' ] | ||
| concurrency: | ||
| group: ${{ github.workflow }}-standalone-haskell-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }} | ||
| cancel-in-progress: true | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
| - name: Download a Build Artifact | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: ExtractionHaskell-source-${{ matrix.coq-version }} | ||
| path: src/ExtractionHaskell | ||
| - name: standalone-haskell | ||
| run: etc/ci/github-actions-make.sh -f Makefile.standalone -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' | ||
| - name: upload Haskell files | ||
| uses: actions/upload-artifact@v4 | ||
| with: | ||
| name: ExtractionHaskell-${{ matrix.coq-version }} | ||
| path: src/ExtractionHaskell | ||
| if: always () | ||
| test-amd64: | ||
| runs-on: ubuntu-latest | ||
| concurrency: | ||
| group: ${{ github.workflow }}-test-amd64-${{ github.head_ref || github.run_id }} | ||
| cancel-in-progress: true | ||
| needs: build | ||
| steps: | ||
| - name: checkout repo | ||
| uses: actions/checkout@v4 | ||
| with: | ||
| submodules: recursive | ||
| - name: Download a Build Artifact | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: ExtractionOCaml-docker-master | ||
| path: src/ExtractionOCaml | ||
| - name: make binaries executable | ||
| run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x | ||
| - name: only-test-amd64-files | ||
| run: etc/ci/github-actions-make.sh -f Makefile.examples -j2 only-test-amd64-files SLOWEST_FIRST=1 | ||
| env: | ||
| ALLOW_DIFF: 1 | ||
| test-standalone: | ||
| strategy: | ||
| fail-fast: false | ||
| matrix: | ||
| source-name: [ 'docker-master' , 'alpine-edge' , 'archlinux' , 'debian-sid' , 'windows' , 'macos' ] | ||
| os: [ {name: 'Ubuntu', runs-on: 'ubuntu-latest', container: {name: '', image: ''} } | ||
| , {name: 'Windows', runs-on: 'windows-latest', container: {name: '', image: ''} } | ||
| , {name: 'macOS', runs-on: 'macos-latest', container: {name: '', image: ''} } | ||
| , {container: { name: 'coqorg/coq', image: 'coqorg/coq:dev' }, name: 'Ubuntu', runs-on: 'ubuntu-latest'} | ||
| , {container: { name: 'alpine', image: 'alpine:edge' }, name: 'Ubuntu', runs-on: 'ubuntu-latest'} | ||
| , {container: { name: 'archlinux', image: 'archlinux' }, name: 'Ubuntu', runs-on: 'ubuntu-latest'} | ||
| , {container: { name: 'debian', image: 'debian:sid' }, name: 'Ubuntu', runs-on: 'ubuntu-latest'} | ||
| runs-on: ${{ matrix.os.runs-on }} | ||
| name: test-standalone-${{ matrix.source-name }}-on-${{ matrix.os.name }}-${{ matrix.os.container.name }} | ||
| container: ${{ matrix.os.container.image }} | ||
| needs: build | ||
| steps: | ||
| - name: Install System Dependencies (coqorg/coq) | ||
| run: | | ||
| sudo apt-get -o Acquire::Retries=30 update -y | ||
| sudo apt-get -o Acquire::Retries=30 install -y --allow-unauthenticated file | ||
| if: matrix.os.container.name == 'coqorg/coq' | ||
| - uses: actions/checkout@v4 | ||
| - name: Download standalone | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: standalone-${{ matrix.source-name }} | ||
| path: dist/ | ||
| - name: List files | ||
| run: find dist | ||
| - run: chmod +x dist/fiat_crypto | ||
| - name: Test files | ||
| run: | | ||
| echo "::group::file fiat_crypto" | ||
| file dist/fiat_crypto | ||
| echo "::endgroup::" | ||
| echo "::group::ldd fiat_crypto" | ||
| ldd dist/fiat_crypto | ||
| echo "::endgroup::" | ||
| etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto | ||
| publish-standalone: | ||
| runs-on: ubuntu-latest | ||
| needs: build | ||
| permissions: | ||
| contents: write # IMPORTANT: mandatory for making GitHub Releases | ||
| steps: | ||
| - uses: actions/checkout@v4 | ||
| with: | ||
| fetch-depth: 0 # Fetch all history for all tags and branches | ||
| tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version | ||
| - name: Download standalone alpine-edge | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: standalone-alpine-edge | ||
| path: dist-linux/ | ||
| - name: Download standalone Windows | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: standalone-windows | ||
| path: dist-windows/ | ||
| - name: Download standalone MacOS | ||
| uses: actions/download-artifact@v4 | ||
| with: | ||
| name: standalone-macos | ||
| path: dist-macos/ | ||
| - name: List files | ||
| run: find dist* | ||
| - run: mkdir dist | ||
| - name: Rename Linux files | ||
| run: | | ||
| echo "::group::find arch" | ||
| arch="$(etc/ci/find-arch.sh dist-linux/fiat_crypto "unknown")" | ||
| tag="$(git describe --tags HEAD)" | ||
| fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}" | ||
| echo "$fname" | ||
| mv dist-linux/fiat_crypto "dist/$fname" | ||
| find dist | ||
| - name: Rename MacOS files | ||
| run: | | ||
| arch="$(etc/ci/find-arch.sh dist-macos/fiat_crypto)" | ||
| tag="$(git describe --tags HEAD)" | ||
| fname="Fiat-Cryptography_${tag}_macOS_${arch}" | ||
| echo "$fname" | ||
| mv dist-macos/fiat_crypto "dist/$fname" | ||
| find dist | ||
| - name: Rename Windows files | ||
| run: | | ||
| arch="$(etc/ci/find-arch.sh dist-windows/fiat_crypto.exe "x86_64")" | ||
| tag="$(git describe --tags HEAD)" | ||
| fname="Fiat-Cryptography_${tag}_Windows_${arch}.exe" | ||
| echo "$fname" | ||
| mv dist-windows/fiat_crypto.exe "dist/$fname" | ||
| find dist | ||
| - name: Upload artifacts to GitHub Release | ||
| env: | ||
| GITHUB_TOKEN: ${{ github.token }} | ||
| # Upload to GitHub Release using the `gh` CLI. | ||
| # `dist/` contains the built packages | ||
| run: >- | ||
| gh release upload | ||
| '${{ github.ref_name }}' dist/** | ||
| --repo '${{ github.repository }}' | ||
| if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }} | ||
| check-all: | ||
| runs-on: ubuntu-latest | ||
| needs: [build, validate, build-js-of-ocaml, build-wasm-of-ocaml, deploy-js-wasm-of-ocaml, generated-files, standalone-haskell, test-amd64, test-standalone, publish-standalone] | ||
| if: always() | ||
| steps: | ||
| - run: echo 'build passed' | ||
| if: ${{ needs.build.result == 'success' }} | ||
| - run: echo 'validate passed' | ||
| if: ${{ needs.validate.result == 'success' }} | ||
| - run: echo 'build-js-of-ocaml passed' | ||
| if: ${{ needs.build-js-of-ocaml.result == 'success' }} | ||
| - run: echo 'build-wasm-of-ocaml passed' | ||
| if: ${{ needs.build-wasm-of-ocaml.result == 'success' }} | ||
| - run: echo 'deploy-js-wasm-of-ocaml passed' | ||
| if: ${{ needs.deploy-js-wasm-of-ocaml.result == 'success' }} | ||
| - run: echo 'generated-files passed' | ||
| if: ${{ needs.generated-files.result == 'success' }} | ||
| - run: echo 'standalone-haskell passed' | ||
| if: ${{ needs.standalone-haskell.result == 'success' }} | ||
| - run: echo 'test-amd64 passed' | ||
| if: ${{ needs.test-amd64.result == 'success' }} | ||
| - run: echo 'test-standalone passed' | ||
| if: ${{ needs.test-standalone.result == 'success' }} | ||
| - run: echo 'publish-standalone passed' | ||
| if: ${{ needs.publish-standalone.result == 'success' }} | ||
| - run: echo 'build failed' && false | ||
| if: ${{ needs.build.result != 'success' }} | ||
| - run: echo 'validate failed' && false | ||
| if: ${{ needs.validate.result != 'success' }} | ||
| - run: echo 'build-js-of-ocaml failed' && false | ||
| if: ${{ needs.build-js-of-ocaml.result != 'success' }} | ||
| - run: echo 'build-wasm-of-ocaml failed' && false | ||
| if: ${{ needs.build-wasm-of-ocaml.result != 'success' }} | ||
| - run: echo 'deploy-js-wasm-of-ocaml failed' && false | ||
| if: ${{ needs.deploy-js-wasm-of-ocaml.result != 'success' }} | ||
| - run: echo 'generated-files failed' && false | ||
| if: ${{ needs.generated-files.result != 'success' }} | ||
| - run: echo 'standalone-haskell failed' && false | ||
| if: ${{ needs.standalone-haskell.result != 'success' }} | ||
| - run: echo 'test-amd64 failed' && false | ||
| if: ${{ needs.test-amd64.result != 'success' }} | ||
| - run: echo 'test-standalone failed' && false | ||
| if: ${{ needs.test-standalone.result != 'success' }} | ||
| - run: echo 'publish-standalone failed' && false | ||
| if: ${{ needs.publish-standalone.result != 'success' }} | ||
