search

rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
53 stars 28 forks source link

CN: Enable lemma CI #455

Open dc-mak opened 3 months ago

dc-mak commented 3 months ago

https://github.com/rems-project/cerberus/commit/20d9d5ce2e982c4744ef6911a25a3be9307518f3 fixed the existing CN lemma tests, but these should really be part of the CI. This requires re-working the CI script a bit to ensure coq and cerberus are on the same switch (it is possible, CHERI-C does it, but I couldn't figure it out and I'm away for the next 1.5 weeks).

septract commented 3 months ago

Likewise, we have Coq tests the cn-tutorial repo. But these are currently not run in CI because CN is not compiled with Coq enabled. See https://github.com/rems-project/cn-tutorial/pull/40