Provide standalone binaries

Fixes #1724 Note that we keep the non-unified binaries (and use them to build generated files) to avoid OOMs on Coq's CI. It's unfortunate that compilation is so slow here, taking almost an hour on my machine just to extract and compile the various binaries. <details><summary>Timing Diff</summary> <p> ``` Time | Peak Mem | File Name ---------------------------------------------------------------------------------- 53m02.47s | 2463008 ko | Total Time / Peak Mem ---------------------------------------------------------------------------------- 2m21.70s | 2462928 ko | ExtractionOCaml/fiat_crypto 2m19.85s | 2463008 ko | ExtractionOCaml/bedrock2_fiat_crypto 1m53.82s | 1863716 ko | ExtractionOCaml/solinas_reduction 1m36.75s | 2462904 ko | ExtractionOCaml/with_bedrock2_fiat_crypto 1m33.30s | 2316820 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml 1m30.98s | 2300660 ko | ExtractionOCaml/fiat_crypto.ml 1m30.25s | 2075840 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery 1m26.51s | 2074640 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery 1m25.26s | 1829432 ko | ExtractionOCaml/word_by_word_montgomery 1m22.38s | 1780504 ko | ExtractionOCaml/bedrock2_unsaturated_solinas 1m20.72s | 2147524 ko | ExtractionOCaml/bedrock2_solinas_reduction 1m20.62s | 2336764 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml 1m18.57s | 1416332 ko | ExtractionOCaml/with_bedrock2_base_conversion 1m16.74s | 1469000 ko | ExtractionOCaml/bedrock2_dettman_multiplication 1m14.80s | 1780196 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas 1m14.67s | 1415232 ko | ExtractionOCaml/base_conversion 1m08.91s | 1416276 ko | ExtractionOCaml/bedrock2_base_conversion 1m08.90s | 1415436 ko | ExtractionOCaml/dettman_multiplication 1m07.90s | 1415368 ko | ExtractionOCaml/saturated_solinas 1m07.63s | 1525784 ko | ExtractionOCaml/unsaturated_solinas 1m07.23s | 1449720 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication 1m07.09s | 1447196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas 1m07.02s | 1439752 ko | ExtractionOCaml/bedrock2_saturated_solinas 1m06.29s | 1448860 ko | ExtractionOCaml/with_bedrock2_solinas_reduction 1m05.35s | 2190452 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml 1m03.87s | 2137192 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml 1m01.18s | 2137308 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml 0m58.53s | 2057100 ko | ExtractionOCaml/solinas_reduction.ml 0m56.27s | 2063328 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml 0m55.76s | 1836424 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml 0m55.38s | 2030208 ko | ExtractionOCaml/word_by_word_montgomery.ml 0m52.90s | 1413320 ko | ExtractionOCaml/perf_unsaturated_solinas 0m51.44s | 2063536 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml 0m51.16s | 1950720 ko | ExtractionOCaml/bedrock2_base_conversion.ml 0m50.96s | 1989736 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml 0m49.61s | 1936244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml 0m49.39s | 1936412 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml 0m49.38s | 1753040 ko | ExtractionOCaml/perf_unsaturated_solinas.ml 0m48.72s | 1938204 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml 0m48.29s | 1952524 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml 0m48.16s | 1938444 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml 0m47.28s | 1962520 ko | ExtractionOCaml/unsaturated_solinas.ml 0m46.15s | 1823484 ko | ExtractionOCaml/base_conversion.ml 0m42.74s | 1413036 ko | ExtractionOCaml/perf_word_by_word_montgomery 0m41.95s | 1882704 ko | ExtractionOCaml/dettman_multiplication.ml 0m38.36s | 1846056 ko | ExtractionOCaml/saturated_solinas.ml 0m04.57s | 1035968 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo 0m00.93s | 106556 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi 0m00.90s | 102844 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi 0m00.89s | 103608 ko | ExtractionOCaml/dettman_multiplication.cmi 0m00.87s | 105352 ko | ExtractionOCaml/unsaturated_solinas.cmi 0m00.84s | 102728 ko | ExtractionOCaml/fiat_crypto.cmi 0m00.83s | 103608 ko | ExtractionOCaml/saturated_solinas.cmi 0m00.83s | 103844 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi 0m00.81s | 102720 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi 0m00.80s | 103684 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi 0m00.76s | 102640 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi 0m00.76s | 107620 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi 0m00.75s | 102300 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi 0m00.75s | 103592 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi 0m00.75s | 102900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi 0m00.74s | 102780 ko | ExtractionOCaml/bedrock2_base_conversion.cmi 0m00.72s | 103088 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi 0m00.71s | 105644 ko | ExtractionOCaml/word_by_word_montgomery.cmi 0m00.70s | 103272 ko | ExtractionOCaml/base_conversion.cmi 0m00.69s | 103100 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi 0m00.67s | 102580 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi 0m00.67s | 103236 ko | ExtractionOCaml/solinas_reduction.cmi 0m00.42s | 58808 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi 0m00.39s | 60084 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi ``` </p> </details>
mit-plv · Nov 15, 2023 · 4964ba1 · 4964ba1
1 parent 4f53772
commit 4964ba1
Show file tree

