diff options
author | courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 06:49:50 +0000 |
---|---|---|
committer | courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 06:49:50 +0000 |
commit | 831886a339af8bd5cd14f9d7e5ea4f9ff9ecd744 (patch) | |
tree | 10dfbd93f7d18df58ad25f5194a2ef8527e81fdf | |
parent | 5c18d2b232c85b8148ec86bd453440a634c38230 (diff) |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1612 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend | 4 | ||||
-rw-r--r-- | Makefile | 62 | ||||
-rw-r--r-- | config/coq_config.mli | 3 | ||||
-rwxr-xr-x | configure | 101 | ||||
-rw-r--r-- | distrib/Makefile | 8 | ||||
-rw-r--r-- | lib/options.ml | 2 | ||||
-rw-r--r-- | lib/options.mli | 2 | ||||
-rw-r--r-- | scripts/coqc.ml | 5 | ||||
-rw-r--r-- | toplevel/coqinit.ml | 24 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 3 | ||||
-rw-r--r-- | toplevel/usage.ml | 1 |
11 files changed, 98 insertions, 117 deletions
@@ -898,8 +898,8 @@ proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx parsing/printer.cmx \ proofs/proof_trees.cmx proofs/tacmach.cmx proofs/tactic_debug.cmi -scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi -scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx +scripts/coqc.cmo: config/coq_config.cmi lib/options.cmi toplevel/usage.cmi +scripts/coqc.cmx: config/coq_config.cmx lib/options.cmx toplevel/usage.cmx scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \ @@ -37,11 +37,11 @@ noargument: # Compilation options ########################################################################### -LOCALINCLUDES= -I config -I tools -I scripts -I lib -I kernel -I library \ - -I proofs -I tactics -I pretyping -I parsing -I toplevel \ - -I contrib/omega -I contrib/ring -I contrib/xml \ - -I contrib/extraction -I contrib/correctness \ - -I contrib/interface +LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \ + -I proofs -I tactics -I pretyping -I parsing -I toplevel \ + -I contrib/omega -I contrib/ring -I contrib/xml \ + -I contrib/extraction -I contrib/correctness \ + -I contrib/interface INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB) @@ -55,12 +55,7 @@ OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) CAMLP4EXTENDFLAGS=-I . pa_extend.cmo q_MLast.cmo CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' -COQINCLUDES=-I states -R theories Coq -R contrib Coq -# -I contrib/omega -I contrib/ring -I contrib/xml \ -# -I theories/Init -I theories/Logic -I theories/Arith \ -# -I theories/Bool -I theories/Zarith -I theories/Lists \ -# -I theories/Sets -I theories/Relations -I theories/Wellfounded \ -# -I theories/Reals +COQINCLUDES=-R theories Coq -R contrib Coq ########################################################################### # Objects files @@ -215,12 +210,12 @@ CMX=$(CMO:.cmo=.cmx) # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -COQMKTOP=bin/coqmktop -COQC=bin/coqc -COQTOPBYTE=bin/coqtop.byte -COQTOPOPT=bin/coqtop.opt -BESTCOQTOP=bin/coqtop.$(BEST) -COQINTERFACE=bin/coq-interface bin/parser +COQMKTOP=bin/coqmktop$(EXE) +COQC=bin/coqc$(EXE) +COQTOPBYTE=bin/coqtop.byte$(EXE) +COQTOPOPT=bin/coqtop.opt$(EXE) +BESTCOQTOP=bin/coqtop.$(BEST)$(EXE) +COQINTERFACE=bin/coq-interface$(EXE) bin/parser COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQINTERFACE) @@ -307,7 +302,7 @@ states: states/barestate.coq states/initial.coq SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v syntax/PPTactic.v states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP) - $(BESTCOQTOP) -q -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq + $(BESTCOQTOP) -boot -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/DatatypesSyntax.vo theories/Init/Prelude.vo \ @@ -317,7 +312,7 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/Logic_TypeSyntax.vo theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) - $(COQC) -$(BEST) -bindir bin -q -R theories Coq -is states/barestate.coq $< + $(COQC) -boot -$(BEST) $(INCLUDES) -R theories Coq -is states/barestate.coq $< init: $(INITVO) @@ -328,13 +323,13 @@ TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo \ tactics/EqDecide.vo $(EXTRACTIONVO) tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) - $(COQC) -$(BEST) -bindir bin -q -I tactics -is states/barestate.coq $< + $(COQC) -boot -$(BEST) $(INCLUDES) -I tactics -is states/barestate.coq $< contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC) - $(COQC) -$(BEST) -bindir bin -q -I contrib/extraction -is states/barestate.coq $< + $(COQC) -boot -$(BEST) $(COQINCLUDES) -is states/barestate.coq $< states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) $(BESTCOQTOP) - $(BESTCOQTOP) -q -batch -silent -is states/barestate.coq -I tactics -R theories Coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq + $(BESTCOQTOP) -boot -silent -is states/barestate.coq $(COQINCLUDES) $(INCLUDES) -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq clean:: rm -f states/*.coq @@ -467,10 +462,10 @@ XMLVO = contrib/xml/Xml.vo INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE) - $(COQC) -q -byte -bindir bin $(COQINCLUDES) $< + $(COQC) -boot -byte $(COQINCLUDES) $< -contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) - $(COQC) -q -byte -bindir bin $(COQINCLUDES) $< +contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq + $(COQC) -boot -byte $(COQINCLUDES) $< CONTRIBVO = $(OMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) $(CORRECTNESSVO)\ $(INTERFACEV0) @@ -494,13 +489,12 @@ archclean:: # tools ########################################################################### -COQDEP=bin/coqdep -COQMAKEFILE=bin/coq_makefile -GALLINA=bin/gallina -COQTEX=bin/coq-tex +COQDEP=bin/coqdep$(EXE) +COQMAKEFILE=bin/coq_makefile$(EXE) +GALLINA=bin/gallina$(EXE) +COQTEX=bin/coq-tex$(EXE) -tools: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \ - tools/coq.elc dev/top_printers.cmo +tools: $(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) dev/top_printers.cmo COQDEPCMO=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo @@ -536,7 +530,7 @@ MINICOQCMO=$(CONFIG) $(LIB) $(KERNEL) \ parsing/lexer.cmo parsing/g_minicoq.cmo \ toplevel/fhimsg.cmo toplevel/minicoq.cmo -MINICOQ=bin/minicoq +MINICOQ=bin/minicoq$(EXE) $(MINICOQ): $(MINICOQCMO) $(OCAMLC) $(INCLUDES) -o $@ -custom $(CMA) $(MINICOQCMO) $(OSDEPLIBS) @@ -584,7 +578,7 @@ install-library: $(MKDIR) $(FULLCOQLIB)/states cp states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLEMACSLIB) - cp tools/coq.el tools/coq.elc $(FULLEMACSLIB) + cp tools/coq.el $(FULLEMACSLIB) MANPAGES=tools/coq-tex.1 tools/coqdep.1 tools/gallina.1 @@ -707,7 +701,7 @@ clean:: $(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $< .v.vo: - $(COQC) -q -$(BEST) -bindir bin $(COQINCLUDES) $< + $(COQC) -boot -$(BEST) $(COQINCLUDES) $< .el.elc: echo "(setq load-path (cons \".\" load-path))" > $*.compile diff --git a/config/coq_config.mli b/config/coq_config.mli index 4f8c8f6d6..7482a45c9 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -23,7 +23,7 @@ val best : string (* byte/opt *) val arch : string (* architecture *) val osdeplibs : string (* OS dependant link options for ocamlc *) -val defined : string list (* options for lib/ocamlpp *) +(* val defined : string list (* options for lib/ocamlpp *) *) val version : string (* version number of Coq *) val versionsi : string (* version number of Coq\_SearchIsos *) @@ -33,3 +33,4 @@ val compile_date : string (* compile date *) val theories_dirs : string list val contrib_dirs : string list +val exec_extension : string (* "" under Unix, ".exe" under MS-windows *) @@ -183,16 +183,16 @@ case $emacslib_spec in yes) EMACSLIB=$emacslib;; esac -case $emacs_spec in - no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?" - read EMACS +# case $emacs_spec in +# no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?" +# read EMACS - case $EMACS in - "") EMACS=$emacs_def;; - *) true;; - esac;; - yes) EMACS=$emacs;; -esac +# case $EMACS in +# "") EMACS=$emacs_def;; +# *) true;; +# esac;; +# yes) EMACS=$emacs;; +# esac # OS dependent libraries @@ -383,59 +383,37 @@ rm -f $COQTOP/config/Makefile case $ARCH in win32) - sed -e "s|LOCALINSTALLATION|$local|" \ - -e "s|COQTOPDIRECTORY|$COQTOP|" \ - -e "s|COQVERSION|$VERSION|" \ - -e "s|BINDIRDIRECTORY|`echo $BINDIR |sed -e 's|\\\|/|g'`|" \ - -e "s|COQLIBDIRECTORY|`echo $LIBDIR |sed -e 's|\\\|/|g'`|" \ - -e "s|MANDIRDIRECTORY|`echo $MANDIR |sed -e 's|\\\|/|g'`|" \ - -e "s|EMACSLIBDIRECTORY|`echo $EMACSLIB |sed -e 's|\\\|/|g'`|" \ - -e "s|EMACSCOMMAND|$EMACS|" \ - -e "s|ARCHITECTURE|$ARCH|" \ - -e "s|OSDEPENDANTLIBS|$OSDEPLIBS|" \ - -e "s|OSDEPENDANTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \ - -e "s|STRLIBRARY|$WITH_STR|" \ - -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ - -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \ - -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ - -e "s|CAMLP4TOOL|$camlp4o|" \ - -e "s|OSKIND|$OSTYPE|" \ - -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ - -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ - -e "s|BESTCOMPILER|$best_compiler|" \ - -e "s|EXECUTEEXTENSION|$EXE|" \ - -e "s|BYTECAMLC|$bytecamlc|" \ - -e "s|NATIVECAMLC|$nativecamlc|" \ - -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \ - $COQTOP/config/Makefile.template > $COQTOP/config/Makefile;; - *) - sed -e "s|LOCALINSTALLATION|$local|" \ - -e "s|COQTOPDIRECTORY|$COQTOP|" \ - -e "s|COQVERSION|$VERSION|" \ - -e "s|BINDIRDIRECTORY|$BINDIR|" \ - -e "s|COQLIBDIRECTORY|$LIBDIR|" \ - -e "s|MANDIRDIRECTORY|$MANDIR|" \ - -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \ - -e "s|EMACSCOMMAND|$EMACS|" \ - -e "s|ARCHITECTURE|$ARCH|" \ - -e "s|OSDEPENDANTLIBS|$OSDEPLIBS|" \ - -e "s|OSDEPENDANTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \ - -e "s|STRLIBRARY|$WITH_STR|" \ - -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ - -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \ - -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ - -e "s|CAMLP4TOOL|$camlp4o|" \ - -e "s|OSKIND|$OSTYPE|" \ - -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ - -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ - -e "s|BESTCOMPILER|$best_compiler|" \ - -e "s|EXECUTEEXTENSION|$EXE|" \ - -e "s|BYTECAMLC|$bytecamlc|" \ - -e "s|NATIVECAMLC|$nativecamlc|" \ - -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \ - $COQTOP/config/Makefile.template > $COQTOP/config/Makefile;; + BINDIR=`echo $BINDIR |sed -e 's|\\\|/|g'` + LIBDIR=`echo $LIBDIR |sed -e 's|\\\|/|g'` + MANDIR=`echo $MANDIR |sed -e 's|\\\|/|g'`;; esac +sed -e "s|LOCALINSTALLATION|$local|" \ + -e "s|COQTOPDIRECTORY|$COQTOP|" \ + -e "s|COQVERSION|$VERSION|" \ + -e "s|BINDIRDIRECTORY|$BINDIR|" \ + -e "s|COQLIBDIRECTORY|$LIBDIR|" \ + -e "s|MANDIRDIRECTORY|$MANDIR|" \ + -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \ + -e "s|EMACSCOMMAND|$EMACS|" \ + -e "s|ARCHITECTURE|$ARCH|" \ + -e "s|OSDEPENDANTLIBS|$OSDEPLIBS|" \ + -e "s|OSDEPENDANTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \ + -e "s|STRLIBRARY|$WITH_STR|" \ + -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ + -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \ + -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ + -e "s|CAMLP4TOOL|$camlp4o|" \ + -e "s|OSKIND|$OSTYPE|" \ + -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ + -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ + -e "s|BESTCOMPILER|$best_compiler|" \ + -e "s|EXECUTEEXTENSION|$EXE|" \ + -e "s|BYTECAMLC|$bytecamlc|" \ + -e "s|NATIVECAMLC|$nativecamlc|" \ + -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \ + $COQTOP/config/Makefile.template > $COQTOP/config/Makefile + chmod a-w $COQTOP/config/Makefile # Building the $COQTOP/dev/ocamldebug-v7 file @@ -466,11 +444,12 @@ let camlp4lib = "$CAMLP4LIB" let best = "$best_compiler" let arch = "$ARCH" let osdeplibs = "$OSDEPLIBS" -let defined = [ "$OSTYPE" ] +(* let defined = [ "$OSTYPE" ] *) let version = "$VERSION" let versionsi = "$VERSIONSI" let date = "$DATE" let compile_date = "$COMPILEDATE" +let exec_extension = "$EXE" END_OF_COQ_CONFIG diff --git a/distrib/Makefile b/distrib/Makefile index 88f870a47..0bb793b5b 100644 --- a/distrib/Makefile +++ b/distrib/Makefile @@ -1,6 +1,6 @@ # Building the different files of the coq distribution -include config.distrib +sinclude config.distrib LOCALARCH=`uname -m` ARCH=`uname -m | sed -e 's/i.86/i386/'` SYSTEM=`uname -s` @@ -41,6 +41,7 @@ noarguments: @echo "make arch-rpm-ftp-install |repository supposed" @echo "make arch-tar-gz-ftp-install |to be already" @echo "make contrib-ftp-install |prepared" + @echo "make deb to build a debian package" ################## Main targets @@ -259,3 +260,8 @@ contrib-ftp-install: prep-ftp-install patch-ftp-install: prep-ftp-install cp patch-${VERSION}-$(PREVIOUSVERSION).gz ${FTPDIR}/V${VERSION}/ chmod g+w ${FTPDIR}/V${VERSION}/patch-${VERSION}-$(PREVIOUSVERSION).gz + +deb: + rm -rf ../debian + cp -a debian .. + cd .. ; dpkg-buildpackage -rfakeroot -uc -us diff --git a/lib/options.ml b/lib/options.ml index 52babfdb2..b00d52373 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -10,6 +10,8 @@ open Util +let boot = ref false + let batch_mode = ref false let debug = ref false diff --git a/lib/options.mli b/lib/options.mli index 8d1d7e2fd..e70d38669 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -10,6 +10,8 @@ (* Global options of the system. *) +val boot : bool ref + val batch_mode : bool ref val debug : bool ref diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 0ef69ab08..022656720 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -127,6 +127,9 @@ let parse_args () = keep := true ; parse (cfiles,args) rem | ("-verbose" | "--verbose") :: rem -> verbose := true ; parse (cfiles,args) rem + | "-boot" :: rem -> + bindir:= Filename.concat Coq_config.coqtop "bin"; + parse (cfiles, "-boot"::args) rem | "-bindir" :: d :: rem -> bindir := d ; parse (cfiles,args) rem | "-bindir" :: [] -> @@ -182,7 +185,7 @@ let main () = usage () end; let coqtopname = - if !image <> "" then !image else Filename.concat !bindir !binary + if !image <> "" then !image else Filename.concat !bindir (!binary ^ Coq_config.exec_extension) in List.iter (compile coqtopname args) cfiles diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 7b3fa1628..01dec915a 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -70,22 +70,14 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft (* Initializes the LoadPath according to COQLIB and Coq_config *) let init_load_path () = - if Coq_config.local then begin - (* local use (no installation) *) - List.iter - (fun s -> coq_add_path (Filename.concat Coq_config.coqtop s)) - ["states"; "dev"]; - coq_add_rec_path (Filename.concat Coq_config.coqtop "theories"); - coq_add_path (Filename.concat Coq_config.coqtop "tactics"); - coq_add_rec_path (Filename.concat Coq_config.coqtop "contrib") - end else begin - (* default load path; variable COQLIB overrides the default library *) - let coqlib = getenv_else "COQLIB" Coq_config.coqlib in - coq_add_path (Filename.concat coqlib "states"); - coq_add_rec_path (Filename.concat coqlib "theories"); - coq_add_path (Filename.concat coqlib "tactics"); - coq_add_rec_path (Filename.concat coqlib "contrib") - end; + (* developper specific directories to open *) + let dev = if Coq_config.local then [ "dev" ] else [] in + let dirs = "states" :: dev @ [ "theories"; "tactics"; "contrib" ] in + let coqlib = + if Coq_config.local || !Options.boot then Coq_config.coqtop + (* variable COQLIB overrides the default library *) + else getenv_else "COQLIB" Coq_config.coqlib in + List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs; let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in add_ml_include camlp4; Mltop.add_path "." [Nametab.default_root]; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0778b7735..9e9c3436a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -120,7 +120,8 @@ let parse_args () = | "-full" :: rem -> warning "option -full deprecated\n"; parse rem | "-batch" :: rem -> set_batch_mode (); parse rem - + | "-boot" :: rem -> boot := true; no_load_rc (); set_batch_mode (); + parse rem | "-outputstate" :: s :: rem -> set_outputstate s; parse rem | "-outputstate" :: [] -> usage () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8dc848d3c..f9d5decd9 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -47,6 +47,7 @@ let print_usage_channel co command = -init-file f set the rcfile to f -user u use the rcfile of user u -batch batch mode (exits just after arguments parsing) + -boot boot mode (implies -q and -batch) -emacs tells Coq it is executed under Emacs " |