Hi, I have a coq project that has the following structure
- dune-project - src/ - dune - extraction/ - dune (..)
With the usual .opam files, README etc not shown here. src/ is a collection of Coq files (definition, lemma, etc), whereas extractions/ is for extracting a subset of it. This works fine so far.
Now, I would like to add a couple of examples or tests as a separate directory, e.g. examples/ at the root of the source directory but still using dune to compile and install the library.
My intent is that these examples serve as illustration for the code base and that they could be evaluated for correctness during the build process, but they are not part of the library itself, and I have no need to have them installed (I won't mind if they are though).
Is there any recommendation on how to structure a dune project to achieve this type of project architecture?
I have explored multiple documentation and the closest that I could reuse was: https://github.com/coq-community/manifesto/wiki/Recommended-Project-Structure that I reused for my initial project.
Reviewing https://github.com/mattam82/Coq-Equations/tree/master/examples , it seems an approach is to have a non dune part for the examples, with its own makefile and _CoqProject. Is this the recommended practice?
Thanks for your suggestion.
I think you can do
- test/ - dune # coq.theory with no (package ...) field
so it will be built (unless you explicitly ignore it) but not installed.
Indeed, I tried some combinations
does not work, dune complains that name is missing.
Fair enough, but if I reuse the name I have in src/ then it reports a duplicate name.
So the trick is to do the following
(coq.theory (name Oqarina_tests) (theories Oqarina) )
i.e. give a different
name but populate
theories to point to the hierarchy in
Thanks for the starter @Li-yao
Jerome Hugues has marked this topic as resolved.
Last updated: Jan 30 2023 at 18:04 UTC