diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml
deleted file mode 100644
index 6a5f228892f..00000000000
--- a/.github/workflows/coq-alpine.yml
+++ /dev/null
@@ -1,213 +0,0 @@
-name: CI (Coq, Alpine)
-
-on:
-  push:
-    branches: [ master ]
-  pull_request:
-  merge_group:
-  workflow_dispatch:
-  release:
-    types: [published]
-  schedule:
-    - cron: '0 0 1 * *'
-
-jobs:
-  build:
-
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-        - alpine: 'edge'
-#        - alpine: 'latest-stable'
-
-    runs-on: ubuntu-latest
-    name: alpine-${{ matrix.alpine }}
-
-    concurrency:
-      group: ${{ github.workflow }}-alpine-${{ matrix.alpine }}-${{ github.head_ref || github.run_id }}
-      cancel-in-progress: true
-
-    steps:
-    - 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 bash sudo
-    - 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
-    - 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 TIMED=1 TIMING=1 -j2 deps
-    - name: all-except-generated-and-js-of-ocaml
-      shell: alpine.sh {0}
-      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@v4
-      with:
-        name: standalone-${{ matrix.alpine }}
-        path: dist/fiat_crypto
-#    - name: upload standalone js files
-#      uses: actions/upload-artifact@v4
-#      with:
-#        name: standalone-html-${{ matrix.alpine }}
-#        path: fiat-html
-    - name: upload OCaml files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionOCaml-${{ matrix.alpine }}
-        path: src/ExtractionOCaml
-      if: always ()
-#    - name: upload js_of_ocaml files
-#      uses: actions/upload-artifact@v4
-#      with:
-#        name: ExtractionJsOfOCaml-${{ matrix.alpine }}
-#        path: src/ExtractionJsOfOCaml
-#      if: always ()
-    - name: generated-files
-      shell: alpine.sh {0}
-      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@v4
-      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@v4
-      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@v4
-      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@v4
-      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, 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' }}
diff --git a/.github/workflows/coq-archlinux.yml b/.github/workflows/coq-archlinux.yml
deleted file mode 100644
index 0a3f3abc328..00000000000
--- a/.github/workflows/coq-archlinux.yml
+++ /dev/null
@@ -1,184 +0,0 @@
-name: CI (Coq, Arch Linux)
-
-on:
-  push:
-    branches: [ master ]
-  pull_request:
-  merge_group:
-  workflow_dispatch:
-  release:
-    types: [published]
-  schedule:
-    - cron: '0 0 1 * *'
-
-jobs:
-  build:
-
-    runs-on: ubuntu-latest
-    container: archlinux
-    name: archlinux
-
-    concurrency:
-      group: ${{ github.workflow }}-archlinux-${{ github.head_ref || github.run_id }}
-      cancel-in-progress: true
-
-    steps:
-    - name: Install system dependencies
-      run: |
-        pacman --noconfirm -Syu base-devel git make python3 which jq ghc ghc-static time diffutils coq ocaml-zarith --needed
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - name: work around coq issue 15663
-      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
-    - name: Work around https://github.com/actions/checkout/issues/766
-      run: git config --global --add safe.directory "*"
-    - name: chroot build params
-      run: etc/ci/describe-system-config.sh
-    - name: make deps
-      run: etc/ci/github-actions-make.sh -j2 deps
-    - name: all-except-generated-and-js-of-ocaml
-      run: etc/ci/github-actions-make.sh -j2 all-except-generated-and-js-of-ocaml
-    - name: generated-files
-      run: etc/ci/github-actions-make.sh -j2 generated-files
-    - run: tar -czvf generated-files.tgz fiat-*/
-      if: ${{ failure() }}
-    - name: upload generated files
-      uses: actions/upload-artifact@v4
-      with:
-        name: generated-files-archlinux
-        path: generated-files.tgz
-      if: ${{ failure() }}
-    - name: install-standalone-unified-ocaml
-      run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist
-    #- name: standalone-js-of-ocaml
-    #  run: etc/ci/github-actions-make.sh -j2 standalone-js-of-ocaml
-    #- name: install-standalone-js-of-ocaml
-    #  run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml
-    - name: upload standalone files
-      uses: actions/upload-artifact@v4
-      with:
-        name: standalone-archlinux
-        path: dist/fiat_crypto
-    #- name: upload standalone js files
-    #  uses: actions/upload-artifact@v4
-    #  with:
-    #    name: standalone-html-archlinux
-    #    path: fiat-html
-    - name: upload OCaml files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionOCaml-archlinux
-        path: src/ExtractionOCaml
-      if: always ()
-    #- name: upload js_of_ocaml files
-    #  uses: actions/upload-artifact@v4
-    #  with:
-    #    name: ExtractionJsOfOCaml-archlinux
-    #    path: src/ExtractionJsOfOCaml
-    #  if: always ()
-    - name: standalone-haskell
-      run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS'
-    - name: upload Haskell files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionHaskell-archlinux
-        path: src/ExtractionHaskell
-      if: always ()
-    - name: only-test-amd64-files-lite
-      run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
-    - name: install
-      run: etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
-    - name: install-without-bedrock2
-      run: etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
-    - name: install-dev
-      run: etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
-    - name: display timing info
-      run: cat time-of-build-pretty.log
-    - name: display per-line timing info
-      run: etc/ci/github-actions-display-per-line-timing.sh
-
-  test-standalone:
-    runs-on: ubuntu-latest
-    container: archlinux
-    needs: build
-    steps:
-    - name: Install system dependencies
-      run: |
-        pacman --noconfirm -Syu git --needed
-    - uses: actions/checkout@v4
-    - name: Download standalone archlinux
-      uses: actions/download-artifact@v4
-      with:
-        name: standalone-archlinux
-        path: dist/
-    - name: List files
-      run: find dist
-    - run: chmod +x dist/fiat_crypto
-    - name: Test files (container)
-      run: |
-        echo "::group::file fiat_crypto"
-        file dist/fiat_crypto
-        echo "::endgroup::"
-        echo "::group::ldd fiat_crypto"
-        ldd dist/fiat_crypto
-        echo "::endgroup::"
-        etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
-
-  publish-standalone-dry-run:
-    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 archlinux
-      uses: actions/download-artifact@v4
-      with:
-        name: standalone-archlinux
-        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_archlinux_${arch}"
-        echo "$fname"
-        mv dist/fiat_crypto "dist/$fname"
-        find dist
-#    - 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' }}
-
-  archlinux-check-all:
-    runs-on: ubuntu-latest
-    needs: [build, test-standalone, publish-standalone-dry-run]
-    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-dry-run passed'
-      if: ${{ needs.publish-standalone-dry-run.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-dry-run failed' && false
-      if: ${{ needs.publish-standalone-dry-run.result != 'success' }}
diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
deleted file mode 100644
index 34883bc00c6..00000000000
--- a/.github/workflows/coq-debian.yml
+++ /dev/null
@@ -1,211 +0,0 @@
-name: CI (Coq, Debian)
-
-on:
-  push:
-    branches: [ master , sp2019latest ]
-  pull_request:
-  merge_group:
-  workflow_dispatch:
-  release:
-    types: [published]
-  schedule:
-    - cron: '0 0 1 * *'
-
-jobs:
-  build:
-
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-        - env: { DEBIAN: "sid" }
-        #- env: { DEBIAN: "bookworm" }# restore once 8.17 lands in Debian stable
-
-    runs-on: 'ubuntu-22.04'
-    env: ${{ matrix.env }}
-    name: debian-${{ matrix.env.DEBIAN }}
-
-    concurrency:
-      group: ${{ github.workflow }}-${{ matrix.env.DEBIAN }}-${{ github.head_ref || github.run_id }}
-      cancel-in-progress: true
-
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - name: setup Debian chroot
-      run: etc/ci/setup-debian-chroot.sh "$DEBIAN"
-    - name: host build params
-      run: etc/ci/describe-system-config.sh
-    - name: chroot build params
-      shell: in-debian-chroot.sh {0}
-      run: CI=1 etc/ci/describe-system-config.sh
-    - name: make deps
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 deps
-    - name: all-except-generated-and-js-of-ocaml
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 all-except-generated-and-js-of-ocaml
-    - name: generated-files
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 generated-files
-    - run: tar -czvf generated-files.tgz fiat-*/
-      if: ${{ failure() }}
-    - name: upload generated files
-      uses: actions/upload-artifact@v4
-      with:
-        name: generated-files-${{ matrix.env.DEBIAN }}
-        path: generated-files.tgz
-      if: ${{ failure() }}
-    - name: install-standalone-unified-ocaml
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist
-    - name: standalone-js-of-ocaml
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 standalone-js-of-ocaml
-    - name: install-standalone-js-of-ocaml
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml
-    - name: upload standalone files
-      uses: actions/upload-artifact@v4
-      with:
-        name: standalone-${{ matrix.env.DEBIAN }}
-        path: dist/fiat_crypto
-    - name: upload standalone js files
-      uses: actions/upload-artifact@v4
-      with:
-        name: standalone-html-${{ matrix.env.DEBIAN }}
-        path: fiat-html
-    - name: upload OCaml files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionOCaml-${{ matrix.env.DEBIAN }}
-        path: src/ExtractionOCaml
-      if: always ()
-    - name: upload js_of_ocaml files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionJsOfOCaml-${{ matrix.env.DEBIAN }}
-        path: src/ExtractionJsOfOCaml
-      if: always ()
-    - name: standalone-haskell
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS'
-    - name: upload Haskell files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionHaskell-${{ matrix.env.DEBIAN }}
-        path: src/ExtractionHaskell
-      if: always ()
-    - name: only-test-amd64-files-lite
-      shell: in-debian-chroot.sh {0}
-      run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
-    - name: install
-      shell: in-debian-chroot.sh {0}
-      run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
-    - name: install-without-bedrock2
-      shell: in-debian-chroot.sh {0}
-      run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
-    - name: install-dev
-      shell: in-debian-chroot.sh {0}
-      run: sudo etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
-    - name: display timing info
-      run: cat time-of-build-pretty.log
-    - name: display per-line timing info
-      run: etc/ci/github-actions-display-per-line-timing.sh
-
-  test-standalone:
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-        - debian: sid
-        #- debian: bookworm # restore once 8.17 lands in Debian stable
-    runs-on: ubuntu-latest
-    needs: build
-    steps:
-    - uses: actions/checkout@v4
-    - name: Download standalone ${{ matrix.debian }}
-      uses: actions/download-artifact@v4
-      with:
-        name: standalone-${{ matrix.debian }}
-        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
-        echo "::endgroup::"
-        etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
-    - name: setup Debian chroot
-      run: etc/ci/setup-debian-chroot.sh "${{ matrix.debian }}"
-    - name: Test files (container)
-      shell: in-debian-chroot.sh {0}
-      run: |
-        echo "::group::file fiat_crypto"
-        file dist/fiat_crypto
-        echo "::endgroup::"
-        echo "::group::ldd fiat_crypto"
-        ldd dist/fiat_crypto
-        echo "::endgroup::"
-        etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
-
-  publish-standalone-dry-run:
-    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 sid
-      uses: actions/download-artifact@v4
-      with:
-        name: standalone-sid
-        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_debian_sid_${arch}"
-        echo "$fname"
-        mv dist/fiat_crypto "dist/$fname"
-        find dist
-#    - 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' }}
-
-  debian-check-all:
-    runs-on: ubuntu-latest
-    needs: [build, test-standalone, publish-standalone-dry-run]
-    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-dry-run passed'
-      if: ${{ needs.publish-standalone-dry-run.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-dry-run failed' && false
-      if: ${{ needs.publish-standalone-dry-run.result != 'success' }}
diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml
deleted file mode 100644
index a6fc7379528..00000000000
--- a/.github/workflows/coq-macos.yml
+++ /dev/null
@@ -1,218 +0,0 @@
-name: CI (Coq, MacOS)
-
-on:
-  push:
-    branches: [ master , sp2019latest , v8.6 , v8.8 , v8.10 ]
-  pull_request:
-  merge_group:
-  workflow_dispatch:
-  release:
-    types: [published]
-  schedule:
-    - cron: '0 0 1 * *'
-
-jobs:
-  build:
-
-    runs-on: macOS-11
-
-    concurrency:
-      group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
-      cancel-in-progress: true
-
-    env:
-      NJOBS: "2"
-      COQ_VERSION: "8.18.0" # pick a version not tested on other platforms
-      COQCHKEXTRAFLAGS: ""
-      SKIP_BEDROCK2: "0"
-
-    name: macos
-
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - name: Set up OCaml
-      uses: ocaml/setup-ocaml@v2
-      with:
-        ocaml-compiler: 4.11.1
-
-    - name: Install system dependencies
-      run: |
-        set -e
-        brew install gnu-time coreutils
-
-    - name: Install Coq
-      run: |
-        set -e
-        eval $(opam env)
-        opam update
-        opam pin add coq ${COQ_VERSION}
-      env:
-        OPAMYES: "true"
-        OPAMCONFIRMLEVEL: "unsafe-yes"
-
-    - name: Install js_of_ocaml
-      run: |
-        set -e
-        eval $(opam env)
-        opam install js_of_ocaml
-      env:
-        OPAMYES: "true"
-        OPAMCONFIRMLEVEL: "unsafe-yes"
-
-    - name: echo build params
-      run: |
-        eval $(opam env)
-        etc/ci/describe-system-config-macos.sh
-    - name: deps
-      run: |
-        eval $(opam env)
-        etc/ci/github-actions-make.sh -j2 deps
-    - name: all
-      run: |
-        eval $(opam env)
-        etc/ci/github-actions-make.sh -j2 all
-
-    - name: install-standalone-unified-ocaml
-      run: |
-        eval $(opam env)
-        etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist
-
-    - name: install-standalone-js-of-ocaml
-      run: |
-        eval $(opam env)
-        etc/ci/github-actions-make.sh install-standalone-js-of-ocaml
-
-    - name: only-test-amd64-files-lite
-      run: |
-        eval $(opam env)
-        etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
-
-    - name: upload OCaml files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionOCaml
-        path: src/ExtractionOCaml
-    - name: upload js_of_ocaml files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionJsOfOCaml
-        path: src/ExtractionJsOfOCaml
-    - name: upload standalone files
-      uses: actions/upload-artifact@v4
-      with:
-        name: standalone-macos
-        path: dist/fiat_crypto
-    - name: upload standalone js files
-      uses: actions/upload-artifact@v4
-      with:
-        name: standalone-html-macos
-        path: fiat-html
-    - name: install
-      run: |
-        eval $(opam env)
-        etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
-    - name: install-without-bedrock2
-      run: |
-        eval $(opam env)
-        etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
-    - name: install-dev
-      run: |
-        eval $(opam env)
-        etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
-    - name: display timing info
-      run: cat time-of-build-pretty.log
-    - name: display per-line timing info
-      run: etc/ci/github-actions-display-per-line-timing.sh
-#    - name: upload timing and .vo info
-#      uses: actions/upload-artifact@v4
-#      with:
-#        name: build-outputs
-#        path: .
-#      if: always ()
-#    - name: validate
-#      run: |
-#        eval $(opam env)
-#        make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"
-#      if: github.event_name != 'pull_request'
-
-  test-standalone:
-    runs-on: macos-latest
-    needs: build
-    steps:
-    - uses: actions/checkout@v4
-    - name: Download standalone MacOS
-      uses: actions/download-artifact@v4
-      with:
-        name: standalone-macos
-        path: dist/
-    - name: List files
-      run: find dist
-    - run: chmod +x dist/fiat_crypto
-    - name: Test files
-      run: |
-        echo "::group::file fiat_crypto"
-        file dist/fiat_crypto
-        echo "::endgroup::"
-        echo "::group::otool -L fiat_crypto"
-        otool -L dist/fiat_crypto
-        echo "::endgroup::"
-        echo "::group::lipo -info fiat_crypto"
-        lipo -info dist/fiat_crypto
-        echo "::endgroup::"
-        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 MacOS
-      uses: actions/download-artifact@v4
-      with:
-        name: standalone-macos
-        path: dist/
-    - name: List files
-      run: find dist
-    - name: Rename files
-      run: |
-        arch="$(etc/ci/find-arch.sh dist/fiat_crypto)"
-        tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_macOS_${arch}"
-        echo "$fname"
-        mv dist/fiat_crypto "dist/$fname"
-        find dist
-    - 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' }}
-
-  macos-check-all:
-    runs-on: ubuntu-latest
-    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' }}
diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml
deleted file mode 100644
index 2dcfc23e568..00000000000
--- a/.github/workflows/coq-windows.yml
+++ /dev/null
@@ -1,238 +0,0 @@
-name: CI (Coq, Windows)
-
-# Note that we must split up each command into a separate step for Windows, because otherwise we don't get error code
-# See also https://github.com/avsm/setup-ocaml/issues/72
-
-on:
-  push:
-    branches: [ master , sp2019latest , v8.6 , v8.8 , v8.10 ]
-  pull_request:
-  merge_group:
-  workflow_dispatch:
-  release:
-    types: [published]
-  schedule:
-    - cron: '0 0 1 * *'
-
-jobs:
-  build:
-
-    runs-on: windows-latest
-    name: windows
-
-    concurrency:
-      group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
-      cancel-in-progress: true
-
-    env:
-      NJOBS: "2"
-      COQ_VERSION: "8.17.0" # minimal major version required for bedrock2 components
-      COQEXTRAFLAGS: "-async-proofs-j 1"
-      COQCHKEXTRAFLAGS: ""
-      OPAMYES: "true"
-      OPAMCONFIRMLEVEL: "unsafe-yes"
-
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        submodules: recursive
-    - name: Setup Python
-      uses: actions/setup-python@v5
-      with:
-        python-version: 3.x
-    - name: Set up OCaml
-      uses: ocaml/setup-ocaml@v2
-      with:
-        ocaml-compiler: 4.11.1
-        opam-repositories: |
-          opam-repository-mingw: https://github.com/ocaml-opam/opam-repository-mingw.git#sunset
-          default: https://github.com/ocaml/opam-repository.git
-    - run: opam depext coq.${{ env.COQ_VERSION }}
-    - run: opam pin add --kind=version coq ${{ env.COQ_VERSION }}
-    - run: opam install js_of_ocaml
-
-    - name: Install System Dependencies
-      run: |
-        %CYGWIN_ROOT%\setup-x86_64.exe -qnNdO -P time,zip
-      shell: cmd
-
-    - name: Work around https://github.com/actions/checkout/issues/766
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'git config --global --add safe.directory "*"'
-      shell: cmd
-
-    - name: echo build params
-      run: |
-        %cd%\etc\ci\describe-system-config-win.bat
-      shell: cmd
-    - name: deps
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} deps'
-      shell: cmd
-    - name: standalone-ocaml
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} standalone-ocaml'
-      shell: cmd
-    - name: install-standalone-unified-ocaml
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist'
-      shell: cmd
-
-    - name: coq
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 coq'
-      shell: cmd
-    - name: all-except-generated-and-js-of-ocaml
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 all-except-generated-and-js-of-ocaml'
-      shell: cmd
-    - name: standalone-js-of-ocaml
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 standalone-js-of-ocaml'
-      shell: cmd
-    - name: install-standalone-js-of-ocaml
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh install-standalone-js-of-ocaml'
-      shell: cmd
-    - name: c-files lite-generated-files
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} c-files lite-generated-files'
-      shell: cmd
-    - name: only-test-amd64-files-lite
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} only-test-amd64-files-lite SLOWEST_FIRST=1'
-      shell: cmd
-    - name: upload OCaml files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionOCaml
-        path: src/ExtractionOCaml
-    - name: upload js_of_ocaml files
-      uses: actions/upload-artifact@v4
-      with:
-        name: ExtractionJsOfOCaml
-        path: src/ExtractionJsOfOCaml
-    - name: upload standalone files
-      uses: actions/upload-artifact@v4
-      with:
-        name: standalone-windows
-        path: dist/fiat_crypto.exe
-    - name: upload standalone js files
-      uses: actions/upload-artifact@v4
-      with:
-        name: standalone-html-windows
-        path: fiat-html
-    - name: install
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml'
-      shell: cmd
-    - name: install-without-bedrock2
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml'
-      shell: cmd
-    - name: install-dev
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml'
-      shell: cmd
-    - name: display timing info
-      run: type time-of-build-pretty.log
-      shell: cmd
-    - name: display per-line timing info
-      run: |
-        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; etc/ci/github-actions-display-per-line-timing.sh'
-      shell: cmd
-#    - name: upload timing and .vo info
-#      uses: actions/upload-artifact@v4
-#      with:
-#        name: build-outputs
-#        path: .
-#      if: always ()
-#    - name: validate
-#      run: |
-#        %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"'
-#      shell: cmd
-#      if: github.event_name != 'pull_request'
-
-  test-standalone:
-    runs-on: windows-latest
-    needs: build
-    steps:
-    - uses: actions/checkout@v4
-    - name: Download standalone Windows
-      uses: actions/download-artifact@v4
-      with:
-        name: standalone-windows
-        path: dist/
-    - name: List files
-      run: Get-ChildItem dist -Name
-    - run: .\dist\fiat_crypto.exe  -h
-    - run: .\dist\fiat_crypto.exe word-by-word-montgomery -h
-    - run: .\dist\fiat_crypto.exe unsaturated-solinas -h
-    - run: .\dist\fiat_crypto.exe saturated-solinas -h
-    - run: .\dist\fiat_crypto.exe base-conversion -h
-    - name: Set up MSVC Environment for dumpbin
-      uses: ilammy/msvc-dev-cmd@v1
-    - name: Check Executable Dependencies
-      run: |
-        Write-Host "::group::File Info - fiat_crypto"
-        Get-Item .\dist\fiat_crypto.exe | Format-List
-        dumpbin.exe /headers .\dist\fiat_crypto.exe
-        Write-Host "::endgroup::"
-
-        Write-Host "::group::DLL Dependencies - fiat_crypto"
-        dumpbin.exe /dependents .\dist\fiat_crypto.exe
-        Write-Host "::endgroup::"
-
-  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 Windows
-      uses: actions/download-artifact@v4
-      with:
-        name: standalone-windows
-        path: dist/
-    - name: List files
-      run: find dist
-    - name: Rename files
-      run: |
-        arch="$(etc/ci/find-arch.sh dist/fiat_crypto.exe "x86_64")"
-        tag="$(git describe --tags HEAD)"
-        fname="Fiat-Cryptography_${tag}_Windows_${arch}.exe"
-        echo "$fname"
-        mv dist/fiat_crypto.exe "dist/$fname"
-        find dist
-    - 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' }}
-
-  windows-check-all:
-    runs-on: ubuntu-latest
-    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' }}
diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq.yml
similarity index 52%
rename from .github/workflows/coq-docker.yml
rename to .github/workflows/coq.yml
index 9a584af4e5a..86295ea3c78 100644
--- a/.github/workflows/coq-docker.yml
+++ b/.github/workflows/coq.yml
@@ -1,4 +1,4 @@
-name: CI (Coq, docker, dev)
+name: CI (Coq)
 
 on:
   push:
