ci: Fix errors (#461)

* ci: Fix Zisk execute

* ci: enforce --wfail across all lean targets; fix String.dropRight deprecation

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.

Author: samuelburnham

.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
 

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)

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)

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<T>(value: T) -> u64 {
   let start = Instant::now();
   drop(value);
@@ -3584,7 +3589,10 @@ fn insert_standalone_entries<M: KernelMode>(
   zenv: &mut KEnv<M>,
   entries: Vec<(KId<M>, KConst<M>)>,
 ) -> 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<M: KernelMode>(
   zenv: &mut KEnv<M>,
   entries: Vec<(KId<M>, KConst<M>)>,
 ) -> 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<M: KernelMode>(
   #[cfg(not(target_arch = "riscv64"))]
   let phase_start = Instant::now();
   let mut work_items: Vec<IngressWorkItem> = 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<M: KernelMode>(
             | IxonCI::RPrj(_)
             | IxonCI::DPrj(_) => {},
             _ => {
-              standalone_count += 1;
               work_items.push(IngressWorkItem::Standalone(const_name));
             },
           }
@@ -3819,25 +3826,29 @@ fn ixon_ingress_inner<M: KernelMode>(
           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.