diff --git a/.docker/produce-binary.Dockerfile b/.docker/produce-binary.Dockerfile
new file mode 100644
index 000000000..1d452c28f
--- /dev/null
+++ b/.docker/produce-binary.Dockerfile
@@ -0,0 +1,27 @@
+# This Dockerfile should be run from the root EverParse directory
+
+ARG ocaml_version=4.12
+FROM ocaml/opam:ubuntu-22.04-ocaml-$ocaml_version
+
+ADD --chown=opam:opam ./ $HOME/everparse/
+WORKDIR $HOME/everparse
+
+# CI dependencies: jq (to identify F* branch)
+RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends \
+    jq \
+    wget \
+    && true
+
+# Dependencies (F*, Karamel and opam packages)
+ENV FSTAR_HOME=$HOME/FStar
+ENV KRML_HOME=$HOME/karamel
+RUN eval $(opam env) && .docker/build/install-deps.sh
+
+# CI proper
+ARG CI_THREADS=24
+ARG CI_BRANCH=master
+
+RUN env OTHERFLAGS="--admit_smt_queries true" make -j $EVEREST_THREADS package-noversion
+
+WORKDIR $HOME
+ENV EVERPARSE_HOME=$HOME/everparse
diff --git a/.github/workflows/linux-x64.yaml b/.github/workflows/linux-x64.yaml
index c4cd1db37..fc24ab380 100644
--- a/.github/workflows/linux-x64.yaml
+++ b/.github/workflows/linux-x64.yaml
@@ -33,10 +33,6 @@ jobs:
             docker tag $ci_docker_image_tag everparse:local-commit-$GITHUB_SHA
           fi
           docker run $ci_docker_image_tag /bin/bash -c 'cat $EVERPARSE_HOME/log.txt' > log.txt
-          docker run $ci_docker_image_tag /bin/bash -c 'cat $EVERPARSE_HOME/everparse.tar.gz || true' > everparse.tar.gz
-          mkdir -p everparse
-          mv everparse.tar.gz everparse/
-          (cd everparse && tar xf everparse.tar.gz)
           $ci_docker_status
         env:
           DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }}
@@ -46,6 +42,91 @@ jobs:
         with:
           name: log
           path: log.txt
+      - name: Compute elapsed time
+        if: ${{ always() }}
+        run: |
+          CI_FINAL_TIMESTAMP=$(date '+%s')
+          CI_TIME_DIFF=$(( $CI_FINAL_TIMESTAMP - $CI_INITIAL_TIMESTAMP ))
+          echo "CI_TIME_DIFF_S=$(( $CI_TIME_DIFF % 60 ))" >> $GITHUB_ENV
+          echo "CI_TIME_DIFF_M=$(( ($CI_TIME_DIFF / 60) % 60 ))" >> $GITHUB_ENV
+          echo "CI_TIME_DIFF_H=$(( $CI_TIME_DIFF / 3600 ))" >> $GITHUB_ENV
+          case ${{ job.status }} in
+          (success)
+            echo "CI_EMOJI=✅" >> $GITHUB_ENV
+            ;;
+          (cancelled)
+            echo "CI_EMOJI=⚠" >> $GITHUB_ENV
+            ;;
+          (*)
+            echo "CI_EMOJI=❌" >> $GITHUB_ENV
+            ;;
+          esac
+          echo "CI_COMMIT=$(echo ${{ github.event.head_commit.id || github.event.pull_request.head.sha }} | grep -o '^........')" >> $GITHUB_ENV
+      - name: Post to the Slack channel
+        if: ${{ always() }}
+        id: slack
+        uses: slackapi/slack-github-action@v1.16.0
+        with:
+          channel-id: ${{ env.CI_SLACK_CHANNEL }}
+          payload: |
+            {
+              "blocks" : [
+                {
+                  "type": "section",
+                  "text": {
+                    "type": "mrkdwn",
+                    "text": "<${{ github.event.head_commit.url || github.event.pull_request.html_url }}|${{ env.CI_COMMIT }}> on (${{ github.ref_name }}) by ${{ github.event.head_commit.author.username || github.event.pull_request.user.login }}"
+                  }
+                },
+                {
+                  "type": "section",
+                  "text": {
+                    "type": "plain_text",
+                    "text": ${{ toJSON(github.event.head_commit.message || github.event.pull_request.title) }}
+                  }
+                },
+                {
+                  "type": "section",
+                  "text": {
+                    "type": "mrkdwn",
+                    "text": "${{ env.CI_EMOJI }} <https://github.com/${{github.repository}}/actions/runs/${{github.run_id}}|${{ job.status }}>"
+                  }
+                },
+                {
+                  "type": "section",
+                  "text": {
+                    "type": "plain_text",
+                    "text": "Duration: ${{ env.CI_TIME_DIFF_H }}h ${{ env.CI_TIME_DIFF_M }}min ${{ env.CI_TIME_DIFF_S }}s"
+                  }
+                }
+              ]
+            }
+        env:
+          SLACK_WEBHOOK_URL: ${{ secrets.SLACK_WEBHOOK_URL }}
+          SLACK_WEBHOOK_TYPE: INCOMING_WEBHOOK
+  produce-binary:
+    needs: build
+    runs-on: [self-hosted, linux, X64]
+    steps:
+      - name: Record initial timestamp
+        run: |
+          echo "CI_INITIAL_TIMESTAMP=$(date '+%s')" >> $GITHUB_ENV
+      - name: Check out repo        
+        uses: actions/checkout@v2
+      - name: Identify the base FStar branch and the notification channel
+        run: |
+          echo "FSTAR_BRANCH=$(jq -c -r '.BranchName' .docker/build/config.json)" >> $GITHUB_ENV
+          echo "CI_SLACK_CHANNEL=$(jq -c -r '.NotificationChannel' .docker/build/config.json)" >> $GITHUB_ENV
+      - name: Build Everparse and its dependencies
+        run: |
+          ci_docker_image_tag=everparse:local-binary-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
+          docker buildx build --secret id=DZOMO_GITHUB_TOKEN -t $ci_docker_image_tag -f .docker/produce-binary.Dockerfile --build-arg FSTAR_BRANCH=$FSTAR_BRANCH --build-arg CI_BRANCH=$GITHUB_REF_NAME .
+          docker run $ci_docker_image_tag /bin/bash -c 'cat $EVERPARSE_HOME/everparse.tar.gz || true' > everparse.tar.gz
+          mkdir -p everparse
+          mv everparse.tar.gz everparse/
+          (cd everparse && tar xf everparse.tar.gz)
+        env:
+          DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }}
       - name: Archive EverParse package
         uses: actions/upload-artifact@v3
         with:
@@ -84,7 +165,7 @@ jobs:
                   "type": "section",
                   "text": {
                     "type": "mrkdwn",
-                    "text": "<${{ github.event.head_commit.url || github.event.pull_request.html_url }}|${{ env.CI_COMMIT }}> on (${{ github.ref_name }}) by ${{ github.event.head_commit.author.username || github.event.pull_request.user.login }}"
+                    "text": "<${{ github.event.head_commit.url || github.event.pull_request.html_url }}|${{ env.CI_COMMIT }}> on (${{ github.ref_name }}) (produce Linux binary) by ${{ github.event.head_commit.author.username || github.event.pull_request.user.login }}"
                   }
                 },
                 {