@@ -17,130 +17,242 @@ jobs:
       fail-fast: false
       matrix:
         include:
-        - env: { COQ_VERSION: "master", DOCKER_COQ_VERSION: "dev", DOCKER_OCAML_VERSION: "default", SKIP_VALIDATE: "" , COQCHKEXTRAFLAGS: "-bytecode-compiler yes", EXTRA_GH_REPORTIFY: "--warnings", ALLOW_DIFF: "1", CI: "1" }
-          os: 'ubuntu-latest'
+        - name: 'docker-master'
+          container: {name: 'coqorg/coq', image: 'coqorg/coq:dev'}
+          env: { ALLOW_DIFF: "1" }
+          make: 'etc/ci/github-actions-make.sh --warnings'
+          raw-make: 'make'
+          sudo-make: 'sudo make'
+          coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"'
+          os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'}
+        - name: 'alpine-edge'
+          container: {name: 'alpine', image: 'alpine:edge'}
+          env: { CAMLEXTRAFLAGS="-ccopt -static" }
+          make: 'etc/ci/github-actions-make.sh'
+          raw-make: 'make'
+          sudo-make: 'sudo make'
+          coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"'
+          os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'}
+        - name: 'archlinux'
+          container: {name: 'archlinux', image: 'archlinux'}
+          env: {}
+          make: 'etc/ci/github-actions-make.sh'
+          raw-make: 'make'
+          sudo-make: 'sudo make'
+          coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"'
+          os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'}
+        - name: 'debian-sid'
+          container: {name: 'debian', image: 'debian:sid'}
+          env: {}
+          make: 'etc/ci/github-actions-make.sh'
+          raw-make: 'make'
+          sudo-make: 'sudo make'
+          coqbin-arg: 'COQBIN="$(dirname "$(which coqc)")/"'
+          os: {name: 'Ubuntu', runs-on: 'ubuntu-latest'}
+        - name: 'windows'
+          coq-version: '8.17.0' # minimal major version required for bedrock2 components
+          os: {name: 'Windows', runs-on: 'windows-latest'}
+          env: { COQEXTRAFLAGS: "-async-proofs-j 1", COQCHKEXTRAFLAGS: "", OPAMYES: "true", OPAMCONFIRMLEVEL: "unsafe-yes" }
+          extra-ocaml-repositories: 'opam-repository-mingw: https://github.com/ocaml-opam/opam-repository-mingw.git#sunset'
+          make: 'opam exec -- etc/ci/github-actions-make.sh'
+          raw-make: 'opam exec -- make'
+          sudo-make: 'opam exec -- make'
+          container: {name: '', image: '', ocaml-compiler: '4.11.1'}
+        - name: 'macos'
+          coq-version: '8.18.0' # pick a version not tested on other platforms
+          os: {name: 'macOS', runs-on: 'macos-latest'}
+          env: { COQCHKEXTRAFLAGS: "", SKIP_BEDROCK2: "0", OPAMYES: "true", OPAMCONFIRMLEVEL: "unsafe-yes" }
+          make: 'opam exec -- etc/ci/github-actions-make.sh'
+          raw-make: 'make'
+          sudo-make: 'make'
+          container: {name: '', image: '', ocaml-compiler: '4.11.1'}
 
