Build failure when "Compile Before Require" meets imported OCaml plugins

[RalfJung]

To reproduce, try building https://gitlab.mpi-sws.org/iris/diaframe. This needs Coq 8.17 (8.18 does not seem to work for other reasons). The dependencies can be installed as described here; then run make -jN and make testexamples -jN. Then open supplements/diaframe_heap_lang_examples/comparison/spin_lock.v in PG and step to the end of a file.

I get an error:

*** Error: in file
           /home/r/Dokumente/Unisachen/iris/coq-users/diaframe/diaframe/utils_ltac2.v,
           could not find META.coq-diaframe.

This shouldn't happen, since everything works fine in make. If I just disable "Compile Before Require", things also work fine. Opening that utils_ltac2.v file and stepping to the end, everything works fine. So it seems like it's something about "Compile Before Require" building the file in a way that is different both from what make does and what PG does when opening the file directly, and it leads to this error.

This is with PG 19ca6e0 built from source. Relevant part of my .emacs:

 '(coq-compile-before-require t)
 '(coq-compile-parallel-in-background t)
 '(coq-compile-quick 'no-quick)
 '(coq-compile-vos 'vos)
 '(coq-one-command-per-line nil)

 '(proof-follow-mode 'followdown)
 '(proof-next-command-insert-space nil)
 '(proof-splash-enable nil)
 '(proof-three-window-enable t)
 '(proof-three-window-mode-policy 'hybrid)

[hendriktews]

Hi, thanks for the report!

Can you check proof-omit-proofs-option (C-h v proof-omit-proofs-option)? If it is t, please try again after setting it to nil.

[RalfJung]

I've only set the options listed above, everything else is at default level.

The command you described says "Its value is nil".

[hendriktews]

OCaml plugins are not supported, see https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Current-Limitations, nevertheless I wanted to investigate, but I was not able to install diaframe.

I have an opam switch with

coq            8.17.1                    pinned to version 8.17.1
coq-core       8.17.1                    The Coq Proof Assistant -- Core Binaries and Tools
coq-iris       dev.2024-02-05.0.a013468e A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-stdlib     8.17.1                    The Coq Proof Assistant -- Standard Library
coq-stdpp      dev.2024-02-02.1.a2456618 An extended "Standard Library" for Coq
coqide-server  8.17.1                    The Coq Proof Assistant, XML protocol server
dune           3.13.1                    Fast, portable, and opinionated build system
ocaml          4.14.1                    The OCaml compiler (virtual package)
ocaml-config   2                         OCaml Switch Configuration
ocaml-variants 4.14.1+options            Official release of OCaml 4.14.1
ocamlfind      1.9.6                     A library manager for OCaml
zarith         1.13                      Implements arithmetic and logical operations over arbitrary-precision integers

then I did

git clone https://gitlab.mpi-sws.org/iris/diaframe.git
cd diaframe/
make builddep-opamfiles
opam pin add builddep/

The last command reports an error "Missing dependency: coq >= 8.18". I nevertheless continued with

make -j 12 diaframe diaframe-heap-lang test

which quickly failed with

File "diaframe/ocaml/define_my_primitive.ml", line 8, characters 37-51:
8 |   Tac2env.define_primitive (pname x) (of_closure y)

How should I setup things to be able to do make in diaframe?

[RalfJung]

OCaml plugins are not supported, see https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General/#Current-Limitations, nevertheless I wanted to investigate, but I was not able to install diaframe.

Oh, I didn't know that. Well that is unfortunate... lucky enough things work just fine when I disable "compile before require".

How should I setup things to be able to do make in diaframe?

Seems like diaframe recently dropped support for Coq 8.17, so you'll have to update to Coq 8.18. Not sure why opam didn't do that by itself, maybe try opam install coq.8.18.0 and then again opam pin add builddep/.

[hendriktews]

OK, I can reproduce now.
Previously opam did not install 8.18, because I pinned 8.17, because you wrote 8.18 does not work.
Plugins being not supported means that auto-compilation does not and cannot (re-)build plugins. This would certainly hit you when you start without building or when you change a plugin. The error reported here however is a different problem.
The problem here is that coqdep fails on diaframe/diaframe/utils_ltac2.v. The failing coqdep command line contains all the -Q and -I options from _CoqProject, however, it does not contain any -m option that would point coqdep to your META file diaframe/ocaml/META.coq-diaframe.
Can you confirm that the coqdep command line generated by make contains -m diaframe/ocaml/META.coq-diaframe?

[RalfJung]

Can you confirm that the coqdep command line generated by make contains -m diaframe/ocaml/META.coq-diaframe?

I think the answer is yes:

"coqdep" -m "diaframe/ocaml/META.coq-diaframe" -vos -dyndep var -f ._CoqProject_make   > ".CoqMakefile.d" || ( RV=$?; rm -f ".CoqMakefile.d"; exit $RV )

[hendriktews]

OK, thanks for the quick answer. Do you know if this -m option is added automatically by coq_makefile or if somebody did something special to get it added?

[hendriktews]

A simple work around is to add this -m option manually, unfortunately there was no user option in the code to do this. I added this in PR #735. Note that you have to use absolute path', because coqdep does also run in /tmp on temp files. Best do in .dir-locals.el, eg

((nil .
      ((coq-compile-extra-coqdep-arguments
        . ("-m" "/home/tews/coq/diaframe/diaframe/ocaml/META.coq-diaframe")))))

[RalfJung]

OK, thanks for the quick answer. Do you know if this -m option is added automatically by coq_makefile or if somebody did something special to get it added?

No idea... the diaframe makefile contains a bunch of stuff I can't see through.
I'll try to forward this question to its author.

[snyke7]

Author here, I have not heard of this -m option before, so I guess coq_makefile adds it automatically..?

[hendriktews]

Yes, it is difficult to find documentation about it, but coq/coq#15220 referenced in
https://coq.inria.fr/doc/V8.19.0/refman/changes.html#id579 states that coq_makefile adds the -m option for a META found in _CoqProject.

[hendriktews]

I suggest to close this issue now in favor of #736, which is more to the point.

[RalfJung]

Yes makes sense. Thanks for the investigation!