From 191a3d662dff1015d43aa4e6ca046d08c5ed6944 Mon Sep 17 00:00:00 2001
From: Jared Roesch <roeschinc@gmail.com>
Date: Tue, 23 May 2017 15:39:40 -0700
Subject: [PATCH] feat(leanpkg): add initial support for test command

---
 leanpkg/leanpkg/main.lean          | 18 ++++++++++++++++--
 library/init/meta/interactive.lean |  3 +++
 library/init/meta/tactic.lean      |  7 +++++++
 3 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/leanpkg/leanpkg/main.lean b/leanpkg/leanpkg/main.lean
index 81a7f448b9..5955ee0366 100644
--- a/leanpkg/leanpkg/main.lean
+++ b/leanpkg/leanpkg/main.lean
@@ -45,11 +45,23 @@ assg ← solve_deps d,
 path_file_cnts ← mk_path_file <$> construct_path assg,
 write_file "leanpkg.path" path_file_cnts
 
-def make : io unit :=
-exec_cmd { cmd := "lean", args := ["--make"], env := [("LEAN_PATH", none)] }
+
+def make : io unit := do
+manifest ← read_manifest,
+let src_path := manifest.path.get_or_else "src",
+exec_cmd {
+  cmd := "lean",
+  args := ["--make", src_path],
+  env := [("LEAN_PATH", none)]
+}
 
 def build := configure >> make
 
+def make_test : io unit :=
+exec_cmd { cmd := "lean", args := ["--make", "test"], env := [("LEAN_PATH", none)] }
+
+def test := configure >> make_test
+
 def init_gitignore_contents :=
 "*.olean
 /_target
@@ -120,6 +132,7 @@ Usage: leanpkg <command>
 
 configure       download dependencies
 build           download dependencies and build *.olean files
+test            download dependencies and run test files
 
 new <dir>       creates a lean package in the specified directory
 init <name>     adds a leanpkg.toml file to the current directory, and sets up .gitignore
@@ -136,6 +149,7 @@ dump            prints the parsed leanpkg.toml file (for debugging)
 def main : ∀ (args : list string), io unit
 | ["configure"] := configure
 | ["build"] := build
+| ["test"] := test
 | ["new", dir] := new dir
 | ["init", name] := init name
 | ["add", dep] := add dep
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 42ed5b9a19..e9360a2df0 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -790,6 +790,9 @@ tactic.apply_auto_param
 meta def fail_if_success (tac : itactic) : tactic unit :=
 tactic.fail_if_success tac
 
+meta def success_if_fail (tac : itactic) : tactic unit :=
+tactic.success_if_fail tac
+
 meta def guard_expr_eq (t : expr) (p : parse $ tk ":=" *> texpr) : tactic unit :=
 do e ← to_expr p, guard (alpha_eqv t e)
 
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 1c5fac3db5..6064539a28 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -86,6 +86,13 @@ meta def fail_if_success {α : Type u} (t : tactic α) : tactic unit :=
  (λ a s, mk_exception "fail_if_success combinator failed, given tactic succeeded" none s)
  (λ e ref s', success () s)
 
+meta def success_if_fail {α : Type u} (t : tactic α) : tactic unit :=
+λ s, match t s with
+| (interaction_monad.result.exception _ _ s') := success () s
+| (interaction_monad.result.success a s) :=
+   mk_exception "success_if_fail combinator failed, given tactic succeeded" none s
+end
+
 open nat
 /- (repeat_at_most n t): repeat the given tactic at most n times or until t fails -/
 meta def repeat_at_most : nat → tactic unit → tactic unit