Stream: Coq devs & plugin devs

Topic: coqdep and plugin META


view this post on Zulip Karl Palmskog (May 09 2022 at 09:33):

I have to say I don't really understand what's going on with coqdep anymore. Is coqdep really supposed to require META.<stuff> just for running? I have a plugin branch I build with Dune, and I get this now:

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

However, it looks like the plugin is actually built. It seems like a chicken-and-egg problem, where META.<stuff> is built by Dune on demand, but only after running coqdep on all files. Any advice if this error should be ignored or not?

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

The coqdep rule is being run too eagerly and this is a bug in dune

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

I had a look at it yesterday, and the coqdep rule doesn't actually depend on the META file

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

If you run dune build twice you will see that it actually succeeds

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

The location that dune reports is also buggy, but I have submitted a patch for that upstream.

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

That will just point to the coq.theory stanza

view this post on Zulip Karl Palmskog (May 09 2022 at 09:46):

right, yes, I see that dune build succeeds the first time. But it sounds like the error can just be ignored then?

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

Yes, but the fact that it requires two builds isn't great

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

coq.theory depends on mllpack files from what I read in the source and doesn't really know about META

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

Here is something that is super-not-documented that I found browsing source code yesterday. There is a tool called dune rules which will dump the internal rules used by dune. @Karl Palmskog could you do a clean build with dune rules instead of dune build and find and paste whichever coqdep expression it generates.

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

We can then see what dune considers the dependencies of the coqdep rule

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

It won't be a well-formed rule since that tool is not really used/documented/tested much, but will have the relevant info.

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

I ran dune rules, but where is the dump?

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

Hmm if you pass --display=short then maybe the output is dumped. I suspect that dune is swallowing the output due to being in quiet mode. (Alternatively just pass --verbose)

view this post on Zulip Ali Caglayan (May 09 2022 at 11:15):

@Karl Palmskog Did it work?

view this post on Zulip Karl Palmskog (May 09 2022 at 11:17):

$ dune rules --display=short
       coqpp searchdepend.ml
   ocamlyacc dpd_parse.{ml,mli}
    ocamldep .dpd2dot.eobjs/dpd2dot.ml.d
    ocamldep .dpdgraph.objs/searchdepend.ml.d
    ocamldep .dpd_lex.objs/dpd_parse.ml.d
       coqpp graphdepend.ml
    ocamldep .dpd2dot.eobjs/dpd_dot.ml.d
    ocamllex dpd_lex.ml
    ocamldep .dpdgraph.objs/graphdepend.ml.d
    ocamldep .dpd_lex.objs/dpd_lex.ml.d
    ocamldep .dpd_lex.objs/dpd_parse.mli.d
File "_unknown_", line 1, characters 0-0:
      coqdep dpdgraph.v.d (exit 1)
*** Error: in file dpdgraph.v, could not find META.coq-dpdgraph.

view this post on Zulip Ali Caglayan (May 09 2022 at 11:20):

OK let's try --verbose too just in case

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

