Build universal (x86_64+arm64) binaries for MacOS

.github/workflows/coq-macos.yml

@@ -14,10 +14,20 @@ on:
 jobs:
   build:
 
-    runs-on: macOS-11
+    strategy:
+      fail-fast: false
+      matrix:
+        # macOS 11, 12, 13 are x86_64; macOS 14 is arm64
+        include:
+        - os: { name: 'macOS 11', arch: 'x86_64', runs-on: 'macos-11' } # move to macOS-12 when 11 is removed
+          ocaml-compiler: '4.11.1'
+        - os: { name: 'macOS 14', arch: 'arm64' , runs-on: 'macos-14' }
+          ocaml-compiler: '4.14.2'
+
+    runs-on: ${{ matrix.os.runs-on }}
 
     concurrency:
-      group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+      group: ${{ github.workflow }}-${{ matrix.os.runs-on }}-${{ matrix.ocaml-compiler }}-${{ github.head_ref || github.run_id }}
       cancel-in-progress: true
 
     env:
@@ -28,7 +38,7 @@ jobs:
       OPAMYES: "true"
       OPAMCONFIRMLEVEL: "unsafe-yes"
 
-    name: macos
+    name: ${{ matrix.os.name }} (${{ matrix.os.arch }})
 
     steps:
     - uses: actions/checkout@v4
@@ -37,7 +47,7 @@ jobs:
     - name: Set up OCaml
       uses: ocaml/setup-ocaml@v2
       with:
-        ocaml-compiler: 4.11.1
+        ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
     - name: Install system dependencies
       run: brew install gnu-time gnu-sed coreutils grep
@@ -48,34 +58,41 @@ jobs:
       run: etc/ci/describe-system-config-macos.sh
     - name: deps
       run: opam exec -- etc/ci/github-actions-make.sh -j2 deps
+    - name: all-except-js-of-ocaml
+      run: opam exec -- etc/ci/github-actions-make.sh -j2 all-except-js-of-ocaml
+    - name: pre-standalone-extracted
+      run: opam exec -- etc/ci/github-actions-make.sh -j2 pre-standalone-extracted
     - name: all
       run: opam exec -- etc/ci/github-actions-make.sh -j2 all
+      if: ${{ matrix.os.arch != 'arm64' }}
+      # js_of_ocaml is too heavy for M1 GH Action runners which have only 7GB RAM, cf https://github.com/ocsigen/js_of_ocaml/issues/1612, https://docs.github.com/en/actions/using-github-hosted-runners/about-github-hosted-runners/about-github-hosted-runners#standard-github-hosted-runners-for-public-repositories
     - name: install-standalone-unified-ocaml
       run: opam exec -- etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist
     - name: install-standalone-js-of-ocaml
       run: opam exec -- etc/ci/github-actions-make.sh install-standalone-js-of-ocaml
+      if: ${{ matrix.os.arch != 'arm64' }}
     - name: only-test-amd64-files-lite
       run: opam exec -- etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
 
     - name: upload OCaml files
       uses: actions/upload-artifact@v3
       with:
-        name: ExtractionOCaml
+        name: ExtractionOCaml-${{ matrix.os.arch }}
         path: src/ExtractionOCaml
     - name: upload js_of_ocaml files
       uses: actions/upload-artifact@v3
       with:
-        name: ExtractionJsOfOCaml
+        name: ExtractionJsOfOCaml-${{ matrix.os.arch }}
         path: src/ExtractionJsOfOCaml
     - name: upload standalone files
       uses: actions/upload-artifact@v3
       with:
-        name: standalone-macos
+        name: standalone-macos-${{ matrix.os.arch }}
         path: dist/fiat_crypto
     - name: upload standalone js files
       uses: actions/upload-artifact@v3
       with:
-        name: standalone-html-macos
+        name: standalone-html-macos-${{ matrix.os.arch }}
         path: fiat-html
     - name: install
       run: opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
@@ -90,7 +107,7 @@ jobs:
 #    - name: upload timing and .vo info
 #      uses: actions/upload-artifact@v3
 #      with:
-#        name: build-outputs
+#        name: build-outputs-${{ matrix.os.arch }}
 #        path: .
 #      if: always ()
 #    - name: validate
@@ -99,20 +116,57 @@ jobs:
 #        make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"
 #      if: github.event_name != 'pull_request'
 
-  test-standalone:
+  combine-standalone:
     runs-on: macos-latest
     needs: build
     steps:
     - uses: actions/checkout@v4
