Le 15/08/2018 à 05:30, Ziqing Luo a écrit :
I noticed that once I imported the theory "clone int.Exponentiation ...",
there are several additional goals get imported as well.
Why3 no longer assumes that the user is fully aware of all the silently
imported axioms when cloning a module. So, by
It works, thank you for your help.
I have another question:
I used to use why3 0.88.3 and now plan to update it to 1.0.0
I noticed that once I imported the theory "clone int.Exponentiation ...",
there are several additional goals get imported as well.
Then I will always have these unwanted output
Le 14/08/2018 à 19:15, Ziqing Luo a écrit :
I'd like to use the Why3 GUI but I don't see the command "ide" in why3
1.0.0:
If you have installed why3 using opam (certainly the easiest way), make
sure you have also installed the why3-ide package.
If you are compiling by hand, check the output
I'd like to use the Why3 GUI but I don't see the command "ide" in why3
1.0.0:
'ide' is not a Why3 command.
Available commands:
config
doc
execute
extract
prove
realize
replay
session
shell
wc
webserver
On Tue, Aug 14, 2018 at 12:05 PM, Guillaume Melquiond <
guil
Le 14/08/2018 à 18:59, Ziqing Luo a écrit :
I have another question: is it possible to let why3 automatically try
different provers ? So far I use the command "why3 prove -P [prover]
[filename]", with which why3 only uses one prover and there are always
few goals left unproved.
I highly rec
Hi Guillaume,
Thank you for your help. Now it works.
I have another question: is it possible to let why3 automatically try
different provers ? So far I use the command "why3 prove -P [prover]
[filename]", with which why3 only uses one prover and there are always few
goals left unproved.
Thanks,
Le 14/08/2018 à 18:36, Stephen Siegel a écrit :
Thanks, Guillaume, I figured it was something like that. Is this due to a
change of syntax in the language, and are these changes documented somewhere?
These changes are summarily documented in the appendix of the user manual:
http://why3.lri.f
Thanks, Guillaume, I figured it was something like that. Is this due to a
change of syntax in the language, and are these changes documented somewhere?
My student Ziqing has tried to use 1.0 but got this:
File “why3_solution_challenge_1.mlw”, line 13, characters 2-13:
Library file not found: in
Le 14/08/2018 à 18:05, Stephen Siegel a écrit :
Hello Why3 Club,
I am trying to apply Why3 to the example here:
http://toccata.lri.fr/gallery/verifythis_2017_pair_insertion_sort.en.html
I downloaded the zip archive and executed, but got a syntax error:
siegel$ why3 prove verifythis_2017_pair_ins
Hello Why3 Club,
I am trying to apply Why3 to the example here:
http://toccata.lri.fr/gallery/verifythis_2017_pair_insertion_sort.en.html
I downloaded the zip archive and executed, but got a syntax error:
siegel$ why3 prove verifythis_2017_pair_insertion_sort.mlw
File "verifythis_2017_pair_insert
10 matches
Mail list logo