Hide file tree

Showing 20 changed files with 385 additions and 244 deletions.
diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml
@@ -65,14 +65,14 @@ jobs:
         name: generated-files-${{ matrix.alpine }}
         path: generated-files.tgz
       if: ${{ failure() }}
-    - name: package-standalone-ocaml
+    - name: install-standalone-unified-ocaml
       shell: alpine.sh {0}
-      run: make package-standalone-ocaml
+      run: make install-standalone-unified-ocaml BINDIR=dist
     - name: upload standalone files
       uses: actions/upload-artifact@v3
       with:
         name: standalone-${{ matrix.alpine }}
-        path: standalone.tar.gz
+        path: dist/fiat_crypto
     - name: upload OCaml files
       uses: actions/upload-artifact@v3
       with:
@@ -112,32 +112,25 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-${{ matrix.alpine }}
-        path: dist-${{ matrix.alpine }}/
+        path: dist/
     - name: List files
-      run: find dist-edge
-    - name: Rename files
-      run: |
-        mkdir dist
-        mv dist-${{ matrix.alpine }}/standalone.tar.gz dist/fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz
-        find dist
-        tar -tvf dist/fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz
-    - name: Unpack files
-      run: |
-        cd dist
-        tar -xzvf fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz
-        ls -la .
+      run: find dist
+    - run: chmod +x dist/fiat_crypto
     - name: Test files (host)
       run: |
         cd dist
-        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
-          echo "::group::file $prog"
-          file $prog
-          echo "::endgroup::"
-          echo "::group::ldd $prog"
-          ldd $prog || true
-          echo "::endgroup::"
+        echo "::group::file fiat_crypto"
+        file fiat_crypto
+        echo "::endgroup::"
+        echo "::group::ldd fiat_crypto"
+        ldd fiat_crypto || true
+        echo "::endgroup::"
+        echo "::group::fiat_crypto"
+        ./fiat_crypto -h
+        echo "::endgroup::"
+        for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do
           echo "::group::$prog"
-          ./$prog -h
+          ./fiat_crypto $prog -h
           echo "::endgroup::"
         done
     - uses: jirutka/setup-alpine@v1
@@ -148,9 +141,12 @@ jobs:
       shell: alpine.sh {0}
       run: |
         cd dist
-        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
+        echo "::group::fiat_crypto"
+        ./fiat_crypto -h
+        echo "::endgroup::"
+        for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do
           echo "::group::$prog"
-          ./$prog -h
+          ./fiat_crypto $prog -h
           echo "::endgroup::"
         done
 
@@ -168,21 +164,19 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-edge
-        path: dist-edge/
+        path: dist/
     - name: List files
-      run: find dist-edge
+      run: find dist
     - name: Unpack files
       run: |
-        mkdir dist
         echo "::group::find arch"
-        ( cd dist-edge && tar -xzvf standalone.tar.gz )
-        arch="$(etc/ci/find-arch.sh dist-edge/word_by_word_montgomery "unknown")"
+        arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")"
         tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_Linux_${arch}.tar.gz"
