Other GitHub versions of ALEA

[palmskog]

Please check if the following versions of ALEA contain additional useful code:

• https://github.com/EasyCrypt/certicrypt/tree/master/ALEA
• https://github.com/hivert/Coq-HookLength/tree/master/ALEA
• https://github.com/hivert/Coq-Combi/tree/master/3rdparty/ALEA

[anton-trunov]

Ok, this has been done. Relevant discussion starts here -- coq-community/manifesto#55 (comment).

[palmskog]

The discussion there is clear w.r.t. the EasyCrypt copy of ALEA, but have you also considered the additional ALEA-derived lemmas added in the Coq-Combi project? For example: https://github.com/hivert/Coq-Combi/blob/master/3rdparty/ALEA/Qmeasure.v

Even if this is not essential to add right now, I think it could be desirable to incorporate this into some future "unified" ALEA release that solves many use cases.

[anton-trunov]

You are right. I guess I missed that addition. Thanks.

[palmskog]

It also looks like a lot of examples from the original ALEA releases are currently missing, for example:

• Program for computing a Bernoulli distribution (Bernoulli.v)
• Construction of a distribution to pick uniformly an element in a list. (RandomList.v)