Karl Palmskog (May 09 2022 at 09:33): 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?
Ali Caglayan (May 09 2022 at 09:45):The coqdep rule is being run too eagerly and this is a bug in dune
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
Ali Caglayan (May 09 2022 at 09:45):If you run dune build twice you will see that it actually succeeds
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.
Ali Caglayan (May 09 2022 at 09:46):That will just point to the coq.theory stanza
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?
Ali Caglayan (May 09 2022 at 09:46):Yes, but the fact that it requires two builds isn't great
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
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.
Ali Caglayan (May 09 2022 at 09:53):We can then see what dune considers the dependencies of the coqdep rule
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.
Karl Palmskog (May 09 2022 at 09:55):I ran dune rules, but where is the dump?
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)
Ali Caglayan (May 09 2022 at 11:15):@Karl Palmskog Did it work?
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.
OK let's try --verbose too just in case
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.
oh it seems to have dumped into rules
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.
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
Ali Caglayan (May 09 2022 at 11:24):There is probably a file called rules however, thats what happened to me
Karl Palmskog (May 09 2022 at 11:24):dune rules -o dump gives nothing
Ali Caglayan (May 09 2022 at 11:28):Oh I've worked out whats wrong
Ali Caglayan (May 09 2022 at 11:28):I'm trying dune master
Ali Caglayan (May 09 2022 at 11:33):Actually I have no idea whats wrong anymore :/
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
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
Ali Caglayan (May 09 2022 at 11:41):I suspect you will still get the error if you do dune build theories tho.
Ali Caglayan (May 09 2022 at 11:41):I think its just that now it happens to build src first
Ali Caglayan (May 09 2022 at 11:41):Maybe because [s]rc comes before [t]heories in the alphabet? who knows
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.
Ali Caglayan (May 09 2022 at 11:43):hmm ok so it is really an issue with mixing .ml and .v files
Ali Caglayan (May 09 2022 at 11:43):Let's cc @Rudi Grinberg for when he is around later
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
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.
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?
Rudi Grinberg (May 09 2022 at 14:30):But for some background knowledge first, why does coqdep need to read META files?
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.
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.
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
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
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.
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
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
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.
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?
Emilio Jesús Gallego Arias (May 09 2022 at 15:35):@Karl Palmskog with the new loading system it just doesn't work
Karl Palmskog (May 09 2022 at 15:36):not even with the old form of Declare ML Module?
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
Ali Caglayan (May 09 2022 at 15:41):Doesn't dune have compatibility patch support?
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?
Emilio Jesús Gallego Arias (May 09 2022 at 15:49):I'm not sure what you mean
Ali Caglayan (May 09 2022 at 16:07):Nevermind, I must have misremembered.
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.
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.
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
Enrico Tassi (May 10 2022 at 06:47):I don't know the internals of dune, so I can't fix this myself
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: Oct 12 2024 at 12:01 UTC