From 20c70573181f81c99ea4e8797615dac8308a9b18 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 17 Dec 2014 15:24:17 +0100
Subject: Use OCaml's .opt compilers when available. Cleanups in configure.

---
 Makefile      | 16 ++++++++-------
 Makefile.extr | 65 ++++++++++++++++++++++++++++++++++++++++++++---------------
 configure     | 33 +++++++++++++++++++++---------
 3 files changed, 82 insertions(+), 32 deletions(-)

diff --git a/Makefile b/Makefile
index 5406bc28..78d386d6 100644
--- a/Makefile
+++ b/Makefile
@@ -135,25 +135,27 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach
 .depend.extr: extraction/STAMP tools/modorder
 	$(MAKE) -f Makefile.extr depend
 
-ccomp: .depend.extr compcert.ini
+ccomp: .depend.extr compcert.ini FORCE
 	$(MAKE) -f Makefile.extr ccomp
-ccomp.byte: .depend.extr compcert.ini
+ccomp.byte: .depend.extr compcert.ini FORCE
 	$(MAKE) -f Makefile.extr ccomp.byte
 
-cchecklink: .depend.extr compcert.ini
+cchecklink: .depend.extr compcert.ini FORCE
 	$(MAKE) -f Makefile.extr cchecklink
-cchecklink.byte: .depend.extr compcert.ini
+cchecklink.byte: .depend.extr compcert.ini FORCE
 	$(MAKE) -f Makefile.extr cchecklink.byte
 
-clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo
+clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE
 	$(MAKE) -f Makefile.extr clightgen
-clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo
+clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE
 	$(MAKE) -f Makefile.extr clightgen.byte
 
 runtime:
 	$(MAKE) -C runtime
 
-.PHONY: proof extraction runtime
+FORCE:
+
+.PHONY: proof extraction runtime FORCE
 
 documentation: doc/coq2html $(FILES)
 	mkdir -p doc/html
diff --git a/Makefile.extr b/Makefile.extr
index 60fee407..732df31e 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -17,30 +17,58 @@
 
 include Makefile.config
 
+# Directories containing plain Caml code (no preprocessing)
+
 DIRS=extraction \
   lib common $(ARCH) backend cfrontend cparser driver \
   exportclight
 
-ALLDIRS=$(DIRS)
+# Directories containing Caml code that must be preprocessed by Camlp4
+
 ifeq ($(CCHECKLINK),true)
-ALLDIRS+=checklink
+DIRS_P4=checklink
+else
+DIRS_P4=
 endif
 
+ALLDIRS=$(DIRS) $(DIRS_P4)
+
 INCLUDES=$(patsubst %,-I %, $(ALLDIRS))
 
+# Control of warnings:
+# warning 3 = deprecated feature.  Turned off for OCaml 4.02 (bytes vs strings)
+# warning 20 = unused function argument.  There are some in extracted code
+
 WARNINGS=-w -3
 extraction/%.cmx: WARNINGS +=-w -20
 extraction/%.cmo: WARNINGS +=-w -20
 
+COMPFLAGS=-g $(INCLUDE) $(WARNINGS)
+
+# Using the bitstring library and syntax extension (for checklink)
+
 BITSTRING=-package bitstring,bitstring.syntax -syntax bitstring.syntax,camlp4o
 
-OCAMLC=ocamlc -g $(INCLUDES) $(WARNINGS)
-OCAMLOPT=ocamlopt -g $(INCLUDES) $(WARNINGS)
-OCAMLDEP=ocamldep $(INCLUDES)
+# Using .opt compilers if available
 
-OCAMLC_P4=ocamlfind $(OCAMLC) $(BITSTRING)
-OCAMLOPT_P4=ocamlfind $(OCAMLOPT) $(BITSTRING)
-OCAMLDEP_P4=ocamlfind $(OCAMLDEP) $(BITSTRING)
+ifeq ($(OCAML_OPT_COMP),true)
+DOTOPT=.opt
+else
+DOTOPT=
+endif
+
+# Compilers used for non-preprocessed code
+
+OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS)
+OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS)
+OCAMLDEP=ocamldep$(DOTOPT) $(INCLUDES)
+
+# Compilers used for Camlp4-preprocessed code.  Note that we cannot
+# use the .opt compilers (because ocamlfind doesn't support them).
+
+OCAMLC_P4=ocamlfind ocamlc $(COMPFLAGS) $(BITSTRING)
+OCAMLOPT_P4=ocamlfind ocamlopt $(COMPFLAGS) $(BITSTRING)
+OCAMLDEP_P4=ocamlfind ocamldep $(INCLUDES) $(BITSTRING)
 
 MENHIR=menhir --explain
 OCAMLLEX=ocamllex -q
@@ -54,6 +82,8 @@ LIBS=str.cmxa
 EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte
 GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml)
 
