bedrock2 lightbulb example is incompatible with native_compute

[JasonGross]

Fiat Crypto is failing on Coq's CI with

COQNATIVE /builds/coq/coq/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo
ocamlopt.opt got signal and exited
Error: Native compiler exited with status 2 (in case of stack overflow,
       increasing stack size (typically with "ulimit -s") often helps)
Command exited with non-zero status 1
/builds/coq/coq/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo.native (real: 5214.51, user: 60.09, sys: 13.67, mem: 3542188 ko)

https://gitlab.com/coq/coq/-/jobs/3117535414
https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/fiat.20crypto.20broken

Are there any Defined that can be replaced with Qed? Or is there a way to make Fiat Crypto depend only on a subset of bedrock2_ex that does not include lightbulb? Or can bedrock2 be configured to pass -native-compiler ondemand or whatever when building examples?

[samuelgruetter]

Are there any Defined that can be replaced with Qed?

There is one Defined in that file, which takes 260.522 secs, and if it is replaced by Qed, it takes 289.524 secs.
How does Defined vs Qed affect native_compute?

[SkySkimmer]

BTW it's not just lightbulb, swap also fails https://gitlab.com/coq/coq/-/jobs/3132610528

[JasonGross]

Qedd definitions are not compiled to native code, because native_compute will never reduce them. Defined definitions can be reduced by native_compute, and so are compiled. But let's just pass -arg -native-compiler -arg ondemand to coq_makefile for the examples.

[SkySkimmer]

Still happening, I think bedrock didn't get bumped in fiat-crypto https://gitlab.com/coq/coq/-/jobs/3138724899 (job ran with mit-plv/fiat-crypto@d926dcf)

[JasonGross]

mit-plv/fiat-crypto#1414 should automerge once the CI passes, updating the submodule to include this