Ali Caglayan (Nov 25 2021 at 23:30): 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
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
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: May 28 2023 at 13:30 UTC