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

@@ -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,83 +50,51 @@ 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/[email protected]
-      with:
-        branch: gh-pages # The branch the action should deploy to.
-        folder: fiat-html # The folder the action should deploy.
-        git-config-email: [email protected]
-        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
       uses: actions/upload-artifact@v3
       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/[email protected]
+      with:
+        branch: gh-pages # The branch the action should deploy to.
+        folder: fiat-html # The folder the action should deploy.
+        git-config-email: [email protected]
+        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