diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-07-07 14:08:24 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-07 14:08:24 +0200 |
| commit | 9af28924713d14d833dcaf95cd3338ef68fbfc97 (patch) | |
| tree | 4be68320227ebe6acb4a11a3397596ee118de3e5 /configure | |
| parent | 3b1f3dd57d8c10c1c29f67f0f745e3263d9d3daf (diff) | |
| download | compcert-9af28924713d14d833dcaf95cd3338ef68fbfc97.tar.gz compcert-9af28924713d14d833dcaf95cd3338ef68fbfc97.zip | |
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
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 17 |
1 files changed, 14 insertions, 3 deletions
@@ -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 |