META · Dune devs & users · Zulip Chat Archive

Stream: Dune devs & users

Topic: META

Ali Caglayan (Apr 28 2022 at 20:02):

When dune complains like:

File "_unknown_", line 1, characters 0-0:
Error: File unavailable:
/home/ali/repos/coq-dpdgraph/_build/install/default/lib/coq-dpdgraph/META

What should I do to fix it?

Ali Caglayan (Apr 28 2022 at 20:03):

The error goes away if I redo the build shortly after

Ali Caglayan (Apr 28 2022 at 20:13):

Here is the project in question: https://github.com/coq-community/coq-dpdgraph/pull/101

Emilio Jesús Gallego Arias (Apr 29 2022 at 12:12):

What dune version is this? We saw this bug with the cache and symlinks

Rudi Grinberg (Apr 29 2022 at 15:21):

Another obvious bug in that error is that the failed rule doesn't have a proper location.

Rudi Grinberg (Apr 29 2022 at 15:22):

@Ali Caglayan do you want to try and fix the location bug?

Ali Caglayan (Apr 30 2022 at 09:53):

That was 3.1

Ali Caglayan (May 02 2022 at 21:52):

@Rudi Grinberg Not sure where to start with that one.

Rudi Grinberg (May 02 2022 at 22:34):

Ali Caglayan said:

Rudi Grinberg Not sure where to start with that one.

Should be in install_rules.ml. Look for Gen_meta.gen and the most adjacent call to add_rule that creates the rule for the META. The location is likely not passed in. We should pass the location of the corresponding library stanza there.

Ali Caglayan (May 08 2022 at 22:19):

@Rudi Grinberg I've patched dune to pass the location, here is the difference:

File "_unknown_", line 1, characters 0-0:
*** Error: in file dpdgraph.v, could not find META.coq-dpdgraph.

File "dune", line 44, characters 0-205:
44 | (coq.theory
45 |  (name dpdgraph)
46 |  (package coq-dpdgraph)
47 |  (synopsis "Compute dependencies between Coq objects (definitions, theorems) and produce graphs")
48 |  (libraries coq-dpdgraph.plugin)
49 |  (flags -w +default))
*** Error: in file dpdgraph.v, could not find META.coq-dpdgraph.

Ali Caglayan (May 08 2022 at 22:19):

It is not particularly useful here tbh

Ali Caglayan (May 08 2022 at 22:20):

Can I make it more useful?

Ali Caglayan (May 08 2022 at 22:20):

Or I guess you weren't intending to fix the bug, but rather report the location better.

Rudi Grinberg (May 08 2022 at 22:20):

You can. You can push a custom error message onto the stack. But what's this error about? What would you replace the message with instead?

Ali Caglayan (May 08 2022 at 22:20):

In that case, I found a few other discarded locations before a add_rule. Should I try to add those in as well?

Ali Caglayan (May 08 2022 at 22:21):

Rudi Grinberg said:

You can. You can push a custom error message onto the stack. But what's this error about? What would you replace the message with instead?

Yeah I guess the real bug is in coq.theory here

Rudi Grinberg (May 08 2022 at 22:22):

Ali Caglayan said:

In that case, I found a few other discarded locations before a add_rule. Should I try to add those in as well?

Sure, if you can add a sensible location then it's always welcome.

Ali Caglayan (May 08 2022 at 22:27):

@Rudi Grinberg Do you know about https://github.com/coq/coq/issues/15952?

Ali Caglayan (May 08 2022 at 22:28):

I wonder if I can fix that too, not sure where to look tho.

Ali Caglayan (May 08 2022 at 22:54):

Hmm I think this is https://github.com/ocaml/dune/issues/4039

Ali Caglayan (May 08 2022 at 22:54):

Too unrelated to what I am doing probably

Rudi Grinberg (May 09 2022 at 14:20):