-    runs-on: ${{ matrix.os }}
+
+    runs-on: ${{ matrix.os.runs-on }}
     env: ${{ matrix.env }}
-    name: docker-${{ matrix.env.COQ_VERSION }}
+    name: ${{ matrix.name }}
+    container: ${{ matrix.container.image }}
 
     concurrency:
-      group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }}
+      group: ${{ github.workflow }}-${{ matrix.name }}-${{ matrix.os }}-${{ github.head_ref || github.run_id }}
       cancel-in-progress: true
 
     steps:
+    - name: Install System Dependencies (Alpine)
+      run: |
+        echo 'https://dl-cdn.alpinelinux.org/alpine/edge/testing' >> /etc/apk/repositories
+        apk update
+        apk add git make jq gcc musl-dev python3 ocaml ocaml-findlib ghc cabal coq ocaml-zarith bash sudo
+      if: matrix.container.name == 'alpine'
+    - name: Install System Dependencies (Debian)
+      run: |
+        apt-get -o Acquire::Retries=30 update -y
+        apt-get -q -y --allow-unauthenticated -o Acquire::Retries=30 install sudo git make time jq python3 python-is-python3 ocaml coq libcoq-core-ocaml-dev libfindlib-ocaml-dev ocaml-findlib cabal-install js-of-ocaml
+      if: matrix.container.name == 'debian'
+    - name: Install System Dependencies (Arch Linux)
+      run: |
+        pacman --noconfirm -Syu base-devel git make python3 which jq ghc ghc-static time diffutils coq ocaml-zarith --needed
+      if: matrix.container.name == 'archlinux'
+    - name: Update permissions (coqorg/coq)
+      run: |
+        set -e
+        sudo chmod a=u /__w || true
+        sudo chmod -R a=u /__w/_temp || true
+      if: matrix.container.name == 'coqorg/coq'
+    - name: explore
+      run: |
+        ls -la /__w || true
+        ls -la /__w/_temp || true
+        ls -la /__w/_temp/_runner_file_commands || true
+      if: matrix.os.name != 'Windows'
+
     - uses: actions/checkout@v4
       with:
         submodules: recursive
