Stream: Dune devs & users

Topic: ✔ Adding examples/ directory to dune Coq build


view this post on Zulip Jerome Hugues (Feb 28 2022 at 15:20):

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.

view this post on Zulip Li-yao (Feb 28 2022 at 15:32):

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.

view this post on Zulip Jerome Hugues (Feb 28 2022 at 15:39):

Indeed, I tried some combinations

(coq.theory )

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 src/

Thanks for the starter @Li-yao

view this post on Zulip Notification Bot (Feb 28 2022 at 15:40):

Jerome Hugues has marked this topic as resolved.


Last updated: Jan 30 2023 at 18:04 UTC