Issues building coq-elpi.1.19.3 on Windows (Coq Platform. cygwin MinGW cross)

[MSoegtropIMC]

I have issue sbuilding coq-elpi.1.19.3 in Coq Platform for Windows.

I added a dune patch which fixed most Windows build issues, but this remains.

The error message is:

OCAMLLIBDEP src/elpi_coercion_plugin.mlpack
COQDEP VFILES
FILL .merlin
CAMLOPT -c -for-pack Elpi_coercion_plugin src/coq_elpi_coercion_hook.ml
ocamlfind: Package `coq-elpi.elpi' not found
make[3]: *** [Makefile.coq:757: src/coq_elpi_coercion_hook.cmx] Error 2
make[2]: *** [Makefile.coq:409: all] Error 2
make[1]: *** [Makefile:15: build] Error 2

What I don't quite understand is how ocamlfind could possibly find a coq-elpi package before coq-elpi is installed.

I have:

$ ocamlfind list | grep elpi
elpi                (version: 1.17.4)
elpi.lexer_config   (version: 1.17.4)
elpi.parser         (version: 1.17.4)
elpi.trace          (version: n/a)
elpi.trace.ppx      (version: 1.17.4)
elpi.trace.runtime  (version: 1.17.4)
elpi.util           (version: 1.17.4)

Is there a mechanism that ocamlfind looks for packages in the local build folders?

[gares]

I think coqc passes all the paths given via -I to ocamlfind's initialization. See:

https://github.com/coq/coq/blob/8d0d5471677699a14fdd6872ed8e3df4d16c709b/sysinit/coqinit.ml#L144

and I have -I src/ in _CoqProject and I do also have a META.coq-elpi in src/

[gares]

FTR, I did not change thing recently

[MSoegtropIMC]

I, see - let me see if I can find it with this information.

I btw. tested if it works without my ocamlfind reloction patches for installers (which are used on all platforms) - it also doesn't work.

It is likely some sort of Windows path normalization issue, but right now I don't see what happens - you seem to use relative paths only - which is good.

FTR, I did not change thing recently

The last version I used successfully was elpi.1.16.9 coq-elpi.1.17.1.

[MSoegtropIMC]

One question: you have an entry src/META.coq-elpi in your _CoqProject file - I wonder what effects this has. Is this file processed in some way?

[gares]

I think it is passed to coqdep -m so that it knows how to process directives like Declare ML Module "coq-elpi.plugin".

[gares]

given the error message it seems that it is the call to findlib (the binary) which is wrong. I think I found it: https://github.com/LPCIC/coq-elpi/blob/e1ee4432c40ccf489d3ae9948e7274fae4cd8286/apps/coercion/Makefile.coq.local#L2 on windows the separator should be ; and not : (as we do in the ocaml code I link above) In Coq's CI makefiles we do

if which cygpath >/dev/null 2>&1; then OCAMLFINDSEP=\;; else OCAMLFINDSEP=:; fi

I'll craft a patch