From 7ec3bed074ec9cc1d1bac837dd6d4f9d686f6307 Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Wed, 31 Aug 2022 18:50:41 -0700
Subject: [PATCH 01/15] Switch to using Lean to run the tests (so it runs on
 Windows)

---
 README.md     |  4 +--
 lakefile.lean | 82 ++++++++++++++++++++++++++++++++++++++++++++++++
 test/Makefile | 10 ------
 test/test.sh  | 87 ---------------------------------------------------
 4 files changed, 84 insertions(+), 99 deletions(-)
 delete mode 100644 test/Makefile
 delete mode 100755 test/test.sh

diff --git a/README.md b/README.md
index 2e456b0..36ffcc6 100644
--- a/README.md
+++ b/README.md
@@ -93,9 +93,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 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.
 
-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
 
diff --git a/lakefile.lean b/lakefile.lean
index 5731248..359ae4f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,5 +1,7 @@
 import Lake
+import Init.System.IO
 open System Lake DSL
+open System.FilePath
 
 package leanInk
 
@@ -10,3 +12,83 @@ lean_exe leanInk {
   root := `Main
   supportInterpreter := true
 }
+
+def fileExists (p : FilePath) : BaseIO 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 realPath ← IO.FS.realPath leanInkExe
+
+  if ! (← fileExists leanInkExe) then
+    IO.println s!"Could not find leanInk executable at {leanInkExe}"
+    IO.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 (← fileExists lakefile) then
+        IO.println s!"Running test {test} using lake..."
+        args := args ++ #["--lake", "lakefile.lean"]
+      else
+        IO.println s!"Running test {test}..."
+
+    let out ← IO.Process.output { cmd := realPath.normalize.toString, args := args, cwd := test.parent }
+    if out.exitCode = 0 then
+      return 0
+    else
+      IO.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 UInt32 := do
+  let actualStr ← IO.FS.readFile actual
+  let expectedStr ← IO.FS.readFile expected
+  if actualStr.trim = expectedStr.trim then
+    return 0
+  else
+    return 1
+
+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. -/
+def execute (capture : Bool) : IO UInt32 := do
+  let root : FilePath := "." / "test"
+  let dirs ← walkDir root
+  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 (← fileExists expected) then
+          let rc ← runLeanInk test
+          if rc ≠ 0 then
+            return 1
+          else if (capture) then
+            IO.println s!"  UPDATING {expected}"
+            copyFile actual expected
+          else
+            let d ← runDiff actual expected
+            if d = 0 then
+              IO.println s!"  SUCCESS"
+            else
+              IO.println s!"  FAILED: diff {expected} {actual}"
+              return 1
+  return 0
+
+script runTests (args) do
+  IO.println "Running diff tests for leanInk"
+  return ← execute False
+
+script capture (args) do
+  IO.println "Updating .leanInk.expected output files"
+  return ← execute True
\ No newline at end of file
diff --git a/test/Makefile b/test/Makefile
deleted file mode 100644
index cf5b01a..0000000
--- a/test/Makefile
+++ /dev/null
@@ -1,10 +0,0 @@
-LEANINK ?= ../build/bin/leanInk
-
-build:
-	./test.sh build_leanink
-
-capture: 
-	./test.sh run_capture
-
-run_tests:
-	./test.sh run_tests
\ No newline at end of file
diff --git a/test/test.sh b/test/test.sh
deleted file mode 100755
index 79cd335..0000000
--- a/test/test.sh
+++ /dev/null
@@ -1,87 +0,0 @@
-#!/usr/bin/env bash
-
-ulimit -s 8192
-DIFF=diff
-if diff --color --help >/dev/null 2>&1; then
-    DIFF="diff --color";
-fi
-
-_realpath () (
-  OURPWD=$PWD
-  cd "$(dirname "$1")"
-  LINK=$(readlink "$(basename "$1")")
-  while [ "$LINK" ]; do
-    cd "$(dirname "$LINK")"
-    LINK=$(readlink "$(basename "$1")")
-  done
-  REALPATH="$PWD/$(basename "$1")"
-  cd "$OURPWD"
-  echo "$REALPATH"
-)
-
-REALPATH=realpath
-
-if ! command -v realpath &> /dev/null; then
-    REALPATH=_realpath
-fi
-
-LEANINK=$($REALPATH "../build/bin/leanInk")
-
-error () {
-    echo $1
-    exit 1
-}
-
-build_leanink () {
-    lake build || error "Failed to compile leanInk"zsh -df
-}
-
-run_leanink () {
-    file=$1
-    directory=${file%/*}
-    filename=${file##*/}
-    # If the folder in which the file resides contains a lakefile we will use it to resolve any dependencies for the file
-    if [[ -f "$directory/lakefile.lean" ]]; then
-        echo "Running LeanInk with lakefile.lean - $file"
-        (cd $directory && $LEANINK analyze $filename --x-enable-type-info --x-enable-docStrings --x-enable-semantic-token --lake lakefile.lean --prettify-output) || error "LeanInk failed - $file"
-    else
-        echo "Running LeanInk - $file"
-        (cd $directory && $LEANINK analyze $filename --x-enable-type-info --x-enable-docStrings --x-enable-semantic-token --prettify-output) || error "LeanInk failed - $file"
-    fi
-}
-
-run_tests () {
-    echo "Running diff tests for leanInk"
-    retVal=0
-    for file in $(find . -name '*.lean'); do
-        if [[ ${file##*/} != "lakefile.lean" && $file != *"/lean_packages/"* ]]; then 
-            if test "$file.leanInk.expected"; then
-                run_leanink $file
-                if $DIFF -au --strip-trailing-cr "$file.leanInk.expected" "$file.leanInk"; then
-                    echo "SUCCESSFULL! ($file)"
-                else
-                    echo "FAILED! ($file)"
-                    retVal=1
-                fi
-            else
-                error "No expected output file found: $file.leanInk.expected"
-            fi
-        fi
-    done
-
-    exit $retVal
-}
-
-run_capture () {
-    echo "Create new expected output files for leanInk tests. Overriding previous output files!"
-    for file in $(find . -name '*.lean'); do
-        if [[ ${file##*/} != "lakefile.lean" ]] && [[ $file != *"/lean_packages/"* ]]; then 
-            run_leanink $file
-            mv "$file.leanInk" "$file.leanInk.expected"
-            echo "Generated $file.leanInk.expected"
-        fi
-    done
-}
-
-# Allows to call a function based on arguments passed to the script
-$*

From 47b7b4597c74708c188f75406a747c1177fc27ed Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Wed, 31 Aug 2022 19:00:01 -0700
Subject: [PATCH 02/15] fix: update workflow

---
 .github/workflows/build.yml | 8 ++++----
 lakefile.lean               | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index f600a7c..ada95c9 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -9,7 +9,7 @@ on:
   workflow_dispatch:
 
 jobs:
-  build: 
+  build:
     name: ${{ matrix.name }}
     runs-on: ${{ matrix.os }}
     defaults:
@@ -37,7 +37,7 @@ jobs:
           set -o pipefail
           curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly -y
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      
+
       - name: Install Elan (Ubuntu)
         if: matrix.os == 'ubuntu-latest'
         run: |
@@ -60,7 +60,7 @@ jobs:
       # Build and test
       - name: Build LeanInk
         run: lake build
-        
+
       # Upload artifact
       - name: Upload artifacts
         uses: actions/upload-artifact@v2
@@ -69,4 +69,4 @@ jobs:
           path: build
 
       - name: Run tests
-        run: make -C test run_tests
+        run: lake script run runTests
diff --git a/lakefile.lean b/lakefile.lean
index 359ae4f..25e6ed2 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,7 +13,7 @@ lean_exe leanInk {
   supportInterpreter := true
 }
 
-def fileExists (p : FilePath) : BaseIO Bool :=
+def fileExists (p : FilePath) : IO Bool :=
   return (← p.metadata.toBaseIO).toBool
 
 /-! Run the leanInk that is built locally to analyze the given test file.

From 2d428f6ddd2404cd88cf67c4f4c7926b61f8afe7 Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Wed, 31 Aug 2022 19:06:42 -0700
Subject: [PATCH 03/15] fix: optimize workflow

---
 .github/workflows/build.yml | 18 ++++++------------
 1 file changed, 6 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index ada95c9..bea225a 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -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,27 +35,21 @@ 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" >> $GITHUB_PATH
 
       # Build and test
       - name: Build LeanInk

From 7712fb3220d630488bad25f0c9520a91bcbbcc72 Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Wed, 31 Aug 2022 19:10:26 -0700
Subject: [PATCH 04/15] fix: GITHUB_PATH has to use backslashes on windows.

---
 .github/workflows/build.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index bea225a..936586c 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -49,7 +49,7 @@ jobs:
         run: |
           curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
           .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+          echo "$HOME\.elan\bin" >> $env:GITHUB_PATH
 
       # Build and test
       - name: Build LeanInk

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 05/15] 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

From 93447fd743c448f0d2b7eb3b59be6dec625bb7cf Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Thu, 1 Sep 2022 10:04:50 -0700
Subject: [PATCH 06/15] fix: run all tests so we can report how many tests
 failed

---
 lakefile.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index 8f2d2cd..ea8d9a3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -59,6 +59,7 @@ different. -/
 def execute (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
@@ -76,8 +77,10 @@ def execute (capture : Bool) : IO UInt32 := do
               IO.println s!"  SUCCESS"
             else
               IO.println s!"  FAILED: diff {expected} {actual}"
-              return 1
-  return 0
+              retVal := retVal + 1
+  if retVal > 0 then
+    IO.println s!"FAILED: {retVal} tests failed!"
+  return retVal
 
 script tests (args) do
   IO.println "Running diff tests for leanInk"

From cbf73c9ab11a50e82b2194474532a6f3f2d2a9de Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Thu, 1 Sep 2022 10:09:46 -0700
Subject: [PATCH 07/15] fix: add reporting of missing expected output files .

---
 lakefile.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/lakefile.lean b/lakefile.lean
index ea8d9a3..cae14af 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -78,6 +78,10 @@ def execute (capture : Bool) : IO UInt32 := do
             else
               IO.println s!"  FAILED: diff {expected} {actual}"
               retVal := retVal + 1
+        else
+          IO.println s!"  FAILED: expected output file is missing: {expected}"
+          retVal := retVal + 1
+
   if retVal > 0 then
     IO.println s!"FAILED: {retVal} tests failed!"
   return retVal

From 03460c5571ff02cf83103ebc8e5f884ddfbbf873 Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Thu, 1 Sep 2022 18:47:48 -0700
Subject: [PATCH 08/15] fix: Port the install.sh to lakefile.lean also.

---
 README.md     |  7 ++++++-
 init.sh       |  4 +---
 install.sh    | 34 ----------------------------------
 lakefile.lean | 51 ++++++++++++++++++++++++++++++++++++++++++++++-----
 4 files changed, 53 insertions(+), 43 deletions(-)
 delete mode 100644 install.sh

diff --git a/README.md b/README.md
index 858af6d..eccc869 100644
--- a/README.md
+++ b/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,11 @@ cd LeanInk
 lake build
 ```
 
+To install this built version to your `$HOME/.elan/bin` folder run:
+```bash
+lake script run install
+```
+
 # 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.
diff --git a/init.sh b/init.sh
index 39c73fe..c39da19 100644
--- a/init.sh
+++ b/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
\ No newline at end of file
+lake script run install && cd .. && rm -rf ./leanInk
\ No newline at end of file
diff --git a/install.sh b/install.sh
deleted file mode 100644
index 4ea6b32..0000000
--- a/install.sh
+++ /dev/null
@@ -1,34 +0,0 @@
-#!/bin/bash
-
-error () {
-    echo $1
-}
-
-echo "Compiling LeanInk..."
-# First we have to build leanInk.
-lake build > /dev/null || error "Failed to build leanInk. Make sure your lean install is correct!"
-
-# As we can assume that lean is already installed as expected we can assume
-# that the .elan folder already exists and is correctly linked.
-ELAN_BIN="$HOME/.elan/bin/"
-
-echo "Installing LeanInk..."
-if [[ -f "$ELAN_BIN/leanInk" ]]; then
-    OLD_LEAN_INK=$(eval "$ELAN_BIN/leanInk -v")
-    NEW_LEAN_INK=$(eval "./build/bin/leanInk -v")
-    echo "LeanInk ($OLD_LEAN_INK) already installed. Do you want to overwrite it with LeanInk ($NEW_LEAN_INK) [Y|n]?"
-    read < /dev/stdin
-    SHOULD_OVERWRITE="$(tr '[:upper:]' '[:lower:]' <<< "${REPLY}")"
-    if [[ "${SHOULD_OVERWRITE}" == "y" ]]; then 
-        cp -f ./build/bin/leanInk ~/.elan/bin/ || error "Failed copying LeanInk to .elan/bin!"
-        echo "New LeanInk version successfully installed!"
-    else
-        echo "New LeanInk version not installed!"
-    fi
-else        
-    if cp ./build/bin/leanInk "$ELAN_BIN"; then
-        echo "LeanInk version successfully installed!"
-    else
-        echo "Failed copying LeanInk to .elan/bin!"
-    fi
-fi
diff --git a/lakefile.lean b/lakefile.lean
index cae14af..83d5f8b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,12 +13,16 @@ lean_exe leanInk {
   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 (test : FilePath) : IO UInt32 := do
+def getLeanInkExePath : IO (FilePath × FilePath) := do
   let leanInk : FilePath := "build" / "bin" / "leanInk"
   let leanInkExe := leanInk.withExtension FilePath.exeExtension
   let realPath ← IO.FS.realPath leanInkExe
+  return (leanInkExe, realPath)
+
+/-! 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 (leanInkExe, realPath) ← getLeanInkExePath
 
   if ! (← leanInkExe.pathExists) then
     IO.println s!"Could not find leanInk executable at {leanInkExe}"
@@ -50,7 +54,25 @@ def runDiff (actual : FilePath) (expected : FilePath) : IO Bool := do
   return actualStr.trim = expectedStr.trim
 
 def copyFile (src : FilePath) (dst : FilePath) : IO Unit := do
-  IO.FS.writeFile dst (← IO.FS.readFile src)
+  IO.FS.writeBinFile dst (← IO.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)
+
+def getTargetLeanInkPath : IO (Option FilePath) := do
+  let (leanInkExe, _) ← getLeanInkExePath
+  let lakePath ← IO.appPath
+  let index := indexOf? lakePath.components ".elan"
+  if let some i := index then
+    if let some fileName := leanInkExe.fileName then
+      let elanPath := lakePath.components.take (i + 1)
+      let sep := pathSeparator.toString
+      let elanPath : FilePath := sep.intercalate elanPath
+      let leanInkPath := elanPath / "bin" / fileName
+      return some leanInkPath
+  return none
 
 /-! 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`
@@ -92,4 +114,23 @@ script tests (args) do
 
 script capture (args) do
   IO.println "Updating .leanInk.expected output files"
-  execute True
\ No newline at end of file
+  execute True
+
+script install (args) do
+  IO.println "Installing leanInk..."
+  IO.println "  Building leanInk..."
+  if let some targetPath ← getTargetLeanInkPath then
+    let (_, realPath) ← getLeanInkExePath
+    let out ← IO.Process.output { cmd := "lake", args := #["build"] }
+      if out.exitCode = 0 then
+        IO.println s!"  Built {realPath}..."
+        IO.println s!"  Installing {targetPath}..."
+        copyFile realPath targetPath
+        IO.println s!"  LeanInk successfully installed!"
+        return 0
+      else
+        IO.println s!"### Failed to build leanInk:\n{out.stdout} {out.stderr}"
+        return out.exitCode
+  else
+    IO.println "### Cannot find .elan target directory"
+    return 1

From d35a9ea66f48c91d5e1cd80394153bcf16cb174a Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Fri, 2 Sep 2022 09:40:57 -0700
Subject: [PATCH 09/15] fix: install leanink somewhere else - do not hijack
 elan install location.

---
 lakefile.lean | 76 +++++++++++++++++++++++++++------------------------
 1 file changed, 41 insertions(+), 35 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index 83d5f8b..eefd608 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -1,7 +1,7 @@
 import Lake
 import Init.System.IO
 open System Lake DSL
-open System.FilePath
+open System.FilePath IO IO.FS
 
 package leanInk
 
@@ -16,7 +16,7 @@ lean_exe leanInk {
 def getLeanInkExePath : IO (FilePath × FilePath) := do
   let leanInk : FilePath := "build" / "bin" / "leanInk"
   let leanInkExe := leanInk.withExtension FilePath.exeExtension
-  let realPath ← IO.FS.realPath leanInkExe
+  let realPath ← realPath leanInkExe
   return (leanInkExe, realPath)
 
 /-! Run the leanInk that is built locally to analyze the given test file.
@@ -25,8 +25,8 @@ def runLeanInk (test : FilePath) : IO UInt32 := do
   let (leanInkExe, realPath) ← getLeanInkExePath
 
   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"
+    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
@@ -34,27 +34,27 @@ def runLeanInk (test : FilePath) : IO UInt32 := do
     if let some dir := test.parent then
       let lakefile := dir / "lakefile.lean"
       if (← lakefile.pathExists) then
-        IO.println s!"Running test {test} using lake..."
+        println s!"Running test {test} using lake..."
         args := args ++ #["--lake", "lakefile.lean"]
       else
-        IO.println s!"Running test {test}..."
+        println s!"Running test {test}..."
 
-    let out ← IO.Process.output { cmd := realPath.normalize.toString, args := args, cwd := test.parent }
+    let out ← Process.output { cmd := realPath.normalize.toString, args := args, cwd := test.parent }
     if out.exitCode = 0 then
       return 0
     else
-      IO.println s!"leanInk failed with {out.stdout} {out.stderr}"
+      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 ← IO.FS.readFile actual
-  let expectedStr ← IO.FS.readFile expected
+  let actualStr ← FS.readFile actual
+  let expectedStr ← FS.readFile expected
   return actualStr.trim = expectedStr.trim
 
 def copyFile (src : FilePath) (dst : FilePath) : IO Unit := do
-  IO.FS.writeBinFile dst (← IO.FS.readBinFile src)
+  FS.writeBinFile dst (← FS.readBinFile src)
 
 def indexOf? [BEq α] (xs : List α) (s : α) (start := 0): Option Nat :=
   match xs with
@@ -63,15 +63,14 @@ def indexOf? [BEq α] (xs : List α) (s : α) (start := 0): Option Nat :=
 
 def getTargetLeanInkPath : IO (Option FilePath) := do
   let (leanInkExe, _) ← getLeanInkExePath
-  let lakePath ← IO.appPath
-  let index := indexOf? lakePath.components ".elan"
-  if let some i := index then
-    if let some fileName := leanInkExe.fileName then
-      let elanPath := lakePath.components.take (i + 1)
-      let sep := pathSeparator.toString
-      let elanPath : FilePath := sep.intercalate elanPath
-      let leanInkPath := elanPath / "bin" / fileName
-      return some leanInkPath
+  if let some fileName := leanInkExe.fileName then
+    let loc := if System.Platform.isWindows then "LOCALAPPDATA" else "HOME"
+    let val? ← getEnv loc
+    if let some homePath := val? then
+      let targetPath : FilePath := homePath / ".leanink" / "bin"
+      if !(← targetPath.pathExists) then
+        createDirAll targetPath
+      return some (targetPath / fileName)
   return none
 
 /-! Walk the `test` folder looking for every `.lean` file that's not a `lakefile` or part of an
@@ -92,45 +91,52 @@ def execute (capture : Bool) : IO UInt32 := do
           if rc ≠ 0 then
             return 1
           else if (capture) then
-            IO.println s!"  UPDATING {expected}"
+            println s!"  UPDATING {expected}"
             copyFile actual expected
           else
             if (← runDiff actual expected) then
-              IO.println s!"  SUCCESS"
+              println s!"  SUCCESS"
             else
-              IO.println s!"  FAILED: diff {expected} {actual}"
+              println s!"  FAILED: diff {expected} {actual}"
               retVal := retVal + 1
         else
-          IO.println s!"  FAILED: expected output file is missing: {expected}"
+          println s!"  FAILED: expected output file is missing: {expected}"
           retVal := retVal + 1
 
   if retVal > 0 then
-    IO.println s!"FAILED: {retVal} tests failed!"
+    println s!"FAILED: {retVal} tests failed!"
   return retVal
 
 script tests (args) do
-  IO.println "Running diff tests for leanInk"
+  if args.length > 0 then
+    println s!"Unexpected arguments: {args}"
+  println "Running diff tests for leanInk"
   execute False
 
 script capture (args) do
-  IO.println "Updating .leanInk.expected output files"
+  if args.length > 0 then
+    println s!"Unexpected arguments: {args}"
+  println "Updating .leanInk.expected output files"
   execute True
 
 script install (args) do
-  IO.println "Installing leanInk..."
-  IO.println "  Building leanInk..."
+  if args.length > 0 then
+    println s!"Unexpected arguments: {args}"
   if let some targetPath ← getTargetLeanInkPath then
+    println s!"Installing leanInk to {targetPath}"
+    println "Please ensure this location is in your PATH"
     let (_, realPath) ← getLeanInkExePath
-    let out ← IO.Process.output { cmd := "lake", args := #["build"] }
+    println "  Building leanInk..."
+    let out ← Process.output { cmd := "lake", args := #["build"] }
       if out.exitCode = 0 then
-        IO.println s!"  Built {realPath}..."
-        IO.println s!"  Installing {targetPath}..."
+        println s!"  Built {realPath}..."
+        println s!"  Copying to {targetPath}..."
         copyFile realPath targetPath
-        IO.println s!"  LeanInk successfully installed!"
+        println s!"  LeanInk successfully installed!"
         return 0
       else
-        IO.println s!"### Failed to build leanInk:\n{out.stdout} {out.stderr}"
+        println s!"### Failed to build leanInk:\n{out.stdout} {out.stderr}"
         return out.exitCode
   else
-    IO.println "### Cannot find .elan target directory"
+    println "### Cannot find .elan target directory"
     return 1

From a575e5a3c30d819c8f9f701e98a0b8d8dace669e Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Fri, 2 Sep 2022 10:00:19 -0700
Subject: [PATCH 10/15] fix: add more help on installation.

---
 lakefile.lean | 34 +++++++++++++++++++---------------
 1 file changed, 19 insertions(+), 15 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index eefd608..a7fb0fe 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,17 +13,15 @@ lean_exe leanInk {
   supportInterpreter := true
 }
 
-def getLeanInkExePath : IO (FilePath × FilePath) := do
+def getLeanInkExePath : FilePath :=
   let leanInk : FilePath := "build" / "bin" / "leanInk"
-  let leanInkExe := leanInk.withExtension FilePath.exeExtension
-  let realPath ← realPath leanInkExe
-  return (leanInkExe, realPath)
+  leanInk.withExtension FilePath.exeExtension
 
 /-! 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 (leanInkExe, realPath) ← getLeanInkExePath
-
+  let leanInkExe := getLeanInkExePath
+  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"
@@ -61,8 +59,8 @@ def indexOf? [BEq α] (xs : List α) (s : α) (start := 0): Option Nat :=
   | [] => none
   | a :: tail => if a == s then some start else indexOf? tail s (start+1)
 
-def getTargetLeanInkPath : IO (Option FilePath) := do
-  let (leanInkExe, _) ← getLeanInkExePath
+def getTargetLeanInkPath : IO (Option (FilePath × FilePath)) := do
+  let leanInkExe := getLeanInkExePath
   if let some fileName := leanInkExe.fileName then
     let loc := if System.Platform.isWindows then "LOCALAPPDATA" else "HOME"
     let val? ← getEnv loc
@@ -70,7 +68,7 @@ def getTargetLeanInkPath : IO (Option FilePath) := do
       let targetPath : FilePath := homePath / ".leanink" / "bin"
       if !(← targetPath.pathExists) then
         createDirAll targetPath
-      return some (targetPath / fileName)
+      return (targetPath, targetPath / fileName)
   return none
 
 /-! Walk the `test` folder looking for every `.lean` file that's not a `lakefile` or part of an
@@ -123,15 +121,21 @@ script install (args) do
   if args.length > 0 then
     println s!"Unexpected arguments: {args}"
   if let some targetPath ← getTargetLeanInkPath then
-    println s!"Installing leanInk to {targetPath}"
-    println "Please ensure this location is in your PATH"
-    let (_, realPath) ← getLeanInkExePath
+    println s!"Installing leanInk to {targetPath.1}"
+    println "Please ensure this location is in your PATH using:"
+    if System.Platform.isWindows then
+      println s!"set PATH=%PATH%:{targetPath.1}"
+    else
+      println s!"echo 'export PATH=$PATH:{targetPath.1}' >> ~/.profile && source ~/.profile"
     println "  Building leanInk..."
     let out ← Process.output { cmd := "lake", args := #["build"] }
       if out.exitCode = 0 then
-        println s!"  Built {realPath}..."
-        println s!"  Copying to {targetPath}..."
-        copyFile realPath targetPath
+        let leanInkExe := getLeanInkExePath
+        let realPath ← realPath leanInkExe
+        println s!"  Built {realPath}"
+        println s!"  Copying to {targetPath}"
+        copyFile realPath targetPath.2
+        setAccessRights targetPath.2  { user := { read := true, write := true, execution := true } };
         println s!"  LeanInk successfully installed!"
         return 0
       else

From 3e98ee02d8e509502ee6c08b0114dbdb816be8e6 Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Fri, 2 Sep 2022 10:08:56 -0700
Subject: [PATCH 11/15] fix: windows path

---
 lakefile.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index a7fb0fe..3cf6403 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -65,7 +65,10 @@ def getTargetLeanInkPath : IO (Option (FilePath × FilePath)) := do
     let loc := if System.Platform.isWindows then "LOCALAPPDATA" else "HOME"
     let val? ← getEnv loc
     if let some homePath := val? then
-      let targetPath : FilePath := homePath / ".leanink" / "bin"
+      let targetPath : FilePath := if System.Platform.isWindows then
+        homePath / "Programs" / "LeanInk" / "bin"
+      else
+        homePath / ".leanink" / "bin"
       if !(← targetPath.pathExists) then
         createDirAll targetPath
       return (targetPath, targetPath / fileName)
@@ -126,14 +129,14 @@ script install (args) do
     if System.Platform.isWindows then
       println s!"set PATH=%PATH%:{targetPath.1}"
     else
-      println s!"echo 'export PATH=$PATH:{targetPath.1}' >> ~/.profile && source ~/.profile"
+      println s!"echo 'export PATH=$PATH;{targetPath.1}' >> ~/.profile && source ~/.profile"
     println "  Building leanInk..."
     let out ← Process.output { cmd := "lake", args := #["build"] }
       if out.exitCode = 0 then
         let leanInkExe := getLeanInkExePath
         let realPath ← realPath leanInkExe
         println s!"  Built {realPath}"
-        println s!"  Copying to {targetPath}"
+        println s!"  Copying to {targetPath.2}"
         copyFile realPath targetPath.2
         setAccessRights targetPath.2  { user := { read := true, write := true, execution := true } };
         println s!"  LeanInk successfully installed!"

From 46826e3d10be0ab3c46834ee10739db6775c984a Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Fri, 2 Sep 2022 17:33:48 -0700
Subject: [PATCH 12/15] dox: remove references to .elan install target

---
 README.md     | 2 +-
 lakefile.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index eccc869..489c080 100644
--- a/README.md
+++ b/README.md
@@ -28,7 +28,7 @@ cd LeanInk
 lake build
 ```
 
-To install this built version to your `$HOME/.elan/bin` folder run:
+To install this built version run:
 ```bash
 lake script run install
 ```
diff --git a/lakefile.lean b/lakefile.lean
index 3cf6403..94cd2e3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -145,5 +145,5 @@ script install (args) do
         println s!"### Failed to build leanInk:\n{out.stdout} {out.stderr}"
         return out.exitCode
   else
-    println "### Cannot find .elan target directory"
+    println "### Cannot find target install directory"
     return 1

From 435714feddb33086c8a8fb8e79a06439d695f999 Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Wed, 7 Sep 2022 11:21:22 -0700
Subject: [PATCH 13/15] fix: add proper implementation of getLeanInkExePath

---
 lakefile.lean | 73 ++++++++++++++-------------------------------------
 1 file changed, 20 insertions(+), 53 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index 94cd2e3..6ee02f1 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,14 +13,9 @@ lean_exe leanInk {
   supportInterpreter := true
 }
 
-def getLeanInkExePath : FilePath :=
-  let leanInk : FilePath := "build" / "bin" / "leanInk"
-  leanInk.withExtension FilePath.exeExtension
-
 /-! 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 leanInkExe := getLeanInkExePath
+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}"
@@ -59,26 +54,11 @@ def indexOf? [BEq α] (xs : List α) (s : α) (start := 0): Option Nat :=
   | [] => none
   | a :: tail => if a == s then some start else indexOf? tail s (start+1)
 
-def getTargetLeanInkPath : IO (Option (FilePath × FilePath)) := do
-  let leanInkExe := getLeanInkExePath
-  if let some fileName := leanInkExe.fileName then
-    let loc := if System.Platform.isWindows then "LOCALAPPDATA" else "HOME"
-    let val? ← getEnv loc
-    if let some homePath := val? then
-      let targetPath : FilePath := if System.Platform.isWindows then
-        homePath / "Programs" / "LeanInk" / "bin"
-      else
-        homePath / ".leanink" / "bin"
-      if !(← targetPath.pathExists) then
-        createDirAll targetPath
-      return (targetPath, targetPath / fileName)
-  return none
-
 /-! 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
+def execute (leanInkExe: FilePath) (capture : Bool) : IO UInt32 := do
   let root : FilePath := "." / "test"
   let dirs ← walkDir root
   let mut retVal : UInt32 := 0
@@ -88,7 +68,7 @@ def execute (capture : Bool) : IO UInt32 := do
         let actual := test.withFileName (fileName ++ ".leanInk")
         let expected := test.withFileName (fileName ++ ".leanInk.expected")
         if (← expected.pathExists) then
-          let rc ← runLeanInk test
+          let rc ← runLeanInk leanInkExe test
           if rc ≠ 0 then
             return 1
           else if (capture) then
@@ -108,42 +88,29 @@ def execute (capture : Bool) : IO UInt32 := do
     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}"
