Le 19/05/2021 à 08:40, Loïc Correnson a écrit :
Indeed, the new upcoming version of Frama-C will require why3 1.4.0 and will be
marked conflicting with why3 1.5*
However, from a user point of view, it is really annoying to let opam install
why3 and alt-ergo versions that are incompatible with
Le 18/05/2021 à 21:33, David MENTRÉ a écrit :
In fact, frama-c 22 from opam explicitly requires Why3 1.3.3 version
only. And it also installs Alt-Ergo 2.4.0, probably because Why3 has no
requirement on Alt-Ergo version. That's why the situation occurred to me
I think.
Presumably, yes.
Maybe
Le 16/05/2021 à 15:20, David MENTRÉ a écrit :
Thank you for the info. Looking forward for the next release.
You do not need to wait for the next release. Why3 1.4.0 already
supports Alt-Ergo 2.4.0.
Best regards,
Guillaume
___
Why3-club mailing
Le 28/03/2021 à 11:41, Junon a écrit :
I can't seem to get why3 + Alt Ergo to run the Einstein's Logic Problem
example. It seems as though the processed Why script is missing a few `axiom`
keywords where Cloning occurs.
The issue is much simpler. Alt-Ergo now recognizes "of" as a keyword, so
Le 18/03/2021 à 16:07, marc.pan...@toulouse-inp.fr a écrit :
> Thanks to all the why3 developers.
>
> When do you think this version will be pushed to opam (only to see if I wait
> a bit more before building it on my own) ?
The pull request was submitted last week, so it should not take much
Le 15/03/2021 à 00:11, Frank Pfenning a écrit :
> It is not feasible for us to switch versions in the middle of the semester
> so I was wondering if the standard libraries and documentation for
> version 1.3.3 are still available somewhere?
You can get the older versions by suffixing the version
We are happy to announce a new release of Why3, version 1.4.0, available
from the Web page http://why3.lri.fr/
There have been numerous changes since the last release (see below for a
list). Here are some of the most important ones.
- Standalone executable files `why3config`, `why3prove`, etc,
Le 17/02/2021 à 18:48, Frank Pfenning a écrit :
> Thanks, Mário! If there is a print statement as indicated in the 2018
> paper, I couldn't find a way to access it.
It is only available for reflection-based proofs. (No good reason, it
just never got ported to the other execution engines.) So, if
Le 25/01/2021 à 23:07, Frank Pfenning a écrit :
> Why3.Controller_itp.Make(S).TransAlreadyExists("split_vc", "")' was
> raised in a LablGtk callback.
Thanks for the report.
Presumably a duplicate of https://gitlab.inria.fr/why3/why3/-/issues/471
Unfortunately, we have yet to find a way to
Le 13/01/2021 à 03:25, Deepayan Patra a écrit :
> I'm part of a class that uses why3 regularly in instruction but haven't
> been able to get why3-ide to successfully install since updating to Big
> Sur (it had successfully worked on Catalina on my end, which was the
> last time I had used it).
>
Le 03/12/2020 à 09:24, Sandrine Blazy a écrit :
> My other question is about TryWhy3: which version of why3 does it use?
I am updating it at the time of release. So, it should be 1.3.3.
Best regards,
Guillaume
___
Why3-club mailing list
Le 27/10/2020 à 13:55, Laurent Thery a écrit :
> In order to indicate where the vo files can be found, I have added
> a config file :
>
> [prover_modifiers]
> name="Coq"
> option="-R path_to_my_vofiles name_of_my_library"
Looks good to me.
> still when I do
>
> why3 replay --extra-config
Le 25/09/2020 à 19:17, Alain Giorgetti a écrit :
> In the following example, an error 'unbound proposition symbol' Inj ''
> is reported for M2. It is as if the presence of 'as' forced the export.
> Is it wanted and written somewhere?
>
> module MwithAs
> clone "function".Injective as I with
Le 22/09/2020 à 13:45, alain.giorge...@femto-st.fr a écrit :
> Assuming that the goals in it are replaced by lemmas, we would like the
> Bijective module to export all the lemmas of the Injective and Surjective
> modules
> it clones. But these lemmas have the same name, and 'export' and 'as XX'
Le 21/09/2020 à 13:42, Alain Giorgetti a écrit :
> What is the purpose of 'meta coercion function', often used in the
> standard library?
A coercion is automatically inserted whenever the type checker
encounters an error. For example, if a value of type x is expected, but
a value v of type y is
A new release of Why3, version 1.3.3, is available from the Web page
http://why3.lri.fr/
Changes between 1.3.2 and 1.3.3 are as follows:
Bug fixes
* fixed compilation on OpenBSD
Provers
* support for Coq 8.12.0 (released Jul 27, 2020)
___
Le 06/09/2020 à 19:36, Ralf Treinen a écrit :
> the latest version of coq supported by why3 is 8.11.0. Are there plans
> for extending this to more recent versions of coq ? This is currently
> blocking the update of coq in debian/unstable (coq 8.12.0 had to go to
> debian/experimental for this
A new release of Why3, version 1.3.2, is available from the Web page
http://why3.lri.fr/
Changes between 1.3.1 and 1.3.2 are as follows:
Bug fixes
* fixed compilation on BSD/macOS
* fixed use_api examples
* removed support for strings from the default variant of CVC4 1.7
* fixed custom
Le 04/09/2020 à 13:12, Daniel Britten a écrit :
> I have an installation question. When I run `opam install why3` I get
> the error below. I also tried it with ocaml 4.09.0
File src/server/server-unix.cpp is missing a line:
#include
See also https://gitlab.inria.fr/why3/why3/-/issues/499
Le 10/08/2020 à 15:00, Sandrine Blazy a écrit :
> Hi,
> can anyone help with this installation failure?
Your C compiler is right to complain; this is an unfortunate mistake on
Why3's side. So, short of modifying the sources of Why3 by hand as
instructed by the compiler, there is not much you can
Le 06/04/2020 à 20:12, Ralf Treinen a écrit :
> I made a test
> and removed the mathjax lines, and I cannot see a difference.
You can look at doc/html/technical.html#why3:transform-apply and see if
the math formula "\Gamma, h: f_1 \rightarrow f_2 \vdash G: f_2" is
correctly rendered.
> In that
Le 28/03/2020 à 11:16, Julia Lawall a écrit :
> Does saving preferences impact the .why3.config file? I change the editor
> for cvc4 and click on save, but when I leave why3 and restart it,
> the value that I saved is gone and it is back to the default.
Indeed, it seems broken. If you have not
Le 26/03/2020 à 13:08, Julia Lawall a écrit :
> Are there any other possibilities, or other ways to solve the problem of
> finding useless asserts?
I don't have any good solution. But here are a few ideas that might make
it easier for you.
Rather than removing the assertions, make them trivial
Le 25/03/2020 à 10:07, Julia Lawall a écrit :
> It's not clear to me how why3 session update works. I have a file called
> system.mlw, and thus a session directory called system. I tried why3
> session update -rename-file system xxx and I obtain no file containing xxx
> in its name and grep -r
Le 25/03/2020 à 14:43, Ralf Treinen a écrit :
> In case someone else is running into the same problem, the debian
> packages are:
>
> python3-sphinx
> python3-sphinxcontrib.bibtex
A bit more information. The Debian packages above are recent enough
(1.8?) to compile Why3's documentation, I
Le 24/03/2020 à 21:42, Julia Lawall a écrit :
>> * fixed conflicting symbols for CVC4 1.7
>
> I'm not sure what this change is, but after doing a pull of the latest
> version, I still have to remove the --strings-exp option to get cvc4 to
> work.
Yes, this is a different issue. The one that
A new release of Why3, version 1.3.1, is available from the Web page
http://why3.lri.fr/
Changes between 1.3.0 and 1.3.1 are as follows:
Bug fixes
* fixed conflicting symbols for CVC4 1.7
* fixed META file
* fixed infinite loops in strategies
___
Le 20/03/2020 à 10:43, Julia Lawall a écrit :
> I just see a cascade of split_vc, and when I look at the alt-ergo code
> from one to the next, it is identical.
Good catch. I have opened https://gitlab.inria.fr/why3/why3/issues/462
to track the issue.
Best regards,
Guillaume
Le 18/03/2020 à 21:31, Julia Lawall a écrit :
>> * default proof strategies "Auto level 1" and "Auto level 2"
>> have been respectively renamed "Auto level 2" and "Auto level 3";
>> "Auto level 1" now behaves similarly to "Auto level 0" but with a longer
>> time limit; more details
Le 18/03/2020 à 12:28, Julia Lawall a écrit :
> What should I do to get why3 to use the right file? I tried rerunning
> make, but it didn't do anything. Do I need to change my configuration
> file somehow?
The file that is located the "drivers" directory contained in a
directory that is either
Le 18/03/2020 à 09:21, Julia Lawall a écrit :
> I have the impression that it is using drivers/cvc4-realize.drv. I made
> the change you suggested, but if I edit the cvc4 proof, it shows
> ALL_SUPPORTED. Or is drivers/cvc4-realize.drv what is used when editing?
No, cvc4-realize.drv is never
Le 18/03/2020 à 08:45, Julia Lawall a écrit :
> Could the generated code be bigger than before? I tried cvc4 on a proof
> that is simple and has few dependencies and it was fine.
Among the things that changed recently regarding CVC4, here are a few
things you could try:
- In
We are happy to announce a new release of Why3, version 1.3.0, available
from the Web page http://why3.lri.fr/
There have been numerous changes since the last release (see below for a
list). Here are some of the most important ones.
- Module cloning now has much stricter requirements; this fixes
Le 25/02/2020 à 20:46, Jonathan Moerman a écrit :
> Can someone tell me how to use the "hypothesis selection" transformation.
> It doesn't show up in the IDE or when running "why3 --list-transforms".
> The plugin is of course registered in .why3.conf (plugin =
>
Le 01/10/2019 à 17:52, Julia Lawall a écrit :
> Hello,
>
> I have to resort to some explicit applys. When I then change my .mlw
> file, it seems that the why3 proof realignment rarely puts the existing
> applys in the right place. At some times I have thought that they are
> backwards, but I
Le 03/09/2019 à 07:54, Julia Lawall a écrit :
With commit e4e2a2a416ff2e98f6247cdf23f068e5369e7f0e, I gate the
following:
File "src/tools/why3extract.ml", line 1:
Error: The implementation src/tools/why3extract.ml
does not match the interface lib/why3/why3extract.cmi:
The module
Le 28/08/2019 à 18:08, Max Webber a écrit :
Hmm, my intention with the lemma inductive_step was similar to your
lemma function. I wanted to formulate the inductive step as an
additional lemma, so that the SMT solver could use it in the later proof
about insert_preserves_sort.
Is the lemma not
Le 07/08/2019 à 22:42, Benedikt Becker a écrit :
For a long time I have kept my hands off too much mutability in Why3,
but it has become inevitable.
Are there any resources that describe what can and cannot be done with
mutable values in Why3; Or is this just common sense?
I guess it is
[ This message is intentionally written in French. ]
* Merci de faire circuler : premier appel à communications *
JFLA'2020 (http://jfla.inria.fr/jfla2020.html)
Journées Francophones des Langages Applicatifs
Gruissan - du 29 janvier au 1 février 2020
Le 21/05/2019 à 09:48, Raphael Rieu-Helft a écrit :
Dear Evgeny,
With the following change to your program, both invariants are proved
instantly by Alt-Ergo. The reason why the invariants are true is that
the contents of the matrix above the diagonal are unchanged. My change
makes this
Le 16/05/2019 à 16:58, Jean-Jacques Levy a écrit :
can you insert the attribute when the ‘if-statement’ is not in the logic but is
in the code ?
let f (b:bool)(x:int)
ensures { x = 3 }
=
if b then ``` else ```
If it is in the code, then you don't need the attribute. The "split_vc"
Le 16/05/2019 à 14:48, Guillaume Melquiond a écrit :
Le 16/05/2019 à 13:38, Jean-Jacques Levy a écrit :
1- assertions around ‘if-statement’ keep the conditional in the logic.
In previous 0.88.3, they were splitted around the two branches of the
if-statement. Now the provers have to go through
Le 10/05/2019 à 14:39, Jean-Jacques Levy a écrit :
« trigger » ?? meaning? Is it in Why3 manual? I guess it’s related to
attributes such as [@induction], but not sure..
"trigger" is a notion from the SMT community. Triggers are automatically
inferred by SMT solvers, but they can also be
Le 10/05/2019 à 12:57, Евгений Макаров a écrit :
Hello,
I don't fully understand how to invoke Coq from Why3. Suppose I am
working on examples/logic/hello_proof.why. I right-click goal G3 and
select "Coq 8.9.0". CoqIDE starts. I fill in a proof between Proof and
Qed, save the file and quit
Le 10/05/2019 à 00:19, Евгений Макаров a écrit :
Both lemmas are proved instantly, but if I delete lemma l1, then l2 is
not proved. I would expect Why3 to use
axiom extensionality:
forall s1 s2: set 'a. s1 == s2 -> s1 = s2
from module set.Fset to prove l2, which in turn would reduce the
Le 07/05/2019 à 15:23, Benedikt Becker a écrit :
Hello,
An update to a reference `x <- e` is extracted (ocaml64) in two
different ways: Without using `--modular`, the result is simply
`x.contents <- e`. But when using `--modular`, the field of the
reference is qualified as `x.Why3__Ref.contents
Le 07/05/2019 à 08:47, Aurélie Hurault a écrit :
Hello,
I'd like to use higher order functions in Why3, but I have trouble.
Which version of Why3 are you using? I just tried with the latest
version (1.2.0) and your code works without modification (once [...] has
been replaced by three "use"
Le 07/03/2019 à 20:15, Julia Lawall a écrit :
OK, I've been sprinkling
meta "rewrite_def" proposition foo
But I'm not sure if it really has an impact...
This meta is mostly meant for the "compute_specified" transformation. If
you manually apply this transformation, all the tagged
We are happy to announce a new release of Why3, version 1.2.0, available
from the Web page http://why3.lri.fr/
One of the major changes is that WhyML now offers some "let ref"
syntactic sugar to make references look like plain variables, e.g.,
let rec f91_tco (n0: int) : int
= let ref n
A new release of Why3, version 1.1.1, is available from the Web page
http://why3.lri.fr/
Changes between 1.1.0 and 1.1.1 are as follows:
Bug fixes
* prevented broken extraction of `any`
* fixed evaluation order when extracting nested mutators
* fixed extraction of nested recursive
Le 12/11/2018 à 13:10, Alan Schmitt a écrit :
Hello,
On 2018-11-12 09:05, Claude Marché writes:
Since Why3 1.0, there is no polymorphic equality in programs. Hence
there is no symbol (=) for type cell in your code, but only the equality
for type int.
This is interesting. What was the
We are happy to announce a new release of Why3, version 1.1.0, available
from the Web page http://why3.lri.fr/
Note to Opam users: Recently released packages (be it Why3 or other
software) are only available to Opam 2.0 users. Opam 1.2 users need to
resort to abstruse incantations, e.g., opam
Le 20/08/2018 à 21:59, Евгений Макаров a écrit :
Do I understand right that to use the opam version of Why3 with Coq I
need to install the why3-coq package? But this requires installing Coq
via opam in addition to the existing installation. So does this mean
that I have to install Coq and why3
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
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
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:
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
Le 31/07/2018 à 23:22, Kruer, Joseph C. a écrit :
I’ve written the following recursive predicate, below, and I’d like to
prove that it terminates. I’ve added a suitable variant, but I am
getting a vague syntax error for which I found no obvious remedy in the
WIP documentation for 1.0.0 on the
Le 18/07/2018 à 21:19, Kruer, Joseph C. a écrit :
Hello Why3-ople,
I’m working on a verification task working with strings and therefore
find myself doing lots of individual character comparisons.
Just a disclaimer first. The char/string library has been designed seven
years ago, and it has
We are happy to announce a new major release of Why3, version 1.00,
available from the Web page http://why3.lri.fr/.
The detailed changes are listed below. The two major changes of this
release with respect to the former release 0.88.3 concern:
1) the WhyML programming language and the
Le 12/03/2018 à 16:23, Sandrine Blazy a écrit :
I have a function f : ‘a -> int. When I am defining
function sum_set (s: set ‘a) : int = sum s f
I got the following error message:
This term has type set 'a, but is expected to have type set1 ‘xi
What’s wrong with s in this definition ?
Given
Le 08/03/2018 à 13:53, Abhishek Kumar a écrit :
I have downloaded the Why3 tarball and installed using make and |make
install-lib| as given in the documentation for Why3 API. But still when
I do |open Why3|, ocamlc and utop complain |unbound module Why3|.
Can someone please help me how to use
Le 05/03/2018 à 11:43, Sandrine Blazy a écrit :
None of my provers (Alt-Ergo, cvc3, cvc4, Eprover, Z3) is able to prove
any of these 3 assertions. However, if I choose the "get
counter-example" option in the preference window, then cvc4 manages to
prove this test program.
Does it mean that
Le 27/02/2018 à 08:18, Julia Lawall a écrit :
Is it possible to write an ensures that refers to both the original and
final value of an array. For exampe, if one makes a function update ar i
v, one might want to write an ensures that indicates that only the ith
element of the array is updated.
Le 19/02/2018 à 13:59, Julia Lawall a écrit :
Sorry, I don't understand the sequence of operations. First I start up
why3 ide. Then I click on my goal and then on Coq. This gives me a Coq
line with (not yet edited). In the tools menu, I found "Mark as
obsolete". After clicking on that I
Le 19/02/2018 à 11:43, Julia Lawall a écrit :
I have two laptops, one at home, one at work. I tried saving the state
(foo subdirectory, for a foo.mlw file) with git on my home machine, and
pulling onto my work machine. Part of my state is a coq proof. But when
I start up why3 at work and
Le 17/02/2018 à 15:17, Julia Lawall a écrit :
opam install complains that it is not able to obtain why3-base.0.88.3.
opam install --debug shows that it is executing the following command:
/usr/bin/curl --write-out %{http_code}\n --retry 3 --retry-delay 2
--user-agent opam/2.0.0~rc -L -o
Le 30/01/2018 à 13:22, Stefan Berghofer a écrit :
Dear Why3-Club,
I just tried to compile Why3 with the latest OCaml 4.06.0 version, but this
failed due to
a missing Big_int module. I am aware that the Num library is now distributed
separately,
but since the webpage says that Num is outdated,
A new release of Why3, version 0.88.2, is available from the Web page
http://why3.lri.fr/
Changes between 0.88.1 and 0.88.2 are as follows:
Bug fixes
* `why3 session html`: improved compliance of generated files
* `why3 doc`: fixed missing anchors for operator definitions
* improved build
Hi,
For users that are directly using the git repository of Why3, there are
some recent changes that are worth advertising.
First, the "new_system" branch has been merged into "master" and
deleted. So, if you were tracking the "new_system" branch, you have to
switch to the "master" branch.
On 10/11/2017 11:08, Frédéric Blanqui wrote:
> Why don't you specify in opam that why3 0.88.1 is not compatible with
> coq 8.7?
I am not sure to fully understand the question, so let me just say that,
had I been aware of the Coq 8.7 opam issue at the time I released Why3
0.88.1 and published the
On 10/11/2017 09:32, Frédéric Blanqui wrote:
> Hello. FYI, when doing an opam update this morning, I got the following
> error:
> « src/coq-tactic/.why3-vo-byte » a échouée
Which version of Coq is installed in your system? If it is 8.7, the
failure is kind of expected, as the opam package for Coq
A new release of Why3, version 0.88.1, is available from the Web page
http://why3.lri.fr/
Changes between 0.88.0 and 0.88.1 are as follows:
API
* exported function `Call_provers.get_new_results`
Provers
* improved support for Isabelle 2017
* fixed support for Coq 8.7
Miscellaneous
*
On 26/10/2017 11:33, Stefan Berghofer wrote:
> Dear Why3-Club,
>
> while playing around with the latest repository version of Why3, I noticed
> that the left
> toolbar in Why3 IDE has suddenly disappeared. The toolbar used to contain
> buttons for calling
> provers, editing and replaying
On 18/10/2017 21:56, Julien Cretin wrote:
> Hi club,
>
> Can I currently (stdlib-0.88.0) prove the following?
>
> lemma mod_mult: forall x a b.
> 0 <= x ->
> 0 < a ->
> 0 < b ->
> mod (mod x (a * b)) a = mod x a
>
> It looks like I would need an axiom about `div x (a
On 15/10/2017 20:47, Julien Cretin wrote:
> Hi club,
>
> I updated my Why3 from 0.87.3 to 0.88.0 today and had a few issues with
> my existing theories. I got some unbound symbol 'BVC.to_uint_small'
> errors where BVC is an alias for bv.BVConverter_8_64. I suspect this to
> be due to the new
On 15/02/2017 10:20, Jean-Jacques Levy wrote:
> [editor proofgeneral-coq]
> command = "/Applications/Emacs.app/Contents/MacOS/Emacs --eval \"(setq
> coq-load-path '((\\\"%l/coq-tactic\\\" \\\"Why3\\\") (\\\"%l/coq\\\"
> \\\"Why3\\\")))\" %f"
> name = "Emacs/ProofGeneral/Coq"
The issue comes from
On 10/09/2016 22:58, Per Lindgren wrote:
> Hi Folks.
>
> I’ve observed an obstacle to the code extraction of “let” functions with
> ghost parameters. In cases the generated function code drops ghost
> parameters, while the corresponding calls, do not (leading to compilation
> error later on
On 19/08/2016 14:48, Guillaume Melquiond wrote:
>> Should I open a bug on Why3 issue tracker?
>
> Don't bother, it should be easy enough to fix (assuming my
> interpretation is correct).
And the patch is now on the bugfix/v0.87 branch.
Best rega
On 19/08/2016 11:20, David MENTRE wrote:
> Hello,
>
> When trying to execute the attached WhyML file, I get following error:
> """
> $ why3 -C why3.config execute execute_test.mlw Execute_test.test
> Execution of Execute_test.test ():
> type: bool
>
>
> Execution error: Cannot execute
On 09/07/2016 16:59, Gabriel Scherer wrote:
> - either you think that it should work on 4.01, and understand the issue
> and fix it on your side (or maybe it's a glitch on the testing matching,
> but then you need to say so)
Why3 0.87.1 works fine with OCaml 4.01. The testing machine works fine
A new release of Why3, version 0.87.0, is available from the web page
http://why3.lri.fr/ ; OPAM packages for this version of Why3 should soon
be available.
There are no major changes in this release. It mainly provides support
for new versions of provers. There are also some improvements to the
A new release of Why3, version 0.86.3, is available from the Web page
http://why3.lri.fr/
This is a bug-fix/build-fix release, with no new feature with respect to
previous 0.86 versions.
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
A new release of Why3, version 0.86.2, is available from the Web page
http://why3.lri.fr/
This is a bug-fix/build-fix release, with no new feature with respect to
0.86 or 0.86.1.
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
On 08/10/2015 15:54, Matthias Güdemann wrote:
> Dear Why3-club,
>
> when compiling why3 (either from opam, git or 0.86.1 source), I get the
> following error on 'make install':
>
> ,
> | ...
> | rm -f /usr/local/bin/why3doc
> | if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d;
On 17/09/2015 12:23, Per Lindgren wrote:
Execution of ModTest.test ():
type: (int, int, int, int, int, int, int)
result: ((-1), (-2), (-1), 0, 1, 0, 1)
The output produced is correct from my knowledge how modular arithmetics
work in a computer.
No, (-2) mod 2 = -2 certainly is not
On 17/09/2015 13:13, Per Lindgren wrote:
I guess though the axioms in the theory have be proven in Coq, the actual mod
function (mod) is not.
Yes, the Coq proofs only tell that there exists some function that
satisfies the axiom (and thus that they are not inconsistent). It does
not tell
On 24/08/2015 08:21, Per Lindgren wrote:
You have to provide a driver that extends the Ocaml one to tell how these
functions translate to Ocaml code. (A driver is a simple text file, see
drivers/ocaml64.drv.)
Ok, Iooking at FSet it is a theory providing the function cardinal. (and from
On 17/06/2015 01:58, Tiago Cogumbreiro wrote:
Hello,
For an axiom like:
axiom total_diff_wait_tids:
forall x y.
wait_tid x -
wait_tid y -
exists d. diff x y = Some d
I'm having Why3 complain about:
warning: axiom total_diff_wait_tids does not contain any local
abstract
On 21/05/2015 17:10, Gabriel Scherer wrote:
Unfortunately, the link in the documentation to the standard library
( http://why3.lri.fr/stdlib/ ) is dead (403 Forbidden).
If it was yesterday, you presumably hit the website just at the time the
documentation for 0.86.1 was being uploaded.
I
A new release of Why3, version 0.86.1, is available from the Web page
http://why3.lri.fr/
Detailed changes:
IDE
o improved task highlighting for negated premises
(contributed by Mikhail Mandrykin, AstraVer project)
provers
o support for Gappa 1.2 (released May 19, 2015)
bug fixes
o
On 24/03/2015 17:51, Claude Marche wrote:
I tried to investigate this issue. It seems that the following axiom
axiom Pow_zero_y:
forall y:real. y 0.0 - pow 0.0 y = 0.0
from Why3 theory real.PowerReal is exploited by metitarski to derive a
contradiction.
It might be the case that
On 20/03/2015 13:30, K. Siaulys wrote:
When I try to prove the exact same formula directly with MetiTarski from
command line (by calling metit --autoInclude metit.tptp), where contents
of metit.tptpt file are:
Hence, how could I make MetiTarski work with Why3?
That is interesting.
If your
On 26/02/2015 13:33, Alan Schmitt wrote:
# Error while loading
/Users/schmitta/.opam/4.02.1/lib/coq/parsing/grammar.cma: error while linking
/Users/schmitta/.opam/4.02.1/lib/coq/parsing/grammar.cma.
# Reference to undefined global `Camlp4'.
# make: *** [src/coq-tactic/g_why3tac.ml] Error 2
On 26/02/2015 19:17, Alan Schmitt wrote:
In the meantime is there a way to have both why3 and coq installed on my
system? Can I tell opam not to use coq when compiling why3 (it seems to
pick it up automatically when it's installed)?
You need to pass the --disable-coq-tactic option to the
On 09/01/2015 15:38, Stefan Berghofer wrote:
Dear Why3-Club,
I just came across the transformation
simplify_trivial_quantification_in_goal, which seems
to be quite useful for making complex goals more readable. This is
particularly important
when using Why3 in connection with the SPARK2014
On 30/09/2014 15:36, K. Siaulys wrote:
Hello everybody,
I hope this is a right place to ask a question. I am also very new to
Why3, therefore I apologise if the question is trivial.
Basically, I have two theories - one that should hold a declared but
undefined integer term t, and a second one
On 21/07/2014 22:58, Tiago Cogumbreiro wrote:
Hello everyone at the Why3 Club,
Is it required to prove lemma Induction in theory FsetInduction? Or
should it be left out as an axiom?
It should be left out as an axiom.
Are there any examples out there on how to use it? I grep'ed the gallery
On 09/05/2014 10:42, Jean-Jacques Levy wrote:
Yes, it is fair, since the logic of Why3 already assumes it.
In practice, I never had to assume it though, when doing a Coq proof. Indeed,
most of the predicates I get from Why3 are trivially boolean in nature, and
thus do not need excluded
On 17/03/2014 08:52, Jean-Jacques Levy wrote:
Dear Why3 fans,
it looks we have problem with Coq driver in new Why3 0.83:
1- /usr/local/share/why3/drivers/coq.drv exists, but Why3ide seems call
/usr/local/share/why3/drivers/coq_8_4.drv
That can be fixed with a link between these 2
1 - 100 of 102 matches
Mail list logo