$  dune rules --verbose
Shared cache: disabled
Workspace root: <...>/coq-dpdgraph
Auto-detected concurrency: 8
Running[0]: /home/palmskog/.opam/4.11.1.coqdev/bin/ocamlc.opt -config > /tmp/dune_ca27cd_output
Dune context:
 { name = "default"
 ; kind = "default"
 ; profile = Dev
 ; merlin = true
 ; for_host = None
 ; fdo_target_exe = None
 ; build_dir = "default"
 ; toplevel_path =
     Some External "/home/palmskog/.opam/4.11.1.coqdev/lib/toplevel"
 ; ocaml_bin = External "/home/palmskog/.opam/4.11.1.coqdev/bin"
 ; ocaml = Ok External "/home/palmskog/.opam/4.11.1.coqdev/bin/ocaml"
 ; ocamlc = External "/home/palmskog/.opam/4.11.1.coqdev/bin/ocamlc.opt"
 ; ocamlopt =
     Ok External "/home/palmskog/.opam/4.11.1.coqdev/bin/ocamlopt.opt"
 ; ocamldep =
     Ok External "/home/palmskog/.opam/4.11.1.coqdev/bin/ocamldep.opt"
 ; ocamlmklib =
     Ok External "/home/palmskog/.opam/4.11.1.coqdev/bin/ocamlmklib.opt"
 ; env =
     map
       { "DUNE_OCAML_HARDCODED" : "/home/palmskog/.opam/4.11.1.coqdev/lib"
       ; "DUNE_OCAML_STDLIB" : "/home/palmskog/.opam/4.11.1.coqdev/lib/ocaml"
       ; "DUNE_SOURCEROOT" :
           "/home/palmskog/src/coq/coq-community/coq-dpdgraph"
       ; "INSIDE_DUNE" :
           "/home/palmskog/src/coq/coq-community/coq-dpdgraph/_build/default"
       ; "OCAMLFIND_IGNORE_DUPS_IN" :
           "/home/palmskog/src/coq/coq-community/coq-dpdgraph/_build/install/default/lib"
       ; "OCAMLPATH" :
           "/home/palmskog/src/coq/coq-community/coq-dpdgraph/_build/install/default/lib"
       ; "OCAMLTOP_INCLUDE_PATH" :
           "/home/palmskog/src/coq/coq-community/coq-dpdgraph/_build/install/default/lib/toplevel"
       ; "OCAML_COLOR" : "always"
       ; "OPAMCOLOR" : "always"
       }
 ; findlib_path = [ External "/home/palmskog/.opam/4.11.1.coqdev/lib" ]
 ; arch_sixtyfour = true
 ; natdynlink_supported = true
 ; supports_shared_libraries = true
 ; ocaml_config =
     { version = "4.11.1"
     ; standard_library_default =
         "/home/palmskog/.opam/4.11.1.coqdev/lib/ocaml"
     ; standard_library = "/home/palmskog/.opam/4.11.1.coqdev/lib/ocaml"
     ; standard_runtime = "the_standard_runtime_variable_was_deleted"
     ; ccomp_type = "cc"
     ; c_compiler = "gcc"
     ; ocamlc_cflags = [ "-O2"; "-fno-strict-aliasing"; "-fwrapv"; "-fPIC" ]
     ; ocamlc_cppflags = [ "-D_FILE_OFFSET_BITS=64"; "-D_REENTRANT" ]
     ; ocamlopt_cflags =
         [ "-O2"; "-fno-strict-aliasing"; "-fwrapv"; "-fPIC" ]
     ; ocamlopt_cppflags = [ "-D_FILE_OFFSET_BITS=64"; "-D_REENTRANT" ]
     ; bytecomp_c_compiler =
         [ "gcc"
         ; "-O2"
         ; "-fno-strict-aliasing"
         ; "-fwrapv"
         ; "-fPIC"
         ; "-D_FILE_OFFSET_BITS=64"
         ; "-D_REENTRANT"
         ]
     ; bytecomp_c_libraries = [ "-lm"; "-ldl"; "-lpthread" ]
     ; native_c_compiler =
         [ "gcc"
         ; "-O2"
         ; "-fno-strict-aliasing"
         ; "-fwrapv"
         ; "-fPIC"
         ; "-D_FILE_OFFSET_BITS=64"
         ; "-D_REENTRANT"
         ]
     ; native_c_libraries = [ "-lm"; "-ldl" ]
     ; native_pack_linker = [ "ld"; "-r"; "-o" ]
     ; cc_profile = []
     ; architecture = "amd64"
     ; model = "default"
     ; int_size = 63
     ; word_size = 64
     ; system = "linux"
     ; asm = [ "as" ]
     ; asm_cfi_supported = true
     ; with_frame_pointers = false
     ; ext_exe = ""
     ; ext_obj = ".o"
     ; ext_asm = ".s"
     ; ext_lib = ".a"
     ; ext_dll = ".so"
     ; os_type = "Unix"
     ; default_executable_name = "a.out"
     ; systhread_supported = true
     ; host = "x86_64-pc-linux-gnu"
     ; target = "x86_64-pc-linux-gnu"
     ; profiling = false
     ; flambda = false
     ; spacetime = false
     ; safe_string = true
     ; exec_magic_number = "Caml1999X028"
     ; cmi_magic_number = "Caml1999I028"
     ; cmo_magic_number = "Caml1999O028"
     ; cma_magic_number = "Caml1999A028"
     ; cmx_magic_number = "Caml1999Y028"
     ; cmxa_magic_number = "Caml1999Z028"
     ; ast_impl_magic_number = "Caml1999M028"
     ; ast_intf_magic_number = "Caml1999N028"
     ; cmxs_magic_number = "Caml1999D028"
     ; cmt_magic_number = "Caml1999T028"
     ; natdynlink_supported = true
     ; supports_shared_libraries = true
     ; windows_unicode = false
     }
 }
