| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Update headers following #6543. |  Théo Zimmermann | 2018-02-27 |
| | | |||
| * | Add interfaces for checker and remove dead code. |  Maxime Dénès | 2018-01-10 |
| | | |||
| * | Use large arrays in the checker demarshaller. |  Pierre-Marie Pédrot | 2017-11-28 |
| | | | | | | This allows to work around the size limitation of vanilla OCaml arrays on 32-bit platforms, which is rather easy to hit. | ||
| * | Truncate strings in votour to 1024 characters. | Pierre-Marie Pédrot | 2017-11-23 |
| | | | | | | Making it bigger is kind of useless, takes time and clutters the output for no real advantage. | ||
| * | Bypass int and string representation in votour when it's incorrect. | Pierre-Marie Pédrot | 2017-11-23 |
| | | |||
| * | Tail-recursive list traversal in votour. | Pierre-Marie Pédrot | 2017-11-23 |
| | | |||
| * | Implement a tail-recursive traversal of the object in votour. | Pierre-Marie Pédrot | 2017-11-22 |
| | | |||
| * | Bump year in headers. | Pierre-Marie Pédrot | 2017-07-04 |
| | | |||
| * | [checker] [votour] resolve warning 52 fragile constant pattern |  Gaëtan Gilbert | 2017-05-26 |
| | | | | | Also stop using failwith for flow control in tuple_of_string. | ||
| * | [votour] Fix/disable warnings. |  Emilio Jesus Gallego Arias | 2017-05-26 |
| | | |||
| * | [votour] Fix build with -safe-string (bug 5553) | Emilio Jesus Gallego Arias | 2017-05-26 |
| | | |||
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-05-04 |
| |\ | |||
| | * | Make votour a bit more robust/forgiving with respect to user commands (bug ↵ |  Guillaume Melquiond | 2016-05-02 |
| | | | | | | | | | #4702). | ||
| * | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
| |\| | |||
| | * | Update copyright headers. | Maxime Dénès | 2016-01-20 |
| | | | |||
| * | | Displaying the object identifier in votour. | Pierre-Marie Pédrot | 2015-11-15 |
| |/ | |||
| * | Adding a more efficient representation of OCaml objects in votour. | Pierre-Marie Pédrot | 2015-06-25 |
| | | |||
| * | Splitting the library representation on disk in two. | Pierre-Marie Pédrot | 2015-06-24 |
| | | | | | | The first part only contains the summary of the library, while the second one contains the effective content of it. | ||
| * | Votour displays wordsize of segments before loading them. | Pierre-Marie Pédrot | 2015-06-20 |
| | | |||
| * | Exporting memory representation of STM tasks for votour. | Pierre-Marie Pédrot | 2015-03-25 |
| | | |||
| * | Functorized interface over object representation in votour. | Pierre-Marie Pédrot | 2015-03-24 |
| | | | | | | | This gives more safety in object manipulation, as we delimit the uses of Obj functions, and allows for an alternative implementation of the representation of OCaml structures. | ||
| * | Fixing representation of dynamics in votour (again). | Pierre-Marie Pédrot | 2015-03-24 |
| | | |||
| * | Fixing internal representation of Dyn.t in votour. | Pierre-Marie Pédrot | 2015-03-18 |
| | | |||
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| | | |||
| * | checker and votour ported to new vo format (after -vi2vo) |  Enrico Tassi | 2014-02-26 |
| | | |||
| * | votour: better error messages | Enrico Tassi | 2014-02-26 |
| | | |||
| * | .vi files: .vo files without proofs | Enrico Tassi | 2014-01-04 |
| | | | | | | | | | | | | | | | | | | | | | | | | File format: The .vo file format changed: - after the magic number there are 3 segments. A segment is made of 3 components: bynary int, an ocaml value, a digest. The binary int is the position of the digest, so that one can skip the value without unmarshalling it - the first segment is the library, as before - the second segment is the STM task list - the third segment is the opaque table, as before A .vo file has a complete opaque table (all proof terms are there). A .vi file follows the same format of a .vo file, but some entries in the opaque table are missing. A proof task is stocked instead. Utilities: coqc: option -quick generates a .vi insted of a .vo coq_makefile: target quick to generate all .vi coqdep: generate deps for .vi files too votour: can browse .vi files too, the first question is which segment should be read coqchk: rejects .vi files | ||
| * | Adding dynamic value printing to votour through a registering mechanism. |  ppedrot | 2013-08-23 |
| | | | | | | | TODO: register the desired dynamic types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16733 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | Change in vo format : digest aren't Marshalled anymore |  letouzey | 2013-08-22 |
| | | | | | | | | | | | | Since digests are strings (of size 16), we just dump them now in vo files (cf. Digest.output) instead of using Marshal on them : this is cleaner and saves a few bytes. Increased VOMAGIC to clearly identify this change in the format. Please rerun ./configure after this commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | Fixing votour | ppedrot | 2013-08-20 |
| | | | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16718 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | Checker: vo validation checks the absence of Var/Evar/Meta | letouzey | 2013-04-15 |
| | | | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16405 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | votour: a small tool for guided tours of .vo | letouzey | 2013-04-15 |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16403 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |