cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
227 stars 36 forks source link

CI for coq-serapi #70

Open ejgallego opened 2 years ago

ejgallego commented 2 years ago

Hi folks,

I'd be great if I could add Alectryon to Coq SerAPI's CI, so I can test it not being broken by new SerAPI releases.

I guess I need:

cpitclaudel commented 2 years ago

Hi @ejgallego, thanks for your patience!

Since Alectryon is in Python you don't need to explicitly build it.

You can run a serapi sanity check using this command: python3 recipes/tests/doctests.py -k serapi. I think this is the simplest thing to do.

You could run the integration tests by running make test, but it's a bit trickier. make test clears all output in the recipes/ directory and rebuilds it, then a git diff tells you whether anything has changed. To not build PDFs, which I think you don't care about, you would run make -C recipes clean followed by make -C recipes alectryon. The versions of Coq, docutils, and sphinx that the tests expect are in _output/.version-info; one difficulty is that the output that Coq produces changes from version to version, and that will break some tests, so I think the doctest approach above is best.

ejgallego commented 2 years ago

Thanks for all the hints; I'll play a bit with the different targets; I don't see a problem enabling the version-specific Coq tests, usually we stay on the same Coq branch for quite a long time.