GitLab

Test with why3 tests/test_exec.mlw --exec M.x

why3 tests/test-eval.why -P alt-ergo -T T --eval c1 --eval c2 --eval c3

Util now is a small module containing misc functions.

+ rename Debug.Opt to Debug.Args to avoid conflicts

+ create AUTHORS file
+ fix the linking exception in LICENSE
+ update the "About" in IDE
+ remove the trailing whitespace
+ inflate my scores at Ohloh

note: program extraction IS NOT yet implemented

 (metas, debug flags, transformations, formats) except for label.

This description is used in --list-*. The description can use any of
the formatting markup of Format "@ " "@[",...

Transformations can also specify from which metas and labels they
depend, and add informations about how they are interpreted.

TODO:
  - complete and correct the documentation
  - when a transformation use Trans.on_meta, it should be possible to
    add an interpretation of the metas in the documentation.
  - recover a summary version of --list-* ?
  - be able to export in latex?

       Remove the id in prover that is used only for command-line, use
       instead the name,version,alternative of the prover. One can
       also use regular expression (start with ^).

       "Alt-Ergo,0.92,with arrays" corresponds only to one prover
       "Alt-Ergo,^0\.9.*,with arrays" correspond to all the Alt-Ergo prover with arrays which version match "0\.9.*"
       "Alt-Ergo" is the same thing than "Alt-Ergo,^,^"
       "Alt-Ergo,0.92," corresponds only to one prover with the alternate fields empty
       "Alt-Ergo,,with arrays" corresponds to "Alt-Ergo,^,with arrays" since the version is never empty.

       Provers identification are case sensitive even if it is
       currently more complicated for the user because
       case-insensitiveness is not sufficient. Specifiying "alt-ergo"
       for "Alt-Ergo,^,^" is great, but not if there is more than one
       match. A more general system of shortcut would be more
       appropriate.

- change takes function as the first argument
- add_new takes exception as the first argument
- find_default is renamed to find_def and takes the default value
  as the first argument
- find_option is renamed to find_opt (to align with find_exn and find_def)
- default_option is renamed def_option

It's goal is to allow to view and modify sessions.

Currently three sub-commands :
info : can give the provers used, pretty-print in ascii a session,
     can give the corresponding directory
mod : allow to set obsolete, or modify the archive state of proof attempt
    which corresponds to selected provers
copy : copy a proof attempt by modifing its prover

Prover ids are only used for the command line option "-P".
The user can choose what he wants (they must be unique)
The prover name and version should not be modified. If someone want to
test different command line options for a prover he can use the
"alternative" field.

If someone want to replay an external proof but he doesn't have the
corresponding prover (same name,version,alternative), why3ide ask for
a replacement among the known provers. The choice can be saved.

The loaded files are slimmed down version of the standard configuration
file. They only support the following sections and fields:

[main]
  loadpath=
  plugin=
[prover ...]
  option=
  driver=

It is also possible to define brand new [prover] sections.

For now, the only supported frontends are why3 and why3ide.

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.

also add Env.get_loadpath to use for Coq realisation