[windows] Platform binaries can't find libgmp-10.dll when called from a native app

[ejgallego]

For example, when opening VS Code and setting the coq-lsp server to the path, the binary will fail with the message "Can't find libgmp-10.dll`

This is "easily" solved by copying such file to C:\Windows, however it'd be nice if the Coq Platform could setup the right windows magic to this is not necessary.

Clarification on the particular setup:

• install the platform from souces
• Coq (and coq-lsp, etc...) binaries are placed in the corresponding opam folder
• now, if you go and try to run these binaries from the Windows Explorer, the error happens.

Desired result: it shouldn't happen as the binaries should be able to locate the .dll correctly.

[MSoegtropIMC]

@ejgallego : the libgmp-10.dll file does exist in the bin folder of the coq platform installation.

On Windows the only feasible way to make an executable file find a shared library are:

1.) the executable is in the same folder as the DLL (that is you copy coq-lsp into the Coq Platform bin folder, where it would end up if installed with Coq Platform

2.) you use the OCaml findlib modifications I added. This makes findlib work whenever the executable file or shared library requesting the load is somewhere in or below the Coq Platform installation root

Theoretically there is the option to add the Coq Platform bin folder to the PATH, but this would result in a complete disaster if one does this more than once, moves around an installation, installs several versions of Coq Platform, ...

So in summary there is absolutely nothing I can do in case you place the executable outside of the Coq Platform installation root and this is also not an intended use case.

For testing it would probably be best to symlink your executable into the Coq Platform install bin folder.

[MSoegtropIMC]

Please close in case this works for you, otherwise we should discuss in Zulip.

[ejgallego]

I forgot to add that this happened in a "install using the .sh script" platform setup. In this case the platform binaries won't be able to find the gmp dll, unless copied into C:\WINDOWS

I am unsure what PATH or findlib have to do here, isn't this purely an issue of windows dll registration?

[MSoegtropIMC]

@ejgallego : this is definitely not true. Many coq related binaries need GMP and if this would be true, nothing at all would work on Windows if installed by script. E.g. the smoke test kit could never succeed.

What does not work is linking GMP from an executable which is not in the Coq Platform bin folder. For stuff using findlib, I explained the mechanism (it is more relaxed).

The DLL search order for unpackages applications is documented here:

https://learn.microsoft.com/en-us/windows/win32/dlls/dynamic-link-library-search-order#standard-search-order-for-unpackaged-apps

The "PATH" is included in the search for unpackaged apps.

Registering DLLs is (afaik) intended for COM DLLs. You don't register a DLL as a named entity, but as a COM service provider - the services are identified by an interface GUID. This is a Windows specific mechanism not supported by any of the DLLs we are using, since they don't provide any COM services.

Packaging coq as app in the Windows sense could be done but wouldn't help you for anything which lives outside of this package either.

Copying DLLs to system32 would work, but for sure completely break the co installability of different Coq Platform versions - which is an advertised feature.

[ejgallego]

Yes copying is not a good solution.

Note that this problem happens in a very specific context when an app is launched directly from the explorer.

I need to retest again with the new information, but Serapi users on win told me that they had this problem since quite a bit of time.

[MSoegtropIMC]

The serapi delivered with the 2022.09 Coq Platform works as far as I know (I did some simple tests with it). The versions before indeed had issues.

It shouldn't matter how you start the the lsp server, but to work it should be in the Coq Platform bin folder - which will be the case if it is included in Coq Platform.

[MSoegtropIMC]

Triage note: closing since things work as expected.

[ejgallego]

@MSoegtropIMC as far as I can tell it seems to me that issue can be still reproduced with the steps I posted originally, and thus still valid.

[MSoegtropIMC]

@ejgallego: before 2025.01 the status was:

• works with an installed Coq Platform
• if vycoqtop is used from a cygwin installation, one has to set PATH so that cygwin supplied MinGW libraries are in PATH.

I declared this as "expected" because users of the "from sources" method can be expected to set the PATH.

in 2025.01 and main the status is:

• the Coq Platform setup script runs an additional script, which hard links all DLLs into the bin folder, so that the Windows loader finds them without setting PATH. (Hard link is OK because everything is under cygwin root).

The script is here: /~https://github.com/coq/platform/blob/main/windows/link_shared_libraries.sh
and it is called here:

platform/shell_scripts/post_system.sh

Line 17 in c64cb9a

/platform/windows/link_shared_libraries.sh

it is not called automatically if additional executables are installed via opam which use additional DLLs (which is rare), but one can call it manually in this case.

Can you please re-check?

[ejgallego]

Dear @MSoegtropIMC , thanks for the information. Indeed, updating PATH or copying the .dll solve the problem.