compcert: fix ocaml 4.03.0 induced build failure
ocaml's old default "warn-error" list was empty, so all warnings were non-fatal, but as of ocaml 4.03.0, the default setting is now "-warn-error -a+31" (all warnings are non-fatal except 31). This causes the vendored Coq 8.4 build to fail, so restore the old default. Also, restore parallelization for the `make world` part of the Coq 8.4 build, as only `make install` seems to require deparallelization. Closes #1158. Signed-off-by: ilovezfs <ilovezfs@icloud.com>
This commit is contained in:
parent
9e7f47e48a
commit
f15929266d
1 changed files with 11 additions and 5 deletions
|
@ -39,11 +39,17 @@ class Compcert < Formula
|
||||||
system "./configure", "-prefix", buildpath/"coq84",
|
system "./configure", "-prefix", buildpath/"coq84",
|
||||||
"-camlp5dir", Formula["camlp5"].opt_lib/"ocaml/camlp5",
|
"-camlp5dir", Formula["camlp5"].opt_lib/"ocaml/camlp5",
|
||||||
"-coqide", "no",
|
"-coqide", "no",
|
||||||
"-with-doc", "no"
|
"-with-doc", "no",
|
||||||
ENV.deparallelize do
|
# Prevent warning 31 (module is linked twice in the
|
||||||
system "make", "world"
|
# same executable) from being a fatal error, which
|
||||||
system "make", "install"
|
# would otherwise be the default as of ocaml 4.03.0;
|
||||||
end
|
# note that "-custom" is the default value of
|
||||||
|
# coqrunbyteflags, and is necessary, so don't just
|
||||||
|
# overwrite it with "-warn-error -a"
|
||||||
|
"-coqrunbyteflags", "-warn-error -a -custom"
|
||||||
|
|
||||||
|
system "make", "VERBOSE=1", "world"
|
||||||
|
ENV.deparallelize { system "make", "install" }
|
||||||
end
|
end
|
||||||
|
|
||||||
ENV.prepend_path "PATH", buildpath/"coq84/bin"
|
ENV.prepend_path "PATH", buildpath/"coq84/bin"
|
||||||
|
|
Loading…
Reference in a new issue