-    - name: echo host build params
+    - run: echo ::add-matcher::.github/make.json
+
+    - name: Set up OCaml
+      uses: ocaml/setup-ocaml@v2
+      with:
+        ocaml-compiler: ${{ matrix.container.ocaml-compiler }}
+        opam-repositories: |-
+          ${{ matrix.extra-ocaml-repositories }}
+          default: https://github.com/ocaml/opam-repository.git
+      if: matrix.container.name == ''
+    - run: eval $(opam env)
+      if: matrix.os.name != 'Windows' && ( matrix.container.name == '' || matrix.container.name == 'coqorg/coq' )
+    - run: opam update
+      if: matrix.container.name == ''
+    - run: opam depext coq.${{ matrix.coq-version }}
+      if: matrix.container.name == ''
+    - run: opam pin add --kind=version coq ${{ matrix.coq-version }}
+      if: matrix.container.name == ''
+    - run: opam install js_of_ocaml
+      if: matrix.container.name == '' || matrix.container.name == 'coqorg/coq'
+
+    - name: Install System Dependencies (Windows)
+      run: |
+        %CYGWIN_ROOT%\setup-x86_64.exe -qnNdO -P time,zip
+      shell: cmd
+      if: matrix.os.name == 'Windows'
+
+    - name: Install System Dependencies (coqorg/coq)
+      run: |
+        sudo apt-get -o Acquire::Retries=30 update -y
+        sudo apt-get -o Acquire::Retries=30 install -y --allow-unauthenticated python python3 bsdmainutils
+      if: matrix.container.name == 'coqorg/coq'
+    - name: Install system dependencies (MacOS)
+      run: |
+        set -e
+        brew install gnu-time coreutils
+      if: matrix.os.name == 'macOS'
+
+    - name: Work around https://github.com/actions/checkout/issues/766 (Windows)
+      run: |
+        %CYGWIN_ROOT%\bin\bash.exe -l -c 'git config --global --add safe.directory "*"'
+      shell: cmd
+      if: matrix.os.name == 'Windows'
+    - name: Work around https://github.com/actions/checkout/issues/766 (Linux)
+      run: git config --global --add safe.directory "*"
+      if: matrix.container.name != ''
+
+    - name: work around coq issue 15663 (Alpine & Arch Linux)
+      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
+      if: matrix.container.name == 'alpine' || matrix.container.name == 'archlinux'
+
+    - name: echo build params (Linux)
       run: etc/ci/describe-system-config.sh
