Stream: Dune devs & users

Topic: Import file from another directory

Julin S (Feb 26 2023 at 18:40):

Hi. I got some files like this:

├── custom
│   ├── custa.v
│   ├── custb.v
│   └── dune.v
├── theories
│   ├── th_a.v
│   ├── th_b.v
│   └── dune.v
└── dune-project

Is there a way by which I can import the files in theories/ directory inside custa.v when using dune?

Paolo Giarrusso (Feb 26 2023 at 18:51):

Yes; here's a strawman:

theories/dune

(coq.theory
  (name lib1)

custom/dune

(coq.theory
  (name lib2)
  (theories lib1)

this will expose theories as lib1 — like -Q theories lib1. But please pick better names for lib1 and lib2!

Paolo Giarrusso (Feb 26 2023 at 18:52):

those names can contain . but must follow certain rules — foo and foo.custom

Paolo Giarrusso (Feb 26 2023 at 18:53):

however, this is only appropriate if those two folders are separate theories/packages/..., with custom depending on theories but not viceversa. Otherwise, just create a single dune theory in theories, and organize your files using subfolders _inside_ that theory.

Paolo Giarrusso (Feb 26 2023 at 18:54):

Forgot: I always use (include_subdirs qualified) in all dune files for Coq, and you probably want to do that too.

Ali Caglayan (Feb 26 2023 at 19:10):

Paolo Giarrusso said:

Forgot: I always use (include_subdirs qualified) in all dune files for Coq, and you probably want to do that too.

You can also add this stanza to a dune file at the root of your project so you don't have to remember to include it elsewhere. Be aware though, it will also modify the behaviour of OCaml libs if you care about that sort of thing.

Last updated: Jun 04 2023 at 23:30 UTC