Hi Why developers,
I think the below patch against today's git should be applied in order
to make why3.el work well on recent version of emacs.
diff --git a/share/emacs/why3.el b/share/emacs/why3.el
index a243946..251adbe 100644
--- a/share/emacs/why3.el
+++ b/share/emacs/why3.el
@@ -162,7 +162,8
Hi all,
yesterday I sent a wrong patch, please find below the (hopefully)
correct one:
diff --git a/share/emacs/why3.el b/share/emacs/why3.el
index a243946..7091a26 100644
--- a/share/emacs/why3.el
+++ b/share/emacs/why3.el
@@ -162,7 +162,8 @@
;(make-local-variable 'indent-line-function)
;(
Hi Anton,
> I get the message 'Fatal error: exception
> Printer.UnknownPrinter("tptp-fof")' when try to call the E prover from
In my case, I have found this problem to be caused by:
- Not calling Whyconf.load_plugins in my program.
- Having an incorrect ~/.why3.conf [plugin = //tptp] shoul
Hi all,
Jean-Christophe Filliatre
writes:
> There is indeed something similar for Coq (built with the same
> js_of_ocaml technology), so there is no reason you could not integrate
> Coq as well in trywhy3.
>
> Yet it raises the issue of storing and replaying the Coq proofs related
> to VCs. So f
Hi Ziqing,
> If I get an "Unknown" for a goal, does it mean that the goal is invalid if
> I can separately prove the context is consistent ?
I am not sure if this may be of help, but given a goal `P`, instead of
trying to get `Invalid` from it, you could try to get `Valid` for its
negation `not