From 9af28924713d14d833dcaf95cd3338ef68fbfc97 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Tue, 7 Jul 2020 14:08:24 +0200
Subject: Bytecode-only build (#243)

If ocamlopt (the native-code OCaml compiler) is not available,
fall back to building with ocamlc (the bytecode OCaml compiler).

Fixes: #359
---
 Makefile.extr | 16 +++++++++++++++-
 configure     | 17 ++++++++++++++---
 2 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/Makefile.extr b/Makefile.extr
index 5948bfc6..b417945b 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -19,7 +19,8 @@ include Makefile.config
 
 #
 # Variables from Makefile.config:
-# -OCAML_OPT_COMP: can we use the native version
+# -OCAML_NATIVE_COMP: native-code compilation is supported
+# -OCAML_OPT_COMP: can we use the natively-compiled compilers
 # -COMPFLAGS: compile options
 # -LINK_OPT: additional linker flags for the native binary
 #
@@ -71,6 +72,7 @@ OCAMLDEP=ocamldep$(DOTOPT) -slash $(INCLUDES)
 
 OCAMLLEX=ocamllex -q
 MODORDER=tools/modorder .depend.extr
+COPY=cp
 
 PARSERS=cparser/pre_parser.mly
 LEXERS=cparser/Lexer.mll lib/Tokenize.mll \
@@ -88,9 +90,15 @@ ifeq ($(wildcard .depend.extr),.depend.extr)
 
 CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)
 
+ifeq ($(OCAML_NATIVE_COMP),true)
 ccomp: $(CCOMP_OBJS)
 	@echo "Linking $@"
 	@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
+else
+ccomp: ccomp.byte
+	@echo "Copying to $@"
+	@$(COPY) $+ $@
+endif
 
 ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
 	@echo "Linking $@"
@@ -98,9 +106,15 @@ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
 
 CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx)
 
+ifeq ($(OCAML_NATIVE_COMP),true)
 clightgen: $(CLIGHTGEN_OBJS)
 	@echo "Linking $@"
 	@$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+
+else
+clightgen: clightgen.byte
+	@echo "Copying to $@"
+	@$(COPY) $+ $@
+endif
 
 clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo)
 	@echo "Linking $@"
diff --git a/configure b/configure
index 432bacff..d38deeec 100755
--- a/configure
+++ b/configure
@@ -547,7 +547,7 @@ case "$coq_ver" in
 esac
 
 echo "Testing OCaml... " | tr -d '\n'
-ocaml_ver=`ocamlopt -version 2>/dev/null`
+ocaml_ver=`ocamlc -version 2>/dev/null`
 case "$ocaml_ver" in
   4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*)
         echo "version $ocaml_ver -- UNSUPPORTED"
@@ -565,9 +565,19 @@ case "$ocaml_ver" in
         missingtools=true;;
 esac
 
+echo "Testing OCaml native-code compiler..." | tr -d '\n'
+ocamlopt_ver=`ocamlopt -version 2>/dev/null`
+if test "$ocamlopt_ver" = "$ocaml_ver"; then
+  echo "yes"
+  ocaml_native_comp=true
+else
+  echo "no, will build to bytecode only"
+  ocaml_native_comp=false
+fi
+
 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
+ocamlopt_opt_ver=`ocamlopt.opt -version 2>/dev/null`
+if test "$ocamlopt_opt_ver" = "$ocaml_ver"; then
   echo "yes"
   ocaml_opt_comp=true
 else
@@ -680,6 +690,7 @@ LIBDIR=$libdir
 MANDIR=$sharedir/man
 SHAREDIR=$sharedir
 COQDEVDIR=$coqdevdir
+OCAML_NATIVE_COMP=$ocaml_native_comp
 OCAML_OPT_COMP=$ocaml_opt_comp
 MENHIR_DIR=$menhir_dir
 COMPFLAGS=-bin-annot
-- 
cgit