Stream: Coq devs & plugin devs

Topic: ✔ difference between 8.4 and 8.5 docker images?


view this post on Zulip Jason Gross (Mar 20 2023 at 20:42):

What's the difference between the Coq 8.4 and Coq 8.5 docker images? The 8.5 one is capable of building Coq at commit 2374a23fb7ebfa547eb16ce2ab8dc9efb2a3f855, but the 8.4 docker image, which is running ocaml 4.02.3 and camlp5 7.14 (exactly the same as the 8.5 one) instead emits a bunch of

CAMLP4DEPS tactics/tauto.ml4
/bin/sh: 1: Syntax error: ")" unexpected
CAMLP4O   plugins/decl_mode/g_decl_mode.ml4
File "plugins/decl_mode/g_decl_mode.ml4", line 112, characters 3-4:
Parse error: ':' expected after [name] (in [entry])
/bin/sh: 1: Syntax error: ")" unexpected
CAMLP4O   plugins/setoid_ring/newring.ml4
File "plugins/setoid_ring/newring.ml4", line 109, characters 3-4:
Parse error: ':' expected after [name] (in [entry])
/bin/sh: 1: Syntax error: ")" unexpected
CAMLP4O   plugins/omega/g_omega.ml4
File "plugins/omega/g_omega.ml4", line 25, characters 36-45:
Unbound quotation: "tactic"
/bin/sh: 1: Syntax error: ")" unexpected
CAMLP4O   plugins/extraction/g_extraction.ml4
File "plugins/extraction/g_extraction.ml4", line 23, characters 3-8:
Parse error: ':' expected after [name] (in [entry])
/bin/sh: 1: Syntax error: ")" unexpected

and eventually errors with

make[1]: *** No rule to make target 'tactics/hipattern.ml', needed by 'tactics/hipattern.cmx'.  Stop.

See also https://github.com/JasonGross/test-coq-build/actions/runs/4472571065/jobs/7858892552

Are they running different shells or something?

view this post on Zulip Gaëtan Gilbert (Mar 20 2023 at 20:45):

try running with VERBOSE=1 so you can see the actual commands

view this post on Zulip Jason Gross (Mar 20 2023 at 20:56):

When I run with VERBOSE=1, I see things like

echo "tactics/eauto.ml:  " > "tactics/eauto.ml4.d" || (RV=$?; rm -f "tactics/eauto.ml4.d"; exit ${RV})
/bin/sh: 1: Syntax error: ")" unexpected

I tried changing Makefile.build, and now I see (locally, even)

echo "tactics/eauto.ml:  " > "tactics/eauto.ml4.d" || { RV=$?; rm -f "tactics/eauto.ml4.d"; exit ${RV}; }
/bin/sh: 1: Syntax error: ")" unexpected

and I am extremely confused, because there's no ) anywhere in sight, and if I run /bin/sh I do not get any error message if I copy-paste the command...

view this post on Zulip Jason Gross (Mar 20 2023 at 21:05):

Ah, switching the shell to /bin/bash tells me that the issue is the trailing ) in CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#)). But why does this work fine in the 8.5 docker image???

view this post on Zulip Paolo Giarrusso (Mar 20 2023 at 21:06):

what does /bin/sh point to in both images? Was /bin/sh pointing to dash?

view this post on Zulip Paolo Giarrusso (Mar 20 2023 at 21:08):

(probably obvious question)

view this post on Zulip Gaëtan Gilbert (Mar 20 2023 at 21:09):

this has come up before https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs-.26-users/topic/Why.20Coq.208.2E5.2E3.20now.20FTBFS.3F

view this post on Zulip Jason Gross (Mar 20 2023 at 21:13):

Ah, indeed, that patch fixes it, thank you!

view this post on Zulip Notification Bot (Mar 20 2023 at 21:14):

Jason Gross has marked this topic as resolved.


Last updated: Mar 29 2024 at 01:40 UTC