Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Activity

Activity:
Start Date:
End Date:
Time Activity By
2017-04-24
12:58:17 Source Code scm commit: Connecting delete event to exit_function callback. Allow catching clicks on cross button. (commit c0a9864)
12:46:00 Source Code scm commit: python.mlw: update for new_system (commit 98f55b0)
12:27:50 Source Code scm commit: Nothing was odne on reload. corrected. (commit 2f5ad68)
12:15:05 Source Code scm commit: Some error handling. (commit 0bd1fde)
11:57:19 Source Code scm commit: prevent warning non_conservative_extension when cloning (commit 2295177)
10:53:49 Source Code scm commit: Reorganize/further comment why3ide.ml (commit b65df52)
09:50:21 Source Code scm commit: Extraction: printing drivers preludes for flat option (commit fca92f0)
2017-04-23
21:32:59 Source Code scm commit: new example: 2D-version of Kadane algorithm (commit 3b1d439)
21:32:29 Source Code scm commit: fixed OCaml driver for matrices (commit 127dc53)
15:54:22 Source Code scm commit: [wip] extraction (commit d575192)
10:13:17 Source Code scm commit: Missing update for range and float types (commit 8b6183f)
10:08:54 Source Code scm commit: Merge branch 'new_system_master' into new_system (commit a05c402)
10:08:25 Source Code scm commit: merge for float types (commit 845f996)
09:52:21 Source Code scm commit: merge OK up to float types (commit 789247e)
2017-04-22
16:19:16 Source Code scm commit: Adding Mark_obsolete request. Added constructor Obsolete to update_info. (commit b7a803e)
15:24:22 Source Code scm commit: number.Parity: fixed an inconsistent lemma (commit bd53bce)
14:32:20 Source Code scm commit: Adding clean_req. Need testing. (commit f87661d)
2017-04-21
22:55:06 Source Code scm commit: GTK: on reload, ask to save sources. (commit 0d7de10)
14:04:19 Source Code scm commit: ITP: fixed dependencies (commit af024de)
13:44:55 Source Code scm commit: ITP server: commands can now call a function of the controller (commit d1bbf7c)
12:48:31 Source Code scm commit: update session (commit ad39ce9)
12:32:14 Source Code scm commit: Behavior when exception is called and stack_trace is ON has changed. Now print the backtrace and exit. Formerly, the exception was caught by GTK. (commit 56ac198)
11:09:30 Source Code scm commit: solve issue with type range declarations (commit 5d5869d)
10:28:56 Source Code scm commit: Fixed replay. (commit 23cfc26)
2017-04-20
17:24:24 Source Code scm commit: Refinement (wip) (commit 2c2c463)
16:14:03 Source Code scm commit: eval_match: track (commit 52a56bb)
14:35:12 Source Code scm commit: eval_match: cap_equality (commit 640b8ca)
14:03:33 Source Code scm commit: implementation for Array.self_blit (commit f62002a)
13:02:40 Source Code scm commit: Extraction: compatible code with OCaml versions previous to 4.03 (commit e0d4d60)
12:47:43 Source Code scm commit: whitespace (commit e48154d)
09:05:33 Source Code scm commit: binary sort: simplified code (and proof) using self_blit (commit 790d613)
08:34:47 Source Code scm commit: new examples: tree_of_array and binary_sort (commit 98cf448)
07:20:48 Source Code scm commit: Update Makefile. (commit 041e3bd)
2017-04-19
16:26:00 Source Code scm commit: Patching problems in Makefile.in . Still do not work properly. Refuses to fail. (commit 1fe220b)
14:57:16 Source Code scm commit: trywhy3: fixed Makefile for opam-installed ocplib-simplex (commit 7d8d2ba)
14:00:11 Source Code scm commit: New lemma of_list_snoc in theory seq.OfList (commit 23464bd)
13:26:40 Source Code scm commit: Switch to alias behavior for pointer incr (commit 95997a4)
13:17:06 Source Code scm commit: Removed modifications in grammar. (commit 0968eb4)
12:30:47 Source Code scm commit: Merge branch 'mp' into alias (commit 5940d74)
11:33:35 Source Code scm commit: VC server: adding a request to interrupt processes, in progress (commit 28cd735)
11:21:33 Source Code scm commit: renaming (commit 76ada34)
11:11:21 Source Code scm commit: Added the modifiable label in source_view_table and a ref to a boolean which holds the changed state of the source file. To be improved. (commit 964d077)
09:06:04 Trackers Tracker Item [#21300] crash when compiled with flambda Closed Nobody
08:11:13 Source Code scm commit: Moving .merlin file for webserver (commit 4a274c4)
08:10:08 Source Code scm commit: Added message before exitting the ide. (commit 029ffcd)
07:48:56 Source Code scm commit: OCaml 64 driver and printer (minor) (commit f4eb960)
2017-04-18
10:08:07 Source Code scm commit: Proof of concept. Errors ala menhir last version. Example of use on isqrt.mlw. Makefile to be improved. Not yet errors with references to what was computed. (commit 6d8deb7)
09:56:48 Source Code scm commit: Remove now actualize the controller so that it update proved theory/goal.. (commit b3eb543)
2017-04-17
18:08:55 Source Code scm commit: New lemmas ToList.to_list_def_cons and OfList.convolution_to_of_list (commit 5cb42a7)
2017-04-14
15:45:25 Source Code scm commit: Merge branch 'master' into new_system (commit 4822694)
15:21:46 Source Code scm commit: ITP: simple attempt to implement 'interrupt'. IMPORTANT ISSUE: running processes are not killed (commit a892b84)
14:28:47 Source Code scm commit: GTK: Preferences menu, only max task is active so far (commit cce76eb)
13:55:27 Source Code scm commit: Reload now updates the proof_state (if a node is proved or not). (commit 96f16e0)
11:57:53 Source Code scm commit: Reload does not lose session in case of syntax or typing error (commit 0d1f1b9)
11:04:24 Source Code scm commit: Can reload after parse error. (commit 792ac41)
08:59:02 Source Code scm commit: ide gtk: putting back the icons for each row (commit 56e6345)
2017-04-13
15:11:31 Source Code scm commit: Merge branch 'bugfix/v0.87' (commit 7129b25)
15:09:27 Source Code scm commit: Fix release date. (commit a2ff2a1)
2017-04-12
14:41:47 Source Code scm commit: fixed dates and authors (commit 9c4fec8)
14:29:04 Source Code scm commit: Help menu in GTK IDE (commit 5d99335)
14:13:12 Source Code scm commit: Improved display of tasks and transformations (commit 81ec757)
12:27:51 Source Code scm commit: Adding new cntexmps from spark/why3. (commit 084a410)
12:19:25 Source Code scm commit: Merge branch 'master' into itp (commit 84f3751)
12:17:56 Source Code scm commit: update header for year 2017 (commit 216f2ec)
12:10:30 Source Code scm commit: Remove new warning 60 generated by OCaml 4.04 (commit 754e578)
11:38:24 Source Code scm commit: Various improvements in IDEs (commit d0d5849)
06:59:47 Source Code scm commit: Merge branch 'master' into itp (commit d0e1f7b)
06:14:37 Source Code scm commit: doc: update descr of range and float types (commit c7703c3)
2017-04-11
19:54:56 Source Code scm commit: Add a save file notification and edit of source in gtk. (commit e4b1478)
14:36:42 Source Code scm commit: updated Coq realizations (commit e1bd182)
14:18:46 Source Code scm commit: Coq realizations: allow correct update-coq without warnings (commit 36d9477)
14:09:29 Source Code scm commit: Some 80 chars rules modif. (commit dd20690)
13:56:27 Source Code scm commit: Dropped Coq realization of bv/BV_Gen for Coq 8.4 (commit f57a7f1)
13:36:07 Source Code scm commit: Cleaning. (commit 10dd3f7)
13:19:26 Source Code scm commit: Add potentially several files in a tab with the task in top right corner. (commit c4fea41)
12:15:12 Source Code scm commit: Prettier Makefile rules, suppressed a few warnings (commit 011a032)
09:37:26 Source Code scm commit: Updated session of generalogy example (Isabelle proofs) (commit ff1f7ca)
2017-04-10
16:05:54 Source Code scm commit: Added support for generic number literals to Isabelle printer (commit 19b0f79)
10:09:30 Trackers Tracker Item [#21300] crash when compiled with flambda Opened Piotr Trojanek
2017-04-06
15:52:23 Source Code scm commit: Request to locate next unproven node. (commit f534f8d)
2017-04-05
15:00:17 Source Code scm commit: Cleanup some useless parentheses (commit d901b69)
14:58:40 Source Code scm commit: extraction: no need for type ocaml.Ocaml.integer (commit a7c1eea)
14:44:52 Source Code scm commit: Parsing error dont go through Error where they are catched by a debug flag. They are always printed with new message Parse_Or_Type_Error. File_contents and Get_file added where missing. Indentation updated in json_util (commit c7e7758)
13:58:07 Source Code scm commit: OCaml extraction: more tests (commit 2ce68bb)
13:54:27 Source Code scm commit: ITP: attempt to move the selected goal less often (commit 8d00912)
13:37:02 Source Code scm commit: OCaml extraction: optional and named arguments (commit f73ce28)
12:58:06 Source Code scm commit: Code extraction: (commit 40f309b)
12:47:31 Source Code scm commit: Test unproven_goal_around (commit d045b52)
12:24:21 Source Code scm commit: merged with master (commit 28e5aba)
12:22:24 Source Code scm commit: Remove a few compilation warnings (commit 929db30)
12:12:00 Source Code scm commit: ITP: better error messages (commit 46973e4)
12:11:00 Source Code scm commit: use Alt-Ergo 1.30 instead of 1.01 in auto strategies (commit 8bf94dc)
12:11:00 Source Code scm commit: use Alt-Ergo 1.30 instead of 1.01 in auto strategies (commit d649e38)
11:36:18 Source Code scm commit: Temporary and incomplete (unsound) version of subst. (commit 129a918)
09:41:07 Source Code scm commit: server: interprets cmdline correctement in the basic case one file in arg (commit 1dc02a8)
07:37:07 Source Code scm commit: Q301-016 fix previous commit (commit fdecb74)
07:22:23 Source Code scm commit: IEEE float in stdlibdoc + a bit of cleaning (commit e532edf)
07:10:40 Source Code scm commit: modified Makefile (commit c2cd0ce)
07:08:28 Source Code scm commit: Q301-016 update why3 maps to ocaml 4.04 maps (commit 410d4b4)
06:24:05 Source Code scm commit: support for colibri, and Z3 without removal of quantified hypothesis (commit 127dd2b)
2017-04-04
17:41:14 Source Code scm commit: Code extraction: (commit 4b1751e)
15:06:09 Source Code scm commit: list.FoldRight: added a lemma (commit 5d3710f)
13:58:12 Source Code scm commit: new lemmas in map.Occ (commit e2c7115)
13:57:42 Source Code scm commit: new module mach.array.Array63Permut (commit ffbe979)
12:11:01 Source Code scm commit: Refinement (wip) (commit 1a4e2ee)
11:57:22 Source Code scm commit: clear_but. (commit 5e6bcd8)
10:25:20 Source Code scm commit: Left and right transformation. (commit b044db6)
09:57:37 Source Code scm commit: Assert. Destruct_alg that works on polymorphic types. (commit 40e1b18)
09:28:52 Source Code scm commit: extraction: driver for Int63.zero,one (commit 4aa58d7)
08:11:27 Source Code scm commit: Unfold patched. (commit 31410c2)
2017-04-03
16:10:32 Source Code scm commit: Changed merge_trans so that if it does not manage to apply transformation, it does not fail. (commit 1caa8a1)
16:06:40 Source Code scm commit: List in driver. (commit d23d9e7)
16:03:37 Source Code scm commit: added a TODO in extraction (commit f456816)
14:27:00 Source Code scm commit: OCaml extraction: driver for mach.peano.Peano (commit 5c944da)
14:05:26 Source Code scm commit: extraction: fixed OCaml driver for List.length (commit c75a21c)
13:50:51 Source Code scm commit: Fix add_alias; example now works as intended (commit f5c2a48)
13:45:06 Source Code scm commit: Added tactic unfold for logic symbol. Experimental (commit 390f2ac)
13:44:23 Source Code scm commit: record types refinement (wip) (commit acc34fa)
12:13:58 Source Code scm commit: Functions manipulating files now return a boolean avoiding further actions when they fail. Parsing and typing errors are now printed inside the ide. (commit 4d592a0)
11:59:06 Source Code scm commit: Code extraction: better printing of record creation. Theory seq.OfList: refactoring (commit df5d307)
09:28:29 Source Code scm commit: Printing tuple type. (commit c4a5e29)
09:25:59 Source Code scm commit: Printing tuples. (commit 40fcdf4)
2017-04-01
14:46:14 Source Code scm commit: Record types refinement (wip) (commit d548d51)
12:47:54 Source Code scm commit: updated drivers with eliminate_literal (commit c1a666b)
2017-03-31
16:48:11 Source Code scm commit: Removed coq from Dijkstra. (commit 5251bfb)
16:47:46 Source Code scm commit: Added intros n which introduce n times. (commit 803606f)
09:12:56 Source Code scm commit: Record types refinement (wip) (commit 1e8147c)
06:24:26 Source Code scm commit: module ocaml.OCaml: added Int63 and Array63 (commit 19af86f)
06:21:36 Source Code scm commit: extraction: cosmetic changes (commit 203322f)
06:19:49 Source Code scm commit: added Int63.zero,one (commit 1ecfbcc)
05:26:22 Source Code scm commit: missing file (commit fe2dcfe)
2017-03-30
15:11:24 Source Code scm commit: doc proof reading (commit bf1abbb)
14:43:54 Source Code scm commit: new function Extset.print (commit 4421df3)
14:37:54 Source Code scm commit: Code extraction (commit 4ead469)
11:53:21 Source Code scm commit: trying to use the new floats theory for real (commit 4aa3615)
10:21:24 Source Code scm commit: Reload now resend node changed after new_node. (commit 31c951c)
09:29:23 Source Code scm commit: Update doc with range types and float types, first go. (commit f6862c0)
08:22:30 Source Code scm commit: more simple tests on alias clause (commit b5b106f)
2017-03-29
15:02:46 Source Code scm commit: Fix unbound result (commit db03d32)
14:05:55 Source Code scm commit: Example in progress (commit c0b9842)
12:54:23 Source Code scm commit: Code extraction: (commit 7b21845)
11:50:11 Source Code scm commit: Converted examples from C to why3 (commit c579bbb)
11:49:56 Source Code scm commit: Updated itp driver for real and float. (commit 9ccc3cd)
09:10:51 Source Code scm commit: Merge branch 'master' into itp (commit bcd08e1)
08:56:09 Source Code scm commit: new example in progress: approximation of exponential (commit 118e150)
08:13:30 Source Code scm commit: Improve addition (commit 2cb4740)
2017-03-28
16:08:18 Source Code scm commit: WIP add alias keyword (commit c4a8d09)
15:27:36 Source Code scm commit: Q217-025 Allow parsing for reference in counterexamples (commit f9e2170)
2017-03-27
15:56:28 Source Code scm commit: Q327-007 Change printer specific to cvc4 ce (commit ac4f632)
13:18:42 Source Code scm commit: Code extraction (commit bdec33a)
2017-03-20
08:41:16 Source Code scm commit: Q316-004 Remove get-info (commit 9ef97db)
2017-03-16
14:21:05 Source Code scm commit: Q316-004 Parse cvc4 output on mac (commit 4e94e8d)
2017-03-15
08:30:24 Source Code scm commit: Q217-025 Use get-model instead of get-values for CE (commit 1f6da25)
2017-03-14
14:31:00 Source Code scm commit: Q217-025 minor typo (commit cffa317)
09:42:50 Source Code scm commit: example of multiple assignment (commit 85bb06e)
2017-03-09
21:51:53 Source Code scm commit: Q217-025 Printer to smt2: convert bool term inside type to bv (commit a303ae7)
2017-03-01
01:55:50 Source Code scm commit: P802-016 fix pop-ups for prover crashes (commit c77024b)
2017-01-04
10:43:57 Source Code scm commit: PB23-035 enrich information in .spark files (commit a4bf8bd)