Emilio Jesús Gallego Arias

Can we require one and see what the effect is?

> While I am at it, another motivation for this PR is to carefully segregate the huge and rarely used VM data to a single segment that could be then...

Not sure windows timeout implementation was working?

I need more time to look at this, but I'm principle I feel good about going the direction @JasonGross proposes.

Thanks for all the feedback folks, indeed in the CI we took inspiration from the experience some large codebases (Jane Street's OCaml's libs for example) in managing their setup. The...

> I think that 30 lines of straightforward code in a part of the system that is independent of Coq itself is a very reasonable cost for the Coq repository...

Having a bit more shell doesn't worry me; it is true that adding more shell code is a problem for Coq developers because it is hard to maintain; maybe we...

@proux01 , note issue #6459

> Also, do you think declare_local could/should better go in declare.ml? Or a part of it. For instance, in other declare_foo, assumption_message/definition_message and maybe_declare_manual_implicits are done in declare.ml so maybe...

Indeed; I wonder what metaCoq can do here.