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...

Last updated: Dec 05 2023 at 12:01 UTC