Paolo Giarrusso (Jul 15 2020 at 20:01): Paolo Giarrusso (Jul 15 2020 at 20:01):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
Paolo Giarrusso (Jul 15 2020 at 20:03):and with that you can check that the output of Print Assumptions baz. doesn't change.
Karl Palmskog (Jul 15 2020 at 20:04):they [tests] are supported well in dune though, see SerAPI for some examples.
Paolo Giarrusso (Jul 15 2020 at 20:06):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
Paolo Giarrusso (Jul 15 2020 at 20:06):fair enough
Last updated: Oct 03 2023 at 20:01 UTC