Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Activity

Activity:
Start Date:
End Date:
Time Activity By
2017-09-22
13:30:07 Source Code scm commit: remove the naming table in argument of printers: not used anymore (commit 48aa727)
12:27:54 Source Code scm commit: update session (commit da7e211)
11:55:23 Source Code scm commit: apply_trans_to_goal should try introduced taks when does not progress on raw task (commit bded975)
10:58:30 Source Code scm commit: Merge branch 'master' into itp (commit 3a9cf11)
07:21:26 Source Code scm commit: OCaml printer: minor (commit 8d8c999)
2017-09-21
21:00:40 Source Code scm commit: Schorr-Waite: because of writting effects the four memory components must remain non-ghost (commit ebf69ea)
14:26:53 Source Code scm commit: right click does not grab the focus: Allows to select multiple nodes (commit 606a11a)
13:48:38 Source Code scm commit: extraction: fixed printing of arrow types (commit 59d53e9)
13:22:56 Source Code scm commit: cosmetic (commit 6c2310d)
13:02:02 Source Code scm commit: cosmetic: avoid trailing comma in prover parseable format (commit 0986133)
12:52:07 Source Code scm commit: library: simplified module Random (commit 1ccfd59)
12:45:00 Source Code scm commit: adding strategy auto 0, same as level 1 but without split (commit bd97eac)
12:40:41 Source Code scm commit: indicates shortcuts in tooltips (commit f4f179c)
12:20:16 Source Code scm commit: finally restored all former key shortcuts, except 'p' that should be replaced by '0' (commit e228149)
12:11:16 Source Code scm commit: Ctrl-C shortcut for collapse proven goals does not hide Ctrl-C in editor (commit 4048e78)
11:58:45 Source Code scm commit: add one-key shortcuts for strategies (commit 342c682)
11:34:30 Source Code scm commit: put menu "save files" into "files" menu, and add shortcut (commit 69d8d13)
09:23:38 Source Code scm commit: protect not only 'clean' but also 'remove' from removing running proof attempts (commit 5f70822)
09:17:00 Source Code scm commit: add info of running proof attempts in controller. (commit 6e10e3f)
08:47:49 Source Code scm commit: adding new case Undone for pa status. But it does not solve the pb: (commit 5a87990)
2017-09-20
14:51:07 Source Code scm commit: Proverstarted is now sent in ITP mode (it should not be in script mode). (commit 7854f1a)
12:12:32 Source Code scm commit: bug fix: use the proper table for parsing arguments of transformations (commit 4a86dba)
09:44:37 Source Code scm commit: command associated to a prover is its parseable name and not its shortcut (commit 7c80798)
09:37:21 Source Code scm commit: update sessions with old provers (commit ec95601)
2017-09-19
19:23:24 Source Code scm commit: Proof of path_shortest_path (commit 20522d1)
15:18:31 Source Code scm commit: Case for parsing detached. (commit ab33efb)
14:57:01 Source Code scm commit: vstte12_ring_buffer finally proved without bisect but with a cut (commit 8f14f60)
14:46:13 Source Code scm commit: update session on moloch (commit 90ee6ff)
14:41:04 Source Code scm commit: Comments. (commit 106fa46)
14:31:13 Source Code scm commit: Schorr-Waite: the four [val]'s representing a memory component are now ghost (commit 3fc6c7b)
14:29:37 Source Code scm commit: OCaml printer: fixed bug related to [let .. in] scope (commit 9850123)
14:04:08 Source Code scm commit: bisection now works at least for counting_sort (commit 219b805)
09:25:39 Source Code scm commit: make all provers visible both in tools menu and in completion (commit 4b94d0d)
08:06:56 Source Code scm commit: replaced Edit_req request with Edit command. (commit ec5ae5c)
2017-09-18
14:16:50 Source Code scm commit: removed useless case Transform_req (commit b22d53e)
14:11:16 Source Code scm commit: removed useless case Strategy_req (commit d3fd6f3)
13:38:38 Source Code scm commit: bisect continued (commit 029acee)
10:56:51 Source Code scm commit: Do not report counterexamples containing errors. (commit b33da14)
08:43:42 Source Code scm commit: update session (commit edf6a6f)
2017-09-15
14:46:45 Source Code scm commit: Change steps used when replaying a proof (add one step). (commit 18e1c2c)
13:18:37 Source Code scm commit: Remove deprecated comments. (commit 25fa146)
11:13:49 Source Code scm commit: proposition de nouvelle fonction exportée dans controller_itp (commit 013f58b)
2017-09-14
15:11:06 Source Code scm commit: Extraction: new label [ocaml:remove] (commit 4e0de3e)
12:50:30 Source Code scm commit: Useless cases in scheduling (commit 7f939be)
2017-09-13
15:32:39 Source Code scm commit: proof scripts: text of goal must be modified when input source changes (commit 189b726)
15:24:14 Source Code scm commit: blocking is a new parameter of module type scheduler. (commit 7089acc)
14:42:47 Source Code scm commit: menage: plus de UnEdited et JustEdited (commit e8e4bf5)
14:42:06 Source Code scm commit: Using new forward_result to get new results from why3server. (commit d1c876e)
13:43:24 Source Code scm commit: second time edition indeed works now (commit d894799)
13:31:03 Source Code scm commit: editing and replaying proofs with interactive provers, works better (commit 1eb02c1)
12:15:52 Source Code scm commit: fix several pbs with interactive provers replay and proof scripts edition (commit ffb325b)
07:19:20 Source Code scm commit: update session with polypaver (commit afab61c)
07:05:25 Source Code scm commit: Improving support for detached theories and goals (commit 42502a3)
2017-09-12
14:22:53 Source Code scm commit: avoid silent failures in presence of detached theories (commit ff18a1f)
13:38:44 Source Code scm commit: Adapt to Coq 8.7. (commit 7d82e6a)
13:24:43 Source Code scm commit: Extraction: error location for failed extraction of [val] declarations (commit cda5ad7)
12:41:05 Source Code scm commit: When focus is not yet defined, notify still sends notification that are not node-specific. (commit 3b637fb)
12:18:05 Source Code scm commit: Allow focusing on several nodes at once. (commit 25d4536)
2017-09-11
13:40:13 Source Code scm commit: Extraction test: commented [val] declaration that was never used. (commit 8bbd91c)
13:39:23 Source Code scm commit: Extraction: test if a [val] declaration is assigned in the driver (commit 8318903)
13:38:16 Source Code scm commit: Schorr Waite: two functions marked ghost as they are only used in ghost code (commit bb13766)
09:23:03 Source Code scm commit: Port examples/f_puzzle. (commit 8495e91)
08:44:25 Source Code scm commit: Extraction (commit 81842fd)
2017-09-08
16:21:47 Source Code scm commit: ebauche de bisect (commit f0ebb81)
12:46:35 Source Code scm commit: why3replay displays progress, unless -q is set (commit 8ab1a7e)
12:23:03 Source Code scm commit: update proofs that where made with bisect before that now work easily (commit b54f57c)
11:32:40 Source Code scm commit: adapted limits should not be stored in session (commit 65eea47)
2017-09-07
15:45:07 Source Code scm commit: Removed task_driver. Currently, Pretty is used to print tasks. (commit b326c9d)
15:23:00 Source Code scm commit: Changing adatp_limits so that we keep the steps limit even in failing cases. (commit c4e3110)
10:07:00 Source Code scm commit: do not adapt_limits when use_steps (commit 7966f2c)
2017-09-06
14:41:26 Source Code scm commit: add strategies in tools menu and in commands (commit 4e26f72)
14:14:20 Source Code scm commit: cleaning (commit e66b0a9)
13:30:55 Source Code scm commit: upgrade provers during replay (partial) (commit bf928f1)
13:28:40 Source Code scm commit: update session (commit 302b089)
12:19:39 Source Code scm commit: update session (commit 5a1f529)
11:45:57 Source Code scm commit: Adding the multiplier we use for the number of tasks we send to why3server as a parameter of Scheduler. Cannot be done via set_max_tasks (because this number is sent to why3server and it fails when it is arbitrarily high). (commit 1b6db43)
11:18:45 Source Code scm commit: improve display of running and scheduled statuses (commit 7337228)
11:07:34 Source Code scm commit: fixed memory access bug in why3server (commit 963190d)
09:14:51 Source Code scm commit: update sessions (commit e676e4a)
08:41:33 Source Code scm commit: call callbacks in right order in schedule_proof_attempt (commit fa85d77)
07:54:36 Source Code scm commit: more debug info for replay (commit 2b0dd66)
2017-09-05
08:28:34 Source Code scm commit: For now, do not extract anything related with sequences (commit 429ea0b)
2017-09-04
07:42:28 Source Code scm commit: Small typo (commit 252a522)
07:29:20 Source Code scm commit: Extraction: some more smart constructors (commit d97e766)
2017-09-02
05:27:47 Source Code scm commit: Fix bench. (commit f3d9d8e)
2017-09-01
17:10:50 Source Code scm commit: Remove some pointless proofs. (commit f580a3c)
17:05:36 Source Code scm commit: Remove some obsolete Coq proofs. (commit ff24f5f)
16:53:23 Source Code scm commit: Remose some obsolete Coq proofs. (commit a734c3c)
16:45:44 Source Code scm commit: Remove some obsolete Coq proofs. (commit cfbcceb)
16:37:33 Source Code scm commit: Remove some obsolete Coq proofs. (commit 148c841)
16:04:02 Source Code scm commit: Port knuth_prime_numbers. (commit 8a7eccf)
13:41:55 Source Code scm commit: attempt to fix replay mistake (not sure) (commit 6f2bb17)
13:12:53 Source Code scm commit: restore the adapt_limits and fuzzy_result effects of old sessions (commit 8a3558d)
13:11:54 Source Code scm commit: document new exported function (commit 04acb47)
11:55:40 Source Code scm commit: restore automatic 'intro' if transformation arguments need it (commit 4ae4d63)
11:04:33 Source Code scm commit: do not introduce by default before calling transformation (commit adbcea8)
07:46:01 Source Code scm commit: replay does not block anymore if nothing to replay (commit 98cf7f0)
2017-08-30
16:07:34 Source Code scm commit: McCarthy's 91 function: machine integers implementation. No extra annotations needed in order to prove overflow absence. (commit 075c378)
15:21:20 Source Code scm commit: Fixed bad interaction between collapsing and getting next goal. (commit c7069da)
13:01:55 Source Code scm commit: Merge branch 'master' into itp (commit 26eed36)
12:37:52 Source Code scm commit: send the raw task to provers, instead of the one with intros (commit 3981601)
12:37:19 Source Code scm commit: setup a nightly bench for ITP branch (commit b6e10ef)
12:33:15 Source Code scm commit: strategies can now be executed on transformation node (commit 478ba9f)
12:12:25 Source Code scm commit: remove prompt for why3replay scheduler (commit 6cb5a89)
11:32:11 Source Code scm commit: ITP print task affiche le nom du but, necessaire pour 'replace' par ex (commit 22bda52)
09:13:54 Source Code scm commit: attempt to add command "remove_node" (commit 3401d83)
09:13:32 Source Code scm commit: do_intros is not an argument of get_task anymore (commit 83e4345)
2017-08-29
13:06:53 Source Code scm commit: Force do_intros to false when during label detection (commit cee208d)
12:58:54 Source Code scm commit: suppress GTK warning (commit f1f17ac)
12:49:31 Source Code scm commit: improved use of boxes in Pretty printing terms (commit dd81e64)
12:14:05 Source Code scm commit: Fixed induction. (commit d289873)
11:53:16 Source Code scm commit: bug fix: file name in session was not relative to session file anymore (commit 323473a)
09:19:22 Source Code scm commit: IDE: add a submenu for transformations in the tools menu (commit 501d326)
07:36:31 Source Code scm commit: task is not anymore a field of proof nodes, but in a hashtable of the session (commit 392a4d2)
07:07:54 Source Code scm commit: reload_files now returns a pair of booleans giving info (commit 9fcc1a8)
2017-08-28
12:49:02 Source Code scm commit: implicit intros in display and anywhere in controller (commit 7f2a8aa)
2017-08-25
17:17:13 Source Code scm commit: Extraction of [if-then-else] and [match-with] expressions (commit 88c5725)
13:15:45 Source Code scm commit: Fix printing of negative constants for Yices. (commit b950772)
13:00:58 Source Code scm commit: Set logic to QF_AUFLIRA for Yices-smt2, as it will not even start parsing the input file otherwise. (commit 03147ef)
09:36:41 Source Code scm commit: Port examples/tortoise_and_hare. (commit 889e6779)
09:13:03 Source Code scm commit: Restore some Coq proofs. (commit 75a6094)
09:11:42 Source Code scm commit: update oracles for counterxamples (commit 0b4466b)
09:02:39 Source Code scm commit: Avoid crashing in Libencoding.ls_of_const when producing MetiTarski files. (commit e195352)
08:52:48 Source Code scm commit: fix driver for cvc4 1.5 (commit 9b8b5f1)
08:27:39 Source Code scm commit: do not use normalize_filename (commit 5f2e43a)
08:06:53 Source Code scm commit: deprecate Sysutil.normalize_filename (commit 6fd72ee)
07:59:44 Source Code scm commit: use clicked instead of pressed (commit 31493c6)
2017-08-24
15:59:05 Source Code scm commit: Port examples/vstte10_search_list. (commit 7caea7e)
15:17:09 Source Code scm commit: repair examples/vacid_0_sparse_array (commit 13c8306)
15:03:23 Source Code scm commit: Port examples/vstte10_inverting. (commit 97c8be2)
14:48:59 Source Code scm commit: Restore a Coq proof. (commit fc6117c)
14:47:18 Source Code scm commit: examples/resizable_array (commit 388aa4f)
14:43:38 Source Code scm commit: examples/find (commit b7bd44c)
14:35:27 Source Code scm commit: Restore a Coq proof. (commit 20945b7)
14:11:40 Source Code scm commit: Restore some Coq proofs. (commit cb98dfe)
13:38:00 Source Code scm commit: update examples/bag (commit b555f88)
13:37:34 Source Code scm commit: Typeinv: autosplit multiclause type invariants (commit 6f35272)
13:19:31 Source Code scm commit: update sessions to Coq 8.6.1 (commit c7bd339)
13:18:24 Source Code scm commit: Add a Makefile rule to detect obsolete edited proofs in examples. (commit 9ebc51a)
13:18:24 Source Code scm commit: Add a Makefile rule to detect obsolete edited proofs in examples. (commit 2cbe23b)
13:16:23 Source Code scm commit: examples/bag.mlw (commit 1d9cf68)
13:15:58 Source Code scm commit: Remove some obsolete edited proofs. (commit 50216de)
09:39:41 Source Code scm commit: update Coq proofs to 8.6.1 (commit 42d446f)
09:26:45 Source Code scm commit: Remove some obsolete edited proofs. (commit f8bdc74)
09:03:17 Source Code scm commit: Remove some obsolete edited proofs. (commit 9112c36)
08:16:10 Source Code scm commit: support for Coq 8.6.1 (commit 78502c2)
05:18:16 Source Code scm commit: CE bench: upgrade to new Why3 syntax (commit 9c4127a)