which reminds me, coq_makefile doesn't support tests, so I've reused https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/Makefile.coq.local
and with that you can check that the output of
Print Assumptions baz. doesn't change.
they [tests] are supported well in dune though, see SerAPI for some examples.
I don't find the exact kind of tests I have in mind (compare stdout with a master version), but serapi convinced me it can be done https://github.com/ejgallego/coq-serapi/tree/v8.11/tests
Last updated: Oct 03 2023 at 20:01 UTC