search

coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
127 stars 166 forks source link

release monae 0.7.1 #3191

Closed affeldt-aist closed 1 month ago

palmskog commented 1 month ago

@affeldt-aist there is not a single successful build here due to OOM kills. Can you point to some example of a successful build somewhere?

affeldt-aist commented 1 month ago

The last commit here https://github.com/affeldt-aist/monae is such an example. (Moreover, in the opam file we use "coq-infotheo" { >= "0.7.4"} because this last version of infotheo did not cause the OOM error in the opam CI (see https://github.com/coq/opam/pull/3189), so I am a bit surprised.)

affeldt-aist commented 1 month ago

But it is true that there is a file (that has not changed recently, smallstep.v) that now requires a ridiculous amount of memory and time to compile (very slow Qed).

palmskog commented 1 month ago

I suspected as much (about the single file using lots of memory). But as usual, then please consider making a new release to address this.

affeldt-aist commented 1 month ago

Sure, we will, we really just didn't notice.