- (* Check if any target (ie. pattern) needs to be rebuilt.
- * As with make, a goal with no targets is always run.
- *)
- let rebuild =
- patterns = [] || List.exists (needs_rebuild env loc deps) patterns in
-
- if rebuild then (
- (* Run the code (if any). *)
- (match code with
- | None -> () (* No { CODE } section. *)
-
- | Some code ->
- (* Add some standard variables to the environment. *)
- let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in
- let expr_of_pattern = function
- | Ast.PTactic (loc, tactic, targs) ->
- Ast.ETacticConstructor (loc, tactic, List.map expr_of_substs targs)
- in
- let pexprs = List.map expr_of_pattern patterns in
- let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
- let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in
- let env =
- match deps with
- | [] -> env
- | d :: _ -> Ast.Env.add "^" d env in
- let code = Ast.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
- );
-
- (* Check all targets were updated after the code was
- * run (else it's an error).
- *)
- let pattern_still_needs_rebuild =
- try Some (List.find (needs_rebuild env loc deps) patterns)
- with Not_found -> None in
- match pattern_still_needs_rebuild with
- | None -> ()
- | Some pattern ->
- failwithf "%a: goal ‘%s’ ran successfully but it did not rebuild %a"
- Ast.string_loc loc
- name
- Ast.string_pattern pattern
- )
- )
-
-(* Return whether the target (pattern) needs to be rebuilt. *)
-and needs_rebuild env loc deps pattern =
- Cmdline.debug "%a: testing if %a needs rebuild"
- Ast.string_loc loc Ast.string_pattern pattern;
-
- match pattern with
- | Ast.PTactic (loc, tactic, targs) ->
- (* Look up the tactic. *)
- let params, code = Ast.gettactic env loc tactic in
-
- (* Resolve the targs down to constants. Since needs_rebuild
- * should be called with env containing the goal params, this
- * should substitute any parameters in the tactic arguments.
- *)
- let targs = List.map (Ast.substitute env loc) targs in
- let targs =
- List.map (fun targ ->
- Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in
-
- (* Create a new environment binding parameter names
- * to tactic args.
- *)
- let env =
- let params =
- try List.combine params targs
- with Invalid_argument _ ->
- failwithf "%a: calling tactic ‘%s’ with wrong number of arguments"
- Ast.string_loc loc tactic in
- List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
-
- (* Add some standard variables to the environment. *)
- let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in
- let env =
- match deps with
- | [] -> env
- | d :: _ -> Ast.Env.add "^" d env in
- let code = Ast.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 = 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