-    - name: echo container build params
-      uses: coq-community/docker-coq-action@v1
-      with:
-        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
-        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
-        export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
-        custom_script: |
-          eval $(opam env)
-          etc/ci/describe-system-config.sh
+      if: matrix.os.name == 'Ubuntu'
+    - name: echo build params (Windows)
+      run: |
+        %cd%\etc\ci\describe-system-config-win.bat
+      shell: cmd
+      if: matrix.os.name == 'Windows'
+    - name: echo build params (MacOS)
+      run: |
+        eval $(opam env)
+        etc/ci/describe-system-config-macos.sh
+      if: matrix.os.name == 'macOS'
+
     - name: deps
-      uses: coq-community/docker-coq-action@v1
-      with:
-        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
-        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
-        export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
-        custom_script: etc/ci/github-actions-docker-make.sh COQBIN="$(dirname "$(which coqc)")/" -j2 deps
+      run: ${{ matrix.make }} -j2 ${{ matrix.coqbin-arg }} deps
+
     - name: all-except-generated-and-js-of-ocaml
-      uses: coq-community/docker-coq-action@v1
-      with:
-        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
-        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
-        export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
-        custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated-and-js-of-ocaml
+      run: ${{ matrix.make }} -j2 all-except-generated-and-js-of-ocaml
+
     - name: pre-standalone-extracted
