Building Coq with Bazel - need help with plugins

Developing the Coq system
4

That’s an interesting project, but indeed building OCaml is not so easy. Quoting your message:

Hi folks. I need some help from anybody familiar with the Coq build system. I’m building Coq with Bazel, and I’ve got almost all of it working, but I’ve run into problems with some of the plugins. I’m using -pack and here’s the kind of problem I’m encountering:

$ bazel build plugins/ltac:Ltac_plugin
...
File "bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl/Ltac_plugin.cmx", line 1:
Error: File bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl/Pptactic.cmx
      was compiled without access to the .cmx file for module Tacarg,
      which was produced by `ocamlopt -for-pack'.
      Please recompile bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl/Pptactic.cmx
      with the correct `-I' option so that Tacarg.cmx is found.

I need help interpreting the precise meaning of this message. As far as I can tell, module Pptactic.cmx did have access to Tacarg.cmx , built with -for-pack Ltac_plugin , and all the relevant files are on the search path - the source files (.mli, .ml) and Tacarg.cmi , Tacarg.cmx , Tacarg.o are all right there in bazel-out/darwin-fastbuild/bin/plugins/ltac/__obazl , which was passed using -I to the build command for Pptactic .

I spent most of today trying to figure this one out, and I’m out of ideas. I suspect it must have something to do with the .cmi file, but I need to know exactly what “was compiled without access to” means, etc. If you can help let me know and I can post more info, here or in the OBazl discord server, or wherever is appropriate.

First note that Coq master will stop using -pack in (hopefully) a matter of days, we instead use module aliases for packing, you can check the OCaml manual for an overview of the differences between these two packing methods. As for your concrete problem, it is hard to say anything as you provided little information such as the build log of the project and the concrete ocamlc invocations.

A quick way to debug this is just compare the two build logs, and in concrete, the calls to ocamlc for Pptactic.ml and Tacarg.ml{,i}.