introduce lake command to run test

.github/workflows/test.yml

@@ -24,10 +24,7 @@ jobs:
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: build
-        run: lake build
-
-      - name: run mdgen
-        run: lake exe mdgen Test/Src Test/Out
+        run: lake build --quiet
 
       - name: run test
-        run: lean --run Test.lean
+        run: lake run test

Test.lean

@@ -1,9 +1,3 @@
-/-! # how to test
-
-1. first, run `lake exe mdgen Test/Src Test/Out`
-2. run `lean --run Test.lean`
--/
-
 def main : IO UInt32 := do
   let firstActual ← IO.FS.readFile ⟨"Test/Out/First.md"⟩
   let firstExpected ← IO.FS.readFile ⟨"Test/Exp/First.md"⟩

lakefile.lean

@@ -14,3 +14,19 @@ lean_lib «Mdgen» where
 @[default_target]
 lean_exe «mdgen» where
   root := `Mdgen
+
+def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
+  let out ← IO.Process.output {
+    cmd := cmd
+    args := args
+  }
+  let hasError := out.exitCode != 0
+  if hasError then
+    IO.eprint out.stderr
+  return hasError
+
+-- run `lake run test`
+script test do
+  if ← runCmd "lake" #["exe", "mdgen", "Test/Src", "Test/Out"] then return 1
+  if ← runCmd "lean" #["--run", "Test.lean"] then return 1
+  return 0