- List.iter (
- fun (_, name, goal, args) ->
- run_goal env loc name args goal
- ) goals
+ let with_code, without_code =
+ List.partition (
+ fun (_, _, (_, _, _, code), _) -> code <> None
+ ) goals in
+
+ let (_, name, goal, args), extra_deps =
+ match with_code with
+ | [g] ->
+ let extra_deps =
+ List.flatten (
+ List.map (fun (_, _, (_, _, deps, _), _) -> deps) without_code
+ ) in
+ (g, extra_deps)
+
+ | [] ->
+ (* This is OK, it means we'll rebuild all dependencies
+ * but there is no code to run. Pick the first goal
+ * without code and the dependencies from the other goals.
+ *)
+ let g = List.hd without_code in
+ let extra_deps =
+ List.flatten (
+ List.map (fun (_, _, (_, _, deps, _), _) -> deps)
+ (List.tl without_code)
+ ) in
+ (g, extra_deps)
+
+ | _ :: _ ->
+ failwithf "%a: multiple goals with {code} sections match tactic %s"
+ Ast.string_loc loc tactic in
+
+ run_goal env loc name args goal extra_deps