Stream: Coq users

Topic: Dune cannot compile Ltac2 (?)


view this post on Zulip Arnoud van der Leer (Mar 19 2024 at 15:16):

Hi, for UniMath, we use dune to compile the library. Recently, I thought I'd write an Ltac2 tactic, but when trying to compile this using dune, this yields

Error: Cannot find a physical path bound to logical path Ltac2.Ltac2.

at the line

From Ltac2 Import Ltac2.

Where could the problem lie here? With the version of coq or dune? With some path setting? With something else?

view this post on Zulip Karl Palmskog (Mar 19 2024 at 15:24):

if you have (using coq 0.8), then you have to manually specify that you depend on Ltac2 in the (theories ...) stanza (and more generally, you have to declare all transitive dependencies in this way). This is one reason I personally don't have (using coq 0.8) in projects that use Dune

view this post on Zulip Arnoud van der Leer (Mar 19 2024 at 16:31):

Where should I add that? (what is the syntax)

view this post on Zulip Arnoud van der Leer (Mar 19 2024 at 16:32):

https://dune.readthedocs.io/en/stable/dune-files.html does not give instructions about the theories stanza, apart from the fact that it cannot be autogenerated

view this post on Zulip Li-yao (Mar 19 2024 at 16:34):

Look for (using coq ...) in dune-project at the root of your project

view this post on Zulip Karl Palmskog (Mar 19 2024 at 17:57):

see example here of using (theories ...), but be sure to remove the ;: https://github.com/coq-community/stalmarck/blob/master/theories/Tactic/dune#L6 - (theories Ltac2) in the right place should be enough

view this post on Zulip Arnoud van der Leer (Mar 19 2024 at 18:02):

Should I add theories as a new separate line to dune-project? It currently looks like

(lang dune 3.8)
(using coq 0.8)
(name UniMath)

view this post on Zulip Karl Palmskog (Mar 19 2024 at 18:03):

no, you have to add the theories in a file called dune

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 16:02):

Note that in this case, HoTT doesn't depend on anything so transitive dependencies would not help.

Using Ltac2 from HoTT may be a bit harder (not impossible tho) as Ltac2 depends on the Stdlib as of today, so you will have to declare the dep on the Coq theory too.

view this post on Zulip Karl Palmskog (Mar 20 2024 at 17:27):

but UniMath is different from HoTT I think? Last I checked, Stdlib was "there" but wasn't used (but may have changed)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2024 at 18:02):

Oh yes sorry, in this case all that you need is to declare (theories Ltac2) in the file, maybe also the plugin?

In fact this may be a small bug in our Dune setup, when stdlib=yes, I think we only make Coq visible (with -R), but not Ltac2. But let's first fix the transitive dep stuff, and we see what default is best.


Last updated: Jun 13 2024 at 19:02 UTC