 11 Oct, 2011 40 commits


Asma TafatBouzid authored

Asma TafatBouzid authored

MARCHE Claude authored

MARCHE Claude authored

 08 Oct, 2011 40 commits


JeanChristophe Filliatre authored

JeanChristophe Filliatre authored

 07 Oct, 2011 40 commits


MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

 06 Oct, 2011 40 commits


JeanChristophe Filliatre authored

 05 Oct, 2011 40 commits


JeanChristophe Filliatre authored

 03 Oct, 2011 40 commits


Guillaume Melquiond authored
Remark about the theory: if one considers that the square root is always nonnegative (by definition in Coq), then Lemma Sqrt_positive has an extraneous hypothesis.

Guillaume Melquiond authored

Guillaume Melquiond authored
Note that the files are compiled with: coqc R . '' real/toto.v

Guillaume Melquiond authored
This is just a proof of concept, since most definitions should just be notations for the realization to be userfriendly. Moreover, the format of the file will presumably evolve, if only for some information to properly update it when the theories change. Remark about the theory : Lemma mul_assoc_div has an extraneous hypothesis. Indeed, as long as inverse is a total function, this lemma is an immediate consequence of multiplication associativity.

Asma Tafat authored

Asma Tafat authored

 01 Oct, 2011 40 commits


JeanChristophe Filliatre authored

 30 Sep, 2011 40 commits


Andrei Paskevich authored
How to use it: why3 realize D drivers/coqrealize.drv T real.Real o . produces Real.v in the current directory why3 realize D drivers/coqrealize.drv T real.Real produces real/Real.v in the loadpath near real.why (the directory "real" must exist) If a realization file is already there, it is passed to the printer in order to preserve the proofs. Instead of D <driver_file>, you can use P <prover>, if that prover uses a corresponding driver. However, the prover itself is not used. You can only realize theories from the loadpath. At the moment, coqrealize.drv is the only driver capable to realize theories in some sensible way. For any other driver, the results may be funny. Realization of WhyML modules is not possible so far. Realization may break if you directories and filenames contain nonalphanumeric symbols. The whole thing is in very preliminary stage. Use with caution.

Andrei Paskevich authored

Andrei Paskevich authored
also add Env.get_loadpath to use for Coq realisation

MARCHE Claude authored

 29 Sep, 2011 40 commits


MARCHE Claude authored

Andrei Paskevich authored

MARCHE Claude authored

Andrei Paskevich authored

MARCHE Claude authored
(standalone executable why3realize)

MARCHE Claude authored

MARCHE Claude authored

 28 Sep, 2011 40 commits


Andrei Paskevich authored

Andrei Paskevich authored
For builtin and local theories the prefix is empty.

MARCHE Claude authored