-  println "Running diff tests for leanInk"
-  execute False
+  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}"
-  println "Updating .leanInk.expected output files"
-  execute True
-
-script install (args) do
-  if args.length > 0 then
-    println s!"Unexpected arguments: {args}"
-  if let some targetPath ← getTargetLeanInkPath then
-    println s!"Installing leanInk to {targetPath.1}"
-    println "Please ensure this location is in your PATH using:"
-    if System.Platform.isWindows then
-      println s!"set PATH=%PATH%:{targetPath.1}"
-    else
-      println s!"echo 'export PATH=$PATH;{targetPath.1}' >> ~/.profile && source ~/.profile"
-    println "  Building leanInk..."
-    let out ← Process.output { cmd := "lake", args := #["build"] }
-      if out.exitCode = 0 then
-        let leanInkExe := getLeanInkExePath
-        let realPath ← realPath leanInkExe
-        println s!"  Built {realPath}"
-        println s!"  Copying to {targetPath.2}"
-        copyFile realPath targetPath.2
-        setAccessRights targetPath.2  { user := { read := true, write := true, execution := true } };
-        println s!"  LeanInk successfully installed!"
-        return 0
-      else
-        println s!"### Failed to build leanInk:\n{out.stdout} {out.stderr}"
-        return out.exitCode
+  let leanInkExe ← getLeanInkExePath
+  if let some leanInkExe ← getLeanInkExePath then
+    println "Updating .leanInk.expected output files"
+    execute leanInkExe True
   else
-    println "### Cannot find target install directory"
+    println "Cannot find `leanInk` target path"
     return 1

From 6d11f10cf5ce94babd64bc9955d52d76a2dd460d Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Wed, 7 Sep 2022 11:35:38 -0700
Subject: [PATCH 14/15] fix: remove unused variable.

---
 lakefile.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index 6ee02f1..adadbae 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -107,7 +107,6 @@ script tests (args) do
 script capture (args) do
   if args.length > 0 then
     println s!"Unexpected arguments: {args}"
-  let leanInkExe ← getLeanInkExePath
   if let some leanInkExe ← getLeanInkExePath then
     println "Updating .leanInk.expected output files"
     execute leanInkExe True

From f9a7f6827c021ec653864f71dd5ffa1d3753aa7d Mon Sep 17 00:00:00 2001
From: Chris Lovett <clovett@microsoft.com>
Date: Wed, 7 Sep 2022 14:36:18 -0700
Subject: [PATCH 15/15] doc: fix readme

---
 README.md | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 489c080..e908fc2 100644
--- a/README.md
+++ b/README.md
@@ -28,10 +28,7 @@ cd LeanInk
 lake build
 ```
 
-To install this built version run:
-```bash
-lake script run install
-```
+To install this built version it is recommended you simply add the `LeanInk/build/bin` folder to your PATH environment.
 
 # Usage