On 02/09/2014 16:13, Claude Marché wrote:
>
> The proof obligations for each prover are generated only as temporary
> files by why3, so making them available would require significant changes.
>
> By more importantly: I guess you are mainly interested in the case where
> your favorite prover fa
The proof obligations for each prover are generated only as temporary
files by why3, so making them available would require significant changes.
By more importantly: I guess you are mainly interested in the case where
your favorite prover failed to prove the VC, right ? But then we usually
d
Hi JC,
It's interesting to have a "Why3 Proof Results for Project " at the
end of each (html) report.
But, is it possible/easy to enrich these html files with links to the
proof obligations generated for
each prover ?
- Mohamed.
--
Senior R&D Engineer, OCamlPro
Research Associate, VALS t
Dear Why3 users,
We have updated our gallery of verified programs, so that it is now
synchronized with release 0.84:
http://toccata.lri.fr/gallery/why3.en.html
In the meantime, new examples have been added, including
http://toccata.lri.fr/gallery/avl.en.html
http://tocca
A new release of Why3, version 0.84, is available from the Web page
http://why3.lri.fr.
A major visible change in this release is the way Why3 commands are
invoked: instead of several executables why3, why3config, why3ide,
why3replay, why3session, etc., there is only one Why3 executable
called w