-    - name: Download standalone MacOS
+    - name: Download standalone MacOS x86_64
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-macos-x86_64
+        path: dist-x86_64/
+    - name: Download standalone MacOS arm64
       uses: actions/download-artifact@v3
+      with:
+        name: standalone-macos-arm64
+        path: dist-arm64/
+    - name: Create universal binary
+      run: |
+        mkdir -p dist
+        lipo -create -output dist/fiat_crypto dist-x86_64/fiat_crypto dist-arm64/fiat_crypto
+    - name: upload universal binary
+      uses: actions/upload-artifact@v3
       with:
         name: standalone-macos
+        path: dist/fiat_crypto
+
+  test-standalone:
+    strategy:
+      fail-fast: false
+      matrix:
+        arch: ['', '-x86_64', '-arm64']
+        os: ['macos-11', 'macos-12', 'macos-13', 'macos-14', 'macos-latest']
+        exclude:
+          - os: 'macos-11'
+            arch: '-arm64'
+          - os: 'macos-12'
+            arch: '-arm64'
+          - os: 'macos-13'
+            arch: '-arm64'
+    runs-on: ${{ matrix.os }}
+    needs: [build, combine-standalone]
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone MacOS${{ matrix.arch }}
+      uses: actions/download-artifact@v3
+      with:
+        name: standalone-macos${{ matrix.arch }}
         path: dist/
     - name: List files
       run: find dist
     - run: chmod +x dist/fiat_crypto
-    - name: Test files
+    - name: Test files (${{ matrix.arch }} on ${{ matrix.os }})
       run: |
         echo "::group::file fiat_crypto"
         file dist/fiat_crypto
@@ -126,19 +180,23 @@ jobs:
         etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
 
   publish-standalone:
+    strategy:
+      fail-fast: false
+      matrix:
+        arch: ['', '-x86_64', '-arm64']
     runs-on: ubuntu-latest
-    needs: build
+    needs: [build, combine-standalone]
     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 MacOS
+    - name: Download standalone MacOS${{ matrix.arch }}
       uses: actions/download-artifact@v3
       with:
-        name: standalone-macos
+        name: standalone-macos${{ matrix.arch }}
         path: dist/
     - name: List files
       run: find dist
@@ -150,7 +208,7 @@ jobs:
         echo "$fname"
         mv dist/fiat_crypto "dist/$fname"
         find dist
-    - name: Upload artifacts to GitHub Release
+    - name: Upload macOS-${{ matrix.arch }} artifacts to GitHub Release
       env:
         GITHUB_TOKEN: ${{ github.token }}
       # Upload to GitHub Release using the `gh` CLI.

etc/ci/find-arch.sh

@@ -33,21 +33,47 @@ else
     group() { run "$@"; }
 fi
 
+default_arch() {
+    if [ -z "$default" ]; then
+        printf "%s\n" "$1" | awk '{print $NF}'
+    else
+        printf "%s\n" "$default"
+    fi
+    >&2 echo "::warning::Unknown architecture ${file_info} (using ${arch})"
+}
+
+
 >&2 group file "$fname"
 >&2 group otool -L "$fname" || true
 >&2 group lipo -info "$fname" || true
 file_info="$(file "$fname" 2>&1)"
+
 case "${file_info}" in
+    *"Mach-O universal"*)
+        arches=($(printf '%s' "${file_info}" | grep -o 'Mach-O universal.*' | grep -o '\[[^]:]*' | sed 's/^\[//g'))
+        if [ "${#arches[@]}" -eq 1 ]; then
+            arch="${arches[0]}"
+        elif [ "${#arches[@]}" -gt 1 ]; then
+            arch="universal"
+            if [[ " ${arches[*]} " =~ " arm64 " ]] && [[ " ${arches[*]} " =~ " x86_64 " ]]; then
+                :
+            else
+                for cur_arch in "${arches[@]}"; do
+                    arch="${arch}_${cur_arch}"
+                done
+            fi
+        else
+            arch="$(default_arch "${file_info}")"
+        fi
+        ;;
     *x86_64*|*x86-64*)
         arch=x86_64
         ;;
+    *arm64*)
+        arch=arm64
+        ;;
     *)
-        if [ -z "$default" ]; then
-            arch="$(printf "%s\n" "${file_info}" | awk '{print $NF}')"
-        else
-            arch="$default"
-        fi
-        >&2 echo "::warning::Unknown architecture ${file_info} (using ${arch})"
+        arch="$(default_arch "${file_info}")"
         ;;
 esac