If you understand how flambda’s compilation is supposed to work, the fix should be easy on dune’s side. I think we just lack people with flambda experience on the dune team.

Ali Caglayan (May 09 2022 at 14:31):

I don't particularly see how flambda causes this warning in the first place however. My knowledge of flambda is superficial at best.

Rudi Grinberg (May 09 2022 at 17:13):

Ali Caglayan said:

I don't particularly see how flambda causes this warning in the first place however. My knowledge of flambda is superficial at best.

I haven't fixed this issue for the same reason. I don't know enough about flambda and I don't use it myself. Personally, I'm waiting for flambda2 to come out before investing my time in it.

Ali Caglayan (May 09 2022 at 17:14):

But this is really two bugs right? One bug with the location and one with whatever flambda is causing. I don't particularly care about the latter but perhaps I can fix the first.

Rudi Grinberg (May 09 2022 at 17:19):

I don't think the bad location is from dune. We don't use _none_, we use _unknown_ or <none>. At least as far as I remember.

Ali Caglayan (May 09 2022 at 17:22):

Hmm ok then there is not much to be done I guess

Paolo Giarrusso (May 09 2022 at 18:50):

I'm no flambda expert but the error makes some sense (and why would it change with flambda 2?): Cross-module inlining extends dependencies on interfaces to also depend on object files.

Paolo Giarrusso (May 09 2022 at 18:54):

For Coq users, not using flambda means losing on the order of 20% performance on Coq build times (beware: wide error bars across projects, and I don't have recent measurements)

Karl Palmskog (May 16 2022 at 15:53):

it was suggested here that plugins that want to compile both the OCaml side with Dune and compile at least one Coq file to expose the plugin should be split into two opam packages if they want to avoid the problems with coqdep and META (File "_unknown_", line 1, characters 0-0).

I think this will introduce a large overhead for the whole Coq ecosystem and is not workable. In essence, it would be better to "backport" these plugins to use regular coq_makefile again so that they can be kept in a single package and avoid the coqdep error. I estimate this would be less work than maintaining two packages for all plugins that want to use Dune.

Rudi Grinberg (May 16 2022 at 15:59):

I estimate this would be less work than maintaining two packages for all plugins that want to use Dune.

Could you describe the work of the work two packages instead of one might involve? I do it all the time and it's fairly easy.

Ali Caglayan (May 16 2022 at 16:03):

To be clear, we are talking about dune packages and not the opam packge

Rudi Grinberg (May 16 2022 at 16:03):

What's the difference?

Karl Palmskog (May 16 2022 at 16:03):

for every release, you have to add two packages to the repo and they have to be tested independently. If we remove one of the packages in the future when the issue is solved, all projects that depend on the removed package will break

Ali Caglayan (May 16 2022 at 16:04):

What I mean is that the dune file might have "two packages" but the opam release only has one.

Ali Caglayan (May 16 2022 at 16:04):

Because they would be packaged together

Karl Palmskog (May 16 2022 at 16:04):

I don't really understand how that would work, are you saying the opam package should run two dune install commands?

Rudi Grinberg (May 16 2022 at 16:05):

Karl Palmskog said:

for every release, you have to add two packages to the repo and they have to be tested independently. If we remove one of the packages in the future when the issue is solved, all projects that depend on the removed package will break

You can add a constraint so that they're always the same version. How do you add packages when making a release? It's just one dune-release command invocation regardless of how many packages you have.

Karl Palmskog (May 16 2022 at 16:06):

there are very few projects that actually use dune-release unfortunately

Karl Palmskog (May 16 2022 at 16:08):

but isn't there some opam build clause hacking we could use to avoid having two package definitions?

Karl Palmskog (May 16 2022 at 16:09):

in case of coq-dpdgraph, the Coq theory consists of a single line of code, so couldn't one do two dune build invocations with different parameters?

Rudi Grinberg (May 16 2022 at 16:11):

Karl Palmskog said:

but isn't there some opam build clause hacking we could use to avoid having two package definitions?

Not likely. The issue is that the plugin wants the META file which requires building the entire package. The plugin itself is part of the package so it's a cycle.

Karl Palmskog (May 16 2022 at 16:11):

we are going to need something like that [build command sequence] for the plugins in Coq's CI anyway (since it doesn't use opam)

