Stream: Dune devs & users

Topic: Dune for separate extraction


view this post on Zulip Li-yao (Apr 02 2024 at 13:05):

Right now if I use separate extraction, I have to list the extracted modules first in the coq.extraction stanza and the executable or test stanza, moreover the naming conventions in those two places are different (see example below). Can I only list the intermediate files at most once?

; dune config to run Separate Extraction in main.v

(coq.extraction
  (prelude main)
  (extracted_modules Datatypes IO_Monad IO_RawChar IO_Stdlib
                     main)
  (theories SimpleIO))

(test
  (name main)
  (modules datatypes iO_Monad iO_RawChar iO_Stdlib
           main)
  (flags :standard -w -33-39-67))

view this post on Zulip Josh Cohen (Apr 02 2024 at 18:46):

For dune library stanzas, by default modules does not need to be included, and it will include all the .ml files in the directory. You can instead specify modules which should be excluded (https://dune.readthedocs.io/en/stable/dune-files.html#library). The docs say the behavior should be the same for tests and executable, is this not the case?


Last updated: May 25 2024 at 19:02 UTC