2021.09.0: coq_platform_make.sh fails on ubuntu 21.10, ocaml-base-compiler compilation fails

[jibnew]

Chose full, 8.14, sequential, 2 jobs, compcert, vst
Excerpts from script output:

===== CHECKING VERSION OF INSTALLED OPAM =====
Found opam 2.1.1 - good!
/usr/local/bin/opam

...

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-base-compiler" {= "4.10.0"}]

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
⬇ retrieved ocaml-base-compiler.4.10.0  (https://opam.ocaml.org/cache)
[ERROR] The compilation of ocaml-base-compiler.4.10.0 failed at "make -j1 world.opt".

#=== ERROR while compiling ocaml-base-compiler.4.10.0 =========================#
# context              2.1.1 | linux/x86_64 |  | https://opam.ocaml.org#f00176f2
# path                 ~/.opam/__coq-platform.2021.09.0~8.14+beta2/.opam-switch/build/ocaml-base-compiler.4.10.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j1 world.opt
# exit-code            2
# env-file             ~/.opam/log/ocaml-base-compiler-470-7030e9.env
# output-file          ~/.opam/log/ocaml-base-compiler-470-7030e9.out
### output ###
# [...]
# gcc -c -O2 -fno-strict-aliasing -fwrapv -Wall -fno-common -fno-tree-vrp -ffunction-sections -g -D_FILE_OFFSET_BITS=64 -D_REENTRANT -DCAML_NAME_SPACE   -DNATIVE_CODE -DTARGET_amd64 -DMODEL_default -DSYS_linux   -o signals_n.o signals.c
# gcc -c -O2 -fno-strict-aliasing -fwrapv -Wall -fno-common -fno-tree-vrp -ffunction-sections -g -D_FILE_OFFSET_BITS=64 -D_REENTRANT -DCAML_NAME_SPACE   -DNATIVE_CODE -DTARGET_amd64 -DMODEL_default -DSYS_linux   -o signals_nat_n.o signals_nat.c
# signals_nat.c:194:13: error: variably modified ‘sig_alt_stack’ at file scope
#   194 | static char sig_alt_stack[SIGSTKSZ];
#       |             ^~~~~~~~~~~~~
# make[3]: *** [Makefile:341: signals_nat_n.o] Error 1
# make[3]: Leaving directory '/home/me/.opam/__coq-platform.2021.09.0~8.14+beta2/.opam-switch/build/ocaml-base-compiler.4.10.0/runtime'
# make[2]: *** [Makefile:1013: makeruntimeopt] Error 2
# make[2]: Leaving directory '/home/me/.opam/__coq-platform.2021.09.0~8.14+beta2/.opam-switch/build/ocaml-base-compiler.4.10.0'
# make[1]: *** [Makefile:419: opt.opt] Error 2
# make[1]: Leaving directory '/home/me/.opam/__coq-platform.2021.09.0~8.14+beta2/.opam-switch/build/ocaml-base-compiler.4.10.0'
# make: *** [Makefile:477: world.opt] Error 2



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build ocaml-base-compiler 4.10.0
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install base-bigarray base
│ ∗ install base-threads  base
│ ∗ install base-unix     base
└─

[MSoegtropIMC]

WSL is not officially supported because there are no CI means to test it, but if you help finding the root cause, we will of course fix it.

Can you please try the main branch - it has an updated OCaml compiler (4.10.2). If this doesn't work I would have to ask you to check which OCaml compilers do work. The easiest way to test this might be to change the OCaml version here:

(

platform/shell_scripts/install_opam.sh

Line 170 in 1ee2e0b

COQ_PLATFORM_OCAML_VERSION='ocaml-base-compiler.4.10.2'

)

and then to a "IDE" level Coq Platform build.

If you can't easily find a working OCaml version, this would more be a bug report for OCaml and or opam then for Coq Platform.

Btw.: on Windows the recommended method is to use Cygwin (there is a batch file in the root folder which sets up a suitable Cygwin). This is how we test Coq Platform on Windows in CI.

[jibnew]

Thanks a lot for your prompt reply!

WSL is not officially supported because there are no CI means to test it, but if you help finding the root cause, we will of course fix it.

Can you please try the main branch - it has an updated OCaml compiler (4.10.2). If this doesn't work I would have to ask you to check which OCaml compilers do work. The easiest way to test this might be to change the OCaml version here:

(

platform/shell_scripts/install_opam.sh

Line 170 in 1ee2e0b

COQ_PLATFORM_OCAML_VERSION='ocaml-base-compiler.4.10.2'

)

and then to a "IDE" level Coq Platform build.

If you can't easily find a working OCaml version, this would more be a bug report for OCaml and or opam then for Coq Platform.

Btw.: on Windows the recommended method is to use Cygwin (there is a batch file in the root folder which sets up a suitable Cygwin). This is how we test Coq Platform on Windows in CI.

I changed COQ_PLATFORM_OCAML_VERSION to ocaml-base-compiler.4.13.1 and with the IDE (but not full) level build everything works.

I now wonder if the IDE level would actually also work with 4.10.0 but never mind...

[Zimmi48]

I now wonder if the IDE level would actually also work with 4.10.0 but never mind...

The error happened when building the compiler, so it would be very surprising if the level had any impact. You should be able to check that you can now install the full platform by re-running the script (without undoing your change to the compiler version).

[MSoegtropIMC]

@jibnew : did you check if 4.10.2 does work? You originally tested with 4.10.0. I would find it difficult to change the OCaml version shortly before a release. If 4.10.2 doesn't work I would probably try to detect WSL then and use 4.13.1 just for WSL.

@Zimmi48, @ejgallego : I am always highly confused by OCaml version selection pros and cons. What is the latest lore on this?

[MSoegtropIMC]

P.S.: regarding the level for tests: for such tests one should test the IDE level because the IDE is technically very different from Coq and plugin code. The IDE level builds both Coq and CoqIDE, which should be a > 99.99% test of OCaml features we use.

[Zimmi48]

I am always highly confused by OCaml version selection pros and cons. What is the latest lore on this?

Selecting a major version can be difficult for the various reasons that we previously discussed. However, selecting the latest patch-level release should be a no brainer. If it works in CI, just do the update.

[MSoegtropIMC]

P.P.S.: to judge this properly, I think I would need IDE level build results for OCaml 4.11.3, OCaml 4.12.2 and OCaml 4.13.2 (this are the latest patch releases for 4.11, 4.12 and 4.13). I probably wouldn't use 4.13.1 unless 4.13.2 doesn't work.

@jibnew: Can you please do this? It would really help a lot. When Coq Platform asks if you want to keep or delete the switch, you have to say delete.

[MSoegtropIMC]

@Zimmi48 : well we are discussing 4.13.1 vs 4.10.2 here.

[jibnew]

I now wonder if the IDE level would actually also work with 4.10.0 but never mind...

The error happened when building the compiler, so it would be very surprising if the level had any impact. You should be able to check that you can now install the full platform by re-running the script (without undoing your change to the compiler version).

This was the first thing I did, it failed at the very end with several dependency errors. I next tried everything the same except IDE instead of full and it worked.

[MSoegtropIMC]

Can you tell us what failed?

[Zimmi48]

This was the first thing I did, it failed at the very end with several dependency errors.

That's not terribly surprising because of the issue discussed at https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/coq-bignums.20installation.20fails. I think your best bet is to try what @MSoegtropIMC said: test OCaml 4.10.2.

[jibnew]

Can you tell us what failed?

Here are the places with errors, I hope I don't miss any:

===== INSTALL PREREQUISITES =====
[ERROR] Package conflict!
  * No agreement on the version of ocaml:
    - (invariant) → ocaml-base-compiler >= 4.13.1 → ocaml = 4.13.1
    - elpi >= 1.13.7 → camlp5 < 7.99 → ocaml < 4.00.1
    You can temporarily relax the switch invariant with `--update-invariant'
  * No agreement on the version of ocaml-base-compiler:
    - (invariant) → ocaml-base-compiler >= 4.13.1
    - elpi >= 1.13.7 → camlp5 < 7.99 → ocaml = 3.12.1 → ocaml-base-compiler = 3.12.1
  * Missing dependency:
    - elpi >= 1.13.7 → camlp5 < 7.99 → ocaml = 3.12.1 → ocaml-variants >= 3.12.1 → ocaml-beta
    unmet availability conditions: 'enable-ocaml-beta-repository'

[WARNING] set was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to
          2.0.

...

The following actions will be performed:
  ∗ install coq-mathcomp-zify 1.1.0+1.12+8.13

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved coq-mathcomp-zify.1.1.0+1.12+8.13  (cached)
∗ installed coq-mathcomp-zify.1.1.0+1.12+8.13
Done.
[ERROR] Package conflict!
  * No agreement on the version of ocaml:
    - (invariant) → ocaml-base-compiler >= 4.13.1 → ocaml = 4.13.1
    - coq-mathcomp-analysis = 0.3.10 → coq-hierarchy-builder >= 0.10.0 → coq-elpi → ocaml < 4.12~
    You can temporarily relax the switch invariant with `--update-invariant'
  * No agreement on the version of ocaml-base-compiler:
    - (invariant) → ocaml-base-compiler >= 4.13.1
    - coq-mathcomp-analysis = 0.3.10 → coq-hierarchy-builder >= 0.10.0 → coq-elpi → elpi != 1.13.0~ → camlp5 <
      8.00~alpha01 → ocaml = 3.12.1 → ocaml-base-compiler = 3.12.1
  * Missing dependency:
    - coq-mathcomp-analysis = 0.3.10 → coq-hierarchy-builder >= 0.10.0 → coq-elpi → elpi < 1.13.0~ →
      ocaml-migrate-parsetree < 2.0.0 → ocaml-variants = 4.08.0+beta2 → ocaml-beta
    unmet availability conditions: 'enable-ocaml-beta-repository'
  * Missing dependency:
    - coq-mathcomp-analysis = 0.3.10 → coq-hierarchy-builder >= 0.10.0 → coq-elpi → elpi < 1.13.0~ →
      ocaml-migrate-parsetree < 2.0.0 → ocaml-variants = 4.08.0+beta3 → ocaml-beta
    unmet availability conditions: 'enable-ocaml-beta-repository'
  * Missing dependency:
    - coq-mathcomp-analysis = 0.3.10 → coq-hierarchy-builder >= 0.10.0 → coq-elpi → elpi != 1.13.0~ → camlp5 <
      8.00~alpha01 → ocaml = 3.12.1 → ocaml-variants >= 3.12.1 → ocaml-beta
    unmet availability conditions: 'enable-ocaml-beta-repository'

No solution found, exiting

I also tried with 4.13.2 but then it stops at the very beginning with

[ERROR] No compiler matching `ocaml-base-compiler.4.13.2' found, use `opam switch list-available' to see what is
        available, or use `--packages' to select packages explicitly.

And indeed opam list-available ends with

ocaml-base-compiler                    4.13.1                                 Official release 4.13.1
ocaml-variants                         4.13.1+options                         Official release of OCaml 4.13.1
ocaml-variants                         4.13.2+trunk                           Latest 4.13 developmet
ocaml-variants                         4.14.0+trunk                           Latest 4.14.0 development
ocaml-variants                         5.00.0+trunk                           Current trunk

How can I switch to 4.13.2?

[Zimmi48]

I also tried with 4.13.2 but then it stops at the very beginning with

4.10.2, not 4.13.2

[Zimmi48]

(the goal is to use an older version of OCaml, which we know is already compatible with the platform)

[jibnew]

I also tried with 4.13.2 but then it stops at the very beginning with

4.10.2, not 4.13.2

4.13.2 was mentioned by MSoegtropIMC as preferred over 4.13.1, that's why I was asking.

[jibnew]

(the goal is to use an older version of OCaml, which we know is already compatible with the platform)

4.10.2 throws exactly the same error as the untouched script (with 4.10.0), as in my very first post

[MSoegtropIMC]

I think we can delay the 4.13.1 vs 4.13.2 question until later. It is odd - the Coq Platform calls opam update and at least I see 4.13.2.

So to summarize:

4.10.0 and 4.10.2 fail at the compilation of the compiler.

4.13.1 works for IDE build, but you have issues with elpi and everything which depends on it.

Did you try the OCaml version in between (latest 4.11 and latest 4.12)?

[jibnew]

I think we can delay the 4.13.1 vs 4.13.2 question until later. It is odd - the Coq Platform calls opam update and at least I see 4.13.2.

So to summarize:

4.10.0 and 4.10.2 fail at the compilation of the compiler.

Confirmed.

4.13.1 works for IDE build, but you have issues with elpi and everything which depends on it.

No no dependency errors only show up at the full level.

Did you try the OCaml version in between (latest 4.11 and latest 4.12)?

I have not. Will try at some point, right now I just stick to the IDE version.

[MSoegtropIMC]

No no dependency errors only show up at the full level.

yes, this is clear - elpi is part of the "full" level.

[jibnew]

No no dependency errors only show up at the full level.

yes, this is clear - elpi is part of the "full" level.

Full level also fails using both 4.11.2 and 4.12.1, with the same error as for 4.10.0 and 4.10.2 (sig_alt_stack in signals_nat.c)

[jibnew]

4.12.1 also fails with the IDE level chosen, wit the same sig_alt_stack error

[Zimmi48]

Yes, this makes sense: the errors below 4.13 are related to building the OCaml compiler itself, so the failures happen whatever level is chosen. OCaml 4.13 doesn't have this issue but Elpi is not compatible with it because it requires Camlp5 < 8.00. @gares Is this feasible to port Elpi to Camlp5 8.00 to make the Coq Platform compatible with OCaml 4.13?

[MSoegtropIMC]

@Zimmi48 : isn't the issue with elpi that for the sake of serapi I pin ppxlib and that this old version is not compatible with newer OCaml?

[Zimmi48]

@MSoegtropIMC That's not what I read from the logs that were posted here. Furthermore, if the issue was with the version of ppxlib, then the failure should occur before any attempt to install Elpi is made. That being said, it is not guaranteed that once Elpi is updated to be compatible with Camlp5 8.00 and OCaml 4.13 the troubles will be over. I'd be surprised if that was the only issue.

[MSoegtropIMC]

I see. So the conclusion is that for now we can't support elpi and everything which depends on it on WSL2?

One should probably have a look into the actual OCaml build error with 4.10.2. It is quite odd that this fails on WSL which is essentially Ubuntu.

@jibnew: I don't know how experienced you are. Can you look into what the actual issue is with OCaml 4.10.2? If not I think we can find someone to look into it.

[Zimmi48]

Can you look into what the actual issue is with OCaml 4.10.2?

I'm not sure what more you'd like to know besides the error report already quoted here. I just had a look at the OCaml bug tracker and this looks very much like ocaml/ocaml#10250. If that's really the issue, then it has to do with the version of glibc, not at all with WSL. It was fixed in 4.13.0 by ocaml/ocaml#10266. Maybe we can push OCaml developers to backport this patch to earlier branches, or include the patch in the platform opam repo...

[Zimmi48]

Actually OCaml developers are already discussing how to backport this patch: ocaml/ocaml#10725

And according to the above PR, glibc 2.34 (the problematic glibc version) is in Ubuntu 21.10, whereas GitHub's ubuntu-latest runners are still on Ubuntu 20.04 (latest LTS), which explains why we didn't notice this issue in CI yet: https://docs.github.com/en/actions/using-github-hosted-runners/about-github-hosted-runners#supported-runners-and-hardware-resources

[MSoegtropIMC]

Thanks @Zimmi48. It makes sense then to include ocaml/ocaml#10266 in the Coq Platform local patch repo for 4.10.2, unless it is fixed upstream within a few days.

[jibnew]

I confirm with this: leaving coq alone I just tried to install various versions of ocaml from opam. All of them before 4.13.0 throw the same sig_alt_stack error; all at 4.13.0 and above compile well.

[MSoegtropIMC]

Thanks for the analysis! I think I will backport the fix which went into 4.13.0 to 4.10.2 in Coq Platform (unless Ocaml does it).

[Zimmi48]

It's possible that OCaml will have it in a matter of days, so this really depends on when the next Coq Platform release happens.

[MSoegtropIMC]

@Zimmi48 : since I want to add coq-hammer and the z3 package is also in discussion I would say the release will be mid next week. I will wait until Monday and then do a local patch.

[gares]

Yes, this makes sense: the errors below 4.13 are related to building the OCaml compiler itself, so the failures happen whatever level is chosen. OCaml 4.13 doesn't have this issue but Elpi is not compatible with it because it requires Camlp5 < 8.00. @gares Is this feasible to port Elpi to Camlp5 8.00 to make the Coq Platform compatible with OCaml 4.13?

Yes, but there is a problem with external deps (of camlp5), see LPCIC/elpi#110

[gares]

But I see the discussion is going in another direction, sorry for the late reply

[MSoegtropIMC]

@gares: yes I wouldn't like to change the OCaml version shortly before a release anyway, so patching 4.10.2 seems to be the most viable option to me.

But in 6 months I might switch to 4.13.

[Zimmi48]

Then, @MSoegtropIMC I think your experience as a macOS / MacPorts user would be helpful to make progress on camlp5/camlp5#78, which is the thing blocking Elpi compatibility with OCaml 4.13.

[gares]

It may not happen in 6 months, but Elpi will eventually drop its dep on camlp5 (FYI) 🪓

[MSoegtropIMC]

@jibnew : I saw that there is an OCaml 4.10.3. Would you mind testing it on WSL?

In case this works, I will simply switch to 4.10.3.

[Zimmi48]

@MSoegtropIMC I cannot find any OCaml 4.10.3 package: the required fix has been backported to the 4.10 branch on the OCaml repository (just two days ago), but it still appears as unreleased changes (according to the changelog), there is no 4.10.3 tag, and no such version in the opam-repository... I suggest you use a local opam package that points to the untagged commit with the fix or that we ask when the new 4.10.3 release is expected.

[MSoegtropIMC]

Well there are these folders in the main Ocaml repo:

https://github.com/ocaml/opam-repository/tree/master/packages/ocaml/ocaml.4.10.3

https://github.com/ocaml/opam-repository/tree/master/packages/ocaml-variants/ocaml-variants.4.10.3+trunk

but indeed opam denies to create a switch with 4.10.3. I am not sure what I am supposed to make out of that.

[Zimmi48]

I don't know what these packages are for, but there is no ocaml-base-compiler, which ocaml depends on for instance. And anyway, they exist since before we had this issue open.

[Zimmi48]

I suggest you use a local opam package that points to the untagged commit with the fix or that we ask when the new 4.10.3 release is expected.

I've asked here: ocaml/ocaml@48ad9be

[Zimmi48]

FYI @gashe reported that there won't be any 4.10.3 release but that opam install 4.10.x should work by installing the maintenance branch.

[Zimmi48]

Actually, if I believe what I see in https://github.com/ocaml/opam-repository/pull/19855/files#diff-c35dd6cd49bb5eee75187261b46b7a3da4bab796e40c922373ab007e86bb5dfa, the fix has been backported (three days ago) to all past OCaml releases, so this shouldn't actually require any change on our end, and this issue can just be closed.

[Zimmi48]

Confirmed: ocaml/ocaml#10250 (comment)

[MSoegtropIMC]

@Zimmi48 : thanks - I will test it on Ubuntu 21 (without WSL2) today and then close!

[MSoegtropIMC]

Tests are successful - Ocaml 4.10.2 has indeed been updated.