Stream: Dune devs & users

Topic: dune build works but cannot import


view this post on Zulip Julin S (Apr 20 2023 at 04:36):

Hi. I got a simple project setup with dune.

dune build works perfectly.

But when I try to step through individual coq files in an editor, it errors saying:

Cannot find a physical path bound to logical path

I guess this is something that I overlooked in the dune documentation. But I couldn't figure out what?

Does anyone here know what it might be?

view this post on Zulip Julin S (Apr 20 2023 at 04:37):

This is my dune-project file:

(lang dune 3.6)
(using coq 0.6)

(generate_opam_files true)

(package
  (name packname)
  (allow_empty)   ; to get rid of an error. not sure
  (depends
    (dune (>= 3.6.0))))

view this post on Zulip Julin S (Apr 20 2023 at 04:38):

The same file that shows error about not finding path for an Import in an editor, works during dune build.

view this post on Zulip Julin S (Apr 20 2023 at 04:41):

Do I need a _CoqProject file as well?

view this post on Zulip Julin S (Apr 20 2023 at 04:50):

Turns out that what I needed was indeed a _Coqproject file. It works now.

view this post on Zulip Julin S (Apr 20 2023 at 04:50):

Can dune be used to generate a _CoqProject file?

view this post on Zulip Julin S (Apr 20 2023 at 04:51):

Or something similar?

view this post on Zulip Rodolphe Lepigre (Apr 20 2023 at 06:52):

You have two options: either you add a _CoqProject file, in which case you need to give mappings to the source directories (optional) and to directories under _build/default/... (source first so that source files are found in the source, and object files are looked up under _build/ as a fallback), or you use dune coq top instead of running coqtop directly, but that currently requires some editor hacking.

view this post on Zulip Rodolphe Lepigre (Apr 20 2023 at 06:53):

And no, dune cannot generate a _CoqProject file for you.

view this post on Zulip Rodolphe Lepigre (Apr 20 2023 at 06:55):

Note that once a project gets complicated enough (using plugins that are loaded with the new "findlib" method), it becomes much harder (perhaps impossible, but I never tried to hack around this) to express the project configuration as a _CoqProject.


Last updated: May 25 2024 at 19:02 UTC