WIP towards #1724

mit-plv · Nov 14, 2023 · c4ca3e1 · c4ca3e1
1 parent 4f53772
commit c4ca3e1
Show file tree

Hide file tree

Showing 18 changed files with 345 additions and 218 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 }}