diff options
| -rw-r--r-- | Makefile | 10 | ||||
| -rw-r--r-- | config/Makefile.template | 16 | ||||
| -rwxr-xr-x | configure | 89 | ||||
| -rw-r--r-- | ide/coq.ml | 30 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 15 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 18 |
6 files changed, 114 insertions, 64 deletions
@@ -37,7 +37,7 @@ NOARG: @echo "For make to be verbose, add VERBOSE=1" # build and install the three subsystems: coq, coqide, pcoq -world: coq coqide pcoq +world: revision coq coqide pcoq install: install-coq install-coqide install-pcoq #install-manpages: install-coq-manpages install-pcoq-manpages @@ -93,7 +93,6 @@ TIME= # is "'time -p'" to get compilation time of .v BOOTCOQTOP= $(TIME) $(BESTCOQTOP) -boot $(COQOPTS) - ########################################################################### # Objects files ########################################################################### @@ -351,7 +350,12 @@ CINCLUDES= -I $(CAMLHLIB) CC=gcc AR=ar RANLIB=ranlib -BYTECCCOMPOPTS=-fno-defer-pop -Wall -Wno-unused + +ifeq ($(CAMLVERSION),OCAML307) + CFLAGS=-fno-defer-pop -Wall -Wno-unused -DOCAML_307 +else + CFLAGS=-fno-defer-pop -Wall -Wno-unused +endif # libcoqrun.a diff --git a/config/Makefile.template b/config/Makefile.template index aa7f2d621..d5c2a1436 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -113,5 +113,21 @@ REALS=REALSOPT # CoqIde (no/byte/opt) HASCOQIDE=COQIDEOPT +# Defining REVISION +CHECKEDOUT=CHECKEDOUTSOURCETREE + +.PHONY: revision + +revision: +ifeq ($(CHECKEDOUT),1) + - /bin/rm -f revision + sed -ne '/url/s/^.*\/\([^\/]\+\)"$$/\1/p' .svn/entries > revision + sed -ne '/revision/s/^.*"\([0-9]\+\)".*$$/r\1/p' .svn/entries >> revision +endif + +archclean:: + /bin/rm -f revision + # make or sed are bogus and believe lines not terminating by a return # are inexistent + @@ -6,8 +6,8 @@ # ################################## -VERSION=8.1beta -DATE="Jun 2006" +VERSION=trunk +DATE="Aug 2006" # a local which command for sh which () { @@ -37,6 +37,7 @@ libdir_spec=no mandir_spec=no emacslib_spec=no emacs_spec=no +camldir_spec=no coqdocdir_spec=no fsets_opt=no fsets=all @@ -81,6 +82,9 @@ while : ; do -coqdocdir|--coqdocdir) coqdocdir_spec=yes coqdocdir="$2" shift;; + -camldir|--camldir) camldir_spec=yes + camldir="$2" + shift;; -arch|--arch) arch_spec=yes arch=$2 shift;; @@ -171,50 +175,63 @@ case $ARCH in fi esac +# Is the source tree checked out from svn ? +if test -e .svn/entries ; then + checkedout=1 +else + checkedout=0 +fi + ######################################### # Objective Caml programs -CAMLC=`which $bytecamlc` -case "$CAMLC" in - "") echo "$bytecamlc is not present in your path !" - echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: " - read CAMLC - +case $camldir_spec in + no) CAMLC=`which $bytecamlc` case "$CAMLC" in - "") CAMLC=/usr/local/bin/$bytecamlc;; - */ocamlc|*/ocamlc.opt) true;; - */) CAMLC="${CAMLC}"$bytecamlc;; - *) CAMLC="${CAMLC}"/$bytecamlc;; - esac + "") echo "$bytecamlc is not present in your path !" + echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: " + read CAMLC + + case "$CAMLC" in + "") CAMLC=/usr/local/bin/$bytecamlc;; + */ocamlc|*/ocamlc.opt) true;; + */) CAMLC="${CAMLC}"$bytecamlc;; + *) CAMLC="${CAMLC}"/$bytecamlc;; + esac + esac;; + yes) CAMLC=$camldir/$bytecamlc bytecamlc="$CAMLC" - nativecamlc=`dirname "$CAMLC"`/$nativecamlc;; + nativecamlc=`dirname "$bytecamlc"`/$nativecamlc;; esac if test ! -f "$CAMLC" ; then - echo "I can not find the executable '$CAMLC'! (Have you installed it?)" - echo "Configuration script failed!" - exit 1 + echo "I can not find the executable '$CAMLC'! (Have you installed it?)" + echo "Configuration script failed!" + exit 1 fi CAMLBIN=`dirname "$CAMLC"` -CAMLVERSION=`"$CAMLC" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` +bytecamlc="$CAMLC" +nativecamlc=$CAMLBIN/$nativecamlc + +CAMLVERSION=`"$bytecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` case $CAMLVERSION in - 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.08.0) + 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.08.0) echo "Your version of Objective-Caml is $CAMLVERSION." if [ "$CAMLVERSION" = "3.08.0" ] ; then - echo "You need Objective-Caml 3.06 or later (to the exception of 3.08.0)!" + echo "You need Objective-Caml 3.06 or later (to the exception of 3.08.0)!" else - echo "You need Objective-Caml 3.06 or later!"; + echo "You need Objective-Caml 3.06 or later!" fi echo "Configuration script failed!" exit 1;; - 3.06|3.07*|3.08*) + 3.06|3.07*|3.08*) echo "You have Objective-Caml $CAMLVERSION. Good!";; - ?*) + ?*) CAMLP4COMPAT="-loc loc" echo "You have Objective-Caml $CAMLVERSION. Good!";; - *) + *) echo "I found the Objective-Caml compiler but cannot find its version number!" echo "Is it installed properly ?" echo "Configuration script failed!" @@ -226,17 +243,18 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"` # do we have a native compiler: test of ocamlopt and its version if [ "$best_compiler" = "opt" ] ; then - CAMLOPT=`which $nativecamlc` - case "$CAMLOPT" in - "") best_compiler=byte - echo "You have only bytecode compilation.";; - *) CAMLOPTVERSION=`"$CAMLOPT" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` - if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then \ - echo "native and bytecode compilers do not have the same version!"; fi - echo "You have native-code compilation. Good!" - esac + if test -e $nativecamlc ; then + CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` + if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then + echo "native and bytecode compilers do not have the same version!"; fi + echo "You have native-code compilation. Good!" + else + best_compiler=byte ; + echo "You have only bytecode compilation." + fi fi + # For coqmktop & bytecode compiler CAMLLIB=`"$CAMLC" -where` @@ -485,7 +503,7 @@ echo "" # An escaped version of a variable escape_var () { -ocaml 2>&1 1>/dev/null <<EOF +$CAMLBIN/ocaml 2>&1 1>/dev/null <<EOF prerr_endline(String.escaped(Sys.getenv"$VAR"));; EOF } @@ -595,6 +613,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|FSETSOPT|$fsets|" \ -e "s|REALSOPT|$reals|" \ -e "s|COQIDEOPT|$COQIDE|" \ + -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \ $COQTOP/config/Makefile.template > $COQTOP/config/Makefile chmod a-w $COQTOP/config/Makefile @@ -625,7 +644,7 @@ fi #################################################### if [ "$LABLGTKGE26" = "yes" ] ; then - cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli; + cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli else cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli fi diff --git a/ide/coq.ml b/ide/coq.ml index 37511f5a7..35201ed0c 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -53,18 +53,24 @@ let version () = let date = if Glib.Utf8.validate Coq_config.date then Coq_config.date - else "<date not printable>" - in - Printf.sprintf - "The Coq Proof Assistant, version %s (%s)\ - \nConfigured on %s\ - \nArchitecture %s running %s operating system\ - \nGtk version is %s\ - \nThis is the %s version (%s is the best one for this architecture and OS)\ - \n" - Coq_config.version date Coq_config.compile_date - Coq_config.arch Sys.os_type - (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) + else "<date not printable>" in + let get_version_date () = + try + let ch = open_in (Coq_config.coqtop^"/revision") in + let ver = input_line ch in + let rev = input_line ch in + (ver,rev) + with _ -> (Coq_config.version,date) in + let (rev,ver) = get_version_date () in + Printf.sprintf + "The Coq Proof Assistant, version %s (%s)\ + \nArchitecture %s running %s operating system\ + \nGtk version is %s\ + \nThis is the %s version (%s is the best one for this architecture and OS)\ + \n" + rev ver + Coq_config.arch Sys.os_type + (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) (if Mltop.get () = Mltop.Native then "native" else "bytecode") (if Coq_config.best="opt" then "native" else "bytecode") diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 180e2b011..ab63ff23a 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -65,6 +65,13 @@ sp is a local copy of the global variable extern_sp. */ # define print_int(i) #endif +/* Wrapper pour caml_modify */ +#ifdef OCAML_307 +#define CAML_MODIFY(a,b) caml_modify(a,b) +#else +#define CAML_MODIFY(a,b) caml_modify(a,b) +#endif + /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } @@ -637,7 +644,7 @@ value coq_interprete Field(accu, 0) = sp[0]; *sp = accu; /* mise a jour du block accumulate */ - caml_modify(&Field(p[i], 1),*sp); + CAML_MODIFY(&Field(p[i], 1),*sp); sp++; } pc += nfunc; @@ -808,21 +815,21 @@ value coq_interprete Instruct(SETFIELD0){ print_instr("SETFIELD0"); - caml_modify(&Field(accu, 0),*sp); + CAML_MODIFY(&Field(accu, 0),*sp); sp++; Next; } Instruct(SETFIELD1){ print_instr("SETFIELD1"); - caml_modify(&Field(accu, 1),*sp); + CAML_MODIFY(&Field(accu, 1),*sp); sp++; Next; } Instruct(SETFIELD){ print_instr("SETFIELD"); - caml_modify(&Field(accu, *pc),*sp); + CAML_MODIFY(&Field(accu, *pc),*sp); sp++; pc++; Next; } diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0dea6415b..70c85ca4c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -21,18 +21,16 @@ open Coqinit let get_version_date () = try - let ch = open_in (Coq_config.coqtop^"/make.result") in - let l = input_line ch in - let i = String.index l ' ' in - let j = String.index_from l (i+1) ' ' in - "checked out on "^(String.sub l (i+1) (j-i-1)) - with _ -> Coq_config.date + let ch = open_in (Coq_config.coqtop^"/revision") in + let ver = input_line ch in + let rev = input_line ch in + (ver,rev) + with _ -> (Coq_config.version,Coq_config.date) let print_header () = - Printf.printf "Welcome to Coq %s (%s)\n" - Coq_config.version - (get_version_date ()); - flush stdout + let (ver,rev) = (get_version_date ()) in + Printf.printf "Welcome to Coq %s (%s)\n" ver rev; + flush stdout let memory_stat = ref false |