Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Activity

Activity:
Start Date:
End Date:
Time Activity By
2017-05-29
13:56:56 Source Code scm commit: SHELL IDE: Remove failing cases for some notifications (commit 0015ffe)
13:47:13 Source Code scm commit: doc for extraction (wip) (commit 14b414d)
09:28:36 Source Code scm commit: OCaml64 driver: minor (commit 39d4b1b)
08:12:12 Source Code scm commit: ocaml compatibility (commit 18bd32c)
08:11:58 Source Code scm commit: Focus first implementation (commit 1b910c9)
2017-05-27
22:18:23 Source Code scm commit: Mlw: support Epure in the surface language (with type inference) (commit 7271489)
2017-05-26
17:59:42 Source Code scm commit: corrected xml attributes. (commit 945ca6d)
2017-05-25
22:36:16 Source Code scm commit: Vc: restrict creation of logical terms for expressions (commit 9d21ee4)
21:50:20 Source Code scm commit: Split_goal: ignore "case_split" if an upper split had place (commit e91c22e)
16:43:35 Source Code scm commit: Split_goal: restore aggressive splitting for split_premises (commit 19b6004)
2017-05-24
15:06:53 Source Code scm commit: Update some Coq realizations. (commit 721c086)
14:44:39 Source Code scm commit: Merge branch 'itp' of git+ssh://scm.gforge.inria.fr/git/why3/why3 into itp (commit 1fc1071)
14:39:53 Source Code scm commit: why3 session with new sessions: restored basic usage of why3 session info (commit 091d0cb)
13:34:29 Source Code scm commit: Merge branch 'itp' into itp_new_why3session (commit 368bca4)
13:15:01 Source Code scm commit: Split_goal: make introduce_premises less aggressige (commit 8b80962)
12:56:12 Source Code scm commit: remove_list: removed square bracket (commit c4e6a04)
12:03:59 Source Code scm commit: Removed unused exception. Patched lexer.mli. (commit 83cbbdb)
11:51:56 Source Code scm commit: code layout (commit e65c9dc)
11:48:18 Source Code scm commit: Remove_list to remove list of hypotheses (prsymbol) (commit 97362ba)
10:50:24 Source Code scm commit: Using driver from the controller for interactive provers. (commit f665916)
10:15:25 Source Code scm commit: Merge branch 'master' into itp (commit eb43812)
10:08:48 Source Code scm commit: allow relative pathnames for drivers stored in the Why3 config file (commit eb751c1)
09:40:12 Source Code scm commit: Interactive provers are now usable with their command and replay. (commit 0c327fa)
04:41:46 Source Code scm commit: Update some Coq realizations. (commit 501bde2)
04:30:19 Source Code scm commit: Do no longer play tricks with headers of Coq realizations. (commit b2ca71c)
04:17:35 Source Code scm commit: Preserve realization headers in Coq printer. (commit 2de30b0)
2017-05-23
20:28:18 Source Code scm commit: update obsolete sessions (commit 30fd6bb)
16:11:13 Source Code scm commit: deleted ocaml32 driver (commit 0e68a95)
15:41:34 Source Code scm commit: Adding Edit_req (commit c0d087b)
15:14:56 Source Code scm commit: Sudoku reproved, phew ! (commit 70504c5)
13:45:28 Source Code scm commit: Extraction: all examples ported (commit 6e1ab42)
13:07:29 Source Code scm commit: bench (commit 9b31eaf)
12:49:42 Source Code scm commit: Vc: "vc:keep_precondition" on a function call preserves preconditions (commit cae5a08)
12:34:00 Source Code scm commit: Vc: asymmetric "and" for chains of pre-/post-/invariant goals (commit 22780e8)
12:27:06 Source Code scm commit: Pdecl: add triggers to the invariant axiom (commit 78270aa)
12:04:12 Source Code scm commit: Updated 3 more extraction examples, 1 more to go (commit 12bb1ee)
12:03:44 Source Code scm commit: simplified tree_height example (commit 18a1cef)
2017-05-22
22:52:29 Source Code scm commit: Expr: better handling of implicit post-conditions for local functions (commit 03cc112)
15:37:48 Source Code scm commit: Update some extraction examples of the bench (commit 50b0727)
14:24:00 Source Code scm commit: Vc: no more "liberal_for" (commit fb77f39)
14:07:01 Source Code scm commit: Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr/git/why3/why3 into new_system (commit d5b9da7)
14:04:52 Source Code scm commit: example fibonacci updated (no Coq proofs anymore!) (commit 750ea0b)
11:58:15 Source Code scm commit: Mlw: use a special label to mark user annotations (commit 840c13b)
11:48:10 Source Code scm commit: Merge remote-tracking branch 'origin/master' into new_system (commit 077ae9c)
11:37:23 Source Code scm commit: Fix bug in stdlib int.Exponentiation (commit 3e625c0)
06:03:34 Source Code scm commit: Fix some Coq realizations. (commit be82955)
2017-05-21
19:00:11 Source Code scm commit: more proofs updated (commit 9706083)
18:21:16 Source Code scm commit: update proof of a few examples (commit 211eb27)
06:24:08 Source Code scm commit: Fix some Coq realizations. (commit 3ef4b17)
2017-05-20
14:15:05 Source Code scm commit: Coq: ignore the "type unit = ()" declaration in why3.Unit (commit 4f841f9)
14:01:15 Source Code scm commit: Expr: be less zealous on term-to-fmla conversion (commit 5e4507b)
2017-05-19
15:54:27 Source Code scm commit: IDE GTK: show the tools menu on right click (commit 81bbad2)
15:53:18 Source Code scm commit: update some proofs (commit 1f56973)
15:28:30 Source Code scm commit: nightly bench: put only the last 20 lines of the make bench (commit 4c38b07)
15:20:51 Source Code scm commit: temporarily adapt nightly bench for new system, again (commit f4b3b50)
15:12:34 Source Code scm commit: temporarily adapt nightly bench for new system (commit 59725ac)
14:52:12 Source Code scm commit: Added get_prover_config in Whyconf. (commit 4dcb5f6)
14:51:02 Source Code scm commit: fix Coq header for Parity.v (commit 3ab15af)
14:44:13 Source Code scm commit: update obsolete sessions (commit 931cb8e)
14:18:51 Source Code scm commit: fix realization of number.Parity (commit 185b87d)
13:42:51 Source Code scm commit: Add the official releases of Alt-Ergo to level-1 automation. (commit 5ebaf51)
12:04:08 Source Code scm commit: Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into new_system (commit 6f5784c)
12:04:02 Source Code scm commit: update proof sessions (commit 7f59fa3)
12:02:39 Source Code scm commit: update bench (commit a6016c5)
11:55:04 Source Code scm commit: updated proof sessions (commit 09096e7)
11:53:45 Source Code scm commit: update obsolete session (commit b84ff9b)
11:52:19 Source Code scm commit: update obsolete sessions (commit da9ea02)
10:56:42 Source Code scm commit: move example ieee_float into test-provers, it is more adequate and is not fully proved anyway (commit 0f9dd6d)
10:52:51 Source Code scm commit: update session (commit d49323d)
09:54:40 Source Code scm commit: updated sessions related to bitvectors (commit f181fd7)
09:24:36 Source Code scm commit: Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into new_system (commit 2a84e63)
09:24:28 Source Code scm commit: update proof sessions (commit 553a36b)
09:20:02 Source Code scm commit: updated proof sessions (commit ce7bf93)
09:17:02 Source Code scm commit: update session for example bitwalker (commit 6d1da3a)
09:16:34 Source Code scm commit: hack to allow session update from WhyML 0.8x to WhyML 0.90 (commit 3b371b3)
09:15:02 Source Code scm commit: update proof sessions (commit b73df5d)
09:10:01 Source Code scm commit: update proof sessions (commit ba004b7)
09:07:06 Source Code scm commit: update proof sessions (commit 574642c)
09:05:38 Source Code scm commit: Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into new_system (commit 65c0633)
09:05:29 Source Code scm commit: update proof sessions (commit 47ddeaa)
09:05:23 Source Code scm commit: update 2 examples on bitvectors (commit b5087ad)
09:01:44 Source Code scm commit: Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into new_system (commit 7c1dbac)
09:01:13 Source Code scm commit: examples/avl: portage vers le nouveau système (commit 7b0f17c)
08:53:41 Source Code scm commit: updated proof sessions (commit 4d03eb9)
08:27:25 Source Code scm commit: updated proof sessions (commit 43fbb55)
08:14:24 Source Code scm commit: updated proof sessions (commit ca1a168)
04:37:00 Source Code scm commit: Fix example. (commit d98661f)
2017-05-18
15:33:56 Source Code scm commit: Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into new_system (commit c9a504f)
15:07:41 Source Code scm commit: updated proof sessions (commit fbc46ff)
12:15:54 Source Code scm commit: sequence: minor (commit b11896f)
12:09:34 Source Code scm commit: Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr/gitroot/why3/why3 into new_system (commit 17ff099)
12:09:25 Source Code scm commit: verifythis odd-even : simplify proof and move file (commit f20e058)
10:13:58 Source Code scm commit: GTK IDE: added a mark obsolete in popup_menu. (commit 6cf8e12)
09:26:08 Source Code scm commit: updated proof sessions (61 to go) (commit 3cd1432)
08:46:48 Source Code scm commit: added solutions for VerifyThis 2017 (commit 9bcb407)
2017-05-17
14:59:25 Source Code scm commit: GTK IDE: adding a popup menu on right click (commit 9c13e10)
14:04:08 Source Code scm commit: GTK IDE: time and limits shown in third column (commit dac3b10)
13:55:53 Source Code scm commit: sequence theory: factor definitions/axioms as specs, add a algebraic theory (commit af08d5c)
12:53:20 Source Code scm commit: fix obsolete status and proved status during replay (commit 95ba51b)
12:37:08 Source Code scm commit: fix computation of obsolete status during merge (commit b7dbd0e)
12:34:27 Source Code scm commit: add comments to API of module prove_client (commit 13078bb)
12:18:31 Source Code scm commit: Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into new_system (commit f954b8a)
12:18:09 Source Code scm commit: mach/peano: val constant now available + coercion (commit aec4074)
12:15:40 Source Code scm commit: update doc: syntax changes w.r.t 0.87 (commit e826fd4)
09:17:19 Source Code scm commit: Removed useless use_shapes argument. (commit 3876183)
08:58:00 Source Code scm commit: more session fixing (commit 156e81b)
08:44:19 Source Code scm commit: Remove incorrect ocamldoc comments. (commit 1a74864)
08:26:00 Source Code scm commit: Fix session (commit 9da7adf)
06:40:46 Source Code scm commit: Improve gallery generation. (commit 189b498)
06:24:29 Source Code scm commit: Use proper style markup in why3session html output. (commit 68a7fb1)
06:12:13 Source Code scm commit: Fix missing opening tags in why3session html output. (commit de7f2da)
06:00:24 Source Code scm commit: Remove incorrect closing tag in why3session html output. (commit 56dfee9)
05:45:27 Source Code scm commit: Fix incorrect headers generated by why3session html and add a charset meta. (commit d002262)
2017-05-16
17:57:14 Source Code scm commit: updated proof sessions (commit 579f007)
15:06:08 Source Code scm commit: updated proof sessions (commit 3766147)
14:28:11 Source Code scm commit: bag: added a refinement check (commit 1405cea)
14:04:52 Source Code scm commit: updated proof sessions (commit 477aea3)
13:48:05 Source Code scm commit: updated proof sessions (commit f868ab1)
13:23:34 Source Code scm commit: Fix some syntax errors in examples. (commit 3698ea2)
13:19:00 Source Code scm commit: pmodule: minor (commit 3249980)
13:07:04 Source Code scm commit: Refinement of top-level constants. (commit 95953af)
12:47:53 Source Code scm commit: Fix syntax of some examples and add them to the bench. (commit 7beca01)
12:42:40 Source Code scm commit: updated proof sesssions (commit 65e773f)
12:22:45 Source Code scm commit: updated proof sesssions (commit 63b8f6d)
12:17:23 Source Code scm commit: updated proof sesssions (commit 1c16527)
12:09:17 Source Code scm commit: updated proof sessions (commit dac28bc)
12:01:57 Source Code scm commit: updated proof sessions (commit 3773922)
11:54:14 Source Code scm commit: updated proof sessions (commit 9a7ef34)
07:53:15 Source Code scm commit: update sessions (commit 39e306c)
06:26:35 Source Code scm commit: Improve gallery generation. (commit 5698816)
2017-05-15
19:52:49 Source Code scm commit: Delay function documentation until the first empty line. (commit a4ac168)
15:40:07 Source Code scm commit: Restore compilation of why3doc. (commit 1fc2241)
15:04:30 Source Code scm commit: Fix unbound symbols in AVL examples. (commit ca5748c)
14:38:04 Source Code scm commit: Merge branch 'new_system' into alias (commit 6149c7a)
13:12:01 Source Code scm commit: updated proof sessions (commit a687718)
12:26:58 Source Code scm commit: Merge branch 'master' into new_system (commit 7d06089)
11:53:53 Source Code scm commit: Mark Alt-Ergo 1.30 as the only stable release. (commit fc66666)
11:53:53 Source Code scm commit: Mark Alt-Ergo 1.30 as the only stable release. (commit b6e9cdb)
09:27:20 Source Code scm commit: Use unique identifiers instead of internal tags when referencing meta arguments. (commit 3816f14)
08:40:41 Source Code scm commit: bench: valid goals (commit d8d5512)
2017-05-12
16:35:41 Source Code scm commit: type cloning: a couple of fixes (commit ffd3526)
15:42:22 Source Code scm commit: proposal for a general format of error mesages (commit f9760f3)
15:06:16 Source Code scm commit: Add VerifyThis 2017 bubblesort (commit c34a77c)
13:50:11 Source Code scm commit: Refinement. (commit 6c1f26d)
12:46:14 Source Code scm commit: bench: add missing proofs in stdlib/array (commit bdac2a4)
11:40:51 Source Code scm commit: Change addition primitives (commit 4bdc82b)
11:18:43 Source Code scm commit: Removed useless set_session (commit 8039f0d)
09:20:57 Source Code scm commit: Refinement: type invariant VC. (commit 3c17ee8)
08:35:06 Source Code scm commit: removed dead code, irrelevant comments. (commit 17f2d25)
2017-05-11
16:33:25 Source Code scm commit: Typeinv: commit sum types (commit 8d9366c)
14:10:08 Source Code scm commit: Refinement: optimizations. (commit bca27d4)
12:52:02 Source Code scm commit: Typing: indentation style (commit 43694d1)
10:29:46 Source Code scm commit: Refinement: code refactoring. (commit 5332ee9)
2017-05-10
19:40:17 Source Code scm commit: Refinement (commit 73269a8)
17:10:06 Source Code scm commit: Refinement (commit cac6f91)
15:36:15 Source Code scm commit: porting why3session to session_itp in progress (commit 9482982)
15:05:04 Source Code scm commit: Merge branch 'itp' into itp_new_why3session (commit 6b88767)
15:04:53 Source Code scm commit: use shared get_session_dir also in why3replay (commit 0fc3a92)
14:57:02 Source Code scm commit: Merge branch 'itp' into itp_new_why3session (commit cbad94c)
14:49:40 Source Code scm commit: factorize the interpretation of files on command line, and the creation of controllers (commit 7dda1c7)
12:49:22 Source Code scm commit: create_controller now immediately load the drivers for provers (commit 9b6e2bd)
12:40:19 Source Code scm commit: moved config from server_data to controller (commit 66e0b6e)
12:28:12 Source Code scm commit: upgrade why3session to session_itp format, first step (commit 07533ce)
11:33:06 Source Code scm commit: inplace comments. (commit 435f5b2)
09:02:27 Source Code scm commit: Generate cntexmp according to config file. (commit ccbc7d8)
08:56:21 Source Code scm commit: Merge branch 'master' into itp (commit b7cfc96)
08:41:05 Source Code scm commit: Restore display of actual command line when Call_provers.debug is on (commit 0db24f4)
07:40:19 Source Code scm commit: improve axiom big_float_is_int (commit dbe2858)
07:34:53 Source Code scm commit: [Gappa] Add the constraint that int are integers (commit 432388b)
2017-05-09
13:01:46 Source Code scm commit: Scroll to goal in source if source tab is focused. (commit 0e32c28)
09:45:17 Source Code scm commit: Avoid double selection when switching goal after proof state update. (commit 0555287)
2017-05-07
12:44:06 Source Code scm commit: Pdecl: split type declarations in chunks (commit b6e2a7b)
2017-05-06
13:24:06 Source Code scm commit: range/float types: cosmetic (commit 562e6ef)
11:57:53 Source Code scm commit: examples: update two sessions (commit 7a2aa5b)
2017-05-05
15:40:14 Source Code scm commit: Int63: min_int et max_int (commit 670713d)
15:07:41 Source Code scm commit: ITP: better semantics of clean (commit c7afa20)
14:59:30 Source Code scm commit: session (commit 1f5f5f7)
14:52:26 Source Code scm commit: extraction: removed dead code (commit 61508f6)
14:40:45 Source Code scm commit: ITP: enforce preservation of proof statuses with more robust code (commit e2f51d1)
14:25:10 Source Code scm commit: more session-fixing (commit 4aa1280)
14:10:31 Source Code scm commit: Remove cannot remove subtree containing running or scheduled proof_attempt. (commit 0f0dc89)
13:29:11 Source Code scm commit: Fix session (commit 668a20f)
13:17:05 Source Code scm commit: Experimental detection of clicks on goal_view. To be reverted. (commit 15a7e5b)
13:07:42 Source Code scm commit: Return null when json list is empty (commit c174376)
11:43:23 Source Code scm commit: Fixed koda_ruskey proof (commit 3d0c6a3)
11:14:29 Source Code scm commit: wip fix session (commit c08b0e5)
10:34:17 Source Code scm commit: OCaml printer: local identifiers under modular option (commit 031bddc)
09:28:00 Source Code scm commit: fixed refinement of record types (ghost fields) (commit 45f7124)
09:24:18 Source Code scm commit: fixed refinement of writes (commit a5152b0)
09:23:21 Source Code scm commit: avoid bomb in case of uninstalled prover (commit 96faa1b)
2017-05-04
15:56:07 Source Code scm commit: Merge branch 'master' into itp. Main change is the type of json value which I changed in master and did not follow in ITP. Now record are not sent as List. They are maps as in master. This is quite a big change as json_util completely changes. (commit 72a2b3e)
14:10:08 Source Code scm commit: module mach.int.Random63: less spec and OCaml driver (commit ee1f3fc)
13:46:33 Source Code scm commit: add more plots (commit dac7e02)
13:31:11 Source Code scm commit: Clean up printer and tests (commit f0a3cf9)
13:08:18 Source Code scm commit: OCaml printer: fixed some parentheses in patterns (commit 3a34dce)
13:06:52 Source Code scm commit: Driver for randomize operations (commit 7ba519d)
12:07:33 Source Code scm commit: Clean does not remove running proof attempt. (commit 376cf77)
10:53:35 Source Code scm commit: minor reformating (commit fffc8da)
10:52:28 Source Code scm commit: Mark obsolete now update proof state correctly. (commit 184be63)
08:18:18 Source Code scm commit: New modules mach.int.{Random63, State63} and mach.array.{Array63Exchange,Array63Swap} (commit 932f189)
2017-05-03
13:20:14 Source Code scm commit: IDE GTK: allow multiselection, but not yet supported for remove and mark obsolete (commit ced6feb)
12:27:53 Source Code scm commit: IDE GTK: reorganize menu items (commit 8d03d18)
09:38:53 Source Code scm commit: IDE GTK: reorganize menus, add tooltips, adapt key shortcuts (commit 44916eb)
09:16:38 Source Code scm commit: fix issues for running examples/regtests with new replayer (commit 83c8aee)
09:02:30 Source Code scm commit: Extend mark obsolete to all possible nodes. (commit 1456ecb)
09:00:37 Source Code scm commit: Compilation and make bench work on moloch (commit 9e43e39)
07:53:05 Source Code scm commit: renamed temporary why3newreplay into why3replay (commit 57de2a1)
07:27:30 Source Code scm commit: longer benchmarks (commit c1967cf)
07:27:21 Source Code scm commit: create_type_decl does not return metas anymore (commit 7c454a3)
2017-05-02
20:52:20 Source Code scm commit: Vc: minor fix (commit d094a83)
15:46:23 Source Code scm commit: Tried to include result of lexer in error message. It looks like it could be of use ? (commit ec0fd69)
12:19:08 Source Code scm commit: Vc: check invariants for local let lemmas/functions (commit 8d88c45)
11:21:13 Source Code scm commit: Typeinv: fix a forgotten case (commit b0f1f67)
11:01:32 Source Code scm commit: Vc: check invariants in loops (commit 622cf89)
2017-05-01
20:54:52 Source Code scm commit: Vc: slightly better postconditions at the call site (commit 921d4c7)
20:25:14 Source Code scm commit: Vc: check invariants for assertions (commit 3bb185b)
19:41:00 Source Code scm commit: Vc: check invariants for function calls (commit 6472ba8)
19:04:30 Source Code scm commit: Ity: two fixes in the definition of its_fragile (commit d8f8d56)
19:03:37 Source Code scm commit: Parser: admit braced types in returns (commit 6929ab3)
13:05:00 Source Code scm commit: Vc: check invariants in function definitions (commit f02f041)
2017-04-28
15:06:01 Source Code scm commit: newreplayer: set the proper number of running tasks (commit 968375d)
2016-08-26
13:45:27 Source Code scm commit: Jessie3: array mutation (commit 12fc9ca)