"Argument list too long" error when installing coq-unimath

[DCNick3]

I've made a minimal installation of coq platform (option i in the installer). After this, an attempt to install UniMath with opam install 'coq-unimath' leads to an error:

The following actions will be performed:
  ∗ install coq-unimath 20230321

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved coq-unimath.20230321  (https://github.com/UniMath/UniMath/archive/refs/tags/v20230321.tar.gz)
[ERROR] The installation of coq-unimath failed at "make BUILD_COQ=no install".

#=== ERROR while installing coq-unimath.20230321 ==============================#
# context     2.1.5 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.13.1+options | https://coq.inria.fr/opam/released#2023-07-20 07:40
# path        ~/.opam/__coq-platform.2022.09.1~8.16~2022.09/.opam-switch/build/coq-unimath.20230321
# command     ~/.opam/opam-init/hooks/sandbox.sh install make BUILD_COQ=no install
# exit-code   2
# env-file    ~/.opam/log/coq-unimath-254968-af0cc7.env
# output-file ~/.opam/log/coq-unimath-254968-af0cc7.out
### output ###
# ulimit -v unlimited ; make -f build/CoqMakefile.make all
# make[1]: Entering directory '/home/dcnick3/.opam/__coq-platform.2022.09.1~8.16~2022.09/.opam-switch/build/coq-unimath.20230321'
# make[2]: Nothing to be done for 'real-all'.
# make[1]: Leaving directory '/home/dcnick3/.opam/__coq-platform.2022.09.1~8.16~2022.09/.opam-switch/build/coq-unimath.20230321'
# ulimit -v unlimited ; make -f build/CoqMakefile.make install
# make[1]: Entering directory '/home/dcnick3/.opam/__coq-platform.2022.09.1~8.16~2022.09/.opam-switch/build/coq-unimath.20230321'
# make[1]: /bin/sh: Argument list too long
# make[1]: *** [build/CoqMakefile.make:598: install] Error 127
# make[1]: Leaving directory '/home/dcnick3/.opam/__coq-platform.2022.09.1~8.16~2022.09/.opam-switch/build/coq-unimath.20230321'
# make: *** [Makefile:96: install] Error 2

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ ∗ install coq-unimath 20230321
└─ 
╶─ No changes have been performed
# Run eval (opam env) to update the current shell environment

The actual seems to be the /bin/sh: Argument list too long error...

I think the problem might be that the path to the target directory is too long? not sure though.

[MSoegtropIMC]

This is fixed in main with the 8.17 beta pick - it requires a patch to coq-makefile (to redirect the file list to a file). Which version of Coq did you use? One could back merge the fix to older versions of Coq.

See https://github.com/coq/platform/blob/main/opam/opam-repository/packages/coq-core/coq-core.8.17.0/files/0001-coq_makefile-put-file-to-install-list-in-file-instea.patch.

[MSoegtropIMC]

The issue appeared btw. with the new version of UniMath, which added a few files. With this the command line length for install exceeded 128k - which is a limit hard compiled into the Linux kernel (for whatever reason - neither macOS nor Windows have this).

[DCNick3]

I am using Coq 8.16, the latest release offered by the installer.

What should I do to backmerge it? (or is it something you should do?) Or would using an older version of package pick work?

[MSoegtropIMC]

No - if you want coq-unimath 20230321 you need a patched coq-makefile.

If you want to use Coq 8.16 it might work to copy the above patch file to a subfolder "files" of https://github.com/coq/platform/tree/main/opam/opam-repository/packages/coq/coq.8.16.1 and register it in the opam file https://github.com/coq/platform/blob/main/opam/opam-repository/packages/coq/coq.8.16.1/opam like here

platform/opam/opam-repository/packages/coq-core/coq-core.8.17.0/opam

Line 57 in 608b792

patches: [

.

It might be that you have to adjust the patch file from 8.17 to 8.16 - nut sure if the coq-makefile template changed.

You do these changes in your local copy of Coq Platform. If you build again it should work.

[DCNick3]

Do I need to re-run the ./coq_platform_make.sh script or does it link back to my coq platform directory?

[MSoegtropIMC]

You should run the script, because you need to update the opam repos - the script does this automatically. The script doesn't redo things it already finished before.

If you know how to do this, you can also update the opam repos manually and reinstall coq with opam.

[DCNick3]

I've decided to go the path of least resistance and install coq-unimath.20220816. Thanks for the help 😅

[MSoegtropIMC]

OK. I will anyway see that I back port the fix to 8.16.