Enable Coq export examples in CI

[septract]

No description provided.

[septract]

Huh, this diff worked, but only really by making the with_coq build the only one that's used.

Unsure why the coq build needs to be separate anyway, any thoughts @dc-mak or others?

cc @scuellar

[dc-mak]

Not familiar with lemma stuff unfortunately, @cp526 any thoughts?

[cp526]

I think this must be because the original version of the cn-tutorial github workflow is based on the one from the Cerberus repository and that, in turn, probably has a separate opam with_coq switch to make sure most parts of Cerberus work without the Coq dependency.

For this repository I see no problem with making everything work above the Coq dependency. So, your change looks good; probably we wouldn't even need a separate with_coq opam switch.

[septract]

Sorry, I didn't explain this very clearly. Let me try again.

• The GH action .yml script in rems-project/cn-tutorial is (intentionally) nearly the same as the one in rems-project/cerberus. This is because they both run the same CI test script on the same examples.
• If we enable checking of Coq examples, we need to do it in both the cn-tutorial and cerberus repos. Otherwise we will break CI for one of the repos.
• At the moment, the .yml script inherited from rems-project/cerberus distinguishes between things that are built with Coq and without using the with_coq switch.
• To enable checking of Coq examples, a naive way to do it would be to remove the ocaml switch distinction.

So the question @cp526 is whether this would be a problem if we did it for both cn-tutorial and cerberus repos?

I think my recommendation is we pause and figure this out once the repo split occurs. At that point, we will probably merge all the CN .yml scripts together, and separate out the cerberus CI process.

(We might even generate a release of cerberus and avoid building it altogether in the CN build process)

[cp526]

RE "So the question @cp526 is whether this would be a problem if we did it for both cn-tutorial and cerberus repos?" IIUC, this would not break the Cerberus CI but make it slightly weaker: we would no longer be checking that parts of Cerberus can be built without Coq (although I'm not sure that's a big deal).

But either way, and as you say, probably easiest to do this following the repository split.