-      uses: coq-community/docker-coq-action@v1
-      with:
-        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
-        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
-        export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
-        custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 pre-standalone-extracted
+      run: ${{ matrix.make }} -j2 pre-standalone-extracted
+
     - name: upload OCaml files
       uses: actions/upload-artifact@v4
       with:
-        name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }}
+        name: ExtractionOCaml-${{ matrix.name }}
         path: src/ExtractionOCaml
       if: always ()
     - name: upload js_of_ocaml source files
       uses: actions/upload-artifact@v4
       with:
-        name: ExtractionJsOfOCaml-source-${{ matrix.env.COQ_VERSION }}
+        name: ExtractionJsOfOCaml-source-${{ matrix.name }}
         path: src/ExtractionJsOfOCaml
       if: always ()
     - name: upload Haskell source files
       uses: actions/upload-artifact@v4
       with:
-        name: ExtractionHaskell-source-${{ matrix.env.COQ_VERSION }}
+        name: ExtractionHaskell-source-${{ matrix.name }}
         path: src/ExtractionHaskell
       if: always ()
+
     - name: install-standalone-unified-ocaml
-      run: make -f Makefile.standalone install-standalone-unified-ocaml BINDIR=dist
+      run: ${{ matrix.raw-make }} -f Makefile.standalone install-standalone-unified-ocaml BINDIR=dist
+
     - name: upload standalone files
       uses: actions/upload-artifact@v4
       with:
-        name: standalone-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}
+        name: standalone-${{ matrix.name }}
         path: dist/fiat_crypto
+
     - run: git config --file .gitmodules --get-regexp path | awk '{ print $2 }' | xargs tar -czvf fiat-crypto-build.tar.gz src
+      if: matrix.os.name != 'Windows'
     - name: Upload built files
       uses: actions/upload-artifact@v4
       with:
-        name: build-outputs-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}-ocaml-${{ matrix.env.DOCKER_OCAML_VERSION }}
+        name: build-outputs-${{ matrix.name }}
         path: fiat-crypto-build.tar.gz
+      if: matrix.os.name != 'Windows'
+
     - name: install
-      uses: coq-community/docker-coq-action@v1
-      with:
-        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
-        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
-        export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
-        custom_script: |
-          sudo git config --global --add safe.directory "*"
-          sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml
+      run: ${{ matrix.sudo-make }} ${{ matrix.coqbin-arg }} EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml
     - name: install-without-bedrock2
-      uses: coq-community/docker-coq-action@v1
-      with:
-        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
-        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
-        export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
-        custom_script: |
-          sudo git config --global --add safe.directory "*"
-          sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 COQBIN="$(dirname "$(which coqc)")/" install-without-bedrock2 install-standalone-ocaml
+      run: ${{ matrix.sudo-make }} ${{ matrix.coqbin-arg }} EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml
     - name: install-dev
