Michael Soegtrop (Apr 03 2023 at 17:16): Michael Soegtrop (Apr 03 2023 at 17:16):I just tried to build 8.17.0 on Windows. After copying all the opam packages to the Coq Platform local repo (the MinGW repo doesn't seem to be updated any more, dune 3.7.0 e.g. is also missing) it starts building, but run into this error:
Error:
_build/default/plugins/syntax/.number_string_notation_plugin.objs/number_string_notation_plugin__String_notation.impl.all-deps:
No such file or directory
-> required by
_build/default/plugins/syntax/.number_string_notation_plugin.objs/number_string_notation_plugin__String_notation.impl.all-deps
-> required by _build/default/plugins/syntax/number_string_notation_plugin.a
-> required by
_build/install/default/lib/coq-core/plugins/number_string_notation/number_string_notation_plugin.a
-> required by _build/default/coq-core.install
-> required by alias install
Error:
_build/default/plugins/syntax/.number_string_notation_plugin.objs/number_string_notation_plugin__String_notation.intf.all-deps:
No such file or directory
-> required by
_build/default/plugins/syntax/.number_string_notation_plugin.objs/number_string_notation_plugin__String_notation.intf.all-deps
-> required by
_build/default/plugins/syntax/.number_string_notation_plugin.objs/byte/number_string_notation_plugin__String_notation.cmi
-> required by
_build/install/default/lib/coq-core/plugins/number_string_notation/number_string_notation_plugin__String_notation.cmi
-> required by _build/default/coq-core.install
-> required by alias install
A ls -l in the respective build directory gives:
~/.opam/__coq-platform.2023.03+preview1~8.17~2023.03+beta1/.opam-switch/build/coq-core.8.17.0/_build/default/plugins/syntax
$ ls -l
total 65
-r-xr-xr-x 1 Michael None 22859 Apr 3 19:00 g_number_string.ml
-r-xr-xr-x 1 Michael None 3670 Apr 3 19:00 g_number_string.mlg
-r-xr-xr-x 1 Michael None 23647 Apr 3 19:00 number.ml
-r-xr-xr-x 1 Michael None 1729 Apr 3 19:00 number.mli
-r-xr-xr-x 1 Michael None 408 Apr 3 19:00 number_string_notation_plugin.ml-gen
-r-xr-xr-x 1 Michael None 3656 Apr 3 19:00 string_notation.ml
-r-xr-xr-x 1 Michael None 993 Apr 3 19:00 string_notation.mli
Any thoughts?
Emilio Jesús Gallego Arias (Apr 03 2023 at 17:20):@Michael Soegtrop that's a path length issue
Emilio Jesús Gallego Arias (Apr 03 2023 at 17:21):the new 8.17 plugin name for number_string_notation_plugin + the long path name already in the platform makes paths too long for Cygwin
Emilio Jesús Gallego Arias (Apr 03 2023 at 17:21):Quickest fix is to make the name of the opam switch a bit shorter
Emilio Jesús Gallego Arias (Apr 03 2023 at 17:22):or to rename the plugin, but obviously this whole path length problem is tricky
Michael Soegtrop (Apr 03 2023 at 17:26):Another option is to switch off the path length restriction in Windows. Not sure if this works though, cygwin might have it hard coded in it.
Emilio Jesús Gallego Arias (Apr 03 2023 at 17:27):If you could do that it would be great, not sure if that's possible indeed
Emilio Jesús Gallego Arias (Apr 03 2023 at 17:28):The quick fix for now (tried with my own CI) is to shorten the __coq-plaftorm.... name to something like cp+2023.03
Michael Soegtrop (Apr 03 2023 at 17:30):There is a registry switch. Essentially the restriction has been technically removed a while back in Windows, but it is kept to avoid that apps which don't expect this run into stack overwrite issues or the like.
Michael Soegtrop (Apr 03 2023 at 17:31):Not sure if cygwin belongs to these apps ... I will try. If this doesn't work I will shorten the switch name.
Michael Soegtrop (Apr 03 2023 at 17:33):Here are the docs
Michael Soegtrop (Apr 03 2023 at 18:28):@Emilio Jesús Gallego Arias : cygwin can handle paths of any length (I just tried 1000 nested folders with names 1...1000). Possibly the OCaml Windows wrappers or Dune assume that Windows can't handle this.
Michael Soegtrop (Apr 03 2023 at 18:28):This was btw. changed in Windows in 2016.
Emilio Jesús Gallego Arias (Apr 03 2023 at 18:29):I'm not expert, tho it seems strange that MAX_PATH can go so easily over 260
Paolo Giarrusso (Apr 03 2023 at 21:14):Tip Starting with Windows 10, version 1607, for the unicode version of this function (CreateFileW), you can opt-in to remove the MAX_PATH limitation without prepending "\\?\". See the "Maximum Path Length Limitation" section of Naming Files, Paths, and Namespaces for details.
From https://learn.microsoft.com/en-us/windows/win32/api/fileapi/nf-fileapi-createfilew
Paolo Giarrusso (Apr 03 2023 at 21:16):OTOH (from first link)
Because you cannot use the "\\?\" prefix with a relative path, relative paths are always limited to a total of MAX_PATH characters.
Paolo Giarrusso (Apr 03 2023 at 21:18):But this isn't a correction, and I'm no expert: it just means there's some more limited support for longer paths without the registry setting.
Paolo Giarrusso (Apr 03 2023 at 21:18):But I'm going to stop here and defer to Michael
Michael Soegtrop (Apr 04 2023 at 07:59):When the registry entry I mentioned (docs) is set (which one can usually do without admin rights) all paths (relative and absolute) are unlimited in size. Cygwin can handle this. The issue is that many programs use the MAX_PATH define, which (afaik) is 260. Also in the OCaml sources one can find occurrences of MAX_PATH. This must be removed for this registry setting to work.
Apparently the Coq build system is limited by hard codes MAX_PATH defines in a few places. We should work on removing these. I deduce this from the fact that setting the environment variable does not fix the Coq build. I didn't find anything obvious in the OCaml sources, but I am not sure were the sources for the patches MinGW OCaml are.
Michael Soegtrop (Apr 04 2023 at 08:11):P.S.: for this release I will work around the issue by shortening the switch name. I will run SysMon during the build and record all FileOpens to see what the max path length is, so that one can check the length of the base path (which depends on the cygwin install path and the user name) upfront. Likely this also gives some hint on where the restrictions in the Coq build process come from.
Last updated: Dec 05 2023 at 12:01 UTC