Provide standalone binaries

Fixes #1724 <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 14, 2023 · 4180160 · 4180160
1 parent 4f53772
commit 4180160
Show file tree

Hide file tree

Showing 19 changed files with 380 additions and 239 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 }}