aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build22
-rw-r--r--config/Makefile.template3
-rw-r--r--config/coq_config.mli2
-rwxr-xr-xconfigure15
-rw-r--r--scripts/coqmktop.ml3
5 files changed, 33 insertions, 12 deletions
diff --git a/Makefile.build b/Makefile.build
index 0a60e4bb8..3a5cfd36a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -196,7 +196,7 @@ $(CHICKENOPT): checker/check.cmxa checker/main.ml
$(CHICKENBYTE): checker/check.cma checker/main.ml
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -custom -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
+ $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
$(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
@@ -205,7 +205,7 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
$(COQMKTOPBYTE): $(COQMKTOPCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma \
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma \
$(COQMKTOPCMO) $(OSDEPLIBS)
$(COQMKTOPOPT): $(COQMKTOPCMX)
@@ -227,7 +227,7 @@ scripts/tolink.ml: Makefile.build Makefile.common
$(COQCBYTE): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS)
$(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP)
$(SHOW)'OCAMLOPT -o $@'
@@ -368,7 +368,7 @@ contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
else
contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) -custom $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO)
endif
###########################################################################
@@ -467,7 +467,7 @@ bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX)
bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) -custom -linkall $(BYTEFLAGS) -o $@ \
+ $(HIDE)$(OCAMLC) $(COQRUNBYTEFLAGS) -linkall $(BYTEFLAGS) -o $@ \
dynlink.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO)
bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX)
@@ -588,27 +588,27 @@ tools:: $(TOOLS) $(DEBUGPRINTERS)
$(COQDEP): $(COQDEPCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS)
$(GALLINA): $(GALLINACMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ $(GALLINACMO)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO)
$(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
$(COQTEX): tools/coq-tex.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma tools/coq-tex.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo
$(COQWC): tools/coqwc.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coqwc.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo
$(COQDOC): $(COQDOCCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO)
###########################################################################
# Installation
diff --git a/config/Makefile.template b/config/Makefile.template
index a48bbceb9..cd19503ad 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -21,6 +21,9 @@ COQ_CONFIGURED=yes
# Local use (no installation)
LOCAL=LOCALINSTALLATION
+# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
+COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS
+
# Paths for true installation
# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
# do_Makefile will reside
diff --git a/config/coq_config.mli b/config/coq_config.mli
index e8c1b5304..46404215f 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -24,6 +24,8 @@ val camlp4lib : string (* where is the library of Camlp4 *)
val best : string (* byte/opt *)
val arch : string (* architecture *)
val osdeplibs : string (* OS dependant link options for ocamlc *)
+val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *)
+
(* val defined : string list (* options for lib/ocamlpp *) *)
diff --git a/configure b/configure
index dc1baaffa..11f72d19f 100755
--- a/configure
+++ b/configure
@@ -32,6 +32,8 @@ usage () {
printf "\tSet installation directory to <dir>\n"
echo "-local"
printf "\tSet installation directory to the current source tree\n"
+ echo "-coqrunbyteflags"
+ printf "\tSet link flags for VM-dependent bytecode\n"
echo "-src"
printf "\tSpecifies the source directory\n"
echo "-bindir"
@@ -105,6 +107,7 @@ ar_exec=ar
ranlib_exec=ranlib
local=false
+coqrunbyteflags_spec=no
src_spec=no
prefix_spec=no
bindir_spec=no
@@ -138,6 +141,9 @@ while : ; do
prefix="$2"
shift;;
-local|--local) local=true;;
+ -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
+ coqrunbyteflags="$2"
+ shift;;
-src|--src) src_spec=yes
COQSRC="$2"
shift;;
@@ -755,6 +761,12 @@ case $coqdocdir_spec/$prefix_spec/$local in
esac;;
esac
+case $coqrunbyteflags_spec/$local in
+ yes/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
+ */true) COQRUNBYTEFLAGS="-custom";;
+ *) COQRUNBYTEFLAGS="-custom";;
+esac
+
# case $emacs_spec in
# no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
# read EMACS
@@ -775,6 +787,7 @@ echo " Architecture : $ARCH"
if test ! -z "$OS" ; then
echo " Operating system : $OS"
fi
+echo " Coq VM bytecode link flags : $COQRUNBYTEFLAGS"
echo " OS dependent libraries : $OSDEPLIBS"
echo " Objective-Caml/Camlp4 version : $CAMLVERSION"
echo " Objective-Caml/Camlp4 binaries in : $CAMLBIN"
@@ -863,6 +876,7 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
let local = $local
+let coqrunbyteflags = "$COQRUNBYTEFLAGS"
let bindir = "$ESCBINDIR"
let coqlib = "$ESCLIBDIR"
let coqtop = "$ESCCOQTOP"
@@ -910,6 +924,7 @@ chmod a-w "$mlconfig_file"
rm -f "$COQSRC/config/Makefile"
sed -e "s|LOCALINSTALLATION|$local|" \
+ -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \
-e "s|COQSRCDIRECTORY|$COQSRC|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index ef869a17e..c89ea827e 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -289,7 +289,8 @@ let main () =
(* bytecode (we shunt ocamlmktop script which fails on win32) *)
let ocamlmktoplib = " toplevellib.cma" in
let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in
- let ocamlccustom = ocamlcexec^" -custom -linkall" in
+ let ocamlccustom = Printf.sprintf "%s %s -linkall "
+ ocamlcexec Coq_config.coqrunbyteflags in
(if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
in
(* files to link *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 23:21:49 +0000