git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
stdlib/fedora: Check result from koji latest-build to avoid infinite loop
[goals.git]
/
src
/
run.ml
diff --git
a/src/run.ml
b/src/run.ml
index
2d4e326
..
3a04256
100644
(file)
--- a/
src/run.ml
+++ b/
src/run.ml
@@
-41,8
+41,8
@@
let rec goal_runner env loc name args
(* Add some standard variables to the environment. *)
let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in
let expr_of_pattern = function
(* Add some standard variables to the environment. *)
let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in
let expr_of_pattern = function
- | Ast.P
Tactic (loc, tactic
, targs) ->
- Ast.E
TacticCtor (loc, tactic
, List.map expr_of_substs targs)
+ | Ast.P
Pred (loc, pred
, targs) ->
+ Ast.E
PredCtor (loc, pred
, 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
in
let pexprs = List.map expr_of_pattern patterns in
let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
@@
-54,37
+54,42
@@
let rec goal_runner env loc name args
| d :: _ -> Ast.Env.add "^" d env in
let r = Eval.run_code env loc code in
if r <> 0 then
| d :: _ -> Ast.Env.add "^" d env in
let r = Eval.run_code env loc code in
if r <> 0 then
- failwithf "goal ‘%s’ failed with exit code %d" name r;
+ failwithf "%a: goal ‘%s’ failed with exit code %d"
+ Ast.string_loc loc debug_goal r;
(* Check all targets were updated after the code was
* run (else it's an error).
*)
let pattern_still_needs_rebuild =
try
(* 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 extra_deps) patterns)
+ let pattern =
+ List.find
+ (needs_rebuild ~final_check:true env loc deps extra_deps)
+ patterns in
+ Some pattern
with
Not_found -> None in
match pattern_still_needs_rebuild with
| None -> ()
| Some pattern ->
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"
+ failwithf "%a: goal
‘%s’
ran successfully but it did not rebuild %a"
Ast.string_loc loc debug_goal Ast.string_pattern pattern
)
)
(* Return whether the target (pattern) needs to be rebuilt. *)
Ast.string_loc loc debug_goal Ast.string_pattern pattern
)
)
(* Return whether the target (pattern) needs to be rebuilt. *)
-and needs_rebuild env loc deps extra_deps pattern =
+and needs_rebuild
?(final_check = false)
env loc deps extra_deps pattern =
Cmdline.debug "%a: testing if %a needs rebuild"
Ast.string_loc loc Ast.string_pattern pattern;
match pattern with
Cmdline.debug "%a: testing if %a needs rebuild"
Ast.string_loc loc Ast.string_pattern pattern;
match pattern with
- | Ast.P
Tactic (loc, tactic
, targs) ->
- (* Look up the
tactic
. *)
- let params, code = Ast.get
tactic env loc tactic
in
+ | Ast.P
Pred (loc, pred
, targs) ->
+ (* Look up the
predicate
. *)
+ let params, code = Ast.get
pred env loc pred
in
(* Resolve the targs down to constants. Since needs_rebuild
* should be called with env containing the goal params, this
(* 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.
+ * should substitute any parameters in the
predicate
arguments.
*)
let targs = List.map (Eval.substitute env loc) targs in
let targs =
*)
let targs = List.map (Eval.substitute env loc) targs in
let targs =
@@
-92,19
+97,24
@@
and needs_rebuild env loc deps extra_deps pattern =
Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in
(* Create a new environment binding parameter names
Ast.EConstant (Ast.noloc, Ast.CString targ)) targs in
(* Create a new environment binding parameter names
- * to
tactic
args.
+ * to
predicate
args.
*)
let env =
let params =
try List.combine params targs
with Invalid_argument _ ->
*)
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
+ failwithf "%a: calling
predicate
‘%s’ with wrong number of arguments"
+ Ast.string_loc loc
pred
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 =
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 =
+ (*let b = Ast.EConstant (Ast.noloc, Ast.CBool final_check) in*)
+ let b = Ast.EConstant (Ast.noloc,
+ Ast.CString (if final_check then "1" else "")) in
+ Ast.Env.add "goals_final_check" b env in
+ let env =
(* NB: extra_deps are not added to %^ *)
match deps with
| [] -> env
(* NB: extra_deps are not added to %^ *)
match deps with
| [] -> env
@@
-112,12
+122,17
@@
and needs_rebuild env loc deps extra_deps pattern =
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
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
- failwithf "tactic ‘%s’ failed with exit code %d" tactic r
+ else (
+ let targs = List.map (Ast.string_expr ()) targs in
+ let targs = String.concat ", " targs in
+ failwithf "%a: predicate ‘%s (%s)’ failed with exit code %d"
+ Ast.string_loc loc pred targs r
+ )
-and exists_runner env loc p debug_
tactic
=
- Cmdline.debug "%a: running implicit existence rule for
tactic
%s"
- Ast.string_loc loc debug_
tactic
;
+and exists_runner env loc p debug_
pred
=
+ Cmdline.debug "%a: running implicit existence rule for
predicate
%s"
+ Ast.string_loc loc debug_
pred
;
if needs_rebuild env loc [] [] p then
if needs_rebuild env loc [] [] p then
- failwithf "%a: don't know how to build %s" Ast.string_loc loc debug_tactic
+ failwithf "%a: don't know how to build ‘%s’"
+ Ast.string_loc loc debug_pred