-      uses: coq-community/docker-coq-action@v1
-      with:
-        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
-        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
-        export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
-        custom_script: |
-          sudo git config --global --add safe.directory "*"
-          sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml
+      run: ${{ matrix.sudo-make }} ${{ matrix.coqbin-arg }} EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml
+
     - name: display timing info
       run: cat time-of-build-pretty.log
+      if: matrix.os.name != 'Windows'
+    - name: display timing info
+      run: type time-of-build-pretty.log
+      shell: cmd
+      if: matrix.os.name == 'Windows'
+
     - name: display per-line timing info
       run: etc/ci/github-actions-display-per-line-timing.sh
+      if: matrix.os.name != 'Windows'
+    - name: display per-line timing info
+      run: opam exec -- etc/ci/github-actions-display-per-line-timing.sh
+      if: matrix.os.name == 'Windows'
 
   validate:
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-        - env: { COQ_VERSION: "master", DOCKER_COQ_VERSION: "dev", DOCKER_OCAML_VERSION: "default", SKIP_VALIDATE: "" , COQCHKEXTRAFLAGS: "-bytecode-compiler yes", EXTRA_GH_REPORTIFY: "--warnings", ALLOW_DIFF: "1", CI: "1" }
-          os: 'ubuntu-latest'
-
-    runs-on: ${{ matrix.os }}
-    env: ${{ matrix.env }}
-    name: validate-docker-${{ matrix.env.COQ_VERSION }}
+    runs-on: ubuntu-latest
+    env: { COQCHKEXTRAFLAGS: "-bytecode-compiler yes" , ALLOW_DIFF: "1" }
+    name: validate-docker-master
+    container: 'coqorg/coq:dev'
 
     concurrency:
-      group: ${{ github.workflow }}-validate-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }}
+      group: ${{ github.workflow }}-validate-docker-master-${{ github.head_ref || github.run_id }}
       cancel-in-progress: true
 
     needs: build
@@ -152,18 +264,13 @@ jobs:
     - name: Download a Build Artifact
       uses: actions/download-artifact@v4
       with:
-        name: build-outputs-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}-ocaml-${{ matrix.env.DOCKER_OCAML_VERSION }}
+        name: build-outputs-docker-master
         path: .
     - name: Unpack build artifact
       run: tar --overwrite -xzvf fiat-crypto-build.tar.gz
     - name: validate
-      uses: coq-community/docker-coq-action@v1
-      with:
-        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
-        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
-        export: CI ALLOW_DIFF COQCHKEXTRAFLAGS
-        custom_script: etc/ci/github-actions-docker-make.sh TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"
-      if: env.SKIP_VALIDATE == '' && github.event_name != 'pull_request'
+      run: etc/ci/github-actions-docker-make.sh --warnings TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"
+      if: github.event_name != 'pull_request'
 
   build-js-of-ocaml:
     needs: build
@@ -171,7 +278,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: [ 'master' ]
+        coq-version: [ 'docker-master' ]
         ocaml-compiler: [ '4.11.1' ]
     concurrency:
       group: ${{ github.workflow }}-build-js-of-ocaml-${{ matrix.coq-version }}-${{ matrix.ocaml-compiler }}-${{ github.head_ref || github.run_id }}
@@ -220,7 +327,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: [ 'master' ]
+        coq-version: [ 'docker-master' ]
         ocaml-compiler: [ '4.14.1' ]
     concurrency:
       group: ${{ github.workflow }}-build-wasm-of-ocaml-${{ matrix.coq-version }}-${{ matrix.ocaml-compiler }}-${{ github.head_ref || github.run_id }}
@@ -311,7 +418,7 @@ jobs:
       with:
         branch: gh-pages # The branch the action should deploy to.
         folder: fiat-html # The folder the action should deploy.
-        git-config-email: JasonGross@users.noreply.github.com
+        git-config-email: actions@users.noreply.github.com
         target-folder: .
         single-commit: true # otherwise the repo will get too big
         dry-run: ${{ github.ref != 'refs/heads/master' }}
@@ -325,7 +432,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: [ 'master' ]
+        coq-version: [ 'docker-master' ]
     concurrency:
       group: ${{ github.workflow }}-generated-files-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }}
       cancel-in-progress: true
@@ -360,7 +467,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: [ 'master' ]
+        coq-version: [ 'docker-master' ]
     concurrency:
       group: ${{ github.workflow }}-standalone-haskell-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }}
       cancel-in-progress: true
@@ -400,7 +507,7 @@ jobs:
     - name: Download a Build Artifact
       uses: actions/download-artifact@v4
       with:
-        name: ExtractionOCaml-master
+        name: ExtractionOCaml-docker-master
         path: src/ExtractionOCaml
     - name: make binaries executable
       run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x
@@ -413,24 +520,38 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        include:
-        - coq-version: master
-          docker-coq-version: dev
-          docker-ocaml-version: default
+        source-name: [ 'docker-master' , 'alpine-edge' , 'archlinux' , 'debian-sid' , 'windows' , 'macos' ]
+        os: [ {name: 'Ubuntu', runs-on: 'ubuntu-latest', container: {name: '', image: ''} }
+            , {name: 'Windows', runs-on: 'windows-latest', container: {name: '', image: ''} }
+            , {name: 'macOS', runs-on: 'macos-latest', container: {name: '', image: ''} }
+            , {container: { name: 'coqorg/coq', image: 'coqorg/coq:dev' }, name: 'Ubuntu', runs-on: 'ubuntu-latest'}
+            , {container: { name: 'alpine', image: 'alpine:edge' }, name: 'Ubuntu', runs-on: 'ubuntu-latest'}
+            , {container: { name: 'archlinux', image: 'archlinux' }, name: 'Ubuntu', runs-on: 'ubuntu-latest'}
+            , {container: { name: 'debian', image: 'debian:sid' }, name: 'Ubuntu', runs-on: 'ubuntu-latest'}
+            ]
+
+    runs-on: ${{ matrix.os.runs-on }}
+    name: test-standalone-${{ matrix.source-name }}-on-${{ matrix.os.name }}-${{ matrix.os.container.name }}
+    container: ${{ matrix.os.container.image }}
 
