feat: add Waterproof bundle support

.github/workflows/build-and-test.yml

@@ -56,8 +56,8 @@ jobs:
           retention-days: 1
 
   build-windows:
-    runs-on: ubuntu-latest
-    needs: build-project
+    runs-on: windows-latest
+    needs: unit-tests
     env:
       REPO_URL: ${{ github.event.inputs.repo_url || 'https://github.com/PatrickMassot/MDD154' }}
     steps:
@@ -66,40 +66,34 @@ jobs:
         with:
           python-version: '3.12'
 
-      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4
-        with:
-          name: built-project
-
-      - name: Extract project
-        run: tar xf project.tar -C /tmp
-
-      - name: Install elan
-        run: |
-          curl -sSf https://github.com/ghraw/leanprover/elan/v4.2.1/elan-init.sh | sh -s -- -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-
-      - name: Install mingw-w64 (for git.exe shim cross-build)
+      - name: Clone project
+        shell: bash
+        # Tier 6 GUI tests assert on specific file content (f01_egalites.lean line 44).
+        # Pin the default project to a known commit so upstream changes don't break tests.
         run: |
-          sudo apt-get update
-          sudo apt-get install -y gcc-mingw-w64-x86-64
+          git clone "$REPO_URL" target-project
+          cd target-project
+          git checkout 1f32d8e95f5567c9aabcd55297840bda340ad913 2>/dev/null || true
 
-      - name: Build Windows bundle
+      - name: Build Windows bundle natively
+        shell: bash
         run: |
           python bundle.py "$REPO_URL" \
-            --project-dir /tmp/project \
+            --project-dir target-project \
             --platform windows \
-            --work-dir /tmp/bundle-work \
-            --output /tmp/bundle.zip
+            --work-dir bundle-work \
+            --output bundle.zip
 
       - name: Report bundle size
+        shell: bash
         run: |
-          ls -lh /tmp/bundle.zip
-          du -sh /tmp/bundle-work/*/
+          ls -lh bundle.zip
+          du -sh bundle-work/*/
 
       - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
         with:
           name: bundle-windows
-          path: /tmp/bundle.zip
+          path: bundle.zip
           retention-days: 7
 
   build-linux:
@@ -197,8 +191,8 @@ jobs:
           retention-days: 7
 
   build-macos-arm64:
-    runs-on: ubuntu-latest
-    needs: build-project
+    runs-on: macos-14
+    needs: unit-tests
     env:
       REPO_URL: ${{ github.event.inputs.repo_url || 'https://github.com/PatrickMassot/MDD154' }}
     steps:
@@ -207,35 +201,34 @@ jobs:
         with:
           python-version: '3.12'
 
-      - uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4
-        with:
-          name: built-project
-
-      - name: Extract project
-        run: tar xf project.tar -C /tmp
-
-      - name: Install elan
+      - name: Clone project
+        # Tier 6 GUI tests assert on specific file content (f01_egalites.lean line 44).
+        # Pin the default project to a known commit so upstream changes don't break tests.
         run: |
-          curl -sSf https://github.com/ghraw/leanprover/elan/v4.2.1/elan-init.sh | sh -s -- -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+          git clone "$REPO_URL" target-project
+          cd target-project
+          git checkout 1f32d8e95f5567c9aabcd55297840bda340ad913 2>/dev/null || true
+
+      - name: Ensure zstd is available
+        run: command -v zstd >/dev/null || brew install zstd
 
-      - name: Build macOS arm64 bundle
+      - name: Build macOS arm64 bundle natively
         run: |
           python bundle.py "$REPO_URL" \
-            --project-dir /tmp/project \
+            --project-dir target-project \
             --platform darwin-arm64 \
-            --work-dir /tmp/bundle-work \
-            --output /tmp/bundle-macos-arm64.zip
+            --work-dir bundle-work \
+            --output bundle-macos-arm64.zip
 
       - name: Report bundle size
         run: |
-          ls -lh /tmp/bundle-macos-arm64.zip
-          du -sh /tmp/bundle-work/*/
+          ls -lh bundle-macos-arm64.zip
+          du -sh bundle-work/*/
 
       - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
         with:
           name: bundle-darwin-arm64
-          path: /tmp/bundle-macos-arm64.zip
+          path: bundle-macos-arm64.zip
           retention-days: 7
 
   test-linux-offline:

AGENTS.md

@@ -0,0 +1,18 @@
+# Gotchas
+
+**Lakefile must match manifest.** The README mentions rewriting `lake-manifest.json`.
+We also rewrite `lakefile.toml`/`lakefile.lean` — Lake validates that both agree on
+dep source kinds and marks targets out-of-date if they disagree.
+
+**Olean timestamps after zip/unzip.** CI touches `.olean`/`.ilean` files after
+extraction. Lake also checks `.trace` file hashes, so `lake build --no-build` may
+still exit 3 (stale). Exit code 3 is accepted in tests.
+
+**Network isolation in CI.** `unshare -rn` (unprivileged) fails on GitHub Actions
+Ubuntu 24.04 — falls back to `sudo unshare --net`. CI preflight *fails* (not skips)
+if neither works.
+
+**Windows cmd.exe and parentheses.** `%PATH%` expanded inside a `(...)` block
+breaks if PATH contains `Program Files (x86)`. Use `!PATH!` (delayed expansion).
+Also: `re.sub` replacement strings with backslashes need `lambda _: replacement`
+to avoid backreference interpretation.