coq / platform

Multi platform setup for Coq, Coq libraries and tools
Creative Commons Zero v1.0 Universal
186 stars 49 forks source link

[windows] Newer SerAPI versions fail to build to path length limit #331

Closed ejgallego closed 3 months ago

ejgallego commented 1 year ago

Newer versions of SerAPI do produce files that are too long for windows:

# Error: I/O error: serlib/plugins/syntax/.serlib_number_string_notation_plugin.objs/byte\serlib_number_string_notation_plugin.cmt93d942.tmp: No such file or directory
# Error:
# _build/default/serlib/plugins/syntax/.serlib_number_string_notation_plugin.objs/serlib_number_string_notation_plugin__Ser_number.impl.all-deps:
# No such file or directory

This can be solved by patching SerAPI sources, however it can still become a problem eventually due the long nesting in opam switches.

Not sure how to best solve this.

MSoegtropIMC commented 1 year ago

As discussed in Zulip I would long term recommend to disable the path length restriction in Windows by a registry switch as explained here:

https://learn.microsoft.com/en-us/windows/win32/fileio/maximum-file-path-limitation?tabs=registry#enable-long-paths-in-windows-10-version-1607-and-later

This works since the "anniversary update" of Windows 10 (2016) - so on all maintained Windows systems.

BUT there are several places in OCaml and related insfrastructure which restrict path length on their own on Windows based on the MAX_PATH Windows C API define. This must be removed to work.

I checked that cygwin (which we are using to build Coq Platform) can handle arbitrary length paths (some things get funny beyond 4k) if the above registry change is made.

ejgallego commented 7 months ago

Hi folks,

I've closed ejgallego/coq-serapi#377 in favor of this issue, as it was a duplicate, however note the useful information there.

Also it seems to me that we could close #358 if we find a solution for this.

Manas Jayanth was very kind to provide us with some more info about OCaml path lenght and Windows:

Have you had the chance to read my post on the forum?

https://discuss.ocaml.org/t/ocaml-on-windows-the-long-paths-issue/13283

I found this while working on LIGO, I believe this is the last commit that built on Windows correctly: https://gitlab.com/ligolang/ligo/-/commit/b3f561b8d530a7c49a7f504b8ae558475fd2982b

It needed long paths support.

Also Manas pointed out to these remarks by David to their post on discuss:

Nice! Thanks for writing it up :slightly_smiling_face: For me personally, the focus is steering OCaml 5.x back to having MSVC support (part of finishing off restoring what was "broken" by the multicore merge) but this is the kind of thing which I hope will be able to get more upstream support in the future. In particular, we need to have a big overhaul of the "minimum Windows version"... OCaml 5.2, or possibly 5.3, is likely to raise the Win32 API minimum to needing Windows 8.1, and there are lots of things like this where we can start to take advantage of not being remotely compatible with old versions of Windows. I wouldn't expect the compiler work for this to be too bad, because we already have our linker (in flexlink) which can apply manifests (it does that already on MSVC)... but it's really neat that you've been able to make it work transparently in esy without needing the upstream support straightaway!

NB I've draw a difference between our "supported" versions of Windows and the "required" minimum version of Windows. I don't think the README files on ocaml/ocaml are properly up-to-date, but we support Windows 10 and 11 but, at least time I checked, OCaml programs still run on Windows Vista and Windows 7 but not on Windows 2000 or XP, so we support Windows 10 & 11 but we require Windows Vista.

MSoegtropIMC commented 7 months ago

@ejgallego : thanks for the pointers. I have already seen that setting the registry entry is not enough, but that one needs the manifest in addition (possibly only this).

The question is what is the best point to manifest all involved executables. One could do it in a somewhat hacky way, say go over the bin folder after coq is installed, but I would prefer a more tool supported solution. So it should either be build into the OCaml linker or into dune.

ejgallego commented 7 months ago

Indeed it would be great to get native OCaml support; I guess the next step for us is to check if an upstream issue does exist, or else forward this issue upstream so we can involve the rest of the OCaml windows team in the discussion.

MSoegtropIMC commented 3 months ago

Fixed by commit 315c006