Stream: Coq users

Topic: unit tests in Coq


view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 20:03):

and with that you can check that the output of Print Assumptions baz. doesn't change.

view this post on Zulip Karl Palmskog (Jul 15 2020 at 20:04):

they [tests] are supported well in dune though, see SerAPI for some examples.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 20:06):

fair enough


Last updated: Feb 04 2023 at 21:02 UTC