 03 Oct, 2011 6 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 1 commit


JeanChristophe Filliatre authored

 30 Sep, 2011 4 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 7 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 7 commits


Andrei Paskevich authored

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

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

Asma Tafat authored

 27 Sep, 2011 2 commits


MARCHE Claude authored

Asma TafatBouzid authored

 26 Sep, 2011 7 commits


Andrei Paskevich authored

MARCHE Claude authored

Asma TafatBouzid authored

MARCHE Claude authored

Asma TafatBouzid authored

Asma TafatBouzid authored

MARCHE Claude authored

 25 Sep, 2011 1 commit


Asma Tafat authored

 24 Sep, 2011 3 commits


Guillaume Melquiond authored
When the user wants to write a Coq proof, she needs to run Coq on the goal, wait five seconds for it to fail (it will fail, otherwise there is no point in running Coq on this goal: another prover would have succeeded already), and finally edit it. This is a waste of time. So goals run with an interactive prover are now marked as unknown until their file is edited. Interactive provers could have been detected by a nonempty "editor" string, but there are interactive provers that don't have dedicated editors, and there might be automated provers with dedicated user interfaces. So a new field was added to prover descriptions. TODO: actually run the editor when there is only one selected goal, rather than keeping the current threeclick method of editing proofs.

MARCHE Claude authored

MARCHE Claude authored

 23 Sep, 2011 2 commits


MARCHE Claude authored

MARCHE Claude authored
