X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Frun.ml;h=2df305bf7682e195f6f09421aa7bb85d7cf06a59;hb=d06b73832126c575927af40f3ebf574e8621b2a8;hp=d8cabb91ce4dec5448f4718b4adc08958d59c164;hpb=976bb1b35d77f3058df3c25c1e2a4767147d606b;p=goals.git

diff --git a/src/run.ml b/src/run.ml
index d8cabb9..2df305b 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -21,10 +21,40 @@ open Printf
 
 open Utils
 
-let rec run_targets env exprs =
-  List.iter (run_target env) exprs
+(* Goals uses the goal (name + parameters) as the key to
+ * ensure you cannot have two jobs running at the same time
+ * which would interfere with each other by trying to build
+ * the same target.
+ *)
+module Jobs = Jobs.Make (
+  struct
+    type t = string * Ast.expr list
+    let compare = compare
+    let to_string (name, args) =
+      sprintf "%s (%s)" name
+        (String.concat ", " (List.map (Ast.string_expr ()) args))
+  end
+)
+
+let stop_all = Jobs.stop_all
+
+(* Starts the target expressions running and waits for them to complete. *)
+let rec run_targets_to_completion env exprs =
+  let group = Jobs.new_group () in
+  run_targets group env exprs;
+  Jobs.wait group
+
+(* This starts the targets, adding them to the jobs group, but does not
+ * wait for them to complete.
+ *)
+and run_targets group env exprs =
+  List.iter (run_target group env) exprs
 
-and run_target env = function
+(* This starts a single target, adding the (usually single but can
+ * be multiple) jobs to the jobs group.  It does not wait for the
+ * jobs to complete.
+ *)
+and run_target group env = function
   | Ast.EGoalDefn _ | Ast.EFuncDefn _ | Ast.ETacticDefn _ -> assert false
 
   (* Call a goal or function. *)
@@ -32,10 +62,13 @@ and run_target env = function
      let expr = Ast.getvar env loc name in
      (match expr with
       | Ast.EGoalDefn (_, goal) ->
-         run_goal env loc name args goal []
+         let key = name, args in
+         Jobs.start group key (
+           fun () -> run_goal env loc name args goal []
+         )
       | Ast.EFuncDefn (_, func) ->
          let expr = Eval.call_function env loc name args func in
-         run_target env expr
+         run_target group env expr
       | _ ->
          failwithf "%a: tried to call ‘%s’ which is not a goal or a function"
            Ast.string_loc loc name
@@ -47,7 +80,7 @@ and run_target env = function
       * (strings, in future booleans, numbers, etc).
       *)
      let args = List.map (Eval.to_constant env) args in
-     run_tactic env loc name args
+     run_tactic group env loc name args
 
   (* If this is a goal then it's the same as calling goal().  If not
    * then look up the variable and substitute it.
@@ -56,25 +89,25 @@ and run_target env = function
      let expr = Ast.getvar env loc name in
      (match expr with
       | Ast.EGoalDefn (loc, ([], _, _, _)) ->
-         run_target env (Ast.ECall (loc, name, []))
+         run_target group env (Ast.ECall (loc, name, []))
       | EGoalDefn _ ->
          failwithf "%a: cannot call %s() since this goal has parameters"
            Ast.string_loc loc name
       | _ ->
-         run_target env expr
+         run_target group env expr
      )
 
   (* Lists are inlined when found as a target. *)
   | Ast.EList (loc, exprs) ->
-     run_targets env exprs
+     run_targets group env exprs
 
   (* A string (with or without substitutions) implies *file(filename). *)
   | Ast.ESubsts (loc, str) ->
      let str = Eval.substitute env loc str in
-     run_tactic env loc "*file" [Ast.CString str]
+     run_tactic group env loc "*file" [Ast.CString str]
 
   | Ast.EConstant (loc, c) ->
-     run_tactic env loc "*file" [c]
+     run_tactic group env loc "*file" [c]
 
 (* Run a goal by name. *)
 and run_goal env loc name args (params, patterns, deps, code) extra_deps =
@@ -102,8 +135,10 @@ and run_goal env loc name args (params, patterns, deps, code) extra_deps =
           (List.length params) (List.length args) in
     List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
 
-  (* Check all dependencies have been updated. *)
-  run_targets env (deps @ extra_deps);
+  (* Check all dependencies have been updated.  We must wait
+   * for these to complete before we can continue.
+   *)
+  run_targets_to_completion env (deps @ extra_deps);
 
   (* Check if any target (ie. pattern) needs to be rebuilt.
    * As with make, a goal with no targets is always run.
@@ -132,13 +167,9 @@ and run_goal env loc name args (params, patterns, deps, code) extra_deps =
           match deps with
           | [] -> env
           | d :: _ -> Ast.Env.add "^" d env in
-        let code = Eval.to_shell_script env loc code in
-        let code = "set -e\nset -x\n\n" ^ code in
-        let r = Sys.command code in
-        if r <> 0 then (
-          eprintf "*** goal ‘%s’ failed with exit code %d\n" name r;
-          exit 1
-        );
+        let r = Eval.run_code env loc code in
+        if r <> 0 then
+          failwithf "goal ‘%s’ failed with exit code %d" name r;
 
         (* Check all targets were updated after the code was
          * run (else it's an error).
@@ -193,20 +224,16 @@ and needs_rebuild env loc deps extra_deps pattern =
        match deps with
        | [] -> env
        | d :: _ -> Ast.Env.add "^" d env in
-     let code = Eval.to_shell_script env loc code in
-     let code = "set -e\n" (*^ "set -x\n"*) ^ "\n" ^ code in
-     let r = Sys.command code in
+     let r = Eval.run_code env loc code in
      if r = 99 (* means "needs rebuild" *) then true
      else if r = 0 (* means "doesn't need rebuild" *) then false
-     else (
-       eprintf "*** tactic ‘%s’ failed with exit code %d\n" tactic r;
-       exit 1
-     )
+     else
+       failwithf "tactic ‘%s’ failed with exit code %d" tactic r
 
-(* Find the goal which matches the given tactic and run it.
+(* Find the goal which matches the given tactic and start it.
  * cargs is a list of parameters (all constants).
  *)
-and run_tactic env loc tactic cargs =
+and run_tactic group env loc tactic cargs =
   (* This is used to print the tactic in debug and error messages only. *)
   let debug_tactic =
     Ast.string_expr ()
@@ -253,7 +280,10 @@ and run_tactic env loc tactic cargs =
 
   | [_, name, goal, args] ->
      (* Single goal matches, run it. *)
-     run_goal env loc name args goal []
+     let key = name, args in
+     Jobs.start group key (
+       fun () -> run_goal env loc name args goal []
+     )
 
   | goals ->
      (* Two or more goals match.  Only one must have a CODE section,
@@ -290,7 +320,10 @@ and run_tactic env loc tactic cargs =
           failwithf "%a: multiple goals found which match tactic %s, but more than one of these goals have {code} sections which is not allowed"
             Ast.string_loc loc debug_tactic in
 
-     run_goal env loc name args goal extra_deps
+     let key = name, args in
+     Jobs.start group key (fun () ->
+       run_goal env loc name args goal extra_deps
+     )
 
 (* Test if pattern matches *tactic(cargs).  If it does
  * then we return Some args where args is the arguments that must