Rudi Grinberg (May 16 2022 at 16:11):

Karl Palmskog said:

in case of coq-dpdgraph, the Coq theory consists of a single line of code, so couldn't one do two dune build invocations with different parameters?

If it's a single line, why does it need to exist at all?

Karl Palmskog (May 16 2022 at 16:13):

the single line of code in the .v file is what exposes the plugin to Coq users, as opposed to OCaml programmers.

Karl Palmskog (May 16 2022 at 16:20):

but I'm not sure I fully understand how Dune sees packaging. For example, let's say I've written a test suite that has both OCaml tests and Coq-level tests. I would have to refactor that test suite into different directories, if OCaml and Coq sides live in different packages, right?

Karl Palmskog (May 16 2022 at 16:22):

what would happen if I do something like this in my opam package:

build: [
  ["dune" "build" "-p" "dunepackage1" "-j" jobs]
  ["dune" "build" "-p" "dunepackage2" "-j" jobs]
]
run-test: [
 ["dune" "runtest" "-p" "dunepackage1" "-j" jobs]
 ["dune" "runtest" "-p" "dunepackage2" "-j" jobs]
]

Is there anything fundamental that goes wrong then?

Karl Palmskog (May 16 2022 at 16:27):

finally, if one only has a single Coq file, isn't it an option to add a custom rule that calls coqc (eliding coqdep)?

Karl Palmskog (May 16 2022 at 16:33):

another reason for the overhead of split packages is that our custom solution for generating opam package definitions currently doesn't support generating two or more packages in a single repo. This is a limitation that we have planned to remove but haven't gotten to yet.

At the Dune side, we need to add metadata to our opam files that are currently not recognized by Dune, so specifying the opam packages in Dune is also not a straightforward solution.

Rudi Grinberg (May 16 2022 at 16:33):

At the Dune side, we need to add metadata to our opam files that are currently not recognized by Dune, so specifying the opam packages in Dune is also not a straightforward solution.

What kind of metadata is that?

Karl Palmskog (May 16 2022 at 16:34):

example:

tags: [
  "category:Miscellaneous/Coq Extensions"
  "keyword:dependency graph"
  "keyword:dependency analysis"
  "logpath:dpdgraph"
  "date:2022-05-16"
]

Rudi Grinberg (May 16 2022 at 16:36):

But you know you could write .opam files, dune doesn't prevent you from doing that.

Rudi Grinberg (May 16 2022 at 16:36):

Though we could support writing tags in dune-project files too

Ali Caglayan (May 16 2022 at 16:37):

Rudi Grinberg said:

But you know you could write .opam files, dune doesn't prevent you from doing that.

You mean this? https://dune.readthedocs.io/en/stable/opam.html#opam-template

Rudi Grinberg (May 16 2022 at 16:39):

That could be used as well. Though it's not really necessary. Dune only generates opam files only if you ask it to

Karl Palmskog (May 16 2022 at 16:41):

sure, we can write custom .opam ourselves (and we do, most of the time). I'm just laying out the reasons it can be costly to split plugins into two opam packages right now. I really like using Dune, but for "old" plugins that seemingly build fine with coq_makefile, it's not a straightforward choice to split packages just to get to use Dune without running into the coqdep issue.

With that said, if I wrote a new plugin, I probably wouldn't mind splitting up front.

Karl Palmskog (May 16 2022 at 16:42):

if Dune adds support for tags into dune-project, that would lower the barrier for splitting, though

Ali Caglayan (May 16 2022 at 16:53):

