Stream: Coq devs & plugin devs

Topic: Testing ocaml output in test-suite


view this post on Zulip Ali Caglayan (Nov 25 2021 at 23:30):

Can we test output of extracted files in the test-suite? https://github.com/coq/coq/pull/15098

view this post on Zulip Rudi Grinberg (Nov 30 2021 at 05:20):

I'm not sure if you're asking if it's possible, or should it actually be done. But it's definitely possible with dune:

(coq.extraction (prelude produce_extract_test) (extracted_modules extract_test))
(test (extract_test)) ;; driver should produce extract_test.expected

view this post on Zulip Rudi Grinberg (Nov 30 2021 at 05:21):

And then the usual $ dune runtest will extract, build the executable, run it, and then diff the result the corresponding .expected file in the same dir.


Last updated: Feb 01 2023 at 16:03 UTC