alea icon indicating copy to clipboard operation
alea copied to clipboard

Published 20 hours ago • verified publisher icon coq-community

Other GitHub versions of ALEA

Open palmskog opened this issue 5 years ago • 4 comments

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

palmskog avatar Dec 12 '19 12:12 palmskog

Ok, this has been done. Relevant discussion starts here -- https://github.com/coq-community/manifesto/issues/55#issuecomment-564969619.

anton-trunov avatar Feb 04 '20 08:02 anton-trunov

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.

palmskog avatar Feb 04 '20 08:02 palmskog

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

anton-trunov avatar Feb 04 '20 08:02 anton-trunov

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)

palmskog avatar Feb 05 '20 16:02 palmskog