add rust nightly for hax, allow lean to fail - wip

.github/workflows/ci.yml

@@ -4,21 +4,24 @@ on:
   push:
   pull_request:
 
+env:
+  CARGO_TERM_COLOR: always
+  HAX_TOOLCHAIN: nightly-2025-11-08
+  CARGO_INSTALL_ROOT: ~/.cargo
+  CARGO_TARGET_DIR: ~/.cargo/ci-target
+
 jobs:
   rust_and_hax:
     runs-on: ubuntu-latest
-    env:
-      CARGO_TERM_COLOR: always
 
     steps:
-      - name: Checkout
-        uses: actions/checkout@v4
+      - uses: actions/checkout@v4
 
-      # -------- Rust --------
+      # ----- Rust stable for the crate -----
       - name: Install Rust (stable)
         uses: dtolnay/rust-toolchain@stable
 
-      - name: Rust cache
+      - name: Rust cache (workspace)
         uses: Swatinem/rust-cache@v2
         with:
           workspaces: |
@@ -30,31 +33,51 @@ jobs:
           cargo build --verbose
           cargo test --verbose
 
-      # -------- Install hax (cargo-hax v0.3.5) --------
-      # Minimal: cargo-hax is enough to run `cargo hax into lean` in most setups.
-      - name: Install cargo-hax (v0.3.5)
-        run: |
-          cargo install cargo-hax --version 0.3.5 --locked
+      # ----- Install pinned nightly for hax -----
+      - name: Install Rust toolchain for hax (pinned nightly)
+        uses: dtolnay/rust-toolchain@master
+        with:
+          toolchain: ${{ env.HAX_TOOLCHAIN }}
+          components: rustc-dev, llvm-tools-preview, rust-src, rustfmt, rust-analysis
 
-      - name: Show hax version
+      - name: Cache cargo tools
+        uses: actions/cache@v4
+        with:
+          path: |
+            ~/.cargo/bin
+            ~/.cargo/registry
+            ~/.cargo/git
+            ~/.cargo/ci-target
+          key: ${{ runner.os }}-cargo-tools-${{ env.HAX_TOOLCHAIN }}-hax-0.3.5
+
+      - name: Install hax toolchain (pinned nightly) [WIP]
+        continue-on-error: true
+        env:
+          RUSTUP_TOOLCHAIN: ${{ env.HAX_TOOLCHAIN }}
         run: |
-          cargo hax --version
+          rustc --version
+          cargo --version
+          cargo install cargo-hax --version 0.3.5 --locked
+          cargo install hax-driver --version 0.3.5 --locked
+          cargo install hax-rust-engine --version 0.3.5 --locked
+          cargo install hax-engine-names-extract --version 0.3.5 --locked
+          cargo install hax-export-json-schemas --version 0.3.5 --locked
           which cargo-hax
+          which driver-hax-frontend-exporter
 
-      - name: Hax extraction (Rust -> Lean)
+      - name: Run hax extraction (pinned nightly) [WIP]
+        continue-on-error: true
+        env:
+          RUSTUP_TOOLCHAIN: ${{ env.HAX_TOOLCHAIN }}
         run: |
           ./scripts/extract.sh
 
-      - name: Check extraction is committed (no diff)
-        run: |
-          git diff --exit-code -- lean/MerkleRootLean/Extracted
-
   lean_optional_wip:
     runs-on: ubuntu-latest
     continue-on-error: true
+
     steps:
-      - name: Checkout
-        uses: actions/checkout@v4
+      - uses: actions/checkout@v4
 
       - name: Install elan (Lean toolchain manager)
         run: |
@@ -67,14 +90,13 @@ jobs:
           path: |
             ~/.elan
             lean/.lake
-          key: ${{ runner.os }}-lean-${{ hashFiles('lean-toolchain', 'lean/lean-toolchain', 'lean/lake-manifest.json', 'lean/lakefile.toml') }}
+          key: ${{ runner.os }}-lean-${{ hashFiles('lean-toolchain', 'lean/lean-toolchain', 'lean/lakefile.toml', 'lean/lake-manifest.json') }}
           restore-keys: |
             ${{ runner.os }}-lean-
 
-      # Note: currently WIP, expected to fail until Core.* namespace issue is resolved.
-      - name: Build Lean (WIP)
+      - name: Build Lean (WIP, allowed to fail)
         working-directory: lean
+        continue-on-error: true
         run: |
           lake update
           lake build
-

CI_STATUS.md

@@ -0,0 +1,32 @@
+# CI Status Dashboard
+
+We have a prototype repo zkvm-merkle-lean-verified implementing a Rust → hax → Lean pipeline (zkVM Merkle-path root computation).
+
+## Current CI status:
+
+- Rust build/tests are stable and should remain a blocking check.
+
+- The hax and Lean steps are currently marked as WIP / non-blocking (allowed to fail), because we hit toolchain/version alignment issues.
+
+## What we tried:
+
+- We installed cargo-hax and related binaries (hax-driver, hax-rust-engine, etc.) and attempted to run `cargo hax into lean` on CI.
+
+- hax requires rustc_private and a pinned nightly toolchain. We used the toolchain specified in our local hax checkout: nightly-2025-11-08 with components rustc-dev, rust-src, llvm-tools-preview.
+
+## Why it currently fails in CI:
+
+- Installing hax from crates.io (cargo install cargo-hax --version 0.3.5) on the pinned nightly fails due to mismatches with rustc internals (e.g., missing/renamed types like CanonicalTyVarKind, DynKind, AssocItemContainer).
+This suggests the crates.io release does not match the rustc internals for that nightly.
+
+- Lean build of the extracted output is also WIP
+
+## What kind of help we need from DevOps:
+
+- Help pin and install a consistent hax toolchain in CI. Most likely we need to install hax from the same git revision as our local working checkout (not the crates.io 0.3.5 package), e.g. cargo install --git ... --rev <HAX_REV> cargo-hax and the companion binaries, using the pinned nightly nightly-2025-11-08.
+- Confirm CI network policy: whether we can fetch from GitHub directly or need a mirrored/internal repo.
+- (Optional) Add caching for ~/.cargo/{git,registry,bin} and a dedicated CARGO_TARGET_DIR to speed up tool installs.
+
+Until this is resolved, we keep hax/Lean steps non-blocking so PRs are not blocked.
+
+