From ed3cb656532a98b81cb95fb9bfc7a5cfcc6bc80a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Nov 2023 16:46:50 -0800 Subject: [PATCH] Split up coq-docker job a lot This way we can more easily build both js_of_ocaml and wasm_of_ocaml outputs, which require different ocaml compilers. This would also allow decoupling the testing of Coq versions from OCaml versions on extracted code. --- .github/workflows/coq-docker.yml | 274 ++++++++++++++++++++++++------- 1 file changed, 216 insertions(+), 58 deletions(-) diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 8bf6378a324..46e357678ec 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -32,8 +32,6 @@ jobs: - 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: echo host build params run: etc/ci/describe-system-config.sh - name: echo container build params @@ -52,62 +50,38 @@ jobs: ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} export: CI ALLOW_DIFF COQCHKEXTRAFLAGS custom_script: etc/ci/github-actions-docker-make.sh -j2 deps - - name: all-except-generated + - 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: standalone-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: | - eval $(opam env) - opam update -y - opam install -y js_of_ocaml - etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 standalone-js-of-ocaml - - name: install-standalone-js-of-ocaml - run: make -f Makefile.standalone install-standalone-js-of-ocaml - - run: make -f Makefile.js-html fiat-html/version.js - - name: backup .gitignore - run: mv .gitignore{,.bak} - - name: Deploy js_of_ocaml 🚀 ${{ ( github.ref != 'refs/heads/master' && '(dry run)' ) || '' }} - uses: JamesIves/github-pages-deploy-action@v4.4.3 - 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,} - - name: upload standalone js files + custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 pre-standalone-extracted + - name: upload OCaml files uses: actions/upload-artifact@v3 with: - name: standalone-html-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }} - path: fiat-html - - name: upload js_of_ocaml files + name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }} + path: src/ExtractionOCaml + if: always () + - name: upload js_of_ocaml source files uses: actions/upload-artifact@v3 with: - name: ExtractionJsOfOCaml-${{ matrix.env.COQ_VERSION }} + name: ExtractionJsOfOCaml-source-${{ matrix.env.COQ_VERSION }} path: src/ExtractionJsOfOCaml if: always () - - name: generated-files - run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -f Makefile.examples -j2 generated-files - if: github.event_name == 'pull_request' || ${{ matrix.env.COQ_VERSION }} != 'master' - - run: tar -czvf generated-files.tgz fiat-*/ - if: ${{ failure() }} - - name: upload generated files + - name: upload Haskell source files uses: actions/upload-artifact@v3 with: - name: generated-files-${{ matrix.env.COQ_VERSION }} - path: generated-files.tgz - if: ${{ failure() }} + name: ExtractionHaskell-sources-${{ 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 @@ -115,20 +89,12 @@ jobs: with: name: standalone-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }} path: dist/fiat_crypto - - name: upload OCaml files + - 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@v3 with: - name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }} - path: src/ExtractionOCaml - if: always () - - 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.env.COQ_VERSION }} - path: src/ExtractionHaskell - if: always () + 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: @@ -165,12 +131,36 @@ jobs: 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@v3 -# with: -# name: build-outputs-${{ matrix.env.COQ_VERSION }} -# path: . -# if: always () + + 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@v3 + 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: @@ -180,6 +170,154 @@ jobs: 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 + - name: echo build params + run: etc/ci/describe-system-config.sh + - name: Download a Build Artifact + uses: actions/download-artifact@v3 + with: + name: ExtractionJsOfOCaml-soruce-${{ 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 + + deploy-js-of-ocaml: + needs: build-js-of-ocaml + runs-on: ubuntu-latest + concurrency: + group: ${{ github.workflow }}-deploy-js-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: 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 🚀 ${{ ( github.ref != 'refs/heads/master' && '(dry run)' ) || '' }} + uses: JamesIves/github-pages-deploy-action@v4.4.3 + 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@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: 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: [ '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-${{ matrix.coq-version }} + path: src/ExtractionHaskell + - name: make binaries executable + run: git check-ignore src/ExtractionHaskell/* | grep -v '\.' | xargs chmod +x + - 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 @@ -293,11 +431,21 @@ jobs: docker-check-all: runs-on: ubuntu-latest - needs: [build, test-amd64, test-standalone, publish-standalone-dry-run] + needs: [build, validate, build-js-of-ocaml, deploy-js-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 'deploy-js-of-ocaml passed' + if: ${{ needs.deploy-js-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' @@ -306,6 +454,16 @@ jobs: 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 'deploy-js-of-ocaml failed' && false + if: ${{ needs.deploy-js-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