Can we test output of extracted files in the test-suite? https://github.com/coq/coq/pull/15098
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
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