search

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
295 stars 45 forks source link

bedrock2 lightbulb example is incompatible with native_compute #282

Closed JasonGross closed 2 years ago

JasonGross commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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

JasonGross commented 2 years ago

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 commented 2 years ago

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@d926dcf8981ca94cb04d474aa663d3ee1e6f6768)

JasonGross commented 2 years ago

https://github.com/mit-plv/fiat-crypto/pull/1414 should automerge once the CI passes, updating the submodule to include this