+        fname="Fiat-Cryptography_${tag}_Linux_${arch}"
         echo "$fname"
-        mv dist-edge/standalone.tar.gz "dist/$fname"
+        mv dist/fiat_crypto "dist/$fname"
         find dist
-        tar -tvf "dist/$fname"
+        file "dist/$fname"
     - name: Upload artifacts to GitHub Release
       env:
         GITHUB_TOKEN: ${{ github.token }}

diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
@@ -57,14 +57,14 @@ jobs:
         name: generated-files-${{ matrix.env.DEBIAN }}
         path: generated-files.tgz
       if: ${{ failure() }}
-    - name: package-standalone-ocaml
+    - name: install-standalone-unified-ocaml
       shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh package-standalone-ocaml
+      run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist
     - name: upload standalone files
       uses: actions/upload-artifact@v3
       with:
         name: standalone-${{ matrix.env.DEBIAN }}
-        path: standalone.tar.gz
+        path: dist/fiat_crypto
     - name: upload OCaml files
       uses: actions/upload-artifact@v3
       with:
@@ -103,32 +103,24 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-${{ matrix.debian }}
-        path: dist-${{ matrix.debian }}/
+        path: dist/
     - name: List files
-      run: find dist-${{ matrix.debian }}
-    - name: Rename files
-      run: |
-        mkdir dist
-        mv dist-${{ matrix.debian }}/standalone.tar.gz dist/fiat-crypto-${{ matrix.debian }}.tar.gz
-        find dist
-        tar -tvf dist/fiat-crypto-${{ matrix.debian }}.tar.gz
-    - name: Unpack Files
-      run: |
-        cd dist
-        tar -xzvf fiat-crypto-${{ matrix.debian }}.tar.gz
-        ls -la .
+      run: find dist
     - name: Test files (host)
       run: |
         cd dist
-        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
-          echo "::group::file $prog"
-          file $prog
-          echo "::endgroup::"
-          echo "::group::ldd $prog"
-          ldd $prog
-          echo "::endgroup::"
+        echo "::group::file fiat_crypto"
+        file fiat_crypto
+        echo "::endgroup::"
+        echo "::group::ldd fiat_crypto"
+        ldd fiat_crypto
+        echo "::endgroup::"
+        echo "::group::fiat_crypto"
+        ./fiat_crypto -h
+        echo "::endgroup::"
+        for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do
           echo "::group::$prog"
-          ./$prog -h
+          ./fiat_crypto $prog -h
           echo "::endgroup::"
         done
     - name: setup Debian chroot
@@ -137,15 +129,18 @@ jobs:
       shell: in-debian-chroot.sh {0}
       run: |
         cd dist
-        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
-          echo "::group::file $prog"
-          file $prog
-          echo "::endgroup::"
-          echo "::group::ldd $prog"
-          ldd $prog
-          echo "::endgroup::"
+        echo "::group::file fiat_crypto"
+        file fiat_crypto
+        echo "::endgroup::"
+        echo "::group::ldd fiat_crypto"
+        ldd fiat_crypto
+        echo "::endgroup::"
+        echo "::group::fiat_crypto"
+        ./fiat_crypto -h
+        echo "::endgroup::"
+        for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do
           echo "::group::$prog"
-          ./$prog -h
+          ./fiat_crypto $prog -h
           echo "::endgroup::"
         done
 
@@ -163,21 +158,20 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-sid
-        path: dist-sid/
+        path: dist/
     - name: List files
-      run: find dist-sid
+      run: find dist
+    - run: chmod +x dist/fiat_crypto
     - name: Unpack files
       run: |
         mkdir dist
         echo "::group::find arch"
-        ( cd dist-sid && tar -xzvf standalone.tar.gz )
-        arch="$(etc/ci/find-arch.sh dist-sid/word_by_word_montgomery "unknown")"
+        arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")"
         tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_Linux_debian_sid_${arch}.tar.gz"
+        fname="Fiat-Cryptography_${tag}_Linux_debian_sid_${arch}"
         echo "$fname"
