Erik Martin-Dorel (Jun 28 2022 at 23:51): 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
Karl Palmskog (Jun 29 2022 at 07:37):no idea what is wrong here, is it the same Camlp5 version as before?
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:
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?
Pierre-Marie Pédrot (Jun 29 2022 at 14:19):I think I've seen these errors already, but was unable to fix them.
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
Pierre-Marie Pédrot (Jun 29 2022 at 14:20):IIRC it was a problem with an environment variable like PP or something
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?
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)
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.
Karl Palmskog (Jun 29 2022 at 14:51):OK, so the bash/sh version may be the deciding factor?
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.
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.
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}}
Thank you all!
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.
(But if one of you have some time by then, feel free to do it also!)
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.
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
Debian having /bin/sh not pointing to bash could be also a factor as I see /bin/sh
Emilio Jesús Gallego Arias (Jun 30 2022 at 11:11):before /bin/sh meant /bin/bash , which is quite a jump!
Last updated: Jun 03 2023 at 18:01 UTC