Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Activity

Activity:
Start Date:
End Date:
Time Activity By
2017-07-19
15:08:18 Source Code scm commit: Cursor examples: removed outdated comment (commit 87c1382)
15:00:04 Source Code scm commit: Session files for cursor examples (commit 68af037)
14:55:38 Source Code scm commit: cursor_examples.mlw moved to the gallery (commit f82c19b)
13:19:58 Source Code scm commit: Compile: cosmetic (commit c9b80a7)
10:22:17 Source Code scm commit: Extraction: minor (commit 45a76d0)
10:03:28 Source Code scm commit: Cursor examples (wip) (commit 20cec7c)
05:31:51 Source Code scm commit: display all bench errors at the end of the bench (commit d1afa85)
2017-07-18
16:45:24 Source Code scm commit: Extraction: fixes around the use of mask in match expressions (commit cd7911e)
16:45:02 Source Code scm commit: Cursor module: no more collection in the cursor data type (commit 85c7224)
13:24:21 Source Code scm commit: space in json values (commit 6b2dd01)
12:46:21 Source Code scm commit: Json list and record correct empty values. (commit 59f6bf3)
2017-07-17
12:53:07 Source Code scm commit: Order of arguments in transformation error messages. (commit 6bc0260)
11:57:33 Source Code scm commit: Fixed transformation proved update (commit e8a565b)
10:06:16 Source Code scm commit: Patch on lexer.mli to avoid errors in make. (commit 0186aeb)
09:32:40 Source Code scm commit: Added default value for timeout (as done in former session). (commit 0ea2170)
2017-07-14
06:02:31 Source Code scm commit: fix CE bench for using official CVC4 1.5 release (commit f7def30)
2017-07-13
17:26:19 Source Code scm commit: "Extraction: (commit e3f56e1)
14:53:51 Source Code scm commit: union-find example (wip) (commit 116db59)
12:58:16 Source Code scm commit: Exception for print. (commit 2af6098)
11:23:32 Source Code scm commit: Added list of terms for instantiate. (commit de5927c)
10:10:23 Source Code scm commit: Destruct now possible on implications. (commit 594f552)
06:49:42 Source Code scm commit: Support for CVC4 1.5 (commit a66f4c2)
2017-07-12
20:00:30 Source Code scm commit: a quick and dirty implementation of a builtin Int module (commit 92533db)
14:59:19 Source Code scm commit: Launching provers on file/trans/theory node allowed again. (commit 24de544)
13:54:45 Source Code scm commit: ITP does not use drivers anymore for printing task (commit d3e8e47)
12:53:07 Source Code scm commit: extraction: fixed detection of functors (commit 3b1d5f2)
12:08:11 Source Code scm commit: extraction: fixed global names with --modular (commit 9793440)
08:25:57 Source Code scm commit: Update session using Coq (in progress) (commit 3a923a0)
2017-07-11
18:39:09 Source Code scm commit: Extraction: functors (wip) (commit ce738f7)
15:43:31 Source Code scm commit: Extraction: path for definitions inside sub-modules (commit 6632b3b)
15:10:18 Source Code scm commit: extraction: fixed names for toplevel definitions (wip) (commit 1208fb2)
15:08:06 Source Code scm commit: Simplified the focus_on_label registering. (commit e79e390)
15:03:33 Source Code scm commit: Improved printing on tactics errors (ongoing) (commit fc64eaf)
13:51:45 Source Code scm commit: Extraction of sub-modules (wip) (commit 0dbd3f2)
12:23:44 Source Code scm commit: Fix problem with sanitizer that would prevent = reparsing because of "infix =" naming. (commit 1944283)
09:33:56 Source Code scm commit: Create a tag only once. Repeating this creation causes segmentation faults and raises Gtk exceptions. (commit 89592e9)
09:27:40 Source Code scm commit: minor ungoing improvements to exception raising and error message printing. (commit 541cf77)
2017-07-10
14:39:58 Source Code scm commit: Removing eprintf (commit 2f3fe7b)
12:28:58 Source Code scm commit: Adding documentation of transformation after their failure. Adding catching of an exception. (commit d69b242)
12:11:56 Source Code scm commit: help on specific transformation. (commit a65df87)
11:46:52 Trackers Tracker Item [#21387] can not install why3 Closed Nobody
11:43:09 Source Code scm commit: minor, removed warning (commit 583320c)
11:41:46 Source Code scm commit: slight improvement of Ocaml extraction for ghost variables (commit b27b7e2)
11:19:04 Source Code scm commit: Support for E prover 1.9 and 2.0 (commit e3e20c8)
10:36:03 Source Code scm commit: Cursor example (wip) (commit 724c540)
09:52:26 Source Code scm commit: help can be done at any time. (commit 5617bcc)
2017-07-08
01:02:45 Trackers Tracker Item [#21387] can not install why3 Opened david streader
2017-07-07
14:37:37 Source Code scm commit: Correct a bug that would make a file always proven at load time. Not sure about this. (commit c988bed)
12:46:07 Source Code scm commit: why3printer: fix stupid mistake adding an extra single quote in front of ids (commit e10eb56)
07:04:15 Source Code scm commit: update obsolete sessions (commit e13568e)
2017-07-06
15:00:35 Source Code scm commit: move empty_name_table where it is used (commit 6174ead)
13:27:33 Source Code scm commit: fixed again the sanitizer for Why3 printer and naming_tables (commit 5f88d5f)
10:49:19 Source Code scm commit: naming tables should provide a printer that always prints valid why3 identifiers (commit 8004962)
09:02:34 Source Code scm commit: missing headers (commit 0f270d9)
09:01:03 Source Code scm commit: A bit of cleaning, better renaming, and improvement of API documentation (commit 1844cd8)
07:59:11 Source Code scm commit: Cursor: snapshot type for collection in cursor (commit 2c62256)
07:54:57 Source Code scm commit: New exception Invalid_argument in ocaml.Pervasives (commit c9e1745)
07:54:23 Source Code scm commit: New module Cursor.mlw (commit d236867)
2017-07-05
14:02:54 Source Code scm commit: ITP: support for qualified ident and infix ident (commit bccdfac)
13:39:43 Source Code scm commit: fixed not jumping to the next_unproven_node_id after applying trans. Also typo. (commit ec18704)
13:25:42 Source Code scm commit: Added Tstringlist and intros a,b,c,d. This is not a problem that intros is given names that already exists. (commit f68414e)
12:43:47 Source Code scm commit: searching multiple idents simultaneously, available in IDE (commit d962aa6)
11:32:04 Source Code scm commit: separate the 'search' command from the naming tables (commit bcd79af)
07:38:01 Source Code scm commit: option to select with or without intros in printing why3 tasks (commit 6c4b0d6)
2017-07-04
15:50:01 Source Code scm commit: subst_all substitute all local definitions. Do not work on a lot of definitions of the language. (commit 621a53a)
2017-07-03
13:09:35 Source Code scm commit: Added label detection at initialization for autofocus on a specific node. This ongoing modification should not change the current behaviour. (commit 571b6a6)
2017-07-02
21:57:25 Source Code scm commit: Porting cursor example (wip) (commit 68f6a90)
15:23:17 Source Code scm commit: Added exception for absence of transformation argument (commit 20915ad)
2017-06-30
14:41:04 Source Code scm commit: Context menu keeps open when releasing button 3 (commit 38c3c04)
14:08:31 Source Code scm commit: Remove eprintf that behaves badly with application that cannot understand that stderr is not stdout. (commit 31e03ce)
12:06:28 Source Code scm commit: Deprecated. why3ide cannot be launched without a .mlw file anymore. (commit 539849a)
12:00:23 Source Code scm commit: On typing errors, the arguments is printed colored on the location which is indicated by the error. (commit a1f33dd)
11:34:24 Source Code scm commit: improve multiplication (commit 1c87e21)
09:50:48 Source Code scm commit: ITP: improving task printing a bit more (commit a73e4df)
09:18:17 Source Code scm commit: ITP, task printing: suppressed extra parentheses (commit 16f18e0)
08:44:03 Source Code scm commit: fix the bench: API tests now use session_itp (commit 3982af9)
07:53:15 Source Code scm commit: Merge branch 'master' into itp (commit e6bba4d)
07:41:26 Source Code scm commit: update failing proofs in nightly bench (commit 958c9c9)
07:14:56 Source Code scm commit: few improvements in CE bench (commit a229dcf)
2017-06-29
22:57:11 Source Code scm commit: trywhy3: update syntax and add "5000 steps" option (commit 9ac6d39)
21:44:31 Source Code scm commit: Eliminate_algrebraic: Pervasives.or is deprecated (commit 2ca226c)
15:47:43 Source Code scm commit: Using report_loc for locations reporting of errors in source code. (commit 2586367)
15:25:14 Source Code scm commit: Patched makefile (commit fad7c6f)
15:16:57 Source Code scm commit: attempt to modify task printing (commit 9610d93)
12:46:27 Source Code scm commit: More transformation errors. Fix calling provers on unselected node. (commit 95cc8f9)
12:46:02 Source Code scm commit: new example: gnome sort (commit 04d9283)
10:38:56 Source Code scm commit: Trying to catch errors for transformations with arguments. It raises problems illustrated by the example committed. (commit 540cad5)
10:24:30 Source Code scm commit: Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr/gitroot/why3/why3 into new_system (commit c9e631c)
10:24:26 Source Code scm commit: OCaml printer: better printing for polymorphic recursive functions (commit e9b77c3)
09:11:20 Source Code scm commit: Trying to regroup transformations with arguments into several files instead of having everything in case.ml. (commit b7c18ad)
2017-06-28
16:39:38 Source Code scm commit: Update ce-bench and order printed file (commit 0f7e207)
14:59:22 Source Code scm commit: CE bench: enforce execution with cwd = the directory bench/ (commit bff0a1f)
14:06:02 Source Code scm commit: Args_wrapper now contains typed symbols as before. Untyped symbols can also be used. (commit e256e3b)
13:05:21 Source Code scm commit: [search id] now also do [print id] (commit 788a82d)
09:09:55 Source Code scm commit: proof attempts that have no result in session file are loaded with result Failure (commit e8adc7c)
09:03:12 Source Code scm commit: Adapting existing CE tests to ce-bench. Removed timings. (commit 3f947d7)
08:41:07 Source Code scm commit: resurected why3sesssion_latex (commit 53e0e5b)
2017-06-27
15:06:31 Source Code scm commit: union_find: fixed interface (commit 04d9eb4)
14:55:53 Source Code scm commit: union_find: more realistic code, consistent variable naming (commit eab63c5)
14:25:41 Source Code scm commit: new example union_find (wip) (commit f034e8b)
07:17:50 Source Code scm commit: cleaner benchmarks (commit daaa5db)
06:04:12 Source Code scm commit: Merge branch 'master' into new_system (commit c137bd7)
05:59:43 Source Code scm commit: Merge branch 'master' into itp (commit f05392e)
05:58:40 Source Code scm commit: restored why3session html (commit a465e9b)
2017-06-26
15:26:30 Source Code scm commit: port WP_revisited in progress (commit 3937227)
15:02:29 Source Code scm commit: extraction: Not_found is not from OCaml's Pervasives (commit d1e3b33)
13:12:26 Source Code scm commit: ocaml.Pervasives: added Not_found (commit 934d77c)
11:26:33 Source Code scm commit: ported example vacid_0_binary_heaps (commit 487c25f)
10:50:53 Source Code scm commit: Added no_inversion and no_selector for eliminate_algebraic transformations from a commit by Florian Schanda in 2013 (Spark repo 9b954f4). (commit af6c3d9)
09:45:15 Source Code scm commit: fix non-robust proof in example schorr-waite (commit 98594c8)
08:58:20 Source Code scm commit: in_progress/2wp_gen: example rebased (commit 2015fbd)
06:15:15 Source Code scm commit: avl: update obsolete session (tables) (commit 4863347)
06:10:25 Source Code scm commit: double wp: added invariant witnesses (commit 9cd7a83)
04:43:56 Source Code scm commit: why3 client/server: ensure the socket name does not already exist (commit 6f79556)
2017-06-25
22:01:12 Source Code scm commit: examples: add the missing proofs for type witnesses (commit 9ea8a6a)
21:12:52 Source Code scm commit: examples/use_api: update for eb751c1b (commit 0650b2e)
20:53:21 Source Code scm commit: Pdecl: relax type constraints on invariant witnesses (commit 1a36400)
14:31:03 Source Code scm commit: Patch previous commit. (commit 420977e)
14:24:09 Source Code scm commit: Recovered remove_subtree. Easier to use Why3's API with this in controller. (commit e3f2cb5)
14:12:54 Source Code scm commit: patched remove (commit 8c74709)
13:36:05 Source Code scm commit: Missing json case. (commit cb3db55)
2017-06-23
15:15:49 Source Code scm commit: Detect and/or in conditions and simplify them (commit f581fb6)
14:51:13 Source Code scm commit: ITP sessions: proved status in now inside the session static state and saved on disk (commit d8294ab)
12:38:41 Source Code scm commit: update oracles for bench CE (commit 3a8adda)
12:37:51 Source Code scm commit: update two examples missing proof of witness (commit a4f7b8d)
2017-06-22
19:44:24 Source Code scm commit: Pdecl: do not require the invariant witness to be non-ghost (commit 9b35567)
14:49:53 Source Code scm commit: Extract likely/unlikely annotation labels into __builtin_expect(.,.) (commit 0d5e405)
13:47:40 Source Code scm commit: WhyML: check type invariants (commit 15fc3d6)
13:39:36 Source Code scm commit: Merge branch 'master' into itp (commit e556b0a)
12:43:38 Source Code scm commit: check that alias clauses happen (commit 9f1ec23)
12:13:32 Source Code scm commit: update sessions and shapes after merge with master (improvements on shape computations) (commit 5fb8c95)
08:04:39 Source Code scm commit: Merge branch 'master' into new_system (commit 171085d)
07:40:18 Source Code scm commit: update obsolete session (commit 5c6821f)
07:37:05 Source Code scm commit: yet another attempt (commit af971a1)
06:58:02 Source Code scm commit: protect unix error, another attempt (commit 05a32c4)
06:35:53 Source Code scm commit: attempt to capture connection error (Unix_error(_,"connect",_)) (commit 100fc22)
2017-06-21
14:58:25 Source Code scm commit: make CE regression tests more robust (commit 6e7481f)
14:52:36 Source Code scm commit: Removed commented code. (commit ec3ac79)
14:43:19 Source Code scm commit: adding ce regression tests in nightly bencn (commit 96e70c7)
14:35:38 Source Code scm commit: Merge branch 'new_system' into mp (commit 3635ece)
14:31:22 Source Code scm commit: Extraction: keep labels (commit cb8e5a3)
14:27:37 Source Code scm commit: starting a regression test suite for counterexamples (commit f2f7967)
14:01:15 Source Code scm commit: ITP: print explanation between square brackets (commit e97f94a)
13:57:20 Source Code scm commit: fix session (commit 14a3c1c)
13:10:16 Source Code scm commit: Merge branch 'new_system' into mp (commit f700b13)
12:46:19 Source Code scm commit: special case clz=0 in divmod_1 (commit 9070807)
09:18:16 Source Code scm commit: Clean do clean transformations that are not successful (commit 1fddf96)
07:20:47 Source Code scm commit: Fix empty node status when proof_result is None (commit 60f3cf7)
06:57:00 Source Code scm commit: fix setting of file state after reload (commit 0a38df2)
2017-06-06
10:07:54 Source Code scm commit: Q313-019 Add parsing of hexadecimal for float values (commit 3f4947b)
2017-05-22
12:41:28 Source Code scm commit: Q424-012 Parse z3s boolean expression and floating point value (commit 3a94474)
2017-04-18
15:43:56 Source Code scm commit: Q418-025 Printing arrays with bv indices (commit 3f732c4)