-        mv dist-sid/standalone.tar.gz "dist/$fname"
+        mv dist/fiat_crypto "dist/$fname"
         find dist
-        tar -tvf "dist/$fname"
 #    - name: Upload artifacts to GitHub Release
 #      env:
 #        GITHUB_TOKEN: ${{ github.token }}

diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml
@@ -68,13 +68,13 @@ jobs:
         name: generated-files-${{ matrix.env.COQ_VERSION }}
         path: generated-files.tgz
       if: ${{ failure() }}
-    - name: package-standalone-ocaml
-      run: etc/ci/github-actions-make.sh -f Makefile.standalone package-standalone-ocaml
+    - 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: standalone.tar.gz
+        path: dist/fiat_crypto
     - name: upload OCaml files
       uses: actions/upload-artifact@v3
       with:
@@ -151,32 +151,25 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-docker-coq-${{ matrix.docker-coq-version }}
-        path: dist-docker-coq-${{ matrix.docker-coq-version }}/
+        path: dist/
     - name: List files
-      run: find dist-docker-coq-${{ matrix.docker-coq-version }}
-    - name: Rename files
-      run: |
-        mkdir dist
-        mv dist-docker-coq-${{ matrix.docker-coq-version }}/standalone.tar.gz dist/fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz
-        find dist
-        tar -tvf dist/fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz
-    - name: Unpack Files
-      run: |
-        cd dist
-        tar -xzvf fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz
-        ls -la .
+      run: find dist
+    - run: chmod +x dist/fiat_crypto
     - name: Test files (host)
       run: |
         cd dist
-        for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
-          echo "::group::file $prog"
-          file $prog
-          echo "::endgroup::"
-          echo "::group::ldd $prog"
-          ldd $prog
-          echo "::endgroup::"
+        echo "::group::file fiat_crypto"
+        file fiat_crypto
+        echo "::endgroup::"
+        echo "::group::ldd fiat_crypto"
+        ldd fiat_crypto
+        echo "::endgroup::"
+        echo "::group::fiat_crypto"
+        ./fiat_crypto -h
+        echo "::endgroup::"
+        for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do
           echo "::group::$prog"
-          ./$prog -h
+          ./fiat_crypto $prog -h
           echo "::endgroup::"
         done
     - name: Test files (container)
@@ -190,15 +183,18 @@ jobs:
           sudo apt-get install -y file
           echo "::endgroup::"
           cd dist
-          for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do
-            echo "::group::file $prog"
-            file $prog
-            echo "::endgroup::"
-            echo "::group::ldd $prog"
-            ldd $prog
-            echo "::endgroup::"
+          echo "::group::file fiat_crypto"
+          file fiat_crypto
+          echo "::endgroup::"
+          echo "::group::ldd fiat_crypto"
+          ldd fiat_crypto
+          echo "::endgroup::"
+          echo "::group::fiat_crypto"
+          ./fiat_crypto -h
+          echo "::endgroup::"
+          for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do
             echo "::group::$prog"
-            ./$prog -h
+            ./fiat_crypto $prog -h
             echo "::endgroup::"
           done
 
@@ -216,21 +212,18 @@ jobs:
       uses: actions/download-artifact@v3
       with:
         name: standalone-docker-coq-dev
-        path: dist-docker-coq-dev/
+        path: dist/
     - name: List files
-      run: find dist-docker-coq-dev
+      run: find dist
     - name: Unpack files
       run: |
-        mkdir dist
         echo "::group::find arch"
-        ( cd dist-docker-coq-dev && tar -xzvf standalone.tar.gz )
-        arch="$(etc/ci/find-arch.sh dist-docker-coq-dev/word_by_word_montgomery "unknown")"
+        arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")"
         tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}.tar.gz"
+        fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}"
         echo "$fname"
-        mv dist-docker-coq-dev/standalone.tar.gz "dist/$fname"
+        mv dist/fiat_crypto "dist/$fname"
         find dist
-        tar -tvf "dist/$fname"
 #    - name: Upload artifacts to GitHub Release
 #      env:
 #        GITHUB_TOKEN: ${{ github.token }}