+# Beginning of part that assumes .depend.extr already exists
+
 ifeq ($(wildcard .depend.extr),.depend.extr)
 
 CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)
@@ -94,15 +124,17 @@ include .depend.extr
 
 endif
 
-checklink/%.cmx: checklink/%.ml
-	@echo "OCAMLOPT $<"
-	@$(OCAMLOPT_P4) -c $<
-checklink/%.cmo: checklink/%.ml
+# End of part that assumes .depend.extr already exists
+
+checklink/%.cmi: checklink/%.mli
 	@echo "OCAMLC   $<"
 	@$(OCAMLC_P4) -c $<
-checklink/%.cmi: checklink/%.mli
+checklink/%.cmo: checklink/%.ml
 	@echo "OCAMLC   $<"
 	@$(OCAMLC_P4) -c $<
+checklink/%.cmx: checklink/%.ml
+	@echo "OCAMLOPT $<"
+	@$(OCAMLOPT_P4) -c $<
 
 %.cmi: %.mli
 	@echo "OCAMLC   $<"
@@ -124,11 +156,12 @@ clean:
 	rm -f $(GENERATED)
 	for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done
 
+# Generation of .depend.extr
+
 depend: $(GENERATED)
 	@echo "Analyzing OCaml dependencies"
 	@for d in $(DIRS); do $(OCAMLDEP) $$d/*.mli $$d/*.ml; done > .depend.extr
-ifeq ($(CCHECKLINK),true)
-	@$(OCAMLDEP_P4) checklink/*.mli checklink/*.ml >> .depend.extr
-endif
+ifneq ($(strip $(DIRS_P4)),)
+	@for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .dependif
 
 
diff --git a/configure b/configure
index f3967dc7..7e1417bb 100755
--- a/configure
+++ b/configure
@@ -213,7 +213,7 @@ fi
 missingtools=false
 
 echo "Testing Coq... " | tr -d '\n'
-coq_ver=`coqc -v | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p'`
+coq_ver=`(coqc -v | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') 2>/dev/null`
 case "$coq_ver" in
   8.4pl*)
         echo "version $coq_ver -- good!";;
@@ -223,14 +223,14 @@ case "$coq_ver" in
         missingtools=true;;
   *)
         echo "NOT FOUND"
-        echo "Error: make sure Coq version 8.4pl4 is installed."
+        echo "Error: make sure Coq version 8.4 pl5 is installed."
         missingtools=true;;
 esac
 
 echo "Testing OCaml... " | tr -d '\n'
-ocaml_ver=`ocamlc -version`
+ocaml_ver=`ocamlopt -version 2>/dev/null`
 case "$ocaml_ver" in
-  4.*)
+  [4-9].*)
         echo "version $ocaml_ver -- good!";;
   ?.*)
         echo "version $ocaml_ver -- UNSUPPORTED"
@@ -242,21 +242,35 @@ case "$ocaml_ver" in
         missingtools=true;;
 esac
 
+echo "Testing OCaml .opt compilers... " | tr -d '\n'
+ocaml_opt_ver=`ocamlopt.opt -version 2>/dev/null`
+if test "$ocaml_opt_ver" = "$ocaml_ver"; then
+  echo "yes"
+  ocaml_opt_comp=true
+else
+  echo "no, will do without"
+  ocaml_opt_comp=false
+fi
+
 echo "Testing Menhir... " | tr -d '\n'
-menhir_ver=`menhir --version | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'`
+menhir_ver=`(menhir --version | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p') 2>\dev\null`
 case "$menhir_ver" in
-  20*)
+  201[4-9]*|20[2-9]*)
         echo "version $menhir_ver -- good!";;
+  ?*)
+        echo "version $menhir_ver -- UNSUPPORTED"
+        echo "Error: CompCert requires Menhir version 20140422 or later."
+        missingtools=true;;
   *)
         echo "NOT FOUND"
-        echo "Error: make sure Menhir is installed."
+        echo "Error: make sure Menhir version 20140422 or later is installed."
         missingtools=true;;
 esac
 
-echo "Testing GNU make..." | tr -d '\n'
+echo "Testing GNU make... " | tr -d '\n'
 make=''
 for mk in make gmake gnumake; do
-  make_ver=`$mk -v | head -1 | sed -n -e 's/^GNU Make //p'`
+  make_ver=`($mk -v | head -1 | sed -n -e 's/^GNU Make //p') 2>/dev/null`
   case "$make_ver" in
     3.8*|3.9*|[4-9].*)
         echo "version $make_ver (command '$mk') -- good!"
@@ -299,6 +313,7 @@ PREFIX=$prefix
 BINDIR=$bindir
 LIBDIR=$libdir
 SHAREDIR=$sharedir
+OCAML_OPT_COMP=$ocaml_opt_comp
 EOF
 
 if test "$target" != "manual"; then
-- 
cgit