diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | Makefile.build | 28 | ||||
| -rw-r--r-- | Makefile.common | 9 | ||||
| -rw-r--r-- | checker/checker.ml | 15 | ||||
| -rw-r--r-- | config/coq_config.mli | 1 | ||||
| -rwxr-xr-x | configure | 15 | ||||
| -rw-r--r-- | ide/coq.ml | 22 | ||||
| -rw-r--r-- | toplevel/usage.ml | 16 |
8 files changed, 39 insertions, 69 deletions
@@ -208,7 +208,7 @@ depclean: find . $(FIND_VCS_CLAUSE) -name '*.d' | xargs rm -f cleanconfig: - rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli $(REVISIONML) distclean: clean cleanconfig diff --git a/Makefile.build b/Makefile.build index cbb2d3fe8..1afa656a9 100644 --- a/Makefile.build +++ b/Makefile.build @@ -784,48 +784,52 @@ $(foreach f,$(RECTYPESML),$(eval $(call rectypes-rules-template,$(f)))) # source tree .PHONY: revision -revision: +revision $(REVISIONML): $(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,\}\)/\1/p' > revision.new; \ - svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \ + 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; \ fi endif ifeq ($(CHECKEDOUT),gnuarch) $(HIDE)set -e; \ if test -x "`which tla`"; then \ LANG=C; export LANG; \ - tla tree-version > revision.new ; \ - tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \ + tla tree-version | sed -e 's/\(.*\)/let version = "\1"/' > revision.new ; \ + tla tree-revision | sed -ne 's|.*--\(.*\)|let revision = \"\1\"|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/^\* \(.*\)/\1/p'); \ + GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/let version = "\1"/p'); \ GIT_HOST=$$(hostname --fqdn); \ GIT_PATH=$$(pwd); \ (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ - git log -1 | sed -ne '/^commit /s/^commit[[:space:]]\+\(.*\)/\1/p' >> revision.new; \ + git log -1 | sed -ne '/^commit /s/^commit[[:space:]]\+\(.*\)/let revision = "\1"/p' >> revision.new; \ fi endif $(HIDE)set -e; \ if test -e revision.new; then \ if test -e revision; then \ - if test "`cat revision`" = "`cat revision.new`" ; then \ + if test "`cat $(REVISIONML)`" = "`cat revision.new`" ; then \ rm -f revision.new; \ else \ - mv -f revision.new revision; \ + mv -f revision.new $(REVISIONML); \ fi; \ else \ - mv -f revision.new revision; \ - fi \ - fi + mv -f revision.new $(REVISIONML); \ + fi; \ + else \ + echo 'let version = Coq_config.version' > $(REVISIONML); \ + echo 'let revision = Coq_config.date' >> $(REVISIONML); \ + fi; \ + echo 'let date = "$(shell date +"%h %d %Y %H:%M:%S")"' >> $(REVISIONML) ########################################################################### # Default rules diff --git a/Makefile.common b/Makefile.common index 5a7f50404..9c1962af7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -128,6 +128,9 @@ CAMLP4OBJS:=gramlib.cma CONFIG:=\ config/coq_config.cmo +REVISIONML:=config/revision.ml +REVISIONCMO:=$(REVISIONML:.ml=.cmo) + LIBREP:=\ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ lib/util.cmo lib/bigint.cmo lib/hashcons.cmo lib/dyn.cmo lib/system.cmo \ @@ -227,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:=\ @@ -391,7 +394,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:=\ @@ -440,7 +443,7 @@ COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \ # checker MCHECKER:=\ - config/coq_config.cmo \ + config/coq_config.cmo $(REVISIONCMO) \ 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 \ diff --git a/checker/checker.ml b/checker/checker.ml index 9c1802cab..ebd54f7fb 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -41,17 +41,8 @@ let path_of_string s = let (/) = Filename.concat -let get_version_date () = - 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,Coq_config.date) - let print_header () = - let (ver,rev) = (get_version_date ()) in - Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; + Printf.printf "Welcome to Chicken %s (%s)\n" Revision.version Revision.revision; flush stdout (* Adding files to Coq loadpath *) @@ -166,8 +157,8 @@ let compile_files () = let version () = Printf.printf "The Coq Proof Checker, version %s (%s)\n" - Coq_config.version Coq_config.date; - Printf.printf "compiled on %s\n" Coq_config.compile_date; + Revision.version Revision.revision; + Printf.printf "compiled on %s\n" Revision.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 1eff9c38d..c88d0d170 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -30,7 +30,6 @@ 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 @@ -9,7 +9,7 @@ VERSION=trunk VOMAGIC=08193 STATEMAGIC=19764 -DATE="date unspecified" +DATE=`date +"%B %Y"` # Create the bin/ directory if non-existent test -d bin || mkdir bin @@ -252,15 +252,6 @@ 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 @@ -884,6 +875,7 @@ case $ARCH in ESCCOQTOP="$COQTOP" ESCBINDIR="$BINDIR" ESCSRCDIR="$COQSRC" + ESCDOSSRCDIR="$COQSRC" ESCLIBDIR="$LIBDIR" ESCCAMLDIR="$CAMLBIN" ESCCAMLLIB="$CAMLLIB" @@ -894,6 +886,8 @@ case $ARCH in ESCCAMLP4BIN="$CAMLP4BIN" ESCCAMLP4LIB="$CAMLP4LIB" ESCLABLGTKINCLUDES="$LABLGTKINCLUDES" + ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS" + ESCBUILDLDPATH="$BUILDLDPATH" ;; esac @@ -917,7 +911,6 @@ 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 c60507251..69d8f680f 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -52,31 +52,21 @@ let init () = let i = ref 0 -let get_version_date () = - let date = - if Glib.Utf8.validate Coq_config.date - then Coq_config.date - else "<date not printable>" in - 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 revision = + if Glib.Utf8.validate Revision.revision + then Revision.revision + else "<date not printable>" in + Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" Revision.version revision 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" - ver date + Revision.version Revision.revision 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/toplevel/usage.ml b/toplevel/usage.ml index b411a4f96..fb26f5039 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -8,23 +8,13 @@ (* $Id$ *) -let get_version_date () = - 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,Coq_config.date) - let print_header () = - let (ver,rev) = (get_version_date ()) in - Printf.printf "Welcome to Coq %s (%s)\n" ver rev; + Printf.printf "Welcome to Coq %s (%s)\n" Revision.version Revision.revision; flush stdout let version () = - let (ver,rev) = (get_version_date ()) in - Printf.printf "The Coq Proof Assistant, version %s (%s)\n" ver rev; - Printf.printf "compiled on %s\n" Coq_config.compile_date; + Printf.printf "The Coq Proof Assistant, version %s (%s)\n" Revision.version Revision.revision; + Printf.printf "compiled on %s\n" Revision.date; exit 0 (* print the usage of coqtop (or coqc) on channel co *) |