Pass -native-compiler ondemand for bedrock2 ex
#283
Conversation
|
This change is fine by me but I do not understand why it's necessary for their CI and not ours, and thus whether our repo is actually the right place to fix it. |
|
The Coq packages we use on CI are configured in such a way that coqnative is not run by default on builds. Note that we do this already in Fiat Crypto, I believe, which has similar problems in some places. Plausibly there's some large enough amount of stack and RAM that would allow coqnative to work here, but I don't think it's worth it, and I don't expect many people to suffer for not having the definitions from bedrock2 examples precompiled to native code |
|
But do Coq developers think that the supported usage of Coq is to automatically native-compile everything that ends in Defined? |
|
Depending on how you configure Coq, yes |
|
🤦 |
|
Also depends on which developper you ask and how you phrase the question |
Fixes #282