Home My Page Projects Why3
Summary Activity Tracker Lists SCM Files

Activity

Activity:
Start Date:
End Date:
Time Activity By
2017-03-27
13:18:42 Source Code scm commit: Code extraction (commit bdec33a)
2017-03-24
16:05:06 Source Code scm commit: HTML style: better proportion at startup (commit 8a90c2c)
10:27:35 Source Code scm commit: Cleanup (commit f6974ad)
10:24:54 Source Code scm commit: Fix session (commit 6bab7cb)
2017-03-23
16:03:42 Source Code scm commit: Add addition benchmark (commit c991b3d)
15:14:41 Source Code scm commit: Code extraction (printer); Fold_left for lists and sequences (wip) (commit 5a6d04b)
15:09:19 Source Code scm commit: koda_ruskey: updated Coq proofs for Coq 8.6 (commit 079015c)
14:07:32 Source Code scm commit: extraction: preparing code for extraction of OCaml functors (commit 67f0aa2)
11:10:34 Source Code scm commit: Removing root node (commit b6f3308)
10:16:11 Source Code scm commit: Solved error from merge (commit ab100c4)
10:10:22 Source Code scm commit: merging branch itp (commit 12393a3)
10:09:30 Source Code scm commit: extraction: fixed extraction of scopes (commit a3a2262)
09:37:57 Source Code scm commit: Adding error message. (commit e3ed9e3)
08:19:01 Source Code scm commit: Remove executable file. (commit 2267151)
2017-03-22
16:11:02 Source Code scm commit: Add tentative optimisation, fix graphs, beautify extraction (commit 6caec05)
10:20:51 Source Code scm commit: Cleanup C library (commit 6334796)
2017-03-21
16:32:42 Source Code scm commit: ITP server: adding request and notif for file contents (commit d599fad)
15:55:24 Source Code scm commit: nim.py: passable with trywhy3 (commit 04c5c6c)
15:35:10 Source Code scm commit: avoid detection failure in presence of unknown prover (commit 7c1e907)
15:18:59 Source Code scm commit: Removed bullets (commit cf47667)
15:15:27 Source Code scm commit: ITP web: nicer icons (commit dd79884)
14:55:21 Source Code scm commit: Task do not disappear when right clicking (commit 375a10b)
14:41:40 Source Code scm commit: ITP web: editor for source code made visible again in tab (commit 3c88c17)
13:55:08 Source Code scm commit: Reload first removes existing tree. (commit 67930b1)
13:49:00 Source Code scm commit: Avoid printing null notification in log. (commit ff10a71)
13:35:15 Source Code scm commit: Removed unused description in french. (commit b602ed0)
13:30:39 Source Code scm commit: Remove unused raise and log (commit 6058fec)
13:11:18 Source Code scm commit: webserver: fixed interpretation of several files on cmdline (commit 0aa57b3)
13:10:52 Source Code scm commit: web interface: notif handler started immediately on page load (commit 3913bc7)
12:51:17 Source Code scm commit: explanation text for nodes other than goals (commit 1fa1938)
11:58:43 Source Code scm commit: Remove useless exception. (commit 7bff80d)
10:26:45 Source Code scm commit: python: nim example (commit 78f5354)
10:22:21 Source Code scm commit: fix pb parsing JSON files (commit 7a306e1)
09:39:36 Source Code scm commit: Added proved status. (commit 810d2e7)
2017-03-20
20:30:25 Source Code scm commit: Commands can be executed on nodes. (commit 166964f)
12:55:07 Source Code scm commit: Code extraction: (commit f874cd2)
12:46:16 Source Code scm commit: new theory seq.OfList (commit 2e3cb81)
12:46:07 Source Code scm commit: library: list.FoldLeft and list.FoldRight now use HO (commit 438447a)
10:23:52 Source Code scm commit: fix pb with non-utf8 source files (commit 6119589)
2017-03-18
12:37:18 Source Code scm commit: Cleaning. Notifications handling. (commit 5f7b380)
2017-03-17
16:04:23 Source Code scm commit: python: functions and predicates (commit 272e253)
15:43:07 Source Code scm commit: all log messages in sequence (commit c64bbf2)
14:57:55 Source Code scm commit: investigate bts 20881 (commit f9d6ff7)
14:14:51 Source Code scm commit: add another tab for server log, and make the resize bar work (!) (commit 4b4c635)
13:01:04 Source Code scm commit: Adapted Isabelle realization to changes in bit vector theory (commit 854c219)
12:23:59 Source Code scm commit: json_parser/lexer are generated (commit 06a1fb7)
12:16:35 Source Code scm commit: proof of concept of commands to server. To be cleaned. (commit 9d69852)
11:34:11 Trackers Tracker Item [#21170] invalid URL Closed Claude Marché
11:32:13 Source Code scm commit: fix URL badly handled by hevea (commit 681eeaf)
10:27:05 Source Code scm commit: Moved of why3.ml to why3_js.ml to avoid conflict. Switch from camlp4 to ppx to fix merlin. Added errors panel and button for reload. (commit b4ba8a3)
2017-03-16
16:13:22 Source Code scm commit: Fix data files (commit 7b414b2)
16:10:31 Source Code scm commit: Add gnuplot scripts (commit 4326d25)
2017-03-15
16:02:29 Source Code scm commit: Pmodule: refactor cl_init (commit 3303fda)
16:01:38 Source Code scm commit: Add allocating wrapper function for div_qr (commit 6dff3db)
08:28:19 Source Code scm commit: Code extraction (commit 2e10bbd)
2017-03-14
14:11:55 Source Code scm commit: updated sessions with Coq 8.6 (commit 63b6b62)
13:53:38 Source Code scm commit: canevas for new web ide based on trywhy3 (commit 6bc0938)
2017-03-13
16:08:52 Source Code scm commit: fixed extraction of let x = e1 in e2 (commit 6ca2d4d)
13:10:13 Source Code scm commit: Code extraction: optimizing proxy variables (commit 1c27d9b)
2017-03-10
18:29:48 Source Code scm commit: Typo in driver (commit 1b15d48)
18:22:10 Source Code scm commit: OneTime module added to ocaml64 driver (commit 7166632)
2017-03-09
15:54:51 Source Code scm commit: Improve benchmarks (commit d5a67f9)
14:48:55 Source Code scm commit: python: new example (commit 26e6515)
14:16:27 Source Code scm commit: Add missing dependency of Flocq for real.truncate in makefile (commit 0e33a50)
14:16:01 Source Code scm commit: extraction: cleaning up (commit a621477)
13:51:22 Source Code scm commit: extraction: simplified driver and test (commit 3f75188)
12:10:58 Source Code scm commit: extraction: minor change (commit 64dff8d)
12:08:36 Source Code scm commit: Code extraction (commit 3c8951e)
10:11:50 Source Code scm commit: python plugin: parse function in Py_lexer (commit fec2cd7)
09:54:14 Source Code scm commit: Add missing Coq file and remove superfluous ones (commit d96d3c8)
2017-03-08
16:04:51 Source Code scm commit: fix incorrect order of significand and exponent in the case of denormals in Number.compute_float (commit 33f8886)
15:37:11 Source Code scm commit: Finish division proof (commit f2dd8eb)
14:05:48 Source Code scm commit: Remove superfluous warning on axiom in theory ieee_float (commit 3d9cd96)
09:23:00 Source Code scm commit: Code extraction (wip) (commit d7299a3)
2017-03-07
16:02:12 Source Code scm commit: trywhy3: update try-python.patch (commit 2149715)
15:46:46 Source Code scm commit: trywhy3: reset error markers properly (commit 2978e9b)
15:45:19 Source Code scm commit: reinitialise indentation stack (commit 194dfa8)
15:44:40 Source Code scm commit: .merlin: add src/trywhy3 (commit c266d12)
14:55:12 Source Code scm commit: trywhy3: increment line number on '\n' (commit 91932c0)
10:39:03 Source Code scm commit: Merge branch 'master' into new_float (commit 76b65d7)
10:10:21 Source Code scm commit: Raises the minimum OCaml version requirement to 4.02.3 (commit 0a6d4f2)
2017-03-06
15:54:43 Source Code scm commit: Some headway in division launcher proof (commit 3414daf)
15:24:21 Source Code scm commit: trywhy3: add a patch to switch to the python input (commit 4f60b36)
15:20:05 Source Code scm commit: trywhy3: update the alt-ergo driver (commit 8f0d49d)
15:19:32 Source Code scm commit: triangular.py: use a more natural formalisation (commit 55c3f77)
15:18:50 Source Code scm commit: python: fix an off-by-one in "for ... in range()" (commit 817c536)
12:45:37 Source Code scm commit: trywhy3: avoid infinite loops (commit a9d0aef)
09:29:05 Source Code scm commit: trywhy3: no need for a separate theme for the task viewer (commit e50ea1f)
01:55:59 Source Code scm commit: trywhy3: editor and task_viewer can have different modes (commit a89c05c)
01:31:21 Source Code scm commit: trywhy3: update for Alt-Ergo 1.30 (commit 31d1ddb)
2017-03-05
18:18:32 Source Code scm commit: Code extraction: minor (commit b906cf4)
2017-03-03
13:03:04 Source Code scm commit: Code extraction (commit 682f141)
2017-03-02
16:00:24 Source Code scm commit: Fix div by 1 bug (commit df18156)
13:36:02 Source Code scm commit: Code extraction (wip) (commit da76331)
10:20:35 Source Code scm commit: Code extraction (wip) (commit 56c0394)
2017-03-01
16:21:18 Source Code scm commit: + use literals in ieee_float theory + add 'minInt and 'maxInt attributes for range types + add 'eb and 'sb attributes for float types + make ieee_float realization compatible with Coq 8.4 (commit f88de19)
12:21:42 Source Code scm commit: Prove division by 2-digit number (commit b2f1f77)
08:23:55 Source Code scm commit: recover lost proof in queens_bv (commit fd3cdc2)
2017-02-28
23:14:36 Source Code scm commit: Code extraction (wip) (commit cc1693b)
16:05:37 Source Code scm commit: Some headway in loop proof (commit 33a2d35)
14:05:00 Source Code scm commit: extraction: command line (wip) (commit 8e3ee40)
12:21:27 Source Code scm commit: Code extraction (wip) (commit 4c6efb6)
10:12:32 Source Code scm commit: Generalize negative_or_positive. (commit 788027d)
2017-02-27
22:21:05 Source Code scm commit: Code extraction (wip) (commit 62d43c9)
18:28:32 Source Code scm commit: Code extraction (wip) (commit 58425a2)
16:06:24 Source Code scm commit: Begin work on division by 2 digits (commit f04e25c)
11:57:57 Source Code scm commit: Bug on location. (commit 754b5d3)
2017-02-26
21:22:13 Source Code scm commit: Code extraction (wip) (commit e27b988)
2017-02-03
13:18:03 Source Code scm commit: + rename max_representable_integer into pow2sb + add axioms linking eb, sb, emax and pow2sb and clone them as goal in Float(32/64) + modify section dealing with integers + update realisation (commit 56ac17d)
2016-03-16
16:48:15 Source Code scm commit: Add the ability to * declare range types and float types, * use integer (resp. real) literals for those types through casting, * specify how to print them in drivers. (commit f054786)