chore: fix tests

Author: tydeu

src/lake/Lake/Build/Module.lean

@@ -374,8 +374,8 @@ private def fetchImportInfo
     else if n = 1 then -- common fast path
       let mod := mods[0]
       if imp.importAll && !mod.allowImportAll && pkgName != mod.pkg.name then
-        logError s!"{fileName}: cannot 'import all' \
-          the module `{imp.module}` from {mod.pkg.discriminant}"
+        logError s!"{fileName}: cannot `import all` \
+          the module `{imp.module}` from the package `{mod.pkg.discriminant}`"
         return .error
       let importJob ← mod.exportInfo.fetch
       return s.zipWith (sync := true) (·.addImport nonModule imp ·) importJob

tests/lake/tests/module/test.sh

@@ -20,7 +20,7 @@ public def foo : String := "bar"
 EOF
 
 # Test cross-package `import all` is prevented by default
-test_err "cannot 'import all' across packages" build ErrorTest.CrossPackageImportAll
+test_err 'cannot `import all` the module' build ErrorTest.CrossPackageImportAll
 # Test cross-package `import all` is allowed when `allowImportAll = true` is set
 test_run build Test.CrossPackageImportAll
 

tests/lake/tests/toml/Test.lean

@@ -69,13 +69,13 @@ def expectPrimitive (actualTy : String) (expected : Json) : Except String String
     throw s!"expected value of type '{ty}', got '{actualTy}'"
   return val
 
-def decodeSign (s : String) : Bool × String :=
+def decodeSign (s : String) : Bool × String.Slice :=
   if s.front == '-' then
     (true, s.drop 1)
   else if s.front == '+' then
     (false, s.drop 1)
   else
-    (false, s)
+    (false, s.toSlice)
 
 mutual
 
@@ -91,13 +91,13 @@ partial def expectValue (actual : Value) (expected : Json) : Except String Unit
         throw s!"expected '{expected}', got '{actN}'"
     else
       let (neg, e) := decodeSign expected
-      if e.toLower == "inf" then
+      if e.eqIgnoreAsciiCase "inf".toSlice then
         unless actN.isInf && neg == (actN < 0) do
           throw s!"expected '{e}', got '{actN}'"
       else
           let some flt :=
             (Nat.toFloat <$> e.toNat?) <|>
-            (Syntax.decodeScientificLitVal? e |>.map fun (m,s,e) => .ofScientific m s e)
+            (Syntax.decodeScientificLitVal? e.copy |>.map fun (m,s,e) => Float.ofScientific m s e)
             | throw s!"failed to parse expected float value: {e}"
           expectBEq actN <| if neg then -flt else flt
   | .dateTime _ dt =>
@@ -132,11 +132,6 @@ def expectJson (actual expected : Json) : TestOutcome :=
   if actual == expected then .pass s else .fail s
 
 def testValid (tomlFile : FilePath) : BaseIO TestOutcome := do
-  -- Tests skipped due to bugs in Lean's JSON parser
-  -- TODO: Fix JSON parser (high-low unicode escape pairs)
-  let normPath := tomlFile.toString.map fun c => if c = '\\' then '/' else c
-  for testPath in ["string/quoted-unicode.toml", "key/quoted-unicode.toml"] do
-    if normPath.endsWith testPath then return .skip
   match (← loadToml tomlFile) with
   | .pass t =>
     match (← IO.FS.readFile (tomlFile.withExtension "json") |>.toBaseIO) with
@@ -145,7 +140,7 @@ def testValid (tomlFile : FilePath) : BaseIO TestOutcome := do
       | .ok j =>
         match expectTable t j with
         | .ok _ => return .pass <| ppTable t
-        | .error e => return .fail <| e.trimRight.push '\n'
+        | .error e => return .fail <| e.trimAsciiEnd.copy.push '\n'
       | .error e => return .error s!"invalid JSON: {e}"
     | .error e => return .error (toString e)
   | .fail l => return .fail (← mkMessageLogString l)