GitLab

Note that the file is still generated at compilation time.

The "realized" meta takes two arguments. The first one is the path+name of
the theory, the second one is the translation of it for the target prover.
The meta is supposed to be put into a printer file, so there is no
ambiguity on the target. The second argument can be left empty if it can be
inferred from the first one.

Note that the first argument is not really satisfactory, since it is
redundant with the theory part of the driver. Moreover, its handling is a
bit crude: it does not take into account rich qualifiers and it does not
generate proper error messages if it does not match the theory.

How to use it:

    why3 --realize -D drivers/coq-realize.drv -T real.Real -o .

        produces Real.v in the current directory

    why3 --realize -D drivers/coq-realize.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, coq-realize.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 non-alphanumeric symbols.

The whole thing is in very preliminary stage.
Use with caution.

This is getting tedious. There should be a way to drop the content of a
whole theory.

introduced new transformation eliminate_non_struct_recursion for that purpose
uses Decl.check_termination tomake the check and the pretty-print
(could probably be improved to avoid 3 calls to check_termination)

whycpulimit : Fix return the status of the prover
gappa       : Fix inversion (should use meta showing
              what musn't be instantiated)

- bring driver syntax closer to that of theories
- some simple API improvements

- accept timeout regexps in drivers
- do not take command line from drivers