Stream: Dune devs & users

Topic: META


view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Apr 28 2022 at 20:03):

The error goes away if I redo the build shortly after

view this post on Zulip Ali Caglayan (Apr 28 2022 at 20:13):

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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 12:12):

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

view this post on Zulip 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.

view this post on Zulip Rudi Grinberg (Apr 29 2022 at 15:22):

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

view this post on Zulip Ali Caglayan (Apr 30 2022 at 09:53):

That was 3.1

view this post on Zulip Ali Caglayan (May 02 2022 at 21:52):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 08 2022 at 22:19):

It is not particularly useful here tbh

view this post on Zulip Ali Caglayan (May 08 2022 at 22:20):

Can I make it more useful?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 08 2022 at 22:27):

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

view this post on Zulip Ali Caglayan (May 08 2022 at 22:28):

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

view this post on Zulip Ali Caglayan (May 08 2022 at 22:54):

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

view this post on Zulip Ali Caglayan (May 08 2022 at 22:54):

Too unrelated to what I am doing probably

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 09 2022 at 17:22):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 16 2022 at 16:03):

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

view this post on Zulip Rudi Grinberg (May 16 2022 at 16:03):

What's the difference?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 16 2022 at 16:04):

Because they would be packaged together

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 16 2022 at 16:06):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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"
]

view this post on Zulip Rudi Grinberg (May 16 2022 at 16:36):

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

view this post on Zulip Rudi Grinberg (May 16 2022 at 16:36):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 16 2022 at 20:14):

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

view this post on Zulip Ali Caglayan (May 16 2022 at 20:15):

Something like

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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (May 16 2022 at 20:17):

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

view this post on Zulip Ali Caglayan (May 16 2022 at 20:18):

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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 16 2022 at 20:22):

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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 16 2022 at 20:23):

that looks correct to me

view this post on Zulip Ali Caglayan (May 16 2022 at 20:23):

Looks like the cmxs is also provided

view this post on Zulip Karl Palmskog (May 16 2022 at 20:23):

I think the duplication of the cmxs is by design

view this post on Zulip Paolo Giarrusso (May 16 2022 at 20:23):

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

view this post on Zulip Ali Caglayan (May 16 2022 at 20:24):

By the way that was the coq.theory install

view this post on Zulip Ali Caglayan (May 16 2022 at 20:24):

I'm gonna replicate that by hand now

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (May 16 2022 at 20:26):

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

view this post on Zulip 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)))

view this post on Zulip Ali Caglayan (May 16 2022 at 20:29):

This works.

view this post on Zulip Ali Caglayan (May 16 2022 at 20:29):

Now we need an install rule

view this post on Zulip Ali Caglayan (May 16 2022 at 20:31):

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

view this post on Zulip Ali Caglayan (May 16 2022 at 20:31):

-Q . dpdgraph right?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (May 16 2022 at 20:40):

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

view this post on Zulip Ali Caglayan (May 16 2022 at 20:40):

Everything seems to be working fine

view this post on Zulip Ali Caglayan (May 16 2022 at 20:40):

0:-)

view this post on Zulip 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

view this post on Zulip Ali Caglayan (May 16 2022 at 20:41):

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

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (May 16 2022 at 20:44):

@Rudi Grinberg Any idea what might be going on?

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (May 16 2022 at 20:47):

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

view this post on Zulip Rudi Grinberg (May 16 2022 at 20:47):

Ali Caglayan said:

Rudi Grinberg Any idea what might be going on?

no idea.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Rudi Grinberg (May 16 2022 at 20:48):

we have no such optimization

view this post on Zulip Rudi Grinberg (May 16 2022 at 20:48):

as far as I know at least

view this post on Zulip Ali Caglayan (May 16 2022 at 20:48):

No it is being called

view this post on Zulip 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}

view this post on Zulip Ali Caglayan (May 16 2022 at 20:49):

Very early on in fact

view this post on Zulip Karl Palmskog (May 16 2022 at 20:50):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (May 16 2022 at 20:51):

Coq_module is a complicated coq dep handling module

view this post on Zulip Ali Caglayan (May 16 2022 at 20:52):

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

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (May 16 2022 at 20:54):

What's "prefix handling" in this case?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 16 2022 at 20:55):

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

view this post on Zulip Rudi Grinberg (May 16 2022 at 20:56):

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

view this post on Zulip Ali Caglayan (May 16 2022 at 20:56):

Not necessarily

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (May 16 2022 at 20:57):

Some even have none

view this post on Zulip Rudi Grinberg (May 16 2022 at 20:57):

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

view this post on Zulip Rudi Grinberg (May 16 2022 at 20:57):

Hmm, I guess not.

view this post on Zulip Karl Palmskog (May 16 2022 at 20:57):

some people even skip providing the single .v file

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 16 2022 at 20:59):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 ...

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 16 2022 at 21:03):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rudi Grinberg (May 16 2022 at 21:10):

What are mlpack files used for?

view this post on Zulip Karl Palmskog (May 16 2022 at 21:11):

according to Emilio, they are just boilerplate to get around coqdep design assumptions, if I remember correctly

view this post on Zulip Ali Caglayan (May 16 2022 at 21:12):

https://github.com/coq/coq/blob/2dbc15531d88daa104609d83d666da23d7ca90f1/tools/coqdep/common.ml#L368-L376

view this post on Zulip Karl Palmskog (May 16 2022 at 21:13):

but coq_makefile actually uses the content of .mlpack I believe?

view this post on Zulip Ali Caglayan (May 16 2022 at 21:14):

Perhaps but I am not sure who this warning is helping

view this post on Zulip Ali Caglayan (May 16 2022 at 21:15):

We need to somehow make a coq_makefile test that invokes the warning from coqdep and check that coq_makefile still works

view this post on Zulip Ali Caglayan (May 16 2022 at 21:15):

if it indeed needs an .mlpack

view this post on Zulip Ali Caglayan (May 16 2022 at 21:16):

https://github.com/coq/coq/commit/01fb4ae4f30b1f87eaff2a5ed19133bf8c6933de

view this post on Zulip Ali Caglayan (May 16 2022 at 21:17):

So 11 years ago it was decided that mlpack will be handled, but I can't find any info why

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:36):

the coqdep warning is because it doesn't see the mlpack

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:36):

that should go away once we port for meta

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:37):

I got a way but we need to allow findlib to shut up the "two meta files on the path" warning

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:37):

It is a pity we are having pain with that, because I think the fix is easy

view this post on Zulip Ali Caglayan (May 17 2022 at 15:49):

Right, but why were we looking for mlpack in the first place?

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:49):

That's what coqdep does

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:49):

because it has no information otherwise of when a cmxs file will be generated

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:49):

it is if you want to see it that way

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:50):

a -modules vs non -modules setup

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:50):

but in this case, we can solve it more easily

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:50):

as we can delegate to findlib

view this post on Zulip Emilio Jesús Gallego Arias (May 17 2022 at 15:50):

for .v files that's more of a pain as -modules can't work yet


Last updated: Feb 04 2023 at 01:03 UTC