[Why3-club] [Patch] Correctly set comment-{start, end} in why3 emacs mode

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

Re: [Why3-club] [Patch] Correctly set comment-{start, end} in why3 emacs mode

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) ;(

Re: [Why3-club] Fatal error: exception Printer.UnknownPrinter("tptp-fof")

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

Re: [Why3-club] run Why3 in your browser

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

Re: [Why3-club] A question about the context consistency in Why3 Logic

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