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
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
@Michael Soegtrop that's a path length issue
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
Quickest fix is to make the name of the opam switch a bit shorter
or to rename the plugin, but obviously this whole path length problem is tricky
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.
If you could do that it would be great, not sure if that's possible indeed
The quick fix for now (tried with my own CI) is to shorten the
__coq-plaftorm.... name to something like
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.
Not sure if cygwin belongs to these apps ... I will try. If this doesn't work I will shorten the switch name.
Here are the docs
@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.
This was btw. changed in Windows in 2016.
I'm not expert, tho it seems strange that MAX_PATH can go so easily over 260
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.
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.
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.
But I'm going to stop here and defer to Michael
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.
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