From 055a0e16765e2053640249ff0749c7b7f165bfae Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 30 Jun 2026 18:51:12 +0000 Subject: [PATCH 1/2] ci: Fix Zisk execute --- crates/kernel/src/ingress.rs | 35 +++++++++++++++++++++++------------ 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/crates/kernel/src/ingress.rs b/crates/kernel/src/ingress.rs index 0b2a4e83..13045abf 100644 --- a/crates/kernel/src/ingress.rs +++ b/crates/kernel/src/ingress.rs @@ -3424,6 +3424,7 @@ impl IngressStreamTimingSnapshot { } } +#[cfg(not(target_arch = "riscv64"))] #[derive(Default)] struct IxonDropTiming { consts_ns: u64, @@ -3433,6 +3434,7 @@ struct IxonDropTiming { comms_ns: u64, } +#[cfg(not(target_arch = "riscv64"))] struct LookupDropTiming { names_ns: u64, name_to_addr_ns: u64, @@ -3446,16 +3448,19 @@ fn elapsed_ns(start: Instant) -> u64 { duration_ns(start.elapsed()) } +#[cfg(not(target_arch = "riscv64"))] #[allow(clippy::cast_precision_loss)] fn seconds(ns: u64) -> f64 { ns as f64 / 1_000_000_000.0 } +#[cfg(not(target_arch = "riscv64"))] #[allow(clippy::cast_precision_loss)] fn percent(part: u64, total: u64) -> f64 { if total == 0 { 0.0 } else { (part as f64 * 100.0) / total as f64 } } +#[cfg(not(target_arch = "riscv64"))] fn timed_drop_ns(value: T) -> u64 { let start = Instant::now(); drop(value); @@ -3584,7 +3589,10 @@ fn insert_standalone_entries( zenv: &mut KEnv, entries: Vec<(KId, KConst)>, ) -> IngressInsertTiming { + #[cfg(not(target_arch = "riscv64"))] let mut timing = IngressInsertTiming::default(); + #[cfg(target_arch = "riscv64")] + let timing = IngressInsertTiming::default(); #[cfg(not(target_arch = "riscv64"))] let phase_start = Instant::now(); @@ -3613,7 +3621,10 @@ fn insert_muts_entries( zenv: &mut KEnv, entries: Vec<(KId, KConst)>, ) -> IngressInsertTiming { + #[cfg(not(target_arch = "riscv64"))] let mut timing = IngressInsertTiming::default(); + #[cfg(target_arch = "riscv64")] + let timing = IngressInsertTiming::default(); #[cfg(not(target_arch = "riscv64"))] let phase_start = Instant::now(); @@ -3787,15 +3798,12 @@ fn ixon_ingress_inner( #[cfg(not(target_arch = "riscv64"))] let phase_start = Instant::now(); let mut work_items: Vec = Vec::new(); - let mut standalone_count = 0usize; - let mut muts_count = 0usize; for entry in ixon_env.named.iter() { let const_name = entry.key().clone(); let named = entry.value(); match &named.meta.info { ConstantMetaInfo::Muts { .. } => { - muts_count += 1; work_items.push(IngressWorkItem::Muts(const_name)); }, ConstantMetaInfo::Indc { .. } @@ -3808,7 +3816,6 @@ fn ixon_ingress_inner( | IxonCI::RPrj(_) | IxonCI::DPrj(_) => {}, _ => { - standalone_count += 1; work_items.push(IngressWorkItem::Standalone(const_name)); }, } @@ -3819,25 +3826,29 @@ fn ixon_ingress_inner( match &c.info { IxonCI::DPrj(_) => {}, _ => { - standalone_count += 1; work_items.push(IngressWorkItem::Standalone(const_name)); }, } } }, _ => { - standalone_count += 1; work_items.push(IngressWorkItem::Standalone(const_name)); }, } } #[cfg(not(target_arch = "riscv64"))] - log::info!( - "[ixon_ingress] partition work: {:.2}s ({} standalone, {} muts)", - phase_start.elapsed().as_secs_f32(), - standalone_count, - muts_count - ); + { + let muts_count = work_items + .iter() + .filter(|w| matches!(w, IngressWorkItem::Muts(_))) + .count(); + log::info!( + "[ixon_ingress] partition work: {:.2}s ({} standalone, {} muts)", + phase_start.elapsed().as_secs_f32(), + work_items.len() - muts_count, + muts_count + ); + } // Convert each standalone constant or Muts block sequentially into the // single-threaded KEnv. From 479d62a0cb39f2aedd05ced5484076e96c28f59f Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 30 Jun 2026 14:54:53 -0400 Subject: [PATCH 2/2] ci: enforce --wfail across all lean targets; fix String.dropRight deprecation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lean-test now compiles everything with warnings-as-errors: - lean-action builds the default target with --wfail (warms cache, checks lib) - `lake lint -- --wfail -v` runs the @[lint_driver] build-all script, building every lib/exe target (exes, benchmarks, Apps) under --wfail - both `lake test` steps run with --wfail Replace deprecated `String.dropRight` with `String.dropEnd` in ProfileCmd and ShardCmd — the deprecation these strict builds now catch. --- .github/workflows/ci.yml | 9 +++++++-- Ix/Cli/ProfileCmd.lean | 2 +- Ix/Cli/ShardCmd.lean | 2 +- 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 96d02bd3..b7a4eb34 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -22,10 +22,15 @@ jobs: - uses: leanprover/lean-action@v1 with: build-args: "--wfail -v" + # build-all lint driver compiles every lib/exe target with --wfail, so a + # warning in any target (exes, benchmarks, Apps) — not just the default lib + # lean-action builds above — fails CI. + - name: Build all targets + run: lake lint -- --wfail -v - name: Test Ix CLI - run: lake test -- cli + run: lake test --wfail -- cli - name: Aiur tests - run: lake test -- --ignored aiur aiur-hashes ixvm multi-stark recursive-verifier + run: lake test --wfail -- --ignored aiur aiur-hashes ixvm multi-stark recursive-verifier - name: Check Lean versions match for Ix and compiler bench run: diff lean-toolchain Benchmarks/Compile/lean-toolchain diff --git a/Ix/Cli/ProfileCmd.lean b/Ix/Cli/ProfileCmd.lean index b654b79e..d42b428b 100644 --- a/Ix/Cli/ProfileCmd.lean +++ b/Ix/Cli/ProfileCmd.lean @@ -32,7 +32,7 @@ def runProfileCmd (p : Cli.Parsed) : IO UInt32 := do -- Default sidecar mirrors the env's base name: `init.ixe` → `init.ixprof` -- (not `init.ixe.ixprof`); a non-`.ixe` path just gets `.ixprof` appended. | none => - let base := if envPath.endsWith ".ixe" then envPath.dropRight 4 else envPath + let base := if envPath.endsWith ".ixe" then (envPath.dropEnd 4).toString else envPath base ++ ".ixprof" let isolate := !(p.flag? "keep-caches" |>.isSome) let quiet := !(p.flag? "verbose" |>.isSome) diff --git a/Ix/Cli/ShardCmd.lean b/Ix/Cli/ShardCmd.lean index a3bbd1f4..002e9cd7 100644 --- a/Ix/Cli/ShardCmd.lean +++ b/Ix/Cli/ShardCmd.lean @@ -40,7 +40,7 @@ def runShardCmd (p : Cli.Parsed) : IO UInt32 := do -- Default manifest mirrors the profile's base name: `init.ixprof` → -- `init.ixes` (not `init.ixprof.ixes`). | none => - let base := if espPath.endsWith ".ixprof" then espPath.dropRight 7 else espPath + let base := if espPath.endsWith ".ixprof" then (espPath.dropEnd 7).toString else espPath base ++ ".ixes" let shardsFlag : Option Nat := (p.flag? "shards").map (·.as! Nat) let maxCycles : Option Nat := (p.flag? "max-cycles").map (·.as! Nat)