572f035 | Pierre-Yves Strub | 04 March 2017, 21:08:33 UTC | nits in docker (aprhl) | 04 March 2017, 21:08:33 UTC |
ccea93c | Pierre-Yves Strub | 04 March 2017, 20:38:03 UTC | nits in docker | 04 March 2017, 20:38:12 UTC |
fd2fc2b | Pierre-Yves Strub | 04 March 2017, 09:35:08 UTC | Add support for system level conf. file Format: ini file. Sections: [general]. Options: - why3conf (string) : Why3 configuration file - provers (string list) : -P option (list of used provers) - idirs (string list) : -I option - rdirs (string list) : -R option - no-evict (string list) : -no-evict option INI file location: EasyCrypt lib. directory /etc/easycrypt.ini | 04 March 2017, 09:35:15 UTC |
4afed9d | Pierre-Yves Strub | 04 March 2017, 08:37:24 UTC | remove code dedicated to local toolchain | 04 March 2017, 08:38:49 UTC |
d633c86 | Pierre-Yves Strub | 04 March 2017, 08:27:26 UTC | update files headers (libraries) (copyright) | 04 March 2017, 08:27:26 UTC |
cd4a4d0 | Pierre-Yves Strub | 04 March 2017, 08:26:41 UTC | update files headers (copyright) | 04 March 2017, 08:26:41 UTC |
42ecbc7 | Pierre-Yves Strub | 04 March 2017, 08:26:04 UTC | Fix compilation issues | 04 March 2017, 08:26:04 UTC |
7519681 | Pierre-Yves Strub | 04 March 2017, 08:23:12 UTC | update copyright meta-data (bis) | 04 March 2017, 08:23:12 UTC |
532fd5d | Pierre-Yves Strub | 04 March 2017, 08:19:21 UTC | update copyright meta-data | 04 March 2017, 08:19:21 UTC |
249f7c1 | Pierre-Yves Strub | 02 March 2017, 09:55:54 UTC | README (opam pin) | 02 March 2017, 09:55:54 UTC |
2ebb404 | Pierre-Yves Strub | 02 March 2017, 09:55:36 UTC | [docker]: generic test box | 02 March 2017, 09:55:36 UTC |
a16c59a | Pierre-Yves Strub | 01 March 2017, 22:19:33 UTC | [README]: installing ec-branches via opam | 01 March 2017, 22:19:33 UTC |
8b2bf22 | Pierre-Yves Strub | 01 March 2017, 22:07:07 UTC | Nits on docker boxes | 01 March 2017, 22:07:07 UTC |
624a583 | Pierre-Yves Strub | 01 March 2017, 14:34:59 UTC | docker box for CI (tests) | 01 March 2017, 14:34:59 UTC |
dc91673 | Pierre-Yves Strub | 01 March 2017, 12:25:26 UTC | testting -> testing | 01 March 2017, 12:25:26 UTC |
a7c115c | Pierre-Yves Strub | 01 March 2017, 12:21:50 UTC | [make install] installs the runtest binary | 01 March 2017, 12:21:50 UTC |
bd3b7b0 | Pierre-Yves Strub | 01 March 2017, 12:21:34 UTC | Use the correct env. when printing synced prhl goals | 01 March 2017, 12:21:34 UTC |
da54edb | Pierre-Yves Strub | 01 March 2017, 11:04:22 UTC | [pprint]: when checking that 2 programs are in sync, use alpha-eq without path norm'ion | 01 March 2017, 11:04:22 UTC |
d92f237 | Pierre-Yves Strub | 01 March 2017, 10:59:06 UTC | API: access to alpha-conversion without path norm'ion | 01 March 2017, 10:59:06 UTC |
3e41975 | Pierre-Yves Strub | 01 March 2017, 10:03:32 UTC | Do not try to install non-existent PG files | 01 March 2017, 10:03:32 UTC |
df7ff31 | Pierre-Yves Strub | 01 March 2017, 09:45:31 UTC | Fix english | 01 March 2017, 09:45:31 UTC |
2950852 | Pierre-Yves Strub | 01 March 2017, 09:44:45 UTC | [pprint]: in prhl, when program as sync'ed, only display one | 01 March 2017, 09:44:45 UTC |
8f58725 | Pierre-Yves Strub | 27 February 2017, 13:18:47 UTC | README (travis status) | 27 February 2017, 13:18:47 UTC |
372fed8 | Pierre-Yves Strub | 27 February 2017, 13:14:53 UTC | Docker boxes | 27 February 2017, 13:14:53 UTC |
bec3930 | Pierre-Yves Strub | 27 February 2017, 12:56:22 UTC | Fix Travis syntax | 27 February 2017, 12:56:22 UTC |
4787ab0 | Pierre-Yves Strub | 27 February 2017, 10:44:39 UTC | Add support for travis CI. | 27 February 2017, 12:49:52 UTC |
e055841 | Pierre-Yves Strub | 27 February 2017, 10:40:22 UTC | README | 27 February 2017, 10:40:22 UTC |
ef13e8d | Pierre-Yves Strub | 23 February 2017, 08:43:14 UTC | FIx MANIFEST | 23 February 2017, 08:43:14 UTC |
2d4a41e | Pierre-Yves Strub | 21 February 2017, 22:34:38 UTC | remove emacs-based packaging script Again, docker is the way to go. | 21 February 2017, 22:34:45 UTC |
57ad58b | Pierre-Yves Strub | 21 February 2017, 22:30:40 UTC | removing local toolchain+PG, removing vagrant - opam is the way to go for getting EasyCrypt - EasyCrypt mode for PG has been integrated upstream - Vagrant is a nightmare (docker is the way to go) | 21 February 2017, 22:30:55 UTC |
263740c | François Dupressoir | 19 December 2016, 22:28:21 UTC | 'Fixing' BR93. | 19 December 2016, 22:28:21 UTC |
8acf8d0 | Benjamin Gregoire | 13 December 2016, 10:22:12 UTC | add ring on boolean in StdRing. | 13 December 2016, 10:22:45 UTC |
f993902 | Pierre-Yves Strub | 10 December 2016, 09:56:56 UTC | extra corollary in bigops | 10 December 2016, 09:56:56 UTC |
3425756 | Pierre-Yves Strub | 15 November 2016, 20:54:16 UTC | fix conversion check of expressions (missing quantif) | 15 November 2016, 20:54:22 UTC |
6700014 | Pierre-Yves Strub | 28 October 2016, 15:00:56 UTC | better use deprecated functions than non existing ones | 28 October 2016, 15:01:08 UTC |
2c150a9 | Pierre-Yves Strub | 26 October 2016, 13:57:59 UTC | kill warnings | 26 October 2016, 13:57:59 UTC |
eae4110 | Pierre-Yves Strub | 14 September 2016, 11:29:29 UTC | Makefile | 14 September 2016, 11:29:29 UTC |
495667a | Pierre-Yves Strub | 07 September 2016, 10:14:18 UTC | In `t_crush`, only substitute eqs. in variables local to the eqs. I.e., in eqs. that have been introduced after the last `split` or in all eqs. if no `split` have ocurred. [fix #17339] | 07 September 2016, 10:14:18 UTC |
5b35f66 | Pierre-Yves Strub | 07 September 2016, 10:13:01 UTC | t_subst: allow to do the substitution only in targeted hyps. The new parameter is `?tg` and gives the set of hypotheses identifiers in which the substitution can occur. If `tg` is `None`, the previous behaviour is applied --- i.e. try the substitution in all local hypotheses. | 07 September 2016, 10:13:01 UTC |
c2940eb | Pierre-Yves Strub | 07 September 2016, 10:10:42 UTC | New printer for `LDecl.hyps`. | 07 September 2016, 10:10:42 UTC |
0c51d1f | Pierre-Yves Strub | 31 August 2016, 19:10:48 UTC | Issue a warning when an unknown `pragma` is issued. The behaviour for options (i.e. for `pragma +opt` / `pragma -opt`) is kept. [close #17338] | 31 August 2016, 19:10:48 UTC |
12ed9d6 | Pierre-Yves Strub | 29 August 2016, 10:58:47 UTC | Nits in `zipper_of_cpos` (catch the right exception) | 29 August 2016, 10:58:47 UTC |
6a1a2b5 | Pierre-Yves Strub | 29 August 2016, 10:56:37 UTC | New variant of `inline`: `inline side? codepos`. Inline the procedure call located at position `codepos`. [close #17336] | 29 August 2016, 10:56:37 UTC |
3d8e4b7 | Pierre-Yves Strub | 29 August 2016, 10:25:23 UTC | Add missing cases for inline (phoare / byname) | 29 August 2016, 10:25:23 UTC |
455162b | Pierre-Yves Strub | 27 August 2016, 07:11:21 UTC | Add a pragma for interverting `/=` && `/~=` (and all their variants) The pragma is `redlogic` (i.e. logical reduction in `/=`). It is set by default. [close #17333] | 27 August 2016, 07:12:22 UTC |
d273f1b | Benjamin Gregoire | 24 August 2016, 16:28:20 UTC | add clone ComRing in BitWord | 24 August 2016, 16:28:20 UTC |
9a4f6f0 | Benjamin Gregoire | 24 August 2016, 14:58:28 UTC | add useful lemma | 24 August 2016, 14:58:28 UTC |
44c769a | Pierre-Yves Strub | 19 August 2016, 11:22:30 UTC | Syntax change: arguments of `exists` are now space separated [close #17331] | 19 August 2016, 11:22:30 UTC |
83167f7 | Pierre-Yves Strub | 19 August 2016, 10:36:02 UTC | Fix internal view's proof-term construction. [fix #17330] | 19 August 2016, 10:36:29 UTC |
d7bb00b | François Dupressoir | 11 August 2016, 16:08:59 UTC | Morefiddling with smt. | 11 August 2016, 16:08:59 UTC |
ee33eba | François Dupressoir | 11 August 2016, 12:39:35 UTC | smt all -> smt in AWord. | 11 August 2016, 12:39:35 UTC |
4f9d39d | François Dupressoir | 11 August 2016, 12:38:05 UTC | Stabilize smt in StdRing. | 11 August 2016, 12:38:05 UTC |
59c8860 | Pierre-Yves Strub | 11 August 2016, 01:53:00 UTC | Do not use hash-cons based ordering in places where a stable order in needed. Hash-cons based ordering is not stable from run to run. This commit adds a set a "natural" orderings for paths & related structure and use them in place where a stable ordering is needed. This might affect existing proofs that were, by chance, perfectly working. [fix #17329] | 11 August 2016, 02:10:53 UTC |
c4a059e | Pierre-Yves Strub | 09 August 2016, 20:52:30 UTC | New variants of i.p. `<*>` The variant `<<*>` gives priority to right-to-left substitutions, whereas the variant `<*>>` gives priority to left-to-right substitutions. [closes #17327] | 09 August 2016, 20:52:30 UTC |
8feea6f | Pierre-Yves Strub | 09 August 2016, 11:11:08 UTC | i-p `+` do not reorder goals anymore when separated by non-intro i-p. [fix #17326] | 09 August 2016, 11:11:08 UTC |
80d3044 | Pierre-Yves Strub | 08 August 2016, 13:54:01 UTC | i-p |> do not unfold anymore conclusion when applying `split` [fix #17324] | 08 August 2016, 13:54:10 UTC |
a885d8c | Pierre-Yves Strub | 07 August 2016, 21:16:03 UTC | In `crush`: do not clear substituted variables. They may still be needed by the upper layer. [fix #17323] | 07 August 2016, 21:16:03 UTC |
b0f6ae6 | Pierre-Yves Strub | 06 August 2016, 15:21:27 UTC | In subst: add support for inductive predicates. [fix #17320] | 06 August 2016, 15:21:27 UTC |
b2d38f8 | Pierre-Yves Strub | 06 August 2016, 14:10:22 UTC | In parser: `case` options are not before the colon, not after [fix #17321] | 06 August 2016, 14:10:28 UTC |
30570db | Pierre-Yves Strub | 06 August 2016, 14:05:43 UTC | In parser, do not shuffle proofs/renaming of a clone [fix #17318] | 06 August 2016, 14:05:49 UTC |
ac945f3 | Pierre-Yves Strub | 06 August 2016, 14:05:01 UTC | fix scripts w.r.t new auto DB | 06 August 2016, 14:05:01 UTC |
f6b75ac | Pierre-Yves Strub | 15 July 2016, 15:55:21 UTC | push missing files | 15 July 2016, 15:55:21 UTC |
1188240 | Benjamin Gregoire | 15 July 2016, 15:19:25 UTC | fix simplification of know real expression. | 15 July 2016, 15:19:37 UTC |
8a723c3 | Pierre-Yves Strub | 15 July 2016, 15:04:26 UTC | fix namings | 15 July 2016, 15:04:37 UTC |
293e676 | Pierre-Yves Strub | 15 July 2016, 15:00:52 UTC | some facts on ln | 15 July 2016, 15:01:01 UTC |
920939f | Pierre-Yves Strub | 15 July 2016, 14:50:24 UTC | analysis: some facts on convexity | 15 July 2016, 14:50:24 UTC |
fd59217 | Pierre-Yves Strub | 15 July 2016, 10:28:16 UTC | axiomatized bounds for ln | 15 July 2016, 10:28:29 UTC |
2e8bc62 | Pierre-Yves Strub | 15 July 2016, 10:11:10 UTC | add real square root | 15 July 2016, 10:11:10 UTC |
9a21032 | Pierre-Yves Strub | 15 July 2016, 08:23:33 UTC | async while: fix bugs regarding fresh variables | 15 July 2016, 08:26:46 UTC |
4bc331a | Pierre-Yves Strub | 15 July 2016, 07:34:43 UTC | tremendeous hacks for fixing subst. of locals | 15 July 2016, 08:26:39 UTC |
f7b4f66 | Benjamin Gregoire | 14 July 2016, 20:50:14 UTC | improve usability of async while. | 15 July 2016, 08:26:01 UTC |
c17c154 | Pierre-Yves Strub | 14 July 2016, 14:20:31 UTC | async-while prototype implementation (to be tested) | 14 July 2016, 14:20:31 UTC |
234f832 | Pierre-Yves Strub | 14 July 2016, 09:28:15 UTC | do not use Map.translate on non monotonous funs | 14 July 2016, 09:30:27 UTC |
22d52f3 | Pierre-Yves Strub | 07 July 2016, 10:26:54 UTC | Work around #17319 [references #17319] | 07 July 2016, 10:26:54 UTC |
ec6fca2 | Pierre-Yves Strub | 13 June 2016, 15:36:23 UTC | fix compilation on ocaml 4.03.0 | 13 June 2016, 15:36:32 UTC |
377a2cd | François Dupressoir | 31 May 2016, 13:25:57 UTC | NewFMap: avoid using finite sets when predicates work (eq_except). | 31 May 2016, 13:25:57 UTC |
3c30914 | François Dupressoir | 31 May 2016, 11:56:23 UTC | Stablizing an smt call in NewFMap. | 31 May 2016, 11:56:23 UTC |
c9a0683 | François Dupressoir | 19 May 2016, 10:03:13 UTC | Everything (in theories) is NewFMap. | 19 May 2016, 10:03:39 UTC |
f9d70ed | Pierre-Yves Strub | 18 May 2016, 16:09:18 UTC | balancing .dir-locals | 18 May 2016, 16:09:18 UTC |
4be663f | Pierre-Yves Strub | 17 May 2016, 16:00:05 UTC | README.md | 17 May 2016, 16:00:05 UTC |
fd4bf22 | Pierre-Yves Strub | 07 May 2016, 09:41:02 UTC | Nits. | 07 May 2016, 09:41:02 UTC |
fcf86c2 | Pierre-Yves Strub | 06 May 2016, 19:59:40 UTC | List masking. | 06 May 2016, 19:59:40 UTC |
407be6f | Pierre-Yves Strub | 06 May 2016, 14:34:18 UTC | Killing a bunch of admits in intdiv + defining ediv. | 06 May 2016, 14:34:18 UTC |
3dedf33 | Pierre-Yves Strub | 06 May 2016, 09:43:25 UTC | Don't use the currently printed abbrev. when printing its body. [fix #17135] | 06 May 2016, 09:44:11 UTC |
c8fbd0c | François Dupressoir | 06 May 2016, 08:49:44 UTC | Argmin is now a real argmin. | 06 May 2016, 08:49:44 UTC |
ff23f9a | François Dupressoir | 06 May 2016, 08:39:52 UTC | argmin: remove existentials in premises. | 06 May 2016, 08:39:52 UTC |
22578b4 | Pierre-Yves Strub | 06 May 2016, 07:38:09 UTC | `argmin` operator `argmin p` returns the smaller natural `i` s.t. `p i` or 0 if not such witness exists. | 06 May 2016, 07:38:09 UTC |
fa61550 | Pierre-Yves Strub | 05 May 2016, 19:31:40 UTC | Add negative filters for `clone ... proof * [...]` Filters now have the following syntax: `[-?tag ... -?tag]` Negative tags are of the form `-tag`. Other ones are named positive. An axiom is selected by a filter if: - none of its tags are rejected by a negative filters - one of its tags is accepted by a positive filter or no positive filters exists | 05 May 2016, 19:31:40 UTC |
6c9dfe5 | Pierre-Yves Strub | 05 May 2016, 09:28:49 UTC | Properly equip zmod with a ring structure. The inverse is currently not linked to gcd. | 05 May 2016, 09:29:36 UTC |
bf94ca4 | François Dupressoir | 04 May 2016, 11:21:37 UTC | Moving Word away from Arrays. Updating MEE functional spec accordingly. | 04 May 2016, 11:21:45 UTC |
0670411 | François Dupressoir | 04 May 2016, 11:19:46 UTC | Stabilize smt in MEE instantiation. | 04 May 2016, 11:19:46 UTC |
ccd68ba | Pierre-Yves Strub | 30 April 2016, 13:47:02 UTC | In `clone`: when renaming, don't forget to prepend sub-theorie path as a prefix. [fix #17312] | 30 April 2016, 13:47:02 UTC |
aa6ee8e | Pierre-Yves Strub | 30 April 2016, 11:30:50 UTC | Homogenise module & module type parameters syntax. [fix #17314] | 30 April 2016, 11:30:50 UTC |
6bd35fb | Pierre-Yves Strub | 30 April 2016, 10:53:33 UTC | In mod-typing: clean-up dead code, remove internal exn., fix various bugs. [fix #17313] | 30 April 2016, 10:53:33 UTC |
dff9911 | Pierre-Yves Strub | 29 April 2016, 19:32:49 UTC | bigop: partition | 29 April 2016, 19:33:12 UTC |
0014c65 | François Dupressoir | 27 April 2016, 13:20:53 UTC | Using (semi-)modern libs for MEE-CBC functional spec. Some discussion need to be had: - Should we bring everything back to bitstrings? octetstrings? - Should we get rid of those blasted Arrays? (Yes) | 27 April 2016, 15:06:22 UTC |
8db4a56 | François Dupressoir | 25 April 2016, 16:55:16 UTC | Stabilizing some smt calls and fixing a proof. | 25 April 2016, 16:55:16 UTC |
4702c81 | François Dupressoir | 22 April 2016, 17:58:46 UTC | More systematic construction for the partitioning of final states. | 22 April 2016, 17:58:46 UTC |
4bfe658 | François Dupressoir | 22 April 2016, 15:15:56 UTC | Starting cleanup in Dice_sampling and associated example. | 22 April 2016, 15:15:56 UTC |
179af54 | François Dupressoir | 22 April 2016, 14:34:11 UTC | Preliminary generic argument for event partitioning. This kind of argument is currently difficult to use, but formalizing and using them should give us hints as to what we can and should do to support them more cleanly. This one will be used, once generalized further and cleaned up, to simplify Dice_sampling. | 22 April 2016, 14:44:11 UTC |