No dpdgraph.cmxs file

[bfurmane]

Hi, I use Rocq 9.0.0 and build the coq-dpdgraph from source. When try to run make (after running autoconf && ./configure) i get

make

• build dpdgraph.vo
  make -f Make_coq dpdgraph.vo
  make[1]: Entering directory '/home/bfurmanek/documents/rtls.gpu.ip.fp-numerics/coq-dpdgraph'
  ROCQ compile dpdgraph.v
  File "./dpdgraph.v", line 1, characters 0-40:
  Error: System error: "./././dpdgraph.cmxs: No such file or directory"

make[1]: *** [Make_coq:818: dpdgraph.vo] Error 1
make[1]: *** [dpdgraph.vo] Deleting file 'dpdgraph.glob'
make[1]: Leaving directory '/home/bfurmanek/documents/rtls.gpu.ip.fp-numerics/coq-dpdgraph'
make: *** [Makefile:80: dpdgraph.vo] Error 2

The file dpdgraph.cmxs indeed does not exists in the coq-dpdgraph repository.

Best
Bart.

[ybertot]

I had a hard time figuring it out. Maybe the solution I will give here is not the right one, but it makes it possible to progress.

It seems the capability to compile but not install has been forgotten by recent updates. The dpdgraph.cmxs file is only built if the make install command is called. This is not satisfactory.

Starting from the archive coq-dpdgraph-1.0-9.0.tgz, with coq 9.0 install on opam, I manage to compile locally by doing the following operations:

./configure
make Make_coq
make -f Make_coq dpdgraph.cmxs
make

If I am right, this is a bug in the Makefile, that will need to be fixed.

[gares]

If you still have it, could you please post the entire compilation log?

[ybertot]

@bfurmane : It seems I am not able to reproduce the bug as you reported it on an ubuntu machine. On fedora machines, I am only able to reproduce it on fedora 40 machines, but not on fedora 42 machines.

The fix I propose in #148 is not correct, as it does not take into account the variability provided by the DYNLIB variable.

For now, I only understand that rocq dep produces a wrong file .Make_coq.d where dpdgraph$(DYNLIB) appears with a prefix when it should appear without prefix. rocq dep relies on other commands or configuration, but I don't know which one is wrong.

[ybertot]

Here is a solution to the problem, suggested by @gares

The problem is not at all related to the fact that one may be using ubuntu, fedora, or whatever version. It is related to the fact that you may have installed coq-dpdgraph in the switch where you are working.

YOU CANNOT COMPILE FROM THE SOURCES USING A SWITCH WHERE coq-dpdgraph IS ALREADY INSTALLED!

Before compilation, rocq dep is called on the file "dpdgraph.v", it discovers that the file dpdgraph.cmxs is needed. If coq-dpdgraph (as an opam package) is already installed, then the file $OPAM_SWITCH_PREFIX/lib/coq-dpdgraph/dpdgraph.cmxs is found, and a dependency to that file is added in the file .Make_coq.d

Because of this wrong dependency, when compiling dpdgraph.v, the make process does not understand that the local dpdgraph.cmxs file must be compiled, and this file appears to be missing.

So, the solution to be able to compile coq-dpdgraph from the sources is to make sure you uninstall coq-dpdgraph first, using the command:

opam uninstall coq-dpdgraph

[SkySkimmer]

Sounds like an instance of rocq-prover/rocq#20393

[gares]

So 9.1 is fixed already, great!

[ybertot]

I am not convinced. I performed the following experiment:

• compile coqdep.exe from the tip of the master branch.
• run that version of coqdep.exe using the options
  -I . -R . dpdgraph -coqlib $OPAM_SWITCH_PREFIX/lib/coq -dyndep opt dpdgraph.v

The output still declares a dependency on $OPAM_SWITCH_PREFIX/lib/coq-dpdgraph/dpdgraph.cmxs instead of dpdgraph.cmxs

[ybertot]

I have the feeling, that the rocq dep command does not describe a dependency on a local dpdgraph.cmxs file, because such a file does not exist yet, while it can fine an existing one, but not locally, and the existence overrules the requirement for a local one.

[SkySkimmer]

It may need the META to exist? Not sure

[gares]

The META is generated by coq_makefile, and I'm sure it generates it before calling coqdep, since coqdep is called by the generated makefile itself.

[ybertot]

Okay, I am now convinced that the fix rocq-prover/rocq#20393 is right.

Just to keep an explanation that I may find later in time: rocq dep dpdgraph.v is not happening here. What is happening is rocq dep -vos -dyndep var -f Make and the contents of Make explain that there is a dependence on dpgraph.mllib and searchdepend.mlg and graphdepend.mlg. The Make file contains the -generate-meta-for-package coq-dpdgraph, which guarantees that the file META.coq-dpdgraph is produced. The dependencies for dpdgraph.v are only computed later, so this presence is taken into account. More precisely:

• if dpdgraph.cmxs is already present in $OPAM_SWITCH_PREFIX and META.coq-dpdgraph is absent, then the results of rocq dep -I . -R . dpdgraph dpdgraph.v contains $OPAM_SWITCH_PREFIX/lib/coq-dpdgraph/dpdgraph.cmxs (which is incorrect)
• if we are using a version of rocq that contains the fix, dpdgraph.cmxs is already present in $OPAM_SWITCH_PREFIX and META.coq-dpdgraph has been generated correctly, then the results of rocq dep -I . -R . dpdgraph dpdgraph.v contains dpdgraph.cmxs (which is correct)
• if we are using a version of rocq that does not contain the fix (like rocq.9.0), dpdgraph.cmxs is already present in $OPAM_SWITCH_PREFIX and META.coq-dpdgraph has been generated correctly, then the results of rocq dep -I . -R . dpdgraph dpdgraph.v contains $OPAM_SWITCH_PREFIX/lib/coq-dpdgraph/dpdgraph.cmxs (which is incorrect).