From f15929266dc7132f8f2e8e6a6b29538a27ad901b Mon Sep 17 00:00:00 2001 From: ilovezfs Date: Sat, 14 May 2016 06:39:50 -0700 Subject: [PATCH] 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 --- Formula/compcert.rb | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/Formula/compcert.rb b/Formula/compcert.rb index c559671c82..0899ac4dfc 100644 --- a/Formula/compcert.rb +++ b/Formula/compcert.rb @@ -39,11 +39,17 @@ class Compcert < Formula system "./configure", "-prefix", buildpath/"coq84", "-camlp5dir", Formula["camlp5"].opt_lib/"ocaml/camlp5", "-coqide", "no", - "-with-doc", "no" - ENV.deparallelize do - system "make", "world" - system "make", "install" - end + "-with-doc", "no", + # Prevent warning 31 (module is linked twice in the + # same executable) from being a fatal error, which + # would otherwise be the default as of ocaml 4.03.0; + # 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 ENV.prepend_path "PATH", buildpath/"coq84/bin"