Right but you don't even have to do that. You just have a project.opam.template which contains only the tags field and dune will fill the rest with the generated parts.

Karl Palmskog (May 16 2022 at 16:59):

that's one more metadata file to keep track of, in addition to, in many cases: coq-package.opam, meta.yml, dune, dune-project

Ali Caglayan (May 16 2022 at 20:13):

Karl Palmskog said:

finally, if one only has a single Coq file, isn't it an option to add a custom rule that calls coqc (eliding coqdep)?

We can absolutely do this by the way.

Ali Caglayan (May 16 2022 at 20:14):

I think we just need to specify the install rules too.

Ali Caglayan (May 16 2022 at 20:15):

Something like

(rule
 (deps file.v)
 (targets file.vo)
 (action (run %{bin:coqc} file.v))
)

Ali Caglayan (May 16 2022 at 20:16):

And then make an install rule for the coq-contrib folder or wherever it is supposed to install

Ali Caglayan (May 16 2022 at 20:17):

That way we don't call coqdep (since we don't need to).

Ali Caglayan (May 16 2022 at 20:18):

@Karl Palmskog Would you like me to have a go?

Karl Palmskog (May 16 2022 at 20:19):

@Ali Caglayan OK, feel free to do this in the coq-master+dune branch for coq-dpdgraph. This is to me the best solution there, with only a single Coq theory file with just the module declaration.

Karl Palmskog (May 16 2022 at 20:22):

just remember that it should live in the dpdgraph namespace (dpdgraph.dpdgraph)

Ali Caglayan (May 16 2022 at 20:23):

FTR here is what the install looks like:

_build/install/
└── default
    ├── bin
    │   ├── dpd2dot -> ../../../default/dpd2dot.exe
    │   └── dpdusage -> ../../../default/dpdusage.exe
    ├── doc
    │   └── coq-dpdgraph
    │       ├── CHANGES.md -> ../../../../default/CHANGES.md
    │       ├── LICENSE -> ../../../../default/LICENSE
    │       └── README.md -> ../../../../default/README.md
    └── lib
        ├── coq
        │   └── user-contrib
        │       └── dpdgraph
        │           ├── dpdgraph.cmxs -> ../../../../../../default/dpdgraph.cmxs
        │           ├── dpdgraph.v -> ../../../../../../default/dpdgraph.v
        │           └── dpdgraph.vo -> ../../../../../../default/dpdgraph.vo
        └── coq-dpdgraph
            ├── dune-package -> ../../../../default/coq-dpdgraph.dune-package
            ├── META -> ../../../../default/META.coq-dpdgraph
            ├── opam -> ../../../../default/coq-dpdgraph.opam
            └── plugin
                ├── dpdgraph.a -> ../../../../../default/dpdgraph.a
                ├── dpdgraph.cma -> ../../../../../default/dpdgraph.cma
                ├── dpdgraph.cmi -> ../../../../../default/.dpdgraph.objs/byte/dpdgraph.cmi
                ├── dpdgraph.cmt -> ../../../../../default/.dpdgraph.objs/byte/dpdgraph.cmt
                ├── dpdgraph.cmx -> ../../../../../default/.dpdgraph.objs/native/dpdgraph.cmx
                ├── dpdgraph.cmxa -> ../../../../../default/dpdgraph.cmxa
                ├── dpdgraph.cmxs -> ../../../../../default/dpdgraph.cmxs
                ├── dpdgraph__Graphdepend.cmi -> ../../../../../default/.dpdgraph.objs/byte/dpdgraph__Graphdepend.cmi
                ├── dpdgraph__Graphdepend.cmt -> ../../../../../default/.dpdgraph.objs/byte/dpdgraph__Graphdepend.cmt
                ├── dpdgraph__Graphdepend.cmx -> ../../../../../default/.dpdgraph.objs/native/dpdgraph__Graphdepend.cmx
                ├── dpdgraph.ml -> ../../../../../default/dpdgraph.ml-gen
                ├── dpdgraph__Searchdepend.cmi -> ../../../../../default/.dpdgraph.objs/byte/dpdgraph__Searchdepend.cmi
                ├── dpdgraph__Searchdepend.cmt -> ../../../../../default/.dpdgraph.objs/byte/dpdgraph__Searchdepend.cmt
                ├── dpdgraph__Searchdepend.cmx -> ../../../../../default/.dpdgraph.objs/native/dpdgraph__Searchdepend.cmx
                ├── graphdepend.ml -> ../../../../../default/graphdepend.ml
                └── searchdepend.ml -> ../../../../../default/searchdepend.ml

