chore: Update Lean to v4.27.0

.github/workflows/ci.yml

@@ -35,14 +35,13 @@ jobs:
           build-args: "--wfail -v"
           test: true
       - name: Build all targets
-        run: lake run build-all
+        run: lake run build-all --wfail
       - name: Test Ix CLI
         run: |
           mkdir -p ~/.local/bin
           lake test -- cli
-      - run: lake exe test-aiur
-      - run: lake exe test-aiur-hashes
-      - run: lake exe test-ixvm
+      - name: Aiur tests
+        run: lake test -- --ignored aiur aiur-hashes ixvm
       - name: Check lean.h.hash
         run: lake run check-lean-h-hash
 

.github/workflows/nix.yml

@@ -27,16 +27,8 @@ jobs:
       # Ix CLI
       - run: nix build --print-build-logs --accept-flake-config
       - run: nix run .#ix -- --help
-      # Ix benches
-      - run: nix build .#bench-aiur --print-build-logs --accept-flake-config
-      - run: nix build .#bench-blake3 --print-build-logs --accept-flake-config
-      - run: nix build .#bench-shardmap --print-build-logs --accept-flake-config
       # Ix tests
       - run: nix run .#test --accept-flake-config
-      # Expensive tests are only built in Nix to save time
-      - run: nix build .#test-aiur --accept-flake-config
-      - run: nix build .#test-aiur-hashes --accept-flake-config
-      - run: nix build .#test-ixvm --accept-flake-config
 
   # Tests Nix devShell support on Ubuntu
   nix-devshell:

Benchmarks/Blake3.lean

@@ -45,16 +45,22 @@ def blake3Bench : IO $ Array BenchReport := do
   bgroup "prove blake3" benches.toList { oneShot := true }
 
 def parseFunction (words : List String) (param : String): Option String :=
-  words.find? (·.startsWith param) |> .map (·.stripPrefix param)
+  words.find? (·.startsWith param) |> .map (·.dropPrefix param |>.toString)
 
 def main : IO Unit := do
   let result ← blake3Bench
   let mut sumWeights := 0.0
   let mut weightedSum := 0.0
   for report in result do
     let words := report.function.splitOn
-    let dataSize := (parseFunction words "dataSize=").get!.toNat!
-    let numHashes := (parseFunction words "numHashes=").get!.toNat!
+    let .some dataSizeStr := parseFunction words "dataSize="
+      | throw $ IO.userError s!"Missing dataSize in: {report.function}"
+    let .some dataSize := dataSizeStr.toNat?
+      | throw $ IO.userError s!"Invalid dataSize: {dataSizeStr}"
+    let .some numHashesStr := parseFunction words "numHashes="
+      | throw $ IO.userError s!"Missing numHashes in: {report.function}"
+    let .some numHashes := numHashesStr.toNat?
+      | throw $ IO.userError s!"Invalid numHashes: {numHashesStr}"
     let sizeFloat := (dataSize * numHashes).toFloat
     let throughput := sizeFloat / (report.newBench.getTime.toSeconds )
     weightedSum := weightedSum + sizeFloat * throughput

Benchmarks/Sha256.lean

@@ -45,7 +45,7 @@ def sha256Bench : IO $ Array BenchReport := do
   bgroup "prove sha256" benches.toList { oneShot := true }
 
 def parseFunction (words : List String) (param : String): Option String :=
-  words.find? (·.startsWith param) |> .map (·.stripPrefix param)
+  words.find? (·.startsWith param) |>.map (·.dropPrefix param |>.toString)
 
 def main : IO Unit := do
   let result ← sha256Bench

Ix/Common.lean

@@ -279,8 +279,10 @@ def checkToolchain : IO Unit := do
   match ← runCmd' "lake" #["--version"] with
   | .error e => throw $ IO.userError e
   | .ok out =>
-    let version := (out.splitOn "(Lean version ")[1]!
-    let version := version.splitOn ")" |>.head!
+    let .some version := (out.splitOn "(Lean version ")[1]?
+      | throw $ IO.userError s!"Could not parse Lean version from: {out}"
+    let .some version := (version.splitOn ")").head?
+      | throw $ IO.userError s!"Could not parse Lean version from: {out}"
     let expectedVersion := Lean.versionString
     if version != expectedVersion then
       IO.println s!"Warning: expected toolchain '{expectedVersion}' but got '{version}'"
@@ -298,7 +300,7 @@ def runFrontend (input : String) (filePath : FilePath) : IO Environment := do
   let msgs := s.commandState.messages
   if msgs.hasErrors then
     throw $ IO.userError $ "\n\n".intercalate $
-      (← msgs.toList.mapM (·.toString)).map String.trim
+      (← msgs.toList.mapM (·.toString)).map (String.trimAscii · |>.toString)
   else return s.commandState.env
 
 end Lean

Ix/Meta.lean

@@ -14,7 +14,7 @@ def getFileEnv (path : FilePath) : IO Environment := do
     args := #["env", "printenv", "LEAN_PATH"]
     cwd := path.parent
   }
-  let paths := out.stdout.trim.splitOn ":" |>.map FilePath.mk
+  let paths := out.stdout.trimAscii.toString.splitOn ":" |>.map FilePath.mk
   initSearchPath (← findSysroot) paths
 
   let source ← IO.FS.readFile path
@@ -23,7 +23,7 @@ def getFileEnv (path : FilePath) : IO Environment := do
   let (env, messages) ← processHeader header default messages inputCtx 0
   if messages.hasErrors then
     throw $ IO.userError $ "\n\n".intercalate $
-      (← messages.toList.mapM (·.toString)).map String.trim
+      (← messages.toList.mapM (·.toString)).map (String.trimAscii · |>.toString)
   return env
 
 elab "this_file!" : term => do

Ix/Store.lean

@@ -41,12 +41,11 @@ def storeDir : StoreIO FilePath := do
 def storePath (addr: Address): StoreIO FilePath := do
   let store <- storeDir
   let hex := hexOfBytes addr.hash
-  -- TODO: Use Slice API once it matures
-  let hexChars := hex.toSlice.chars.toList
-  let dir1 := String.ofList [hexChars[0]!, hexChars[1]!]
-  let dir2 := String.ofList [hexChars[2]!, hexChars[3]!]
-  let dir3 := String.ofList [hexChars[4]!, hexChars[5]!]
-  let file := hex.drop 6
+  let s := hex.toSlice
+  let dir1 := (s.take 2).toString
+  let dir2 := (s.drop 2 |>.take 2).toString
+  let dir3 := (s.drop 4 |>.take 2).toString
+  let file := (s.drop 6).toString
   let path := store / dir1 / dir2 / dir3
   if !(<- path.pathExists) then
     IO.toEIO .ioError (IO.FS.createDirAll path)

Tests.lean

@@ -1,19 +1 @@
-import Tests.Aiur
-import Tests.AiurHashes
-import Tests.ByteArray
-import Tests.Ix.Ixon
-import Tests.Ix.Claim
-import Tests.Ix.Commit
-import Tests.Ix.Compile
-import Tests.Ix.Decompile
-import Tests.Ix.RustSerialize
-import Tests.Ix.RustDecompile
-import Tests.Ix.Sharing
-import Tests.Ix.CanonM
-import Tests.Ix.GraphM
-import Tests.Ix.CondenseM
-import Tests.FFI
-import Tests.Keccak
-import Tests.Cli
-import Tests.ShardMap
-import Tests.Common
+import Tests.Main