Running[1]: (cd _build/default && /home/palmskog/.opam/4.11.1.coqdev/bin/coqdep -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/boot -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/clib -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/config -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/engine -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/gramlib -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/interp -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/kernel -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/lib -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/library -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/parsing -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/plugins/ltac -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/pretyping -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/printing -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/proofs -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/stm -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/sysinit -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/tactics -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/vernac -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/vm -I /home/palmskog/.opam/4.11.1.coqdev/lib/findlib -I /home/palmskog/.opam/4.11.1.coqdev/lib/ocaml -I /home/palmskog/.opam/4.11.1.coqdev/lib/ocaml/threads -I /home/palmskog/.opam/4.11.1.coqdev/lib/zarith -I . -R . dpdgraph -dyndep opt dpdgraph.v) > _build/default/dpdgraph.v.d
File "_unknown_", line 1, characters 0-0:
Command [1] exited with code 1:
$ (cd _build/default && /home/palmskog/.opam/4.11.1.coqdev/bin/coqdep -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/boot -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/clib -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/config -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/engine -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/gramlib -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/interp -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/kernel -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/lib -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/library -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/parsing -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/plugins/ltac -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/pretyping -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/printing -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/proofs -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/stm -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/sysinit -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/tactics -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/vernac -I /home/palmskog/.opam/4.11.1.coqdev/lib/coq-core/vm -I /home/palmskog/.opam/4.11.1.coqdev/lib/findlib -I /home/palmskog/.opam/4.11.1.coqdev/lib/ocaml -I /home/palmskog/.opam/4.11.1.coqdev/lib/ocaml/threads -I /home/palmskog/.opam/4.11.1.coqdev/lib/zarith -I . -R . dpdgraph -dyndep opt dpdgraph.v) > _build/default/dpdgraph.v.d
*** Error: in file dpdgraph.v, could not find META.coq-dpdgraph.

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

oh it seems to have dumped into rules

view this post on Zulip Ali Caglayan (May 09 2022 at 11:23):

There is an option to dune rules called -o FILE where you can pass the output file.

view this post on Zulip Ali Caglayan (May 09 2022 at 11:23):

I guess it decides internally not to print to stdout when there is a lot of output

view this post on Zulip Ali Caglayan (May 09 2022 at 11:24):

There is probably a file called rules however, thats what happened to me

view this post on Zulip Karl Palmskog (May 09 2022 at 11:24):

dune rules -o dump gives nothing

view this post on Zulip Ali Caglayan (May 09 2022 at 11:28):

Oh I've worked out whats wrong

view this post on Zulip Ali Caglayan (May 09 2022 at 11:28):

I'm trying dune master

view this post on Zulip Ali Caglayan (May 09 2022 at 11:33):

Actually I have no idea whats wrong anymore :/

view this post on Zulip Karl Palmskog (May 09 2022 at 11:35):

here's one more twist in the story: once I split into src and theories, seems like the "could not find META.coq-dpdgraph" error disappears

view this post on Zulip Karl Palmskog (May 09 2022 at 11:38):

I guess it might be because then the OCaml stuff is fully compiled (with META) before coqdep even runs on the plugin .v file

view this post on Zulip Ali Caglayan (May 09 2022 at 11:41):

I suspect you will still get the error if you do dune build theories tho.

view this post on Zulip Ali Caglayan (May 09 2022 at 11:41):

I think its just that now it happens to build src first

view this post on Zulip Ali Caglayan (May 09 2022 at 11:41):

Maybe because [s]rc comes before [t]heories in the alphabet? who knows

