diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | Makefile.build | 41 | ||||
| -rw-r--r-- | Makefile.common | 10 | ||||
| -rw-r--r-- | checker/checker.ml | 16 | ||||
| -rw-r--r-- | config/coq_config.mli | 1 | ||||
| -rwxr-xr-x | configure | 16 | ||||
| -rw-r--r-- | ide/coq.ml | 22 | ||||
| -rw-r--r-- | tools/coqdoc/main.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 16 | ||||
| -rw-r--r-- | toplevel/usage.ml | 10 | ||||
| -rw-r--r-- | toplevel/usage.mli | 3 |
11 files changed, 87 insertions, 52 deletions
@@ -210,7 +210,7 @@ depclean: find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f cleanconfig: - rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli config/revision.ml + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli distclean: clean cleanconfig diff --git a/Makefile.build b/Makefile.build index c95c053df..7b5bd7d51 100644 --- a/Makefile.build +++ b/Makefile.build @@ -675,6 +675,7 @@ endif # it with libraries -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega + $(INSTALLLIB) revision $(FULLCOQLIB) install-library-light: $(MKDIR) $(FULLCOQLIB) @@ -683,6 +684,7 @@ install-library-light: $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT) $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states + $(INSTALLLIB) revision $(FULLCOQLIB) install-allreals:: $(INSTALLSH) $(FULLCOQLIB) $(ALLREALS) @@ -780,50 +782,47 @@ $(foreach f,$(RECTYPESML),$(eval $(call rectypes-rules-template,$(f)))) # source tree .PHONY: revision -revision config/revision.ml: +revision: $(SHOW)'CHECK revision' $(HIDE)rm -f revision.new ifeq ($(CHECKEDOUT),svn) $(HIDE)set -e; \ if test -x "`which svn`"; then \ export LC_ALL=C;\ - svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/let version = "\1"/p' > revision.new; \ - svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/let revision = "\1"/p'>> revision.new; \ + svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \ + svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \ fi endif ifeq ($(CHECKEDOUT),gnuarch) $(HIDE)set -e; \ if test -x "`which tla`"; then \ LANG=C; export LANG; \ - tla tree-version | sed -e 's/\(.*\)/let version = "\1"/' > revision.new ; \ - tla tree-revision | sed -ne 's|.*--\(.*\)|let revision = \"\1\"|p' >> revision.new ; \ + tla tree-version > revision.new ; \ + tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \ fi endif ifeq ($(CHECKEDOUT),git) $(HIDE)set -e; \ if test -x "`which git`"; then \ LANG=C; export LANG; \ - GIT_BRANCH=$$(git branch -a | sed -ne 's/^\* //p'); \ + GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ GIT_HOST=$$(hostname --fqdn); \ GIT_PATH=$$(pwd); \ - echo "let version = \"$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}\"" > revision.new; \ - echo "let revision = \"$$(git log -1 --pretty='format:%H')\"" >> revision.new; \ + (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ + (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ fi endif $(HIDE)set -e; \ - if test ! -e revision.new; then \ - echo 'let version = Coq_config.version' > revision.new; \ - echo 'let revision = Coq_config.date' >> revision.new; \ - fi; \ - echo 'let date = "$(shell date +"%h %d %Y %H:%M:%S")"' >> revision.new ; \ - if test -e config/revision.ml; then \ - if test "`head -2 config/revision.ml`" = "`head -2 revision.new`" ; then \ - rm -f revision.new; \ - else \ - mv -f revision.new config/revision.ml; \ - fi; \ - else \ - mv -f revision.new config/revision.ml; \ + if test -e revision.new; then \ + if test -e revision; then \ + if test "`cat revision`" = "`cat revision.new`" ; then \ + rm -f revision.new; \ + else \ + mv -f revision.new revision; \ + fi; \ + else \ + mv -f revision.new revision; \ + fi \ fi ########################################################################### diff --git a/Makefile.common b/Makefile.common index 0b714d1f6..9a4f85231 100644 --- a/Makefile.common +++ b/Makefile.common @@ -127,7 +127,7 @@ CLIBS:=unix.cma CAMLP4OBJS:=gramlib.cma CONFIG:=\ - config/coq_config.cmo config/revision.cmo + config/coq_config.cmo LIBREP:=\ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ @@ -230,7 +230,7 @@ TOPLEVEL:=\ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ toplevel/vernacentries.cmo toplevel/whelp.cmo toplevel/vernac.cmo \ toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \ - toplevel/toplevel.cmo toplevel/usage.cmo \ + toplevel/toplevel.cmo $(REVISIONCMO) toplevel/usage.cmo \ toplevel/coqinit.cmo toplevel/coqtop.cmo HIGHTACTICS:=\ @@ -399,7 +399,7 @@ COQENVCMO:=$(CONFIG) lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx) -COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo +COQCCMO:=$(COQENVCMO) $(REVISIONCMO) toplevel/usage.cmo scripts/coqc.cmo COQCCMX:=$(COQCCMO:.cmo=.cmx) INTERFACE:=\ @@ -448,7 +448,7 @@ COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \ # checker MCHECKER:=\ - $(CONFIG) \ + config/coq_config.cmo \ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo \ lib/flags.cmo lib/util.cmo lib/option.cmo lib/hashcons.cmo \ lib/system.cmo lib/envars.cmo \ @@ -517,7 +517,7 @@ STAGE1_CMO:=$(GRAMMARCMO) parsing/q_constr.cmo STAGE1:=parsing/grammar.cma parsing/q_constr.cmo PRINTERSCMO:=\ - $(CONFIG) lib/lib.cma \ + config/coq_config.cmo lib/lib.cma \ kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \ kernel/mod_subst.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo \ kernel/sign.cmo kernel/declarations.cmo kernel/retroknowledge.cmo \ diff --git a/checker/checker.ml b/checker/checker.ml index ebd54f7fb..3d9289334 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -41,8 +41,18 @@ let path_of_string s = let (/) = Filename.concat +let get_version_date () = + try + let coqlib = Envars.coqlib () in + let ch = open_in (Filename.concat coqlib "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 Chicken %s (%s)\n" Revision.version Revision.revision; + let (ver,rev) = (get_version_date ()) in + Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; flush stdout (* Adding files to Coq loadpath *) @@ -157,8 +167,8 @@ let compile_files () = let version () = Printf.printf "The Coq Proof Checker, version %s (%s)\n" - Revision.version Revision.revision; - Printf.printf "compiled on %s\n" Revision.date; + Coq_config.version Coq_config.date; + Printf.printf "compiled on %s\n" Coq_config.compile_date; exit 0 (* print the usage of coqtop (or coqc) on channel co *) diff --git a/config/coq_config.mli b/config/coq_config.mli index c88d0d170..1eff9c38d 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -30,6 +30,7 @@ val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *) val version : string (* version number of Coq *) val date : string (* release date *) +val compile_date : string (* compile date *) val vo_magic_number : int val state_magic_number : int @@ -263,6 +263,15 @@ if [ $prefix_spec = yes -a $local = true ] ; then exit 1 fi +# compile date +DATEPGM=`which date` +case $DATEPGM in + "") echo "I can't find the program \"date\" in your path." + echo "Please give me the current date" + read COMPILEDATE;; + *) COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;; +esac + # Architecture case $arch_spec in @@ -889,8 +898,7 @@ case $ARCH in win32) ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'` ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCSRCDIR=`echo $COQSRC |sed -e 's|\\\|\\\\\\\|g'` - ESCDOSSRCDIR=`cygpath -d $COQSRC |sed -e 's|\\\|\\\\\\\|g'` + ESCSRCDIR=`cygpath -d $COQSRC |sed -e 's|\\\|\\\\\\\|g'` ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'` ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'` @@ -909,7 +917,6 @@ case $ARCH in ESCCOQTOP="$COQTOP" ESCBINDIR="$BINDIR" ESCSRCDIR="$COQSRC" - ESCDOSSRCDIR="$COQSRC" ESCLIBDIR="$LIBDIR" ESCCAMLDIR="$CAMLBIN" ESCCAMLLIB="$CAMLLIB" @@ -934,7 +941,7 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file let local = $local let coqrunbyteflags = "$ESCCOQRUNBYTEFLAGS" let coqlib = "$ESCLIBDIR" -let coqsrc = "$ESCDOSSRCDIR" +let coqsrc = "$ESCSRCDIR" let camlbin = "$ESCCAMLDIR" let camllib = "$ESCCAMLLIB" let camlp4 = "$CAMLP4" @@ -946,6 +953,7 @@ let has_natdynlink = $HASNATDYNLINK let osdeplibs = "$OSDEPLIBS" let version = "$VERSION" let date = "$DATE" +let compile_date = "$COMPILEDATE" let vo_magic_number = $VOMAGIC let state_magic_number = $STATEMAGIC let exec_extension = "$EXE" diff --git a/ide/coq.ml b/ide/coq.ml index e58a1bd19..c6aad9ffa 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -52,21 +52,31 @@ let init () = let i = ref 0 -let short_version () = - let revision = - if Glib.Utf8.validate Revision.revision - then Revision.revision +let get_version_date () = + 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)\n" Revision.version revision + try + let ch = open_in (Coq_config.coqsrc^"/revision") in + let ver = input_line ch in + let rev = input_line ch in + (ver,rev) + with _ -> (Coq_config.version,date) + +let short_version () = + let (ver,date) = get_version_date () in + Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date let version () = + let (ver,date) = 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" - Revision.version Revision.revision + ver date Coq_config.arch Sys.os_type (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) (if Mltop.is_native then "native" else "bytecode") diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index f187ae50d..04f9ee4b0 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -78,7 +78,7 @@ let obsolete s = let banner () = eprintf "This is coqdoc version %s, compiled on %s\n" - Revision.version Revision.date; + Coq_config.version Coq_config.compile_date; flush stderr let target_full_name f = diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b4e23a874..b75ef535f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -19,6 +19,20 @@ open States open Toplevel open Coqinit +let get_version_date () = + try + let coqlib = Envars.coqlib () in + let ch = open_in (Filename.concat coqlib "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 () = + let (ver,rev) = (get_version_date ()) in + Printf.printf "Welcome to Coq %s (%s)\n" ver rev; + flush stdout + let output_context = ref false let memory_stat = ref false @@ -324,7 +338,7 @@ let init is_ide = try parse_args is_ide; re_exec is_ide; - if_verbose Usage.print_header (); + if_verbose print_header (); init_load_path (); inputstate (); set_vm_opt (); diff --git a/toplevel/usage.ml b/toplevel/usage.ml index fb26f5039..4494a01e9 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -8,13 +8,10 @@ (* $Id$ *) -let print_header () = - Printf.printf "Welcome to Coq %s (%s)\n" Revision.version Revision.revision; - flush stdout - let version () = - Printf.printf "The Coq Proof Assistant, version %s (%s)\n" Revision.version Revision.revision; - Printf.printf "compiled on %s\n" Revision.date; + Printf.printf "The Coq Proof Assistant, version %s (%s)\n" + Coq_config.version Coq_config.date; + Printf.printf "compiled on %s\n" Coq_config.compile_date; exit 0 (* print the usage of coqtop (or coqc) on channel co *) @@ -101,4 +98,3 @@ let print_config () = Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib - diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 37d96cfa8..fb973e3ba 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -21,6 +21,3 @@ val print_usage_coqc : unit -> unit (*s Prints the configuration information *) val print_config : unit -> unit - -(*s Prints the header *) -val print_header : unit -> unit |