Karl Palmskog (May 16 2022 at 20:23):

that looks correct to me

Ali Caglayan (May 16 2022 at 20:23):

Looks like the cmxs is also provided

Karl Palmskog (May 16 2022 at 20:23):

I think the duplication of the cmxs is by design

Paolo Giarrusso (May 16 2022 at 20:23):

Won't that rule compile the .v file too early?

Ali Caglayan (May 16 2022 at 20:24):

By the way that was the coq.theory install

Ali Caglayan (May 16 2022 at 20:24):

I'm gonna replicate that by hand now

Paolo Giarrusso (May 16 2022 at 20:25):

That is, won't that let dune call coqc before the plugin is built? Is that okay?

Karl Palmskog (May 16 2022 at 20:26):

for this to work, I think the .vo has to depend on the .cmxs

Ali Caglayan (May 16 2022 at 20:28):

Ok so we have

(rule
 (deps dpdgraph.v dpdgraph.cmxs)
 (targets dpdgraph.vo)
 (action (run %{bin:coqc} dpdgraph.v)))

Ali Caglayan (May 16 2022 at 20:29):

This works.

Ali Caglayan (May 16 2022 at 20:29):

Now we need an install rule

Ali Caglayan (May 16 2022 at 20:31):

Oh actually I think I need to pass some more flags to coqc

Ali Caglayan (May 16 2022 at 20:31):

-Q . dpdgraph right?

Karl Palmskog (May 16 2022 at 20:35):

I put dpdgraph.v into theories, so if you are in the root, I recommend -R theories dpdgraph to follow the old convention

Ali Caglayan (May 16 2022 at 20:40):

I just realized that I didn't check out your branch properly

Ali Caglayan (May 16 2022 at 20:40):

Everything seems to be working fine

Ali Caglayan (May 16 2022 at 20:40):

0:-)

Ali Caglayan (May 16 2022 at 20:41):

Those issues with META seem to only happen when you mix .v files with the .ml files

Ali Caglayan (May 16 2022 at 20:41):

But now that there are separate theories and src dir everything looks ok

Karl Palmskog (May 16 2022 at 20:42):

well, I said before I couldn't replicate the error when I split into src and theories (which is best practice anyway). But I don't know why that solves the coqdep problem, because everything is still in the same opam/Dune package (coq-dpdgraph)

Ali Caglayan (May 16 2022 at 20:44):

@Rudi Grinberg Any idea what might be going on?

Ali Caglayan (May 16 2022 at 20:47):

Having a look at the dune code, there seems to be an explicit dep on mllpack for the coqdep rule.

Ali Caglayan (May 16 2022 at 20:47):

I suspect this is buggy when the directories coincide like in this case

Rudi Grinberg (May 16 2022 at 20:47):

Ali Caglayan said:

Rudi Grinberg Any idea what might be going on?

no idea.

Karl Palmskog (May 16 2022 at 20:47):

I looked at the content of the branch now with dune build --verbose, and it never even calls coqdep after the split into separate theories dir.

Karl Palmskog (May 16 2022 at 20:48):

maybe it's an optimization that a directory with only one .v file never needs a coqdep call?