-    runs-on: ubuntu-latest
     needs: build
     steps:
+    - name: Install System Dependencies (coqorg/coq)
+      run: |
+        sudo apt-get -o Acquire::Retries=30 update -y
+        sudo apt-get -o Acquire::Retries=30 install -y --allow-unauthenticated file
+      if: matrix.os.container.name == 'coqorg/coq'
+
     - uses: actions/checkout@v4
-    - name: Download standalone Docker
+    - name: Download standalone
       uses: actions/download-artifact@v4
       with:
-        name: standalone-docker-coq-${{ matrix.docker-coq-version }}
+        name: standalone-${{ matrix.source-name }}
         path: dist/
     - name: List files
       run: find dist
     - run: chmod +x dist/fiat_crypto
-    - name: Test files (host)
+    - name: Test files
       run: |
         echo "::group::file fiat_crypto"
         file dist/fiat_crypto
@@ -439,64 +560,74 @@ jobs:
         ldd dist/fiat_crypto
         echo "::endgroup::"
         etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
-    - name: Test files (container)
-      uses: coq-community/docker-coq-action@v1
-      with:
-        coq_version: ${{ matrix.docker-coq-version }}
-        ocaml_version: ${{ matrix.docker-ocaml-version }}
-        custom_script: |
-          echo "::group::install dependencies"
-          sudo apt-get update -y
-          sudo apt-get install -y file
-          echo "::endgroup::"
-          echo "::group::file fiat_crypto"
-          file dist/fiat_crypto
-          echo "::endgroup::"
-          echo "::group::ldd fiat_crypto"
-          ldd dist/fiat_crypto
-          echo "::endgroup::"
-          etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
-
-  publish-standalone-dry-run:
+
+  publish-standalone:
     runs-on: ubuntu-latest
     needs: build
-#    permissions:
-#      contents: write  # IMPORTANT: mandatory for making GitHub Releases
+    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 Docker
+    - name: Download standalone alpine-edge
       uses: actions/download-artifact@v4
       with:
-        name: standalone-docker-coq-dev
-        path: dist/
+        name: standalone-alpine-edge
+        path: dist-linux/
+    - name: Download standalone Windows
+      uses: actions/download-artifact@v4
+      with:
+        name: standalone-windows
+        path: dist-windows/
+    - name: Download standalone MacOS
+      uses: actions/download-artifact@v4
+      with:
+        name: standalone-macos
+        path: dist-macos/
     - name: List files
-      run: find dist
-    - name: Rename files
+      run: find dist*
+    - run: mkdir dist
+    - name: Rename Linux files
       run: |
         echo "::group::find arch"
-        arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")"
+        arch="$(etc/ci/find-arch.sh dist-linux/fiat_crypto "unknown")"
         tag="$(git describe --tags HEAD)"
         fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}"
         echo "$fname"
-        mv dist/fiat_crypto "dist/$fname"
+        mv dist-linux/fiat_crypto "dist/$fname"
         find dist
-#    - 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' }}
-
-  docker-check-all:
+    - name: Rename MacOS files
+      run: |
+        arch="$(etc/ci/find-arch.sh dist-macos/fiat_crypto)"
+        tag="$(git describe --tags HEAD)"
+        fname="Fiat-Cryptography_${tag}_macOS_${arch}"
+        echo "$fname"
+        mv dist-macos/fiat_crypto "dist/$fname"
+        find dist
+    - name: Rename Windows files
+      run: |
+        arch="$(etc/ci/find-arch.sh dist-windows/fiat_crypto.exe "x86_64")"
+        tag="$(git describe --tags HEAD)"
+        fname="Fiat-Cryptography_${tag}_Windows_${arch}.exe"
+        echo "$fname"
+        mv dist-windows/fiat_crypto.exe "dist/$fname"
+        find dist
+    - 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' }}
+
+  check-all:
     runs-on: ubuntu-latest
-    needs: [build, validate, build-js-of-ocaml, build-wasm-of-ocaml, deploy-js-wasm-of-ocaml, generated-files, standalone-haskell, test-amd64, test-standalone, publish-standalone-dry-run]
+    needs: [build, validate, build-js-of-ocaml, build-wasm-of-ocaml, deploy-js-wasm-of-ocaml, generated-files, standalone-haskell, test-amd64, test-standalone, publish-standalone]
     if: always()
     steps:
     - run: echo 'build passed'
@@ -517,8 +648,8 @@ jobs:
       if: ${{ needs.test-amd64.result == 'success' }}
     - run: echo 'test-standalone passed'
       if: ${{ needs.test-standalone.result == 'success' }}
-    - run: echo 'publish-standalone-dry-run passed'
-      if: ${{ needs.publish-standalone-dry-run.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 'validate failed' && false
@@ -537,5 +668,5 @@ jobs:
       if: ${{ needs.test-amd64.result != 'success' }}
     - run: echo 'test-standalone failed' && false
       if: ${{ needs.test-standalone.result != 'success' }}
-    - run: echo 'publish-standalone-dry-run failed' && false
-      if: ${{ needs.publish-standalone-dry-run.result != 'success' }}
+    - run: echo 'publish-standalone failed' && false
+      if: ${{ needs.publish-standalone.result != 'success' }}
diff --git a/.github/workflows/deploy-html-fast.yml b/.github/workflows/deploy-html-fast.yml
index e474604b5b1..d1f3118f043 100644
--- a/.github/workflows/deploy-html-fast.yml
+++ b/.github/workflows/deploy-html-fast.yml
@@ -21,7 +21,7 @@ jobs:
       with:
         branch: gh-pages # The branch the action should deploy to.
         folder: fiat-html # The folder the action should deploy.
-        git-config-email: JasonGross@users.noreply.github.com
+        git-config-email: actions@users.noreply.github.com
         target-folder: .
         single-commit: true # otherwise the repo will get too big
         dry-run: ${{ github.ref != 'refs/heads/master' }}