From 5d1a041a5f57430c74b82f21fc0e8884bb6b8d8d 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-macos.yml | 218 ---------- .github/workflows/coq-windows.yml | 238 ----------- .github/workflows/{coq-docker.yml => coq.yml} | 400 +++++++++++------- .github/workflows/deploy-html-fast.yml | 2 +- 7 files changed, 259 insertions(+), 1207 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-macos.yml delete mode 100644 .github/workflows/coq-windows.yml rename .github/workflows/{coq-docker.yml => coq.yml} (53%) 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-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-docker.yml b/.github/workflows/coq.yml similarity index 53% rename from .github/workflows/coq-docker.yml rename to .github/workflows/coq.yml index 9a584af4e5a..0086d07c42c 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq.yml @@ -1,4 +1,4 @@ -name: CI (Coq, docker, dev) +name: CI (Coq) on: push: @@ -17,130 +17,228 @@ jobs: 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' + - 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: ${{ matrix.os.runs-on }} env: ${{ matrix.env }} - name: docker-${{ matrix.env.COQ_VERSION }} + name: ${{ matrix.name }} + container: ${{ matrix.container.image }} concurrency: - group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }} + 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: echo host build params + + - 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 - - 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 + 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 - 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 + run: ${{ matrix.make }} -j2 ${{ matrix.coqbin-arg }} 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 + run: ${{ matrix.make }} -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 + run: ${{ matrix.make }} -j2 pre-standalone-extracted + - name: upload OCaml files uses: actions/upload-artifact@v4 with: - name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }} + 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.env.COQ_VERSION }} + 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.env.COQ_VERSION }} + name: ExtractionHaskell-source-${{ matrix.name }} path: src/ExtractionHaskell if: always () + - name: install-standalone-unified-ocaml - run: make -f Makefile.standalone install-standalone-unified-ocaml BINDIR=dist + 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-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }} + 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-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}-ocaml-${{ matrix.env.DOCKER_OCAML_VERSION }} + name: build-outputs-${{ matrix.name }} path: fiat-crypto-build.tar.gz + if: matrix.os.name != 'Windows' + - 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 + run: ${{ matrix.sudo-make }} ${{ matrix.coqbin-arg }} EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 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 + run: ${{ matrix.sudo-make }} ${{ matrix.coqbin-arg }} EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 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 + 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: - 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 }} + 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-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }} + group: ${{ github.workflow }}-validate-docker-master-${{ github.head_ref || github.run_id }} cancel-in-progress: true needs: build @@ -152,18 +250,13 @@ jobs: - 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 }} + name: build-outputs-docker-master 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' + 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 @@ -171,7 +264,7 @@ jobs: strategy: fail-fast: false matrix: - coq-version: [ 'master' ] + 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 }} @@ -220,7 +313,7 @@ jobs: strategy: fail-fast: false matrix: - coq-version: [ 'master' ] + 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 }} @@ -311,7 +404,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' }} @@ -325,7 +418,7 @@ jobs: strategy: fail-fast: false matrix: - coq-version: [ 'master' ] + coq-version: [ 'docker-master' ] concurrency: group: ${{ github.workflow }}-generated-files-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }} cancel-in-progress: true @@ -360,7 +453,7 @@ jobs: strategy: fail-fast: false matrix: - coq-version: [ 'master' ] + coq-version: [ 'docker-master' ] concurrency: group: ${{ github.workflow }}-standalone-haskell-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }} cancel-in-progress: true @@ -400,7 +493,7 @@ jobs: - name: Download a Build Artifact uses: actions/download-artifact@v4 with: - name: ExtractionOCaml-master + name: ExtractionOCaml-docker-master path: src/ExtractionOCaml - name: make binaries executable run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x @@ -413,24 +506,37 @@ jobs: strategy: fail-fast: false matrix: - include: - - coq-version: master - docker-coq-version: dev - docker-ocaml-version: default + 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 }} - runs-on: ubuntu-latest 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 Docker + - name: Download standalone uses: actions/download-artifact@v4 with: - name: standalone-docker-coq-${{ matrix.docker-coq-version }} + name: standalone-${{ matrix.source-name }} path: dist/ - name: List files run: find dist - run: chmod +x dist/fiat_crypto - - name: Test files (host) + - name: Test files run: | echo "::group::file fiat_crypto" file dist/fiat_crypto @@ -439,64 +545,74 @@ jobs: 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: + + publish-standalone: runs-on: ubuntu-latest needs: build -# permissions: -# contents: write # IMPORTANT: mandatory for making GitHub Releases + 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 + - name: Download standalone alpine-edge uses: actions/download-artifact@v4 with: - name: standalone-docker-coq-dev - path: dist/ + 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 - - name: Rename files + run: find dist* + - run: mkdir dist + - name: Rename Linux files run: | echo "::group::find arch" - arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" + 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/fiat_crypto "dist/$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' }} - - docker-check-all: + - 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-dry-run] + 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' @@ -517,8 +633,8 @@ jobs: 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 'publish-standalone passed' + if: ${{ needs.publish-standalone.result == 'success' }} - run: echo 'build failed' && false if: ${{ needs.build.result != 'success' }} - run: echo 'validate failed' && false @@ -537,5 +653,5 @@ jobs: 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' }} + - 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' }}