view this post on Zulip Karl Palmskog (May 09 2022 at 11:42):

Dune knows that the .v file depends on the src part. When the src stuff is compiled, it generates the META. Then, coqdep is called on the .v file without error.

view this post on Zulip Ali Caglayan (May 09 2022 at 11:43):

hmm ok so it is really an issue with mixing .ml and .v files

view this post on Zulip Ali Caglayan (May 09 2022 at 11:43):

Let's cc @Rudi Grinberg for when he is around later

view this post on Zulip Karl Palmskog (May 09 2022 at 11:43):

it seems like Dune processes dune files sequentially? The src/dune file is handled before the theories/dune file

view this post on Zulip Karl Palmskog (May 09 2022 at 11:45):

but this error will bite anyone who has .ml and .v and plugin in the same directory.

view this post on Zulip Rudi Grinberg (May 09 2022 at 14:29):

It seems like the coqdep rules aren’t completely specified. We can try sandboxing the rules to see if the rules fail then?

view this post on Zulip Rudi Grinberg (May 09 2022 at 14:30):

But for some background knowledge first, why does coqdep need to read META files?

view this post on Zulip Karl Palmskog (May 09 2022 at 14:31):

I can't explain the exact technicalities, but here is the content of the file that coqdep fails on:

Declare ML Module "coq-dpdgraph.plugin".

So presumably this has to do with plugin linking.

view this post on Zulip Ali Caglayan (May 09 2022 at 14:32):

Rudi Grinberg said:

But for some background knowledge first, why does coqdep need to read META files?

That was the findlib change by @Enrico Tassi I believe.

view this post on Zulip Karl Palmskog (May 09 2022 at 14:33):

my guess is that coqdep tries to be smart and emit all the OCaml modules in the plugin (coq-dpdgraph.plugin in this case) as dependencies, and it does this by looking at the META

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

Coq dpdgraph is using the new Declare ML Module form which is not supported by dune

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

you need to revert to the previous form Declare ML Module "coq_dppgraph_plugin" or something like that, history will help.

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

I'm not sure the way the findlib plugin loader was implemented in Coq can be made to work with dune

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

We had a lot of discussion and at several points I convinced myself of yes, then not, then yes. I don't remember

view this post on Zulip Enrico Tassi (May 09 2022 at 15:23):

The META file is used to turn a public findlib name into a cmxs file. That is the dependency one needs, from the v file loading a plugin to the corresponding cmxs file.

view this post on Zulip Karl Palmskog (May 09 2022 at 15:27):

OK, so now we seem to have mixed messages. Is it not recommended to use Dune at all with plugins then?

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

@Karl Palmskog with the new loading system it just doesn't work

view this post on Zulip Karl Palmskog (May 09 2022 at 15:36):

not even with the old form of Declare ML Module?

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

The old form should work, but it'd be better if we could port Dune to use the new one

view this post on Zulip Ali Caglayan (May 09 2022 at 15:41):

Doesn't dune have compatibility patch support?

view this post on Zulip Ali Caglayan (May 09 2022 at 15:41):

That way we could add something that patches the new plugin name to the old plugin name before dune builds?

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

I'm not sure what you mean

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

Nevermind, I must have misremembered.

view this post on Zulip Rudi Grinberg (May 09 2022 at 17:20):

Anyway, I don't see the problem with fixing this. If coqdep is emitting the dependency on a library, it's easy to add it with dune.

view this post on Zulip Rudi Grinberg (May 09 2022 at 17:24):

It's definitely not optimal to depend on the entire META though. It will cause cycle issues that will cause ugly workarounds.

view this post on Zulip Enrico Tassi (May 10 2022 at 06:46):

@Rudi Grinberg would you mind looking at my points here: https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users/topic/Dune.20and.20plugins.20in.208.2E16

view this post on Zulip Enrico Tassi (May 10 2022 at 06:47):

I don't know the internals of dune, so I can't fix this myself

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2022 at 12:04):

Enrico Tassi said:

I don't know the internals of dune, so I can't fix this myself

I can fix that, but sorry Enrico what I don't know what the change we need is


Last updated: Feb 01 2023 at 15:04 UTC