From c99be93a6d49d85d997a277689305aca060a500e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 23 Sep 2020 17:31:39 +0200
Subject: [PATCH] [wp] Add goal name on script error
---
src/plugins/wp/ProverScript.ml | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 7a264f1e5f5..50d39797232 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -324,7 +324,8 @@ let rec crawl env on_child node = function
Task.return ()
| Error(msg,json) :: alternative ->
- Wp_parameters.warning "@[<hov 2>Script Error %S: %a@]@."
+ Wp_parameters.warning "@[<hov 2>Script Error: on goal %a@\n%S: %a@]@."
+ WpPropId.pretty (Env.goal env node).po_pid
msg Json.pp json ;
crawl env on_child node alternative
@@ -349,9 +350,11 @@ let rec crawl env on_child node = function
match jfork (Env.tree env) ?node jtactic with
| None ->
Wp_parameters.warning
- "Script Error: can not apply '%s'@\n\
+ "Script Error: on goal %a@\n\
+ can not apply '%s'@\n\
@[<hov 2>Params: %a@]@\n\
@[<hov 2>Select: %a@]@."
+ WpPropId.pretty (Env.goal env node).po_pid
jtactic.tactic
Json.pp jtactic.params
Json.pp jtactic.select ;
--
GitLab