- 22 Aug, 2012 5 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Guillaume Melquiond authored
-
François Bobot authored
-
Jean-Christophe Filliâtre authored
-
- 21 Aug, 2012 3 commits
-
-
François Bobot authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
- 20 Aug, 2012 4 commits
-
-
François Bobot authored
-
François Bobot authored
- the symbols that appear in the metas are identified in the xml by their position in the task: - in which declaration - in which definition (if that apply otherwise -1) - in which constructor(or case in inductive predicate) (if that apply otherwise -1) - in which field (if that apply otherwise -1) - the md5sum of the prefix of the task that end with the declaration is used to know if the symbol have been changed, and if it is obsolete. - currently metas that contains obsolete symbol are removed.
-
François Bobot authored
- add functions to Hashtbl.S - without ocaml 3.12 its not possible to do that for Hashtbl without copying the signature - "open Stdlib" hides the polymorphic hashtbl, perhaps a good idea since that avoid errors.
-
MARCHE Claude authored
-
- 17 Aug, 2012 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 16 Aug, 2012 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 14 Aug, 2012 3 commits
-
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
note: program extraction IS NOT yet implemented
-
Jean-Christophe Filliâtre authored
-
- 08 Aug, 2012 1 commit
-
-
Andrei Paskevich authored
Provide nine transformations: split_(goal|all|premise)_(full|right|wp). split_*_full splits as far as it can, split_*_right produces linear number of subformulas, split_*_wp stops at the "stop_split" label. The name "split_goal" is kept for compatibility with older session files and denotes the same transformation as "split_goal_wp". Thanks to Johannes Kanig for the suggestion.
-
- 05 Aug, 2012 3 commits
-
-
Andrei Paskevich authored
The full name includes the library path to the theory/module (if any), and the qualifier prefix of the ident in the theory/module.
-
Andrei Paskevich authored
-
Andrei Paskevich authored
For realization, code extraction, metas-in-sessions, etc, we need absolute names for identifiers. To that purpose it is better to have and store the qualified path to every ident.
-
- 04 Aug, 2012 5 commits
-
-
Andrei Paskevich authored
Provers will have native polymorphism support long before people will start writing third-party polymorphism encoding procedures for Why3. (And it's not that I have high hopes about the former.)
-
Andrei Paskevich authored
-
Andrei Paskevich authored
-
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.
-
Andrei Paskevich authored
-
- 03 Aug, 2012 14 commits
-
-
Andrei Paskevich authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
François Bobot authored
comportement was not very clear if an exception was raised.
-
François Bobot authored
TODO: - make the "on hover" prettyer (Find the size used by gtk for the popup message en set pp_set_margin to this size?) - Some transformations (ex: smoke_detector_*) should we mark them specialy during the registration i norder to warn the user?
-
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?
-
François Bobot authored
-
François Bobot authored
session pairing doesn't compute anymore the shape of the goal, it is done before. It was able to compute the shape only when the checksum of the task was different, but computing the checksum of the task is way more time consuming than computing the shape of the goal (and include it). So this commit simplify greatly the function and theoretically augment just a little the time spent. Experimentaly it's the inverse on max_matrix. Until "update_session: done" with or without modifying the checksums: before | after without : 0.21-0.22 s | 0.16-0.17 s with : 0.23-0.26 s | 0.18-0.20 s
-
François Bobot authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-