Switch to using Lean to run the tests (so it runs on Windows)

.github/workflows/build.yml

@@ -9,7 +9,7 @@ on:
   workflow_dispatch:
 
 jobs:
-  build: 
+  build:
     name: ${{ matrix.name }}
     runs-on: ${{ matrix.os }}
     defaults:
@@ -25,7 +25,7 @@ jobs:
           os: macos-latest
         - name: Windows
           os: windows-latest
-          shell: msys2 {0}
+          shell: pwsh
     steps:
       # Checkout repository
       - uses: actions/checkout@v2
@@ -35,32 +35,26 @@ jobs:
         if: matrix.os == 'macos-latest'
         run: |
           set -o pipefail
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      
+
       - name: Install Elan (Ubuntu)
         if: matrix.os == 'ubuntu-latest'
         run: |
-          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: Install MSYS2 (Windows)
-        if: matrix.os == 'windows-latest'
-        uses: msys2/setup-msys2@v2
-        with:
-          path-type: inherit
-          install: curl unzip make mingw-w64-x86_64-gcc mingw-w64-x86_64-gmp diffutils
       - name: Install Elan (Windows)
         if: matrix.os == 'windows-latest'
         run: |
-          curl -sSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh > elan-init.sh
-          ./elan-init.sh -y
-          cygpath -w "$USERPROFILE/.elan/bin" >> $GITHUB_PATH
+          curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
+          .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain none
+          echo "$HOME\.elan\bin" >> $env:GITHUB_PATH
 
       # Build and test
       - name: Build LeanInk
         run: lake build
-        
+
       # Upload artifact
       - name: Upload artifacts
         uses: actions/upload-artifact@v2
@@ -69,4 +63,4 @@ jobs:
           path: build
 
       - name: Run tests
-        run: make -C test run_tests
+        run: lake script run tests

README.md

@@ -11,7 +11,7 @@ For more information about Alectryon make sure to take a look at their repositor
 
 # Installation
 
-You can either build LeanInk and install it yourself or use the build script to install a LeanInk release version:
+You can either build LeanInk and install it yourself as shown below, or you can use the build script to install a LeanInk release version:
 
 ```bash
 sh -c "$(curl https://raw.githubusercontent.com/leanprover/LeanInk/main/init.sh -sSf)"
@@ -28,6 +28,8 @@ cd LeanInk
 lake build
 ```
 
+To install this built version it is recommended you simply add the `LeanInk/build/bin` folder to your PATH environment.
+
 # Usage
 
 Analyzing a simple lean program `Input.lean` is very straightforward. To do so you simply use the `analyze` command (shorthand `a`) and provide LeanInk the input file.
@@ -93,9 +95,9 @@ 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 `make -C test 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.
+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 `make -C test capture` to capture the output for all files or use leanInk itself to generate an output for a single file and rename it afterwards.
+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.
 
 # Contributing
 

init.sh

@@ -4,6 +4,4 @@ cd leanInk
 git fetch --tags -q
 latestTag=$(git describe --tags `git rev-list --tags --max-count=1`)
 git checkout $latestTag -q
-sh install.sh
-cd ..
-rm -rf ./leanInk
+lake script run install && cd .. && rm -rf ./leanInk

lakefile.lean

@@ -1,5 +1,7 @@
 import Lake
+import Init.System.IO
 open System Lake DSL
+open System.FilePath IO IO.FS
 
 package leanInk
 
@@ -10,3 +12,104 @@ lean_exe leanInk {
   root := `Main
   supportInterpreter := true
 }
+
+/-! 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 (leanInkExe: FilePath) (test : FilePath) : IO UInt32 := do
+  let realPath ← realPath leanInkExe
+  if ! (← leanInkExe.pathExists) then
+    println s!"Could not find leanInk executable at {leanInkExe}"
+    println s!"Please run `lake build` in the LeanInk directory"
+    return 1
+
+  if let some fileName := test.fileName then
+    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 (← lakefile.pathExists) then
+        println s!"Running test {test} using lake..."
+        args := args ++ #["--lake", "lakefile.lean"]
+      else
+        println s!"Running test {test}..."
+
+    let out ← Process.output { cmd := realPath.normalize.toString, args := args, cwd := test.parent }
+    if out.exitCode = 0 then
+      return 0
+    else
+      println s!"leanInk failed with {out.stdout} {out.stderr}"
+      return out.exitCode
+  return 1
+
+/-! Compare the text contents of two files -/
+def runDiff (actual : FilePath) (expected : FilePath) : IO Bool := do
+  let actualStr ← FS.readFile actual
+  let expectedStr ← FS.readFile expected
+  return actualStr.trim = expectedStr.trim
+
+def copyFile (src : FilePath) (dst : FilePath) : IO Unit := do
+  FS.writeBinFile dst (← FS.readBinFile src)
+
+def indexOf? [BEq α] (xs : List α) (s : α) (start := 0): Option Nat :=
+  match xs with
+  | [] => none
+  | a :: tail => if a == s then some start else indexOf? tail s (start+1)
+
+/-! 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 (leanInkExe: FilePath) (capture : Bool) : IO UInt32 := do
+  let root : FilePath := "." / "test"
+  let dirs ← walkDir root
+  let mut retVal : UInt32 := 0
+  for test in dirs do
+    if test.extension = "lean" && test.fileName != "lakefile.lean" && !test.components.contains "lean_packages" then
+      if let some fileName := test.fileName then
+        let actual := test.withFileName (fileName ++ ".leanInk")
+        let expected := test.withFileName (fileName ++ ".leanInk.expected")
+        if (← expected.pathExists) then
+          let rc ← runLeanInk leanInkExe test
+          if rc ≠ 0 then
+            return 1
+          else if (capture) then
+            println s!"  UPDATING {expected}"
+            copyFile actual expected
+          else
+            if (← runDiff actual expected) then
+              println s!"  SUCCESS"
+            else
+              println s!"  FAILED: diff {expected} {actual}"
+              retVal := retVal + 1
+        else
+          println s!"  FAILED: expected output file is missing: {expected}"
+          retVal := retVal + 1
+
+  if retVal > 0 then
+    println s!"FAILED: {retVal} tests failed!"
+  return retVal
+
+def getLeanInkExePath : ScriptM (Option FilePath) := do
+  let ws ← Lake.getWorkspace
+  if let some exe := ws.findLeanExe? `leanInk then
+    return exe.file
+  return none
+
+script tests (args) do
+  if args.length > 0 then
+    println s!"Unexpected arguments: {args}"
+  if let some leanInkExe ← getLeanInkExePath then
+    println "Running diff tests for leanInk"
+    execute leanInkExe False
+  else
+    println "Cannot find `leanInk` target path"
+    return 1
+
+script capture (args) do
+  if args.length > 0 then
+    println s!"Unexpected arguments: {args}"
+  if let some leanInkExe ← getLeanInkExePath then
+    println "Updating .leanInk.expected output files"
+    execute leanInkExe True
+  else
+    println "Cannot find `leanInk` target path"
+    return 1