- 20 Oct, 2012 1 commit
-
-
Andrei Paskevich authored
+ create AUTHORS file + fix the linking exception in LICENSE + update the "About" in IDE + remove the trailing whitespace + inflate my scores at Ohloh
-
- 15 Oct, 2012 1 commit
-
-
François Bobot authored
Don't work for Win32 but that keep the possibility for Unix.
-
- 11 Sep, 2012 1 commit
-
-
Claude Marche authored
-
- 04 Aug, 2012 1 commit
-
-
Andrei Paskevich authored
and Debug.register_stop_flag into register_flag. While information flags (selectable by --debug-all) are more common, it is safer to treat a generic debug flag as behaviour-changing by default.
-
- 03 Aug, 2012 1 commit
-
-
François Bobot authored
(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?
-
- 20 Jul, 2012 1 commit
-
-
Jean-Christophe Filliâtre authored
the original file is properly saved and restored upon completion (whatever the result is)
-
- 14 Jul, 2012 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 20 Jun, 2012 1 commit
-
-
MARCHE Claude authored
-
- 08 Jun, 2012 1 commit
-
-
MARCHE Claude authored
-
- 01 Jun, 2012 1 commit
-
-
MARCHE Claude authored
-
- 10 Apr, 2012 1 commit
-
-
Guillaume Melquiond authored
The goal is to keep track of unexpected termination, especially when the output of the prover is empty.
-
- 09 Apr, 2012 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
when replaying proofs.
-
- 16 Mar, 2012 1 commit
-
-
MARCHE Claude authored
-
- 22 Feb, 2012 1 commit
-
-
Andrei Paskevich authored
- 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
-
- 28 Nov, 2011 1 commit
-
-
Andrei Paskevich authored
-
- 20 Nov, 2011 1 commit
-
-
Guillaume Melquiond authored
My first idea was to use "-R @libdir@/coq", or some other variable I would have defined in configure.in, but it didn't work at all. Indeed, such path variables depend on cascaded substitution, which work fine inside make files and shell scripts, but not at all inside Why3 config files. Note that this is a documented feature of Autoconf so I doubt there is any way to circumvent it. So I ended up adding a new format specifier inside call_provers: %l is substituted by Config.libdir.
-
- 18 Nov, 2011 1 commit
-
-
Andrei Paskevich authored
This allows to call editors from IDE in a less hackish way and might even fix the problem with Coq editing on Windows.
-
- 27 Oct, 2011 1 commit
-
-
MARCHE Claude authored
-
- 26 Oct, 2011 1 commit
-
-
MARCHE Claude authored
Hopefully this solves the problem of unreliable answers from some provers like Vampire: there is no such answer "unknown" just 0.01 seconds before the time limit anymore
-
- 01 Jul, 2011 1 commit
-
-
Andrei Paskevich authored
-
- 24 May, 2011 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 20 Feb, 2011 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 21 Dec, 2010 1 commit
-
-
Andrei Paskevich authored
-
- 16 Dec, 2010 1 commit
-
-
François Bobot authored
"%h:%m:%s:%i" (i for mIlliseconds) Spass does'nt give cputime but wallclock. eprover doesn't always give time. so use cpulimit_time for them. add %b for the memlimit in bytes
-
- 15 Dec, 2010 1 commit
-
-
François Bobot authored
from the prover output the time used by the prover. An intermediate format "h:m:s" is used to accept more output than only seconds.
-
- 13 Dec, 2010 1 commit
-
-
MARCHE Claude authored
-
- 09 Dec, 2010 1 commit
-
-
Andrei Paskevich authored
-
- 05 Dec, 2010 1 commit
-
-
François Bobot authored
Scheduler : Schedule the call, precompute the buffer in advance.
-
- 27 Aug, 2010 1 commit
-
-
Francois Bobot authored
-
- 26 Aug, 2010 1 commit
-
-
Andrei Paskevich authored
-
- 02 Jun, 2010 1 commit
-
-
Andrei Paskevich authored
the problem is sent to stdin, but _after_ the problem is written in a file.
-
- 01 Jun, 2010 1 commit
-
-
Jean-Christophe Filliâtre authored
programs: WP for exceptions why.conf: removed -debug flag for alt-ergo
-
- 28 Apr, 2010 2 commits
-
-
Andrei Paskevich authored
-
Jean-Christophe Filliâtre authored
-
- 22 Apr, 2010 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
- 21 Apr, 2010 2 commits
-
-
Andrei Paskevich authored
-
Andrei Paskevich authored
- apply transformations in Driver at print_task/prove_task
-