[Why3-club] Make why3session.xml file from command line?

David MENTRE dmentre at linux-france.org
Mon Nov 12 11:18:57 CET 2012


Hello Claude,

2012/11/9 David MENTRE <dmentre at linux-france.org>:
>> I attach a .ml source file that
>> examplifies how a session can be created from a given .why or .mlw file.
>
> Thanks a lot! I'll test it.

It works... after some tweaking. ;-)

For the record, here is attached the create_session.ml file I am
using. I added handling of -C and -I options (like why3ide). It should
be also able to handle several .why files simultaneously but I did not
test this feature.

Then, to fill the empty proofs with real proof attempts, I am using
why3replayer with the following commit and -force option:
  https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=why3/why3.git;a=commitdiff;h=e4da761d10e3ad71f2ee95e14971f0d54840ebfe

Thanks a lot!

Best regards,
david
-------------- next part --------------
A non-text attachment was scrubbed...
Name: create_session.ml
Type: application/octet-stream
Size: 5040 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20121112/4af978b2/attachment.obj>


More information about the Why3-club mailing list