From f548a15aa0dd4c91bc5a4ceba10d252de19fd506 Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Thu, 1 Sep 2022 09:58:06 -0700
Subject: [PATCH] fix: code review comments

---
 .github/workflows/build.yml |  2 +-
 README.md                   |  2 +-
 lakefile.lean               | 36 +++++++++++++++---------------------
 3 files changed, 17 insertions(+), 23 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 936586c..75e94fa 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -63,4 +63,4 @@ jobs:
           path: build
 
       - name: Run tests
-        run: lake script run runTests
+        run: lake script run tests
diff --git a/README.md b/README.md
index 36ffcc6..858af6d 100644
--- a/README.md
+++ b/README.md
@@ -93,7 +93,7 @@ There are some aspects you might want to take note of when attempting to develop
 
 LeanInk uses simple diffing tests to make sure the core functionality works as expected. These tests are located in the `./test` folder.
 
-You can run these tests using `lake script run runTests`. This will run LeanInk for every `.lean`, that's not a `lakefile` or part of an `lean_package`. It will compare the output of LeanInk to the expected output within the `.lean.leanInk.expected` file.
+You can run these tests using `lake script run tests`. This will run LeanInk for every `.lean`, that's not a `lakefile` or part of an `lean_package`. It will compare the output of LeanInk to the expected output within the `.lean.leanInk.expected` file.
 
 To capture a new expected output file you can either run `lake script run capture` to capture the output for all files or use leanInk itself to generate an output for a single file and rename it afterwards.  Be sure to carefully examine the git diff before committing the new expected baselines.
 
diff --git a/lakefile.lean b/lakefile.lean
index 25e6ed2..8f2d2cd 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,17 +13,14 @@ lean_exe leanInk {
   supportInterpreter := true
 }
 
-def fileExists (p : FilePath) : IO Bool :=
-  return (← p.metadata.toBaseIO).toBool
-
 /-! Run the leanInk that is built locally to analyze the given test file.
 If there is a lakefile.lean present then pass the additional `--lake` option -/
 def runLeanInk (test : FilePath) : IO UInt32 := do
-  let buildDir : FilePath := "build" / "bin"
-  let leanInkExe := if Platform.isWindows then buildDir / "leanInk.exe" else buildDir / "leanInk"
+  let leanInk : FilePath := "build" / "bin" / "leanInk"
+  let leanInkExe := leanInk.withExtension FilePath.exeExtension
   let realPath ← IO.FS.realPath leanInkExe
 
-  if ! (← fileExists leanInkExe) then
+  if ! (← leanInkExe.pathExists) then
     IO.println s!"Could not find leanInk executable at {leanInkExe}"
     IO.println s!"Please run `lake build` in the LeanInk directory"
     return 1
@@ -32,7 +29,7 @@ def runLeanInk (test : FilePath) : IO UInt32 := do
     let mut args := #["analyze", fileName, "--x-enable-type-info", "--x-enable-docStrings", "--x-enable-semantic-token", "--prettify-output"]
     if let some dir := test.parent then
       let lakefile := dir / "lakefile.lean"
-      if (← fileExists lakefile) then
+      if (← lakefile.pathExists) then
         IO.println s!"Running test {test} using lake..."
         args := args ++ #["--lake", "lakefile.lean"]
       else
@@ -47,20 +44,18 @@ def runLeanInk (test : FilePath) : IO UInt32 := do
   return 1
 
 /-! Compare the text contents of two files -/
-def runDiff (actual : FilePath) (expected : FilePath) : IO UInt32 := do
+def runDiff (actual : FilePath) (expected : FilePath) : IO Bool := do
   let actualStr ← IO.FS.readFile actual
   let expectedStr ← IO.FS.readFile expected
-  if actualStr.trim = expectedStr.trim then
-    return 0
-  else
-    return 1
+  return actualStr.trim = expectedStr.trim
 
 def copyFile (src : FilePath) (dst : FilePath) : IO Unit := do
   IO.FS.writeFile dst (← IO.FS.readFile src)
 
-/-! Walk the 'test' folder looking for every `.lean` file that's not a `lakefile` or part of an `lean_package`.
-If `capture` is true then update the `.lean.leanInk.expected` file, otherwise compare the new output
-to the expected output and return an error if they are different. -/
+/-! Walk the `test` folder looking for every `.lean` file that's not a `lakefile` or part of an
+`lean_package` and run `leanInk` on it. If `capture` is true then update the `.lean.leanInk.expected`
+file, otherwise compare the new output to the expected output and return an error if they are
+different. -/
 def execute (capture : Bool) : IO UInt32 := do
   let root : FilePath := "." / "test"
   let dirs ← walkDir root
@@ -69,7 +64,7 @@ def execute (capture : Bool) : IO UInt32 := do
       if let some fileName := test.fileName then
         let actual := test.withFileName (fileName ++ ".leanInk")
         let expected := test.withFileName (fileName ++ ".leanInk.expected")
-        if (← fileExists expected) then
+        if (← expected.pathExists) then
           let rc ← runLeanInk test
           if rc ≠ 0 then
             return 1
@@ -77,18 +72,17 @@ def execute (capture : Bool) : IO UInt32 := do
             IO.println s!"  UPDATING {expected}"
             copyFile actual expected
           else
-            let d ← runDiff actual expected
-            if d = 0 then
+            if (← runDiff actual expected) then
               IO.println s!"  SUCCESS"
             else
               IO.println s!"  FAILED: diff {expected} {actual}"
               return 1
   return 0
 
-script runTests (args) do
+script tests (args) do
   IO.println "Running diff tests for leanInk"
-  return ← execute False
+  execute False
 
 script capture (args) do
   IO.println "Updating .leanInk.expected output files"
-  return ← execute True
\ No newline at end of file
+  execute True
\ No newline at end of file