Rudi Grinberg (May 16 2022 at 20:48):

we have no such optimization

Rudi Grinberg (May 16 2022 at 20:48):

as far as I know at least

Ali Caglayan (May 16 2022 at 20:48):

No it is being called

Ali Caglayan (May 16 2022 at 20:49):

DUNE_CACHE=disabled dune build --display=short
       coqpp src/graphdepend.ml
       coqpp src/searchdepend.ml
   ocamlyacc src/dpd_parse.{ml,mli}
    ocamllex src/dpd_lex.ml
      coqdep theories/dpdgraph.v.d
      ocamlc src/.dpdgraph.objs/byte/dpdgraph.{cmi,cmo,cmt}
    ocamldep src/.dpdgraph.objs/searchdepend.ml.d
    ocamldep src/.dpd2dot.eobjs/dpd2dot.ml.d
    ocamldep src/.dpdgraph.objs/graphdepend.ml.d
      ocamlc src/.dpd_lex.objs/byte/dpd_lex__.{cmi,cmo,cmt}
      ocamlc src/.version.objs/byte/version.{cmi,cmo,cmt}
    ocamlopt src/.dpdgraph.objs/native/dpdgraph.{cmx,o}
    ocamldep src/.dpd_lex.objs/dpd_parse.ml.d
      ocamlc src/version.cma
    ocamldep src/.dpd_lex.objs/dpd_lex.ml.d
    ocamldep src/.dpd_lex.objs/dpd_parse.mli.d
    ocamldep src/.dpd2dot.eobjs/dpd_dot.ml.d
    ocamlopt src/.dpd_lex.objs/native/dpd_lex__.{cmx,o}
    ocamlopt src/.version.objs/native/version.{cmx,o}
      ocamlc src/.dpd2dot.eobjs/byte/dune__exe.{cmi,cmo,cmt}
      ocamlc src/.dpdgraph.objs/byte/dpdgraph__Searchdepend.{cmi,cmo,cmt}
    ocamlopt src/version.{a,cmxa}
    ocamlopt src/.dpd2dot.eobjs/native/dune__exe.{cmx,o}
      ocamlc src/.dpd_compute.objs/byte/dpd_compute.{cmi,cmo,cmt}
      ocamlc src/dpd_compute.cma
      ocamlc src/.dpd_lex.objs/byte/dpd_lex__Dpd_parse.{cmi,cmti}
    ocamlopt src/version.cmxs
      ocamlc src/.dpd_lex.objs/byte/dpd_lex__Dpd_parse.{cmo,cmt}
      ocamlc src/.dpd_lex.objs/byte/dpd_lex.{cmi,cmo,cmt}
      ocamlc src/dpd_lex.cma
    ocamlopt src/.dpd_lex.objs/native/dpd_lex__Dpd_parse.{cmx,o}
    ocamlopt src/.dpdgraph.objs/native/dpdgraph__Searchdepend.{cmx,o}
      ocamlc src/.dpdgraph.objs/byte/dpdgraph__Graphdepend.{cmi,cmo,cmt}
      ocamlc src/.dpdusage.eobjs/byte/dune__exe__Dpdusage.{cmi,cmo,cmt}
    ocamlopt src/.dpd_lex.objs/native/dpd_lex.{cmx,o}
      ocamlc src/dpdgraph.cma
      ocamlc src/.dpd2dot.eobjs/byte/dune__exe__Dpd_dot.{cmi,cmo,cmt}
    ocamlopt src/.dpd_compute.objs/native/dpd_compute.{cmx,o}
    ocamlopt src/dpd_lex.{a,cmxa}
      ocamlc src/.dpd2dot.eobjs/byte/dune__exe__Dpd2dot.{cmi,cmo,cmt}
    ocamlopt src/dpd_compute.{a,cmxa}
    ocamlopt src/.dpdusage.eobjs/native/dune__exe__Dpdusage.{cmx,o}
    ocamlopt src/dpd_lex.cmxs
    ocamlopt src/.dpd2dot.eobjs/native/dune__exe__Dpd2dot.{cmx,o}
    ocamlopt src/dpd_compute.cmxs
    ocamlopt src/.dpd2dot.eobjs/native/dune__exe__Dpd_dot.{cmx,o}
    ocamlopt src/.dpdgraph.objs/native/dpdgraph__Graphdepend.{cmx,o}
    ocamlopt src/dpdgraph.{a,cmxa}
    ocamlopt src/dpdgraph.cmxs
    ocamlopt src/dpdusage.exe
    ocamlopt src/dpd2dot.exe
        coqc theories/.dpdgraph.aux,theories/dpdgraph.{glob,vo}

