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
55a2b8d
..
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,7
+54,8
@@
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).
(* Check all targets were updated after the code was
* run (else it's an error).
@@
-71,7
+72,7
@@
let rec goal_runner env loc name args
match pattern_still_needs_rebuild with
| None -> ()
| Some pattern ->
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
)
)
Ast.string_loc loc debug_goal Ast.string_pattern pattern
)
)
@@
-82,13
+83,13
@@
and needs_rebuild ?(final_check = false) env loc deps extra_deps pattern =
Ast.string_loc loc Ast.string_pattern pattern;
match pattern with
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 =
@@
-96,14
+97,14
@@
and needs_rebuild ?(final_check = false) 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. *)
List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
(* Add some standard variables to the environment. *)
@@
-121,12
+122,17
@@
and needs_rebuild ?(final_check = false) 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