Merge branch 'mit-plv:master' into cache

.github/workflows/c.yml

@@ -31,7 +31,7 @@ jobs:
     - name: GCC Problem Matcher
       uses: ammaraskar/[email protected]
     - name: Set up Go
-      uses: actions/setup-go@v4
+      uses: actions/setup-go@v5
       id: go
     - name: make only-test-c-files CC=gcc
       run: make only-test-c-files CC=gcc EXTERNAL_DEPENDENCIES=1

.github/workflows/coq-alpine.yml

@@ -2,14 +2,18 @@ name: CI (Coq, Alpine)
 
 on:
   push:
-    branches: [ master  ]
+    branches: [ master ]
   pull_request:
+  merge_group:
   workflow_dispatch:
+  release:
+    types: [published]
   schedule:
     - cron: '0 0 1 * *'
 
 jobs:
   build:
+
     strategy:
       fail-fast: false
       matrix:
@@ -18,42 +22,186 @@ jobs:
 #        - alpine: 'latest-stable'
 
     runs-on: ubuntu-latest
-    name: ${{ matrix.alpine }}
+    name: alpine-${{ matrix.alpine }}
+
     concurrency:
-      group: ${{ github.workflow }}-${{ matrix.alpine }}-${{ github.head_ref || github.run_id }}
+      group: ${{ github.workflow }}-alpine-${{ matrix.alpine }}-${{ github.head_ref || github.run_id }}
       cancel-in-progress: true
+
     steps:
-    - uses: actions/checkout@v3
+    - 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
-    - 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
+        packages: git make jq gcc musl-dev python3 ocaml ocaml-findlib ghc cabal coq ocaml-zarith bash sudo
+    - 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 -j2 deps
-    - name: all-except-generated
+      run: make TIMED=1 TIMING=1 -j2 deps
+    - name: all-except-generated-and-js-of-ocaml
       shell: alpine.sh {0}
-      run: make -j2 all-except-generated
+      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@v3
+      with:
+        name: standalone-${{ matrix.alpine }}
+        path: dist/fiat_crypto
+#    - name: upload standalone js files
+#      uses: actions/upload-artifact@v3
+#      with:
+#        name: standalone-html-${{ matrix.alpine }}
+#        path: fiat-html
+    - name: upload OCaml files
+      uses: actions/upload-artifact@v3
+      with:
+        name: ExtractionOCaml-${{ matrix.alpine }}
+        path: src/ExtractionOCaml
+      if: always ()
+#    - name: upload js_of_ocaml files
+#      uses: actions/upload-artifact@v3
+#      with:
+#        name: ExtractionJsOfOCaml-${{ matrix.alpine }}
+#        path: src/ExtractionJsOfOCaml
+#      if: always ()
     - name: generated-files
-      if: github.event_name == 'pull_request' || ${{ matrix.env.VERSION }} != 'master'
       shell: alpine.sh {0}
-      run: make -j2 generated-files
+      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@v3
+      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@v3
+      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@v3
+      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@v3
+      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]
+    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' }}