ad258e9 | Clement Sartori | 27 March 2018, 12:38:51 UTC | no need for List.sort for maps | 27 March 2018, 12:38:51 UTC |
250d260 | Pierre-Yves Strub | 27 March 2018, 11:55:31 UTC | | 27 March 2018, 11:55:31 UTC |
061bb46 | Pierre-Yves Strub | 27 March 2018, 11:47:41 UTC | Merge branch '1.0' into deploy-poly-record | 27 March 2018, 11:47:41 UTC |
dd158c9 | Pierre-Yves Strub | 21 March 2018, 09:30:54 UTC | Why3config: only try user configuration file | 21 March 2018, 09:30:54 UTC |
6453d5f | Pierre-Yves Strub | 21 March 2018, 09:29:50 UTC | Do not load Why3 config files when executing why3config cmd | 21 March 2018, 09:29:50 UTC |
bd4c706 | Pierre-Yves Strub | 21 March 2018, 09:06:16 UTC | New command: why3config | 21 March 2018, 09:06:16 UTC |
0c76343 | Pierre-Yves Strub | 20 March 2018, 09:11:32 UTC | Put configuration files under $XDG | 20 March 2018, 09:11:32 UTC |
500436c | Clement Sartori | 19 March 2018, 13:53:04 UTC | cleaneeeer | 19 March 2018, 13:53:04 UTC |
de52730 | Clement Sartori | 19 March 2018, 12:13:45 UTC | cleaner | 19 March 2018, 12:13:45 UTC |
d4e3f5a | Clement Sartori | 19 March 2018, 10:52:55 UTC | cleaner | 19 March 2018, 10:52:55 UTC |
47336dd | Clement Sartori | 19 March 2018, 10:43:14 UTC | t_case ok? | 19 March 2018, 10:43:14 UTC |
f87b7f9 | Clement Sartori | 19 March 2018, 10:02:07 UTC | t_split looks ok | 19 March 2018, 10:02:07 UTC |
7f5920e | Clement Sartori | 15 March 2018, 15:22:12 UTC | - | 15 March 2018, 15:22:12 UTC |
b2d376e | Clement Sartori | 13 March 2018, 15:17:35 UTC | - | 13 March 2018, 15:17:35 UTC |
18a33a6 | Clement Sartori | 13 March 2018, 11:10:57 UTC | Better pretty printing | 13 March 2018, 11:10:57 UTC |
141d0f5 | Clement Sartori | 12 March 2018, 15:12:12 UTC | - | 12 March 2018, 15:12:12 UTC |
7647c90 | Clement Sartori | 08 March 2018, 15:33:20 UTC | adding values /lots of warning solved | 08 March 2018, 15:33:20 UTC |
43bdb7d | Clement Sartori | 07 March 2018, 13:15:56 UTC | better variable names | 07 March 2018, 13:15:56 UTC |
7518022 | Clement Sartori | 06 March 2018, 15:34:12 UTC | - | 06 March 2018, 15:34:12 UTC |
002c195 | Clement Sartori | 05 March 2018, 15:07:12 UTC | - | 05 March 2018, 15:07:12 UTC |
e76c57d | Clément Sartori | 02 March 2018, 19:44:36 UTC | - | 02 March 2018, 19:44:36 UTC |
e6c3564 | Clément Sartori | 02 March 2018, 19:41:28 UTC | induction scheme for drecords | 02 March 2018, 19:41:28 UTC |
0acd11c | Clement Sartori | 02 March 2018, 14:38:46 UTC | - | 02 March 2018, 14:38:46 UTC |
cba360f | Clement Sartori | 01 March 2018, 17:43:32 UTC | - | 01 March 2018, 17:43:32 UTC |
8c89ae8 | Clement Sartori | 28 February 2018, 13:01:43 UTC | - | 28 February 2018, 13:01:43 UTC |
9867134 | Alley Stoughton | 28 February 2018, 06:58:30 UTC | Fixed bug in SMT option matching The third stage of filtering in the definition of option_matching had a bug, meaning that attempts to rely on it resulted in assertion failures. But that last stage - disambiguating from right to left - was arguably hard for users to predict, anyway. So, fixed the third stage, but left it out of algorithm. (If it's really desired, easy to put it back in, as now it'll work. But do we really think users will understand why, e.g., [prover x=1] means [prover maxlemmas=1] - because the x in maxlemmas comes earlier when working backward as opposed to the x in maxprovers?) This is how option disambiguation works: First filter-in those option names having the letters of the abbreviation abv in the correct order. Then work through the letters of abv in order, keeping only those option names in which each successive letter appears as early as possible | 28 February 2018, 06:58:30 UTC |
e2879a1 | Pierre-Yves Strub | 27 February 2018, 14:45:50 UTC | | 27 February 2018, 14:45:50 UTC |
96b0ca3 | Clement Sartori | 27 February 2018, 14:18:04 UTC | - | 27 February 2018, 14:18:04 UTC |
8ab4986 | Alley Stoughton | 22 February 2018, 18:54:57 UTC | Fixed mistake wrt oiter. | 26 February 2018, 15:04:53 UTC |
9e2c45b | Alley Stoughton | 22 February 2018, 17:44:03 UTC | Fixed poor spacing. | 26 February 2018, 15:04:53 UTC |
1ca374d | Alley Stoughton | 22 February 2018, 17:20:48 UTC | Reworking specification of current provers. All use-only instructions must come first. There are two "universal" use-only instructions: "" (all known provers), and "!" (no provers). It is illegal to mix ""/"!" with prover names (no point in doing so). As before, if the use-only part is empty, it means the currently known provers. The include/exclude instructions are processed in order, acting on the result of the use-only part. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* no-op *) prover [-"Z3"]. (* removes "Z3" from current provers *) prover [+"Z3"]. (* adds "Z3" to current provers *) prover [""]. (* results in "Z3", "Alt-Ergo" *) prover ["!"]. (* results in no provers *) prover ["Z3"]. (* results in "Z3" *) prover ["Z3" "Alt-Ergo"]. (* results in "Z3", "Alt-Ergo" *) prover ["!" +"Z3"]. (* results in "Z3" *) prover ["" -"Z3"]. (* results in "Alt-Ergo" *) | 26 February 2018, 15:04:53 UTC |
36f7f5a | Alley Stoughton | 21 February 2018, 22:32:02 UTC | Added clean way to clear the list of current provers. The elements of prover [...] have one of the following forms, where s is a string: s (add s to the use-only list) +s (add include s to the include/exclude list) -s (add exclude s to the include/exclude list) The include/exclude list is ordered, so that later instructions can supersede earlier ones. The use-only list was not ordered, but now is. The relative order of the use-only and include/exclude lists is irrelevant, so that, e.g., prover ["Z3" +"Alt-Ergo"] and prover [+"Alt-Ergo" "Z3"] are equivalent. The semantics is that the use-only list is first interpreted (if it's empty, one starts with the current provers as the base), and only then are the instructions of the include/exclude list applied to it, in order. There was already the special use-only instruction "ALL". Now, there is also the use-only instruction "CLEAR", which clears the use-only list, but may be superseded by the use-only instructions that follow. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* a no-op *) prover [+"Z3"] (* adds just "Z3" to whatever current provers are *) prover [-"Z3"] (* removes just "Z3" from whatever current provers are *) prover ["ALL"] (* results in "Z3", "Alt-Ergo" *) prover ["CLEAR"] (* results in nothing *) prover ["CLEAR" +"Z3"] (* results in just "Z3" *) prover [+"Z3" "CLEAR"] (* results in just "Z3" *) prover ["CLEAR" "Z3"] (* result in just "Z3" *) prover ["Z3" "CLEAR"] (* results in nothing *) prover [-"Z3" "ALL"] (* results in "Alt-Ergo" *) prover [+"Z3" "ALL" -"Z3"] (* results in "Alt-Ergo" *) prover [-"Z3" "ALL" +"Z3"] (* results in "Z3", "Alt-Ergo" *) | 26 February 2018, 15:04:53 UTC |
5115c89 | François Dupressoir | 23 February 2018, 12:20:12 UTC | SmtMap: rng and basic results | 24 February 2018, 08:13:05 UTC |
9f07d02 | Pierre-Yves Strub | 23 February 2018, 08:37:48 UTC | SmtMap : fdom and related results | 24 February 2018, 08:12:44 UTC |
dd27d32 | François Dupressoir | 22 February 2018, 10:57:52 UTC | whitespace | 22 February 2018, 10:57:52 UTC |
850f427 | Pierre-Yves Strub | 21 February 2018, 16:09:18 UTC | SMT backed map/fmap | 21 February 2018, 16:09:18 UTC |
6c010d0 | Pierre-Yves Strub | 21 February 2018, 15:25:06 UTC | Travis/Docker : sync UID/GID + fix reports publication | 21 February 2018, 15:26:26 UTC |
459d1a1 | François Dupressoir | 21 February 2018, 10:22:19 UTC | focusing smt calls in hashed ElGamal | 21 February 2018, 10:22:19 UTC |
f033f81 | Vincent Laporte | 21 February 2018, 07:28:00 UTC | FSet library: subset is an operator rather than a predicate Inclusion is now written “\subset” (instead of “<=”). Strict inclusion is now written “\proper” (instead of “<”). | 21 February 2018, 08:18:07 UTC |
ae51632 | Pierre-Yves Strub | 19 February 2018, 13:32:08 UTC | | 19 February 2018, 13:32:08 UTC |
5b2f5a7 | Pierre-Yves Strub | 12 February 2018, 17:08:40 UTC | update copyrights | 12 February 2018, 17:08:40 UTC |
e300f4f | Pierre-Yves Strub | 06 February 2018, 13:54:02 UTC | | 06 February 2018, 13:54:02 UTC |
b622d44 | Pierre-Yves Strub | 05 February 2018, 10:30:53 UTC | Docker: force OCaml version 4.03 | 05 February 2018, 10:30:53 UTC |
2ad5a58 | Pierre-Yves Strub | 04 February 2018, 17:12:04 UTC | remove Docker file for aprhl-test-box | 05 February 2018, 10:30:30 UTC |
9e231d4 | nemeras | 04 February 2018, 16:49:10 UTC | Printing of a Dynamic Record | 04 February 2018, 16:49:10 UTC |
316fc53 | Clément Sartori | 01 February 2018, 14:54:07 UTC | -8 warnings | 01 February 2018, 14:54:07 UTC |
97f611c | Pierre-Yves Strub | 01 February 2018, 11:37:48 UTC | typing of polymorphic record types | 01 February 2018, 11:37:48 UTC |
7a7139a | Clément Sartori | 01 February 2018, 10:25:05 UTC | parsing polymorphic records | 01 February 2018, 10:27:05 UTC |
25c632b | Pierre-Yves Strub | 21 January 2018, 23:32:19 UTC | Fix bug in theory-cloning renaming Path substitution was not build using the correct old-path when a theory substitution was in place. [fix #17361] | 21 January 2018, 23:57:32 UTC |
7cce8c6 | François Dupressoir | 19 January 2018, 21:32:01 UTC | documenting br93 further | 19 January 2018, 21:32:01 UTC |
1bca807 | François Dupressoir | 19 January 2018, 17:51:31 UTC | speed PIR example up | 19 January 2018, 17:51:31 UTC |
26b6fd9 | Pierre-Yves Strub | 18 January 2018, 21:21:37 UTC | New tactical: try! `try!` is similar to `try`, but allows `smt` calls to fail in strict mode. This is for debugging purpose only. `try!` immediately fails on non-strict mode. | 18 January 2018, 21:21:37 UTC |
7bc73a4 | Pierre-Yves Strub | 19 December 2017, 11:17:37 UTC | New tactic: solve `solve` is a resolution tactics. Currently, it tries to (recursively) close goals with the lemmas in the hint databases (in the same manner as `done` with the `hint exact` database). However, `solve` can be given hint databases names with the syntax: `solve (db1, db2, ...)` The maximum depth of the resolution tree is controled by an optional argument that comes first (`solve 2` for example). By default, the depth is equal to 1. Databases can be created using the 'hint solve' command: `hint solve $priority $dbname : lemma1 lemma2'. where the priority is optional --- `solve` tries to solve goals using lemmas with a lower $priority first. `hint exact ...` is now an alias for `hint solve 0 ...` | 19 December 2017, 11:21:58 UTC |
19c5eed | Benjamin Gregoire | 18 December 2017, 12:13:27 UTC | more ways to do the proof | 18 December 2017, 12:13:47 UTC |
34d6e51 | Pierre-Yves Strub | 14 December 2017, 12:26:29 UTC | New IP: //> & ||> The IP //> & ||> are equivalent to /> & |> but use a stronger resolution tactic. | 14 December 2017, 12:26:45 UTC |
ddc2701 | Benjamin Gregoire | 14 December 2017, 10:38:21 UTC | Add alternative proof in PIR. | 14 December 2017, 10:38:21 UTC |
fe76f33 | Benjamin Gregoire | 14 December 2017, 10:37:55 UTC | more lemmas on FSet.oflist | 14 December 2017, 10:37:55 UTC |
527d9ad | Benjamin Gregoire | 08 December 2017, 14:56:08 UTC | add new example: Private information retrieval. | 08 December 2017, 14:56:08 UTC |
89618eb | Pierre-Yves Strub | 15 November 2017, 06:54:48 UTC | New tactic: wlog (without loss of generality). Syntax is: wlog: x1 ... xn / form. It transforms the goal G into: |- (forall x1 ... xn, form => G) => G |- form => G | 15 November 2017, 06:54:48 UTC |
1923b91 | François Dupressoir | 14 November 2017, 14:04:42 UTC | Minimal attempt at stabilising Hybrid | 14 November 2017, 14:04:42 UTC |
9bdd6dd | François Dupressoir | 14 November 2017, 13:34:09 UTC | More stabilising smt in ROM | 14 November 2017, 13:34:09 UTC |
2f6312c | François Dupressoir | 13 November 2017, 17:02:56 UTC | Stabilise smt in old ROM.ec | 13 November 2017, 17:06:47 UTC |
b95b795 | Pierre-Yves Strub | 13 November 2017, 15:06:41 UTC | In ROM.ec, help `smt` by using `move=> />`. | 13 November 2017, 15:19:53 UTC |
0c14bcb | Pierre-Yves Strub | 13 November 2017, 14:46:37 UTC | More on (zmodule) exponential & ordering. | 13 November 2017, 15:19:53 UTC |
d3dcd49 | Pierre-Yves Strub | 09 November 2017, 23:27:41 UTC | New syntaxe for `pose`. `pose` can now take arguments as in `pose f i j := i + k`. | 09 November 2017, 23:27:41 UTC |
89f2173 | Pierre-Yves Strub | 07 November 2017, 09:14:11 UTC | Strengthen reduction for le/lt (int/real) | 07 November 2017, 09:14:11 UTC |
7721333 | Alley Stoughton | 05 November 2017, 08:09:52 UTC | Implemented (#2) rewrite Pr [...] for mu_ge0 and mu_le1, corresponding to lemma ge0_mu (d : 'a distr) p : 0%r <= mu d p. lemma le1_mu (d : 'a distr) p : mu d p <= 1%r. from Distr.ec | 05 November 2017, 08:09:52 UTC |
7f64de1 | Pierre-Yves Strub | 04 November 2017, 22:36:30 UTC | docker: add support for sphinx in the doc-box. | 04 November 2017, 22:36:30 UTC |
c7988e8 | Pierre-Yves Strub | 04 November 2017, 22:35:35 UTC | keywords script: add support for python output. | 04 November 2017, 22:35:35 UTC |
d492fcd | Pierre-Yves Strub | 27 October 2017, 07:14:18 UTC | Libraries: distributions: killing more admits | 27 October 2017, 07:14:18 UTC |
65dfe3c | Pierre-Yves Strub | 27 October 2017, 07:03:50 UTC | Libraries: refactoring + killing admits. | 27 October 2017, 07:03:50 UTC |
ab29b3b | Pierre-Yves Strub | 26 October 2017, 21:55:18 UTC | Libraries: distr: killing admits | 26 October 2017, 21:55:18 UTC |
3f125db | Pierre-Yves Strub | 23 October 2017, 07:51:11 UTC | Libraries: proof of the Cauchy-Schwarz inequality. The proof is done for any euclidean R-ev of finite dimension. The proof comes with a characterisation of zeros for 2nd degree real polynomials. | 23 October 2017, 07:51:11 UTC |
9c39dce | Pierre-Yves Strub | 23 October 2017, 07:49:57 UTC | Libraries: extra facts on iterated multiplication. | 23 October 2017, 07:49:57 UTC |
caf9b25 | Pierre-Yves Strub | 23 October 2017, 04:32:43 UTC | Libraries: solving 2nd degree real polynomials. | 23 October 2017, 04:32:43 UTC |
fd7a34f | Pierre-Yves Strub | 23 October 2017, 04:28:35 UTC | Libraries: link Real.(^) with generic one. | 23 October 2017, 04:28:35 UTC |
fb22315 | Pierre-Yves Strub | 23 October 2017, 04:26:57 UTC | Libraries: extra facts on the square root. | 23 October 2017, 04:26:57 UTC |
280f627 | Pierre-Yves Strub | 23 October 2017, 03:51:09 UTC | Add [field] as a rewrite tactic. | 23 October 2017, 03:51:09 UTC |
2d97328 | Pierre-Yves Strub | 23 October 2017, 02:56:49 UTC | build script: pass ECBRANCH to docker | 23 October 2017, 02:56:49 UTC |
3b4aeec | Pierre-Yves Strub | 12 October 2017, 13:17:20 UTC | New facts on lists | 12 October 2017, 13:17:20 UTC |
8999c70 | Pierre-Yves Strub | 12 October 2017, 12:50:02 UTC | New facts on lists | 12 October 2017, 12:50:02 UTC |
cfa0695 | Pierre-Yves Strub | 12 October 2017, 11:24:33 UTC | Few facts on <= and exp | 12 October 2017, 11:24:33 UTC |
56964f5 | Pierre-Yves Strub | 10 October 2017, 07:04:02 UTC | Update installation instructions for Windows (using opam). | 10 October 2017, 07:04:02 UTC |
10a2fc7 | Pierre-Yves Strub | 10 October 2017, 07:03:49 UTC | Binary packages automatisation scripts. | 10 October 2017, 07:03:49 UTC |
89fb774 | François Dupressoir | 02 August 2017, 16:25:38 UTC | exclude examples/incomplete recursively | 28 September 2017, 11:37:51 UTC |
7cee24f | François Dupressoir | 02 August 2017, 16:25:11 UTC | Support recursive exclusions in test targets | 28 September 2017, 11:37:51 UTC |
44ae0e6 | François Dupressoir | 25 August 2017, 09:35:52 UTC | typo in error message (ecHiGoal) | 25 August 2017, 09:36:18 UTC |
3e7dc31 | François Dupressoir | 21 August 2017, 16:29:20 UTC | moving ahead - some admits in FEL application | 21 August 2017, 16:29:20 UTC |
ac19323 | François Dupressoir | 11 August 2017, 16:15:49 UTC | oaep: experimenting with fel flexibility and style | 11 August 2017, 16:15:49 UTC |
2a78686 | François Dupressoir | 11 August 2017, 16:15:05 UTC | typos in Distr (comments) | 11 August 2017, 16:15:05 UTC |
379e448 | François Dupressoir | 10 August 2017, 21:33:27 UTC | oaep: some progress | 10 August 2017, 21:33:31 UTC |
9329d72 | François Dupressoir | 03 August 2017, 15:36:15 UTC | oaep: exploring useful intermediate lemmas | 03 August 2017, 15:36:15 UTC |
a2de959 | François Dupressoir | 02 August 2017, 15:25:38 UTC | Cleanup in examples: deleting some, porting some. | 02 August 2017, 15:25:38 UTC |
c589262 | François Dupressoir | 31 July 2017, 11:27:25 UTC | OAEP progress | 31 July 2017, 11:27:39 UTC |
68f7b62 | Benjamin Gregoire | 28 July 2017, 10:22:23 UTC | remove garbage | 28 July 2017, 10:22:23 UTC |
d5c7c6e | Benjamin Gregoire | 28 July 2017, 09:57:53 UTC | full proof of cramer shoup :-) | 28 July 2017, 09:58:12 UTC |
00a61be | Benjamin Gregoire | 28 July 2017, 06:05:18 UTC | new theory allowing to switch from a sampling d to a sampling d \ X | 28 July 2017, 09:58:12 UTC |
cbeb6f3 | Benjamin Gregoire | 28 July 2017, 06:04:26 UTC | more lemmas | 28 July 2017, 09:58:12 UTC |
55cc1ec | Benjamin Gregoire | 28 July 2017, 06:03:58 UTC | fix bug in typing of projection on tuple. case the tuple as type "glob M" | 28 July 2017, 09:58:12 UTC |
00cc7d0 | Benjamin Gregoire | 28 July 2017, 04:19:44 UTC | intermediary stuff | 28 July 2017, 09:58:12 UTC |