Ali Caglayan (May 16 2022 at 20:49):

Very early on in fact

Karl Palmskog (May 16 2022 at 20:50):

right, I misspotted, it's seemingly being called first? ("Running[1]")

Ali Caglayan (May 16 2022 at 20:51):

Here is the coqdep rule in dune:

let coqdep_rule (cctx : _ Context.t) ~source_rule ~file_flags coq_module =
  (* coqdep needs the full source + plugin's mlpack to be present :( *)
  let source = Coq_module.source coq_module in
  let file_flags =
    [ Command.Args.S file_flags
    ; As [ "-dyndep"; "opt" ]
    ; Dep (Path.build source)
    ]
  in
  let stdout_to = Coq_module.dep_file ~obj_dir:cctx.dir coq_module in
  (* Coqdep has to be called in the stanza's directory *)
  let open Action_builder.With_targets.O in
  Action_builder.with_no_targets cctx.mlpack_rule
  >>> Action_builder.(with_no_targets (goal source_rule))
  >>> Command.run ~dir:(Path.build cctx.dir) ~stdout_to cctx.coqdep file_flags

Ali Caglayan (May 16 2022 at 20:51):

As you can see by <s>Emilio's</s> Rudi's sad face comment that is the issue (Actually I don't know who wrote the comment the git blame says Rudi)

Ali Caglayan (May 16 2022 at 20:51):

Coq_module is a complicated coq dep handling module

Ali Caglayan (May 16 2022 at 20:52):

I think the bug is in there due to incorrect prefix handling

Ali Caglayan (May 16 2022 at 20:52):

in the case .v file and .ml files are in the same dir there is no prefix

Rudi Grinberg (May 16 2022 at 20:54):

What's "prefix handling" in this case?

Ali Caglayan (May 16 2022 at 20:55):

Whatever this is:

module Module = struct
  (* We keep prefix and name separated as the handling of `From Foo Require
     Bar.` may benefit from it. *)
  type t =
    { source : Path.Build.t
    ; prefix : string list
    ; name : Name.t
    }

  let compare { source; prefix; name } t =
    let open Ordering.O in
    let= () = Path.Build.compare source t.source in
    let= () = List.compare prefix t.prefix ~compare:String.compare in
    Name.compare name t.name

  let to_dyn { source; prefix; name } =
    Dyn.record
      [ ("source", Path.Build.to_dyn source)
      ; ("prefix", Dyn.list Dyn.string prefix)
      ; ("name", Name.to_dyn name)
      ]
end

Karl Palmskog (May 16 2022 at 20:55):

hmm, could it be something even more trivial in this case? The output of coqdep is actually not needed here

Karl Palmskog (May 16 2022 at 20:55):

so even though the coqdep call gives an error, the build works fine

Rudi Grinberg (May 16 2022 at 20:56):

@Karl Palmskog does every coq plugin have the same one file boilerplate?

Ali Caglayan (May 16 2022 at 20:56):

Not necessarily

Karl Palmskog (May 16 2022 at 20:57):

no, some have much more stuff and mix plugin with theory at the Coq level (reflective tactics)

Ali Caglayan (May 16 2022 at 20:57):

Some even have none

Rudi Grinberg (May 16 2022 at 20:57):

Okay, but this is the "minimum", right?

Rudi Grinberg (May 16 2022 at 20:57):

Hmm, I guess not.

Karl Palmskog (May 16 2022 at 20:57):

some people even skip providing the single .v file

Karl Palmskog (May 16 2022 at 20:58):

this means that everyone that wants to use the plugin has to do Declare Module ... in their local Coq file

Rudi Grinberg (May 16 2022 at 20:59):

Would it make sense to encode plugin best practices into dune? That is to add a stanza to define a plugin that would take care of these things. It seems pretty bad from the end user's perspective to know all this arbitrary variety can exist

Karl Palmskog (May 16 2022 at 20:59):

we consider this bad practice, and it raises coqdep warnings for the plugin user project

Karl Palmskog (May 16 2022 at 20:59):

I'm all for encoding best practices into Dune, such as splitting the Coq theory and OCaml source into different directories

Ali Caglayan (May 16 2022 at 20:59):

Karl Palmskog said:

we consider this bad practice, and it raises coqdep warnings for the plugin user project

With .v or without .v?

Ali Caglayan (May 16 2022 at 21:00):

Karl Palmskog said:

I'm all for encoding best practices into Dune, such as splitting the Coq theory and OCaml source into different directories

Of course, the story gets a little complicated when people want to mix extraction and ml code tho.

Karl Palmskog (May 16 2022 at 21:00):

the project which uses the plugin that does not have a Coq theory gets a coqdep warning in its .v files that have Declare Module ...

Ali Caglayan (May 16 2022 at 21:01):

Karl Palmskog said:

the project which uses the plugin that does not have a Coq theory gets a coqdep warning in its .v files that have Declare Module ...

Which warning is this specifically?

Ali Caglayan (May 16 2022 at 21:01):

Something like these?

*** Warning: in file bugs/bug_3612.v, declared ML module ./plugins/ltac/ltac_plugin has not been found!
*** Warning: in file bugs/bug_3649.v, declared ML module ./plugins/ltac/ltac_plugin has not been found!
*** Warning: in file bugs/bug_4121.v, declared ML module ./plugins/ltac/ltac_plugin has not been found!
*** Warning: in file micromega/witness_tactics.v, declared ML module ./plugins/micromega/micromega_plugin has not been found!

Ali Caglayan (May 16 2022 at 21:02):

coqdep doesn't actually care about the contents of a plugin, it just points. When the file it is pointing to doesn't exist it emits a warning.

Rudi Grinberg (May 16 2022 at 21:02):

Ali Caglayan said:

Karl Palmskog said:

I'm all for encoding best practices into Dune, such as splitting the Coq theory and OCaml source into different directories

Of course, the story gets a little complicated when people want to mix extraction and ml code tho.

That should always be possible, right? The extraction stanza is special cased so this stuff can be avoided

Karl Palmskog (May 16 2022 at 21:03):

I think the warning was about missing dependencies, yes, "has not been found"

Karl Palmskog (May 16 2022 at 21:04):

yes, I used extraction to build a plugin with Dune just fine, with the src/theories layout...

Ali Caglayan (May 16 2022 at 21:05):

Karl Palmskog said:

I think the warning was about missing dependencies, yes, "has not been found"

I'm thinking that this is really a coqdep bug that these warnings get emitted. If coqc can find the plugin coqdep pointed to no problem, then coqdep ought to have found it too.

Ali Caglayan (May 16 2022 at 21:06):

IIRC coqdep is checking for an mllpack file wherever it was looking but even if you give an existing plugin it complains

Karl Palmskog (May 16 2022 at 21:08):

OK, my best diagnosis here is that a single-Coq-file-in-separate-directory plugin avoids the error due to the .d file never being used anyway, and hence it doesn't matter that it's missing