Stream: coq-community devs & users

Topic: Why Coq 8.5.3 now FTBFS?


view this post on Zulip Erik Martin-Dorel (Jun 28 2022 at 23:51):

Hi,

as a follow-up of https://coq.discourse.group/t/ann-docker-coq-bump-to-debian-11-docker-coq-action-remove-ocaml-version-minimal/1702
I merged https://github.com/coq-community/docker-base/pull/20 and rebuilt all coqorg/coq:* images with Debian 11.

cf. the following GitLab CI pipeline: https://gitlab.com/coq-community/docker-coq/-/pipelines/575403834

However I'm puzzled to see that only Coq 8.5.3 fails to build from source now:
https://gitlab.com/coq-community/docker-coq/-/jobs/2653142564

Moreover, I now see these non-fatal shell errors:
https://gitlab.com/coq-community/docker-coq/-/jobs/2653142564#L1885

- /bin/sh: 1: Syntax error: ")" unexpected
- CAMLP4DEPS parsing/g_vernac.ml4
- /bin/sh: 1: Syntax error: ")" unexpected
- CAMLP4DEPS parsing/lexer.ml4

while last week, everything was fine:
https://gitlab.com/coq-community/docker-coq/-/jobs/2608896671

Ideas on what's going on here? Cc @Théo Zimmermann @Karl Palmskog @Ali Caglayan

view this post on Zulip Karl Palmskog (Jun 29 2022 at 07:37):

no idea what is wrong here, is it the same Camlp5 version as before?

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 12:34):

Yes, both gitlab ci jobs logs mention camlp5 7.14:

https://gitlab.com/coq-community/docker-coq/-/jobs/2608896671 :check:
https://gitlab.com/coq-community/docker-coq/-/jobs/2653142564 :cross_mark:

view this post on Zulip Karl Palmskog (Jun 29 2022 at 12:45):

it may have to do with the version of some external tool used by camlp5 then? Maybe Perl version?

view this post on Zulip Pierre-Marie Pédrot (Jun 29 2022 at 14:19):

I think I've seen these errors already, but was unable to fix them.

view this post on Zulip Karl Palmskog (Jun 29 2022 at 14:20):

we should search the Zulip as well, I'm pretty sure someone has reported having these error messages

view this post on Zulip Pierre-Marie Pédrot (Jun 29 2022 at 14:20):

IIRC it was a problem with an environment variable like PP or something

view this post on Zulip Guillaume Melquiond (Jun 29 2022 at 14:40):

I am a bit surprised at how it could ever have worked. Looking at the error message, the failing command seems to be

CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1)  \#))

So, the shell will get a command line ending with \#) (including the backslash) and thus get an unexpected ). Am I missing something?

view this post on Zulip Karl Palmskog (Jun 29 2022 at 14:41):

maybe it worked due to quirks with the sed version in Debian oldstable then. But if we confirm/know that is the case, we could put together a patch and upstream that to the opam repo (it's valuable to be able to test with Coq 8.5 on occasion)

view this post on Zulip Guillaume Melquiond (Jun 29 2022 at 14:43):

I am not even talking about the sed command, the shell is getting

LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' whatever  \#)

which is ill-formed.

view this post on Zulip Karl Palmskog (Jun 29 2022 at 14:51):

OK, so the bash/sh version may be the deciding factor?

view this post on Zulip Guillaume Melquiond (Jun 29 2022 at 14:52):

Yes, either that or the version of make. For example, there might have been a bug in make that would have caused it to send #) rather than \#) to the shell.

view this post on Zulip Karl Palmskog (Jun 29 2022 at 14:55):

@Erik Martin-Dorel do you have an easy way to test out Guillaume's hypothesis? If you can make a diff/patch and confirm it works, I volunteer to submit upstream to the OCaml opam repo.

view this post on Zulip Guillaume Melquiond (Jun 29 2022 at 14:57):

If my hypothesis is correct, a proper patch is to replace the above line by

CAMLP4DEPS=${shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' ${1}}

view this post on Zulip Erik Martin-Dorel (Jun 29 2022 at 15:00):

Karl Palmskog said:

Erik Martin-Dorel do you have an easy way to test out Guillaume's hypothesis? If you can make a diff/patch and confirm it works, I volunteer to submit upstream to the OCaml opam repo.

Yes, I'll be able to test this, but certainly not before next week. Will let you know then.

Thank you all!

view this post on Zulip Karl Palmskog (Jun 29 2022 at 15:08):

this patch should work assuming the hypothesis works out (patch -p1 < path/to/camlp4deps.patch on CLI): camlp4deps.patch

I might test it out sooner than Erik, but we'll see.

view this post on Zulip Karl Palmskog (Jun 29 2022 at 15:10):

Also explicitly:

diff --git a/Makefile.build b/Makefile.build
index b5c933a..057c9ae 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -117,7 +117,7 @@ $(if $(findstring $@,$(PRIVATEBINARIES)),\
 $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
 endef

-CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
+CAMLP4DEPS=${shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' ${1}}
 ifeq ($(CAMLP4),camlp5)
 CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 else

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2022 at 11:11):

Debian having /bin/sh not pointing to bash could be also a factor as I see /bin/sh

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2022 at 11:11):

before /bin/sh meant /bin/bash , which is quite a jump!


Last updated: Feb 05 2023 at 14:02 UTC