compile-before-require stumbles on .cmxs files (OCaml plug-ins)

[vbgl]

With PG-4.4.1~pre at 73792323172e289b531afc086d3f97323b28ecb6 with Coq-8.8 at 37d464bf9c36a8f52b42a509a31739e8afb96f1d, I’m trying to Require (with compile-before-require enabled; when this option is disabled, everything works fine) the loader for the toy plug-in at https://github.com/ybertot/plugin_tutorials/blob/35b4f622a118cccf5e8dd961dd75b31c3ea9e5fd/tuto3/theories/Loader.v PG fails at understanding a .cmxs (OCaml dynamically linked library) dependency of this module.

Here is what coqdep returns:

$ coqdep -R theories Tuto3 -I src theories/Loader.v
theories/Loader.vo theories/Loader.glob theories/Loader.v.beautified: theories/Loader.v theories/Data.vo src/tuto3_plugin.cmo src/tuto3_plugin.cmxs
theories/Loader.vio: theories/Loader.v theories/Data.vio src/tuto3_plugin.cmo src/tuto3_plugin.cmxs

The *coq-compile-response* buffer shows:

-*- mode: compilation; -*-

coqc -I …/plugin_tutorials/tuto3/src -R …/plugin_tutorials/tuto3/theories Tuto3 …/plugin_tutorials/tuto3/src/tuto3_plugin.cmx
Warning:
File "…/plugin_tutorials/tuto3/src/tuto3_plugin.cmx"
has been implicitly expanded to
"…/plugin_tutorials/tuto3/src/tuto3_plugin.cmx.v"
[file-no-extension,filesystem]
Error:
Can't find file
…/plugin_tutorials/tuto3/src/tuto3_plugin.cmx.v

The *Messages* buffer shows:

Check …/plugin_tutorials/tuto3/theories/Loader.vo
Check …/plugin_tutorials/tuto3/theories/Data.vo
Check …/plugin_tutorials/tuto3/src/tuto3_plugin.cmo
coq-auto-compile: no source file for …/plugin_tutorials/tuto3/src/tuto3_plugin.cmo
Check …/plugin_tutorials/tuto3/src/tuto3_plugin.cmxs
Recompile …/plugin_tutorials/tuto3/src/tuto3_plugin.cmx
proof-extend-queue: ERROR: Recompiling coq library …/plugin_tutorials/tuto3/src/tuto3_plugin.cmx terminated with exit status 1

[hendriktews]

Sorry for the late reply, but this is a known limitation, which is highlighted several times in the documentation.

[vbgl]

You mean the documentation there: https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#index-coq_002dcompile_002dbefore_002drequire?

[hendriktews]

I actually mean "The compilation feature does currently not support ML modules." in 11.3 (https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Multiple-File-Support) and "No support Declare ML Module commands." in 11.3.5 (https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Current-Limitations).

I have never looked into ML modules, therefore the limitation. I would be interested to work with somebody together who is interested in this feature and knows enough about ML module compilation.