aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-12 07:41:13 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-12 07:41:13 +0000
commiteabacd04872bda164e222cdc9b48a1ee95631c8a (patch)
treef8cb18e46b485af966bea5501a0ba347aa8f1c87
parentb579b8930f4fa70d50d1934a9a96871d2e8d9fae (diff)
Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfind
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15603 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xconfigure14
-rw-r--r--scripts/coqmktop.ml9
2 files changed, 14 insertions, 9 deletions
diff --git a/configure b/configure
index 072d4d2ee..bc80f0123 100755
--- a/configure
+++ b/configure
@@ -471,7 +471,7 @@ case $CAMLVERSION in
echo " Configuration script failed!"
exit 1
fi;;
- 3.11.2|3.12*)
+ 3.11.2|3.12*|4.*)
CAMLP4COMPAT="-loc loc"
echo "You have Objective-Caml $CAMLVERSION. Good!";;
*)
@@ -494,7 +494,7 @@ esac
if [ "$coq_debug_flag" = "-g" ]; then
case $CAMLTAG in
- OCAML31*)
+ OCAML31*|OCAML4*)
# Compilation debug flag
coq_debug_flag_opt="-g"
;;
@@ -568,7 +568,7 @@ case $usecamlp5 in
yes)
camlp4oexec=`echo "$camlp4oexec" | tr 4 5`
case `"$camlp4oexec" -v 2>&1` in
- *4.0*|*5.00*)
+ *"version 4.0"*|*5.00*)
echo "Camlp5 version < 5.01 not supported."
echo "Configuration script failed!"
exit 1;;
@@ -654,11 +654,11 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
echo "CoqIde disabled as requested."
else
case $lablgtkdir_spec in
- no)
- if [ -f "${CAMLLIB}/lablgtk2/gSourceView2.mli" ]; then
+ no)
+ if lablgtkdir=$(ocamlfind query lablgtk2.sourceview2 2> /dev/null); then
+ lablgtkdir_spec=yes
+ elif [ -f "${CAMLLIB}/lablgtk2/gSourceView2.mli" ]; then
lablgtkdir=${CAMLLIB}/lablgtk2
- elif [ -f "${CAMLLIB}/site-lib/lablgtk2/gSourceView2.mli" ]; then
- lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
fi;;
yes)
if [ ! -f "$lablgtkdir/gSourceView2.mli" ]; then
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 55e12a30e..bd4dec2b6 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -52,6 +52,8 @@ let top = ref false
let echo = ref false
let no_start = ref false
+let is_ocaml4 = String.sub Coq_config.caml_version 0 2 = "4."
+
let src_dirs () =
[ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ]
@@ -62,7 +64,8 @@ let includes () =
(fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)
(src_dirs ())
(["-I"; "\"" ^ camlp4lib ^ "\""] @
- ["-I"; "\"" ^ coqlib ^ "\""])
+ ["-I"; "\"" ^ coqlib ^ "\""] @
+ if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
(* Transform bytecode object file names in native object file names *)
let native_suffix f =
@@ -261,7 +264,9 @@ let main () =
ocamloptexec^" -linkall"
end else
(* bytecode (we shunt ocamlmktop script which fails on win32) *)
- let ocamlmktoplib = " toplevellib.cma" in
+ let ocamlmktoplib = if is_ocaml4
+ then " ocamlcommon.cma ocamlbytecomp.cma ocamltoplevel.cma"
+ else " toplevellib.cma" in
let ocamlcexec = Filename.concat camlbin "ocamlc" in
let ocamlccustom = Printf.sprintf "%s %s -linkall "
ocamlcexec Coq_config.coqrunbyteflags in