From d8c82be5f8c77e709fd3724477de99f8386f3bc7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 25 Dec 2023 00:40:46 -0800 Subject: [PATCH] Unify Coq CI into a single .yml file This shares structure a lot more, and will also enable us to (eventually) just check if the generated OCaml code is identical across Coq versions and platforms. Note that we no longer check generated files on most platforms, and we only validate on Coq master. --- .github/workflows/coq-alpine.yml | 213 -------- .github/workflows/coq-archlinux.yml | 184 ------- .github/workflows/coq-debian.yml | 211 -------- .github/workflows/coq-docker.yml | 541 -------------------- .github/workflows/coq-macos.yml | 218 -------- .github/workflows/coq-windows.yml | 238 --------- .github/workflows/coq.yml | 678 +++++++++++++++++++++++++ .github/workflows/deploy-html-fast.yml | 2 +- etc/ci/github-actions-make.sh | 2 +- 9 files changed, 680 insertions(+), 1607 deletions(-) delete mode 100644 .github/workflows/coq-alpine.yml delete mode 100644 .github/workflows/coq-archlinux.yml delete mode 100644 .github/workflows/coq-debian.yml delete mode 100644 .github/workflows/coq-docker.yml delete mode 100644 .github/workflows/coq-macos.yml delete mode 100644 .github/workflows/coq-windows.yml create mode 100644 .github/workflows/coq.yml diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml deleted file mode 100644 index 6a5f228892f..00000000000 --- a/.github/workflows/coq-alpine.yml +++ /dev/null @@ -1,213 +0,0 @@ -name: CI (Coq, Alpine) - -on: - push: - branches: [ master ] - pull_request: - merge_group: - workflow_dispatch: - release: - types: [published] - schedule: - - cron: '0 0 1 * *' - -jobs: - build: - - strategy: - fail-fast: false - matrix: - include: - - alpine: 'edge' -# - alpine: 'latest-stable' - - runs-on: ubuntu-latest - name: alpine-${{ matrix.alpine }} - - concurrency: - group: ${{ github.workflow }}-alpine-${{ matrix.alpine }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - uses: jirutka/setup-alpine@v1 - with: - branch: ${{ matrix.alpine }} - extra-repositories: https://dl-cdn.alpinelinux.org/alpine/edge/testing - packages: git make jq gcc musl-dev python3 ocaml ocaml-findlib ghc cabal coq ocaml-zarith bash sudo - - name: work around coq issue 15663 - shell: alpine.sh --root {0} - 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 - - name: host build params - run: etc/ci/describe-system-config.sh - - name: chroot build params - shell: alpine.sh {0} - run: etc/ci/describe-system-config.sh - - name: make deps - shell: alpine.sh {0} - run: make TIMED=1 TIMING=1 -j2 deps - - name: all-except-generated-and-js-of-ocaml - shell: alpine.sh {0} - run: make TIMED=1 TIMING=1 -j2 CAMLEXTRAFLAGS="-ccopt -static" all-except-generated-and-js-of-ocaml - - name: install-standalone-unified-ocaml - shell: alpine.sh {0} - run: make install-standalone-unified-ocaml BINDIR=dist -# - name: install-standalone-js-of-ocaml -# shell: alpine.sh {0} -# run: make install-standalone-js-of-ocaml - - name: upload standalone files - uses: actions/upload-artifact@v4 - with: - name: standalone-${{ matrix.alpine }} - path: dist/fiat_crypto -# - name: upload standalone js files -# uses: actions/upload-artifact@v4 -# with: -# name: standalone-html-${{ matrix.alpine }} -# path: fiat-html - - name: upload OCaml files - uses: actions/upload-artifact@v4 - with: - name: ExtractionOCaml-${{ matrix.alpine }} - path: src/ExtractionOCaml - if: always () -# - name: upload js_of_ocaml files -# uses: actions/upload-artifact@v4 -# with: -# name: ExtractionJsOfOCaml-${{ matrix.alpine }} -# path: src/ExtractionJsOfOCaml -# if: always () - - name: generated-files - shell: alpine.sh {0} - run: make TIMED=1 TIMING=1 -j2 generated-files - - run: tar -czvf generated-files.tgz fiat-*/ - if: ${{ failure() }} - - name: upload generated files - uses: actions/upload-artifact@v4 - with: - name: generated-files-${{ matrix.alpine }} - path: generated-files.tgz - if: ${{ failure() }} - - name: standalone-haskell - shell: alpine.sh {0} - run: make TIMED=1 TIMING=1 -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' - - name: upload Haskell files - uses: actions/upload-artifact@v4 - with: - name: ExtractionHaskell-${{ matrix.alpine }} - path: src/ExtractionHaskell - if: always () - - name: only-test-amd64-files-lite - shell: alpine.sh {0} - run: make TIMED=1 TIMING=1 -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - - name: install - shell: alpine.sh {0} - run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml - - name: install-without-bedrock2 - shell: alpine.sh {0} - run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml - - name: install-dev - shell: alpine.sh {0} - run: sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log || true - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh - - test-standalone: - strategy: - fail-fast: false - matrix: - include: - - alpine: 'edge' -# - alpine: 'latest-stable' - runs-on: ubuntu-latest - name: test-standalone-${{ matrix.alpine }} - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone ${{ matrix.alpine }} - uses: actions/download-artifact@v4 - with: - name: standalone-${{ matrix.alpine }} - path: dist/ - - name: List files - run: find dist - - run: chmod +x dist/fiat_crypto - - name: Test files (host) - run: | - echo "::group::file fiat_crypto" - file dist/fiat_crypto - echo "::endgroup::" - echo "::group::ldd fiat_crypto" - ldd dist/fiat_crypto || true - echo "::endgroup::" - etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto - - uses: jirutka/setup-alpine@v1 - with: - branch: ${{ matrix.alpine }} - extra-repositories: https://dl-cdn.alpinelinux.org/alpine/edge/testing - - name: Test files (container) - shell: alpine.sh {0} - run: 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 edge - uses: actions/download-artifact@v4 - with: - name: standalone-edge - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - echo "::group::find arch" - arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_${arch}" - echo "$fname" - mv dist/fiat_crypto "dist/$fname" - find dist - file "dist/$fname" - - 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' }} - - alpine-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.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 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone failed' && false - if: ${{ needs.publish-standalone.result != 'success' }} diff --git a/.github/workflows/coq-archlinux.yml b/.github/workflows/coq-archlinux.yml deleted file mode 100644 index 0a3f3abc328..00000000000 --- a/.github/workflows/coq-archlinux.yml +++ /dev/null @@ -1,184 +0,0 @@ -name: CI (Coq, Arch Linux) - -on: - push: - branches: [ master ] - pull_request: - merge_group: - workflow_dispatch: - release: - types: [published] - schedule: - - cron: '0 0 1 * *' - -jobs: - build: - - runs-on: ubuntu-latest - container: archlinux - name: archlinux - - concurrency: - group: ${{ github.workflow }}-archlinux-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - - steps: - - name: Install system dependencies - run: | - pacman --noconfirm -Syu base-devel git make python3 which jq ghc ghc-static time diffutils coq ocaml-zarith --needed - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: work around coq issue 15663 - 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 - - name: Work around https://github.com/actions/checkout/issues/766 - run: git config --global --add safe.directory "*" - - name: chroot build params - run: etc/ci/describe-system-config.sh - - name: make deps - run: etc/ci/github-actions-make.sh -j2 deps - - name: all-except-generated-and-js-of-ocaml - run: etc/ci/github-actions-make.sh -j2 all-except-generated-and-js-of-ocaml - - name: generated-files - run: etc/ci/github-actions-make.sh -j2 generated-files - - run: tar -czvf generated-files.tgz fiat-*/ - if: ${{ failure() }} - - name: upload generated files - uses: actions/upload-artifact@v4 - with: - name: generated-files-archlinux - path: generated-files.tgz - if: ${{ failure() }} - - name: install-standalone-unified-ocaml - run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist - #- name: standalone-js-of-ocaml - # run: etc/ci/github-actions-make.sh -j2 standalone-js-of-ocaml - #- name: install-standalone-js-of-ocaml - # run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml - - name: upload standalone files - uses: actions/upload-artifact@v4 - with: - name: standalone-archlinux - path: dist/fiat_crypto - #- name: upload standalone js files - # uses: actions/upload-artifact@v4 - # with: - # name: standalone-html-archlinux - # path: fiat-html - - name: upload OCaml files - uses: actions/upload-artifact@v4 - with: - name: ExtractionOCaml-archlinux - path: src/ExtractionOCaml - if: always () - #- name: upload js_of_ocaml files - # uses: actions/upload-artifact@v4 - # with: - # name: ExtractionJsOfOCaml-archlinux - # path: src/ExtractionJsOfOCaml - # if: always () - - name: standalone-haskell - run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' - - name: upload Haskell files - uses: actions/upload-artifact@v4 - with: - name: ExtractionHaskell-archlinux - path: src/ExtractionHaskell - if: always () - - name: only-test-amd64-files-lite - run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - - name: install - run: etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml - - name: install-without-bedrock2 - run: etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml - - name: install-dev - run: etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh - - test-standalone: - runs-on: ubuntu-latest - container: archlinux - needs: build - steps: - - name: Install system dependencies - run: | - pacman --noconfirm -Syu git --needed - - uses: actions/checkout@v4 - - name: Download standalone archlinux - uses: actions/download-artifact@v4 - with: - name: standalone-archlinux - path: dist/ - - name: List files - run: find dist - - run: chmod +x dist/fiat_crypto - - name: Test files (container) - 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-dry-run: - 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 archlinux - uses: actions/download-artifact@v4 - with: - name: standalone-archlinux - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - echo "::group::find arch" - arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_archlinux_${arch}" - echo "$fname" - mv dist/fiat_crypto "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' }} - - archlinux-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone-dry-run] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.result == 'success' }} - - run: echo 'test-standalone passed' - if: ${{ needs.test-standalone.result == 'success' }} - - run: echo 'publish-standalone-dry-run passed' - if: ${{ needs.publish-standalone-dry-run.result == 'success' }} - - run: echo 'build failed' && false - if: ${{ needs.build.result != 'success' }} - - run: echo 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone-dry-run failed' && false - if: ${{ needs.publish-standalone-dry-run.result != 'success' }} diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml deleted file mode 100644 index 34883bc00c6..00000000000 --- a/.github/workflows/coq-debian.yml +++ /dev/null @@ -1,211 +0,0 @@ -name: CI (Coq, Debian) - -on: - push: - branches: [ master , sp2019latest ] - pull_request: - merge_group: - workflow_dispatch: - release: - types: [published] - schedule: - - cron: '0 0 1 * *' - -jobs: - build: - - strategy: - fail-fast: false - matrix: - include: - - env: { DEBIAN: "sid" } - #- env: { DEBIAN: "bookworm" }# restore once 8.17 lands in Debian stable - - runs-on: 'ubuntu-22.04' - env: ${{ matrix.env }} - name: debian-${{ matrix.env.DEBIAN }} - - concurrency: - group: ${{ github.workflow }}-${{ matrix.env.DEBIAN }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: setup Debian chroot - run: etc/ci/setup-debian-chroot.sh "$DEBIAN" - - name: host build params - run: etc/ci/describe-system-config.sh - - name: chroot build params - shell: in-debian-chroot.sh {0} - run: CI=1 etc/ci/describe-system-config.sh - - name: make deps - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 deps - - name: all-except-generated-and-js-of-ocaml - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 all-except-generated-and-js-of-ocaml - - name: generated-files - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 generated-files - - run: tar -czvf generated-files.tgz fiat-*/ - if: ${{ failure() }} - - name: upload generated files - uses: actions/upload-artifact@v4 - with: - name: generated-files-${{ matrix.env.DEBIAN }} - path: generated-files.tgz - if: ${{ failure() }} - - name: install-standalone-unified-ocaml - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist - - name: standalone-js-of-ocaml - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 standalone-js-of-ocaml - - name: install-standalone-js-of-ocaml - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml - - name: upload standalone files - uses: actions/upload-artifact@v4 - with: - name: standalone-${{ matrix.env.DEBIAN }} - path: dist/fiat_crypto - - name: upload standalone js files - uses: actions/upload-artifact@v4 - with: - name: standalone-html-${{ matrix.env.DEBIAN }} - path: fiat-html - - name: upload OCaml files - uses: actions/upload-artifact@v4 - with: - name: ExtractionOCaml-${{ matrix.env.DEBIAN }} - path: src/ExtractionOCaml - if: always () - - name: upload js_of_ocaml files - uses: actions/upload-artifact@v4 - with: - name: ExtractionJsOfOCaml-${{ matrix.env.DEBIAN }} - path: src/ExtractionJsOfOCaml - if: always () - - name: standalone-haskell - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' - - name: upload Haskell files - uses: actions/upload-artifact@v4 - with: - name: ExtractionHaskell-${{ matrix.env.DEBIAN }} - path: src/ExtractionHaskell - if: always () - - name: only-test-amd64-files-lite - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - - name: install - shell: in-debian-chroot.sh {0} - run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml - - name: install-without-bedrock2 - shell: in-debian-chroot.sh {0} - run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml - - name: install-dev - shell: in-debian-chroot.sh {0} - run: sudo etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh - - test-standalone: - strategy: - fail-fast: false - matrix: - include: - - debian: sid - #- debian: bookworm # restore once 8.17 lands in Debian stable - runs-on: ubuntu-latest - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone ${{ matrix.debian }} - uses: actions/download-artifact@v4 - with: - name: standalone-${{ matrix.debian }} - path: dist/ - - name: List files - run: find dist - - run: chmod +x dist/fiat_crypto - - name: Test files (host) - 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 - - name: setup Debian chroot - run: etc/ci/setup-debian-chroot.sh "${{ matrix.debian }}" - - name: Test files (container) - shell: in-debian-chroot.sh {0} - 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-dry-run: - 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 sid - uses: actions/download-artifact@v4 - with: - name: standalone-sid - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - echo "::group::find arch" - arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_debian_sid_${arch}" - echo "$fname" - mv dist/fiat_crypto "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' }} - - debian-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone-dry-run] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.result == 'success' }} - - run: echo 'test-standalone passed' - if: ${{ needs.test-standalone.result == 'success' }} - - run: echo 'publish-standalone-dry-run passed' - if: ${{ needs.publish-standalone-dry-run.result == 'success' }} - - run: echo 'build failed' && false - if: ${{ needs.build.result != 'success' }} - - run: echo 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone-dry-run failed' && false - if: ${{ needs.publish-standalone-dry-run.result != 'success' }} diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml deleted file mode 100644 index 9a584af4e5a..00000000000 --- a/.github/workflows/coq-docker.yml +++ /dev/null @@ -1,541 +0,0 @@ -name: CI (Coq, docker, dev) - -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: - - env: { COQ_VERSION: "master", DOCKER_COQ_VERSION: "dev", DOCKER_OCAML_VERSION: "default", SKIP_VALIDATE: "" , COQCHKEXTRAFLAGS: "-bytecode-compiler yes", EXTRA_GH_REPORTIFY: "--warnings", ALLOW_DIFF: "1", CI: "1" } - os: 'ubuntu-latest' - - runs-on: ${{ matrix.os }} - env: ${{ matrix.env }} - name: docker-${{ matrix.env.COQ_VERSION }} - - concurrency: - group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: echo host build params - run: etc/ci/describe-system-config.sh - - name: echo container build params - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: | - eval $(opam env) - etc/ci/describe-system-config.sh - - name: deps - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: etc/ci/github-actions-docker-make.sh COQBIN="$(dirname "$(which coqc)")/" -j2 deps - - name: all-except-generated-and-js-of-ocaml - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated-and-js-of-ocaml - - name: pre-standalone-extracted - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 pre-standalone-extracted - - name: upload OCaml files - uses: actions/upload-artifact@v4 - with: - name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }} - path: src/ExtractionOCaml - if: always () - - name: upload js_of_ocaml source files - uses: actions/upload-artifact@v4 - with: - name: ExtractionJsOfOCaml-source-${{ matrix.env.COQ_VERSION }} - path: src/ExtractionJsOfOCaml - if: always () - - name: upload Haskell source files - uses: actions/upload-artifact@v4 - with: - name: ExtractionHaskell-source-${{ matrix.env.COQ_VERSION }} - path: src/ExtractionHaskell - if: always () - - name: install-standalone-unified-ocaml - run: make -f Makefile.standalone install-standalone-unified-ocaml BINDIR=dist - - name: upload standalone files - uses: actions/upload-artifact@v4 - with: - name: standalone-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }} - path: dist/fiat_crypto - - run: git config --file .gitmodules --get-regexp path | awk '{ print $2 }' | xargs tar -czvf fiat-crypto-build.tar.gz src - - name: Upload built files - uses: actions/upload-artifact@v4 - with: - name: build-outputs-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}-ocaml-${{ matrix.env.DOCKER_OCAML_VERSION }} - path: fiat-crypto-build.tar.gz - - name: install - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: | - sudo git config --global --add safe.directory "*" - sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml - - name: install-without-bedrock2 - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: | - sudo git config --global --add safe.directory "*" - sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 COQBIN="$(dirname "$(which coqc)")/" install-without-bedrock2 install-standalone-ocaml - - name: install-dev - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: | - sudo git config --global --add safe.directory "*" - sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh - - validate: - strategy: - fail-fast: false - matrix: - include: - - env: { COQ_VERSION: "master", DOCKER_COQ_VERSION: "dev", DOCKER_OCAML_VERSION: "default", SKIP_VALIDATE: "" , COQCHKEXTRAFLAGS: "-bytecode-compiler yes", EXTRA_GH_REPORTIFY: "--warnings", ALLOW_DIFF: "1", CI: "1" } - os: 'ubuntu-latest' - - runs-on: ${{ matrix.os }} - env: ${{ matrix.env }} - name: validate-docker-${{ matrix.env.COQ_VERSION }} - - concurrency: - group: ${{ github.workflow }}-validate-${{ matrix.env.COQ_VERSION }}-${{ 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-coq-${{ matrix.env.DOCKER_COQ_VERSION }}-ocaml-${{ matrix.env.DOCKER_OCAML_VERSION }} - path: . - - name: Unpack build artifact - run: tar --overwrite -xzvf fiat-crypto-build.tar.gz - - name: validate - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: etc/ci/github-actions-docker-make.sh TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}" - if: env.SKIP_VALIDATE == '' && github.event_name != 'pull_request' - - build-js-of-ocaml: - needs: build - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - coq-version: [ '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: [ '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: JasonGross@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: [ '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: [ '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-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: - include: - - coq-version: master - docker-coq-version: dev - docker-ocaml-version: default - - runs-on: ubuntu-latest - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone Docker - uses: actions/download-artifact@v4 - with: - name: standalone-docker-coq-${{ matrix.docker-coq-version }} - path: dist/ - - name: List files - run: find dist - - run: chmod +x dist/fiat_crypto - - name: Test files (host) - 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 - - name: Test files (container) - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.docker-coq-version }} - ocaml_version: ${{ matrix.docker-ocaml-version }} - custom_script: | - echo "::group::install dependencies" - sudo apt-get update -y - sudo apt-get install -y file - echo "::endgroup::" - 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-dry-run: - 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 Docker - uses: actions/download-artifact@v4 - with: - name: standalone-docker-coq-dev - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - echo "::group::find arch" - arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}" - echo "$fname" - mv dist/fiat_crypto "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' }} - - docker-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-dry-run] - 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-dry-run passed' - if: ${{ needs.publish-standalone-dry-run.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-dry-run failed' && false - if: ${{ needs.publish-standalone-dry-run.result != 'success' }} diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml deleted file mode 100644 index a6fc7379528..00000000000 --- a/.github/workflows/coq-macos.yml +++ /dev/null @@ -1,218 +0,0 @@ -name: CI (Coq, MacOS) - -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: - - runs-on: macOS-11 - - concurrency: - group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - - env: - NJOBS: "2" - COQ_VERSION: "8.18.0" # pick a version not tested on other platforms - COQCHKEXTRAFLAGS: "" - SKIP_BEDROCK2: "0" - - name: macos - - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Set up OCaml - uses: ocaml/setup-ocaml@v2 - with: - ocaml-compiler: 4.11.1 - - - name: Install system dependencies - run: | - set -e - brew install gnu-time coreutils - - - name: Install Coq - run: | - set -e - eval $(opam env) - opam update - opam pin add coq ${COQ_VERSION} - env: - OPAMYES: "true" - OPAMCONFIRMLEVEL: "unsafe-yes" - - - name: Install js_of_ocaml - run: | - set -e - eval $(opam env) - opam install js_of_ocaml - env: - OPAMYES: "true" - OPAMCONFIRMLEVEL: "unsafe-yes" - - - name: echo build params - run: | - eval $(opam env) - etc/ci/describe-system-config-macos.sh - - name: deps - run: | - eval $(opam env) - etc/ci/github-actions-make.sh -j2 deps - - name: all - run: | - eval $(opam env) - etc/ci/github-actions-make.sh -j2 all - - - name: install-standalone-unified-ocaml - run: | - eval $(opam env) - etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist - - - name: install-standalone-js-of-ocaml - run: | - eval $(opam env) - etc/ci/github-actions-make.sh install-standalone-js-of-ocaml - - - name: only-test-amd64-files-lite - run: | - eval $(opam env) - etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - - - name: upload OCaml files - uses: actions/upload-artifact@v4 - with: - name: ExtractionOCaml - path: src/ExtractionOCaml - - name: upload js_of_ocaml files - uses: actions/upload-artifact@v4 - with: - name: ExtractionJsOfOCaml - path: src/ExtractionJsOfOCaml - - name: upload standalone files - uses: actions/upload-artifact@v4 - with: - name: standalone-macos - path: dist/fiat_crypto - - name: upload standalone js files - uses: actions/upload-artifact@v4 - with: - name: standalone-html-macos - path: fiat-html - - name: install - run: | - eval $(opam env) - etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml - - name: install-without-bedrock2 - run: | - eval $(opam env) - etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml - - name: install-dev - run: | - eval $(opam env) - etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh -# - name: upload timing and .vo info -# uses: actions/upload-artifact@v4 -# with: -# name: build-outputs -# path: . -# if: always () -# - name: validate -# run: | -# eval $(opam env) -# make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}" -# if: github.event_name != 'pull_request' - - test-standalone: - runs-on: macos-latest - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone MacOS - uses: actions/download-artifact@v4 - with: - name: standalone-macos - 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::otool -L fiat_crypto" - otool -L dist/fiat_crypto - echo "::endgroup::" - echo "::group::lipo -info fiat_crypto" - lipo -info 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 MacOS - uses: actions/download-artifact@v4 - with: - name: standalone-macos - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - arch="$(etc/ci/find-arch.sh dist/fiat_crypto)" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_macOS_${arch}" - echo "$fname" - mv dist/fiat_crypto "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' }} - - macos-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.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 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone failed' && false - if: ${{ needs.publish-standalone.result != 'success' }} diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml deleted file mode 100644 index 2dcfc23e568..00000000000 --- a/.github/workflows/coq-windows.yml +++ /dev/null @@ -1,238 +0,0 @@ -name: CI (Coq, Windows) - -# Note that we must split up each command into a separate step for Windows, because otherwise we don't get error code -# See also https://github.com/avsm/setup-ocaml/issues/72 - -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: - - runs-on: windows-latest - name: windows - - concurrency: - group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - - env: - NJOBS: "2" - COQ_VERSION: "8.17.0" # minimal major version required for bedrock2 components - COQEXTRAFLAGS: "-async-proofs-j 1" - COQCHKEXTRAFLAGS: "" - OPAMYES: "true" - OPAMCONFIRMLEVEL: "unsafe-yes" - - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Setup Python - uses: actions/setup-python@v5 - with: - python-version: 3.x - - name: Set up OCaml - uses: ocaml/setup-ocaml@v2 - with: - ocaml-compiler: 4.11.1 - opam-repositories: | - opam-repository-mingw: https://github.com/ocaml-opam/opam-repository-mingw.git#sunset - default: https://github.com/ocaml/opam-repository.git - - run: opam depext coq.${{ env.COQ_VERSION }} - - run: opam pin add --kind=version coq ${{ env.COQ_VERSION }} - - run: opam install js_of_ocaml - - - name: Install System Dependencies - run: | - %CYGWIN_ROOT%\setup-x86_64.exe -qnNdO -P time,zip - shell: cmd - - - name: Work around https://github.com/actions/checkout/issues/766 - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'git config --global --add safe.directory "*"' - shell: cmd - - - name: echo build params - run: | - %cd%\etc\ci\describe-system-config-win.bat - shell: cmd - - name: deps - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} deps' - shell: cmd - - name: standalone-ocaml - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} standalone-ocaml' - shell: cmd - - name: install-standalone-unified-ocaml - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist' - shell: cmd - - - name: coq - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 coq' - shell: cmd - - name: all-except-generated-and-js-of-ocaml - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 all-except-generated-and-js-of-ocaml' - shell: cmd - - name: standalone-js-of-ocaml - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 standalone-js-of-ocaml' - shell: cmd - - name: install-standalone-js-of-ocaml - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh install-standalone-js-of-ocaml' - shell: cmd - - name: c-files lite-generated-files - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} c-files lite-generated-files' - shell: cmd - - name: only-test-amd64-files-lite - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} only-test-amd64-files-lite SLOWEST_FIRST=1' - shell: cmd - - name: upload OCaml files - uses: actions/upload-artifact@v4 - with: - name: ExtractionOCaml - path: src/ExtractionOCaml - - name: upload js_of_ocaml files - uses: actions/upload-artifact@v4 - with: - name: ExtractionJsOfOCaml - path: src/ExtractionJsOfOCaml - - name: upload standalone files - uses: actions/upload-artifact@v4 - with: - name: standalone-windows - path: dist/fiat_crypto.exe - - name: upload standalone js files - uses: actions/upload-artifact@v4 - with: - name: standalone-html-windows - path: fiat-html - - name: install - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml' - shell: cmd - - name: install-without-bedrock2 - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml' - shell: cmd - - name: install-dev - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml' - shell: cmd - - name: display timing info - run: type time-of-build-pretty.log - shell: cmd - - name: display per-line timing info - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; etc/ci/github-actions-display-per-line-timing.sh' - shell: cmd -# - name: upload timing and .vo info -# uses: actions/upload-artifact@v4 -# with: -# name: build-outputs -# path: . -# if: always () -# - name: validate -# run: | -# %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"' -# shell: cmd -# if: github.event_name != 'pull_request' - - test-standalone: - runs-on: windows-latest - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone Windows - uses: actions/download-artifact@v4 - with: - name: standalone-windows - path: dist/ - - name: List files - run: Get-ChildItem dist -Name - - run: .\dist\fiat_crypto.exe -h - - run: .\dist\fiat_crypto.exe word-by-word-montgomery -h - - run: .\dist\fiat_crypto.exe unsaturated-solinas -h - - run: .\dist\fiat_crypto.exe saturated-solinas -h - - run: .\dist\fiat_crypto.exe base-conversion -h - - name: Set up MSVC Environment for dumpbin - uses: ilammy/msvc-dev-cmd@v1 - - name: Check Executable Dependencies - run: | - Write-Host "::group::File Info - fiat_crypto" - Get-Item .\dist\fiat_crypto.exe | Format-List - dumpbin.exe /headers .\dist\fiat_crypto.exe - Write-Host "::endgroup::" - - Write-Host "::group::DLL Dependencies - fiat_crypto" - dumpbin.exe /dependents .\dist\fiat_crypto.exe - Write-Host "::endgroup::" - - 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 Windows - uses: actions/download-artifact@v4 - with: - name: standalone-windows - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - arch="$(etc/ci/find-arch.sh dist/fiat_crypto.exe "x86_64")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Windows_${arch}.exe" - echo "$fname" - mv dist/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' }} - - windows-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.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 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone failed' && false - if: ${{ needs.publish-standalone.result != 'success' }} diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml new file mode 100644 index 00000000000..fa103bf6648 --- /dev/null +++ b/.github/workflows/coq.yml @@ -0,0 +1,678 @@ +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' + sudo: 'sudo' + 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' + sudo: 'sudo' + coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"' + os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'} + - name: 'archlinux' + container: {name: 'archlinux', image: 'archlinux'} + env: {} + make: 'etc/ci/github-actions-make.sh' + raw-make: 'make' + sudo-make: 'sudo make' + sudo: 'sudo' + coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"' + os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'} + - name: 'debian-sid' + container: {name: 'debian', image: 'debian:sid'} + env: {} + make: 'etc/ci/github-actions-make.sh' + raw-make: 'make' + sudo-make: 'sudo make' + sudo: 'sudo' + 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: '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'} + + + 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: + - name: Install System Dependencies (Alpine) + run: | + echo 'https://dl-cdn.alpinelinux.org/alpine/edge/testing' >> /etc/apk/repositories + apk update + 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' + - name: Update permissions (coqorg/coq) + run: | + set -e + sudo chmod a=u /__w || true + sudo chmod -R a=u /__w/_temp || true + if: matrix.container.name == 'coqorg/coq' + - name: explore + run: | + ls -la /__w || true + ls -la /__w/_temp || true + ls -la /__w/_temp/_runner_file_commands || true + if: matrix.os.name != 'Windows' + + - uses: actions/checkout@v4 + with: + submodules: recursive + - run: echo ::add-matcher::.github/make.json + + - name: Set up OCaml + uses: ocaml/setup-ocaml@v2 + with: + ocaml-compiler: ${{ matrix.container.ocaml-compiler }} + opam-repositories: |- + ${{ matrix.extra-ocaml-repositories }} + default: https://github.com/ocaml/opam-repository.git + if: matrix.container.name == '' + - run: eval $(opam env) + if: matrix.os.name != 'Windows' && ( 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 "*" + ${{ matrix.sudo }} git config --global --add safe.directory "*" + if: matrix.container.name != '' + + - 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@v3 + with: + name: ExtractionOCaml-${{ matrix.name }} + path: src/ExtractionOCaml + if: always () + - name: upload js_of_ocaml source files + uses: actions/upload-artifact@v3 + with: + name: ExtractionJsOfOCaml-source-${{ matrix.name }} + path: src/ExtractionJsOfOCaml + if: always () + - name: upload Haskell source files + uses: actions/upload-artifact@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + 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@v3 + with: + name: standalone-alpine-edge + path: dist-linux/ + - name: Download standalone Windows + uses: actions/download-artifact@v3 + with: + name: standalone-windows + path: dist-windows/ + - name: Download standalone MacOS + uses: actions/download-artifact@v3 + 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' }} diff --git a/.github/workflows/deploy-html-fast.yml b/.github/workflows/deploy-html-fast.yml index e474604b5b1..d1f3118f043 100644 --- a/.github/workflows/deploy-html-fast.yml +++ b/.github/workflows/deploy-html-fast.yml @@ -21,7 +21,7 @@ jobs: with: branch: gh-pages # The branch the action should deploy to. folder: fiat-html # The folder the action should deploy. - git-config-email: JasonGross@users.noreply.github.com + 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' }} diff --git a/etc/ci/github-actions-make.sh b/etc/ci/github-actions-make.sh index 26f1babf98c..b74fb564954 100755 --- a/etc/ci/github-actions-make.sh +++ b/etc/ci/github-actions-make.sh @@ -21,7 +21,7 @@ if [ "$1" == "--warnings" ]; then shift fi if [ ! -z "${reportify}" ]; then - reportify="COQC=etc/coq-scripts/github/reportify-coq.sh${reportify} ${COQBIN}coqc" + reportify="COQC=$(pwd)/etc/coq-scripts/github/reportify-coq.sh${reportify} ${COQBIN}coqc" fi make_one_time_file_real=""