From cf646d855395a9d0c40613098debbbd895c4eef8 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sat, 22 Nov 2014 14:21:19 +0100
Subject: Replace ocamlbuild by a second-stage makefile to compile the OCaml
 code and produce the executables. configure: add check for GNU make.

---
 Makefile.extr | 134 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 134 insertions(+)
 create mode 100644 Makefile.extr

(limited to 'Makefile.extr')

diff --git a/Makefile.extr b/Makefile.extr
new file mode 100644
index 00000000..60fee407
--- /dev/null
+++ b/Makefile.extr
@@ -0,0 +1,134 @@
+#######################################################################
+#                                                                     #
+#              The Compcert verified compiler                         #
+#                                                                     #
+#          Xavier Leroy, INRIA Paris-Rocquencourt                     #
+#                                                                     #
+#  Copyright Institut National de Recherche en Informatique et en     #
+#  Automatique.  All rights reserved.  This file is distributed       #
+#  under the terms of the GNU General Public License as published by  #
+#  the Free Software Foundation, either version 2 of the License, or  #
+#  (at your option) any later version.  This file is also distributed #
+#  under the terms of the INRIA Non-Commercial License Agreement.     #
+#                                                                     #
+#######################################################################
+
+# Second-stage Makefile, after Coq extraction
+
+include Makefile.config
+
+DIRS=extraction \
+  lib common $(ARCH) backend cfrontend cparser driver \
+  exportclight
+
+ALLDIRS=$(DIRS)
+ifeq ($(CCHECKLINK),true)
+ALLDIRS+=checklink
+endif
+
+INCLUDES=$(patsubst %,-I %, $(ALLDIRS))
+
+WARNINGS=-w -3
+extraction/%.cmx: WARNINGS +=-w -20
+extraction/%.cmo: WARNINGS +=-w -20
+
+BITSTRING=-package bitstring,bitstring.syntax -syntax bitstring.syntax,camlp4o
+
+OCAMLC=ocamlc -g $(INCLUDES) $(WARNINGS)
+OCAMLOPT=ocamlopt -g $(INCLUDES) $(WARNINGS)
+OCAMLDEP=ocamldep $(INCLUDES)
+
+OCAMLC_P4=ocamlfind $(OCAMLC) $(BITSTRING)
+OCAMLOPT_P4=ocamlfind $(OCAMLOPT) $(BITSTRING)
+OCAMLDEP_P4=ocamlfind $(OCAMLDEP) $(BITSTRING)
+
+MENHIR=menhir --explain
+OCAMLLEX=ocamllex -q
+MODORDER=tools/modorder .depend.extr
+
+PARSERS=backend/CMparser.mly cparser/pre_parser.mly
+LEXERS=backend/CMlexer.mll cparser/Lexer.mll lib/Tokenize.mll
+
+LIBS=str.cmxa
+
+EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte
+GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml)
+
+ifeq ($(wildcard .depend.extr),.depend.extr)
+
+CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)
+
+ccomp: $(CCOMP_OBJS)
+	@echo "Linking $@"
+	@$(OCAMLOPT) -o $@ $(LIBS) $+
+
+ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
+	@echo "Linking $@"
+	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+
+
+ifeq ($(CCHECKLINK),true)
+
+CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx)
+
+cchecklink: $(CCHECKLINK_OBJS)
+	@echo "Linking $@"
+	@$(OCAMLOPT_P4) -linkpkg -o $@ $(LIBS) $+
+
+cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo)
+	@echo "Linking $@"
+	@$(OCAMLC_P4) -linkpkg -o $@ $(LIBS:.cmxa=.cma) $+
+
+endif
+
+CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx)
+
+clightgen: $(CLIGHTGEN_OBJS)
+	@echo "Linking $@"
+	@$(OCAMLOPT) -o $@ $(LIBS) $+
+
+clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo)
+	@echo "Linking $@"
+	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+
+
+include .depend.extr
+
+endif
+
+checklink/%.cmx: checklink/%.ml
+	@echo "OCAMLOPT $<"
+	@$(OCAMLOPT_P4) -c $<
+checklink/%.cmo: checklink/%.ml
+	@echo "OCAMLC   $<"
+	@$(OCAMLC_P4) -c $<
+checklink/%.cmi: checklink/%.mli
+	@echo "OCAMLC   $<"
+	@$(OCAMLC_P4) -c $<
+
+%.cmi: %.mli
+	@echo "OCAMLC   $<"
+	@$(OCAMLC) -c $<
+%.cmo: %.ml
+	@echo "OCAMLC   $<"
+	@$(OCAMLC) -c $<
+%.cmx: %.ml
+	@echo "OCAMLOPT $<"
+	@$(OCAMLOPT) -c $<
+
+%.ml %.mli: %.mly
+	$(MENHIR) $<
+%.ml: %.mll
+	$(OCAMLLEX) $<
+
+clean:
+	rm -f $(EXECUTABLES)
+	rm -f $(GENERATED)
+	for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done
+
+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
+
+
-- 
cgit 


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.extr | 65 ++++++++++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 49 insertions(+), 16 deletions(-)

(limited to 'Makefile.extr')

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


From 3262e1e2e71b4fad5d5c47603aafb4dcb2539e27 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 17 Dec 2014 15:49:22 +0100
Subject: Minor bug fixes in configure and Makefile.extr

---
 Makefile.extr | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'Makefile.extr')

diff --git a/Makefile.extr b/Makefile.extr
index 732df31e..35ae5f7b 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -43,7 +43,7 @@ WARNINGS=-w -3
 extraction/%.cmx: WARNINGS +=-w -20
 extraction/%.cmo: WARNINGS +=-w -20
 
-COMPFLAGS=-g $(INCLUDE) $(WARNINGS)
+COMPFLAGS=-g $(INCLUDES) $(WARNINGS)
 
 # Using the bitstring library and syntax extension (for checklink)
 
@@ -162,6 +162,7 @@ depend: $(GENERATED)
 	@echo "Analyzing OCaml dependencies"
 	@for d in $(DIRS); do $(OCAMLDEP) $$d/*.mli $$d/*.ml; done > .depend.extr
 ifneq ($(strip $(DIRS_P4)),)
-	@for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .dependif
+	@for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .depend.extr
+endif
 
 
-- 
cgit