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)