diff options
-rw-r--r-- | Makefile.build | 39 | ||||
-rw-r--r-- | Makefile.common | 18 | ||||
-rw-r--r-- | Makefile.doc | 6 | ||||
-rw-r--r-- | checker/checker.ml | 12 | ||||
-rw-r--r-- | config/coq_config.mli | 7 | ||||
-rwxr-xr-x | configure | 10 | ||||
-rw-r--r-- | contrib/dp/dp_gappa.ml | 4 | ||||
-rw-r--r-- | contrib/interface/parse.ml | 2 | ||||
-rw-r--r-- | contrib/micromega/coq_micromega.ml | 2 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.ml | 2 | ||||
-rwxr-xr-x | doc/stdlib/make-library-files | 6 | ||||
-rw-r--r-- | ide/coq.ml | 4 | ||||
-rw-r--r-- | ide/ideutils.ml | 5 | ||||
-rw-r--r-- | lib/envars.ml | 83 | ||||
-rw-r--r-- | lib/envars.mli | 15 | ||||
-rw-r--r-- | lib/flags.ml | 13 | ||||
-rw-r--r-- | lib/flags.mli | 10 | ||||
-rw-r--r-- | scripts/coqc.ml | 46 | ||||
-rw-r--r-- | scripts/coqmktop.ml | 83 | ||||
-rwxr-xr-x | test-suite/check | 4 | ||||
-rw-r--r-- | tools/coq_makefile.ml4 | 53 | ||||
-rw-r--r-- | tools/coqdep.ml | 18 | ||||
-rw-r--r-- | tools/coqdoc/main.ml | 3 | ||||
-rw-r--r-- | toplevel/coqinit.ml | 24 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 7 | ||||
-rw-r--r-- | toplevel/usage.ml | 8 |
26 files changed, 303 insertions, 181 deletions
diff --git a/Makefile.build b/Makefile.build index 5388b20b0..4e3dd1c5e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -179,12 +179,12 @@ initplugins: $(INITPLUGINSOPT) $(INITPLUGINS) $(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(STRIP) $@ $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ $(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP) cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) @@ -196,12 +196,12 @@ CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(CHICKENOPT): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ unix.cmxa gramlib.cmxa $^ + $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^ $(STRIP) $@ $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma $^ + $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE) @@ -210,11 +210,13 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) $(COQMKTOPBYTE): $(COQMKTOPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma\ + $^ $(OSDEPLIBS) $(COQMKTOPOPT): $(COQMKTOPCMX) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa\ + $^ $(OSDEPLIBS) $(STRIP) $@ $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP) @@ -231,11 +233,11 @@ scripts/tolink.ml: Makefile.build Makefile.common $(COQCBYTE): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $(COQCCMO) $(OSDEPLIBS) $(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ unix.cmxa $(COQCCMX) $(OSDEPLIBS) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $(COQCCMX) $(OSDEPLIBS) $(STRIP) $@ $(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC) @@ -399,12 +401,12 @@ coqide-files: $(IDEFILES) $(COQIDEOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) ide/ide.cmxa $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -ide -opt $(OPTFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -ide -opt $(OPTFLAGS) -o $@ $(STRIP) $@ $(COQIDEBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) ide/ide.cma $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -g -ide -top $(BYTEFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -g -ide -top $(BYTEFLAGS) -o $@ $(COQIDE): cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) @@ -466,21 +468,21 @@ pcoq-binaries:: $(COQINTERFACE) bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(INTERFACE) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE) + $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ $(INTERFACE) bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX) + $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(INTERFACECMX) bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) $(COQRUNBYTEFLAGS) -linkall $(BYTEFLAGS) -o $@ \ - dynlink.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO) + dynlink.cma str.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO) bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \ - $(LIBCOQRUN) $(DYNLINKCMXA) nums.cmxa $(CMXA) $(PARSERCMX) + $(LIBCOQRUN) $(DYNLINKCMXA) str.cmxa nums.cmxa $(CMXA) $(PARSERCMX) pcoq-files:: $(INTERFACEVO) $(INTERFACERC) @@ -595,7 +597,7 @@ tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEP): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS) $(GALLINA): $(GALLINACMO) $(SHOW)'OCAMLC -o $@' @@ -667,11 +669,12 @@ install-library: $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLCOQLIB)/user-contrib - $(INSTALLLIB) $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB) + cp --parents $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB) ifeq ($(BEST),opt) - $(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB) + cp --parents $(LINKCMX) $(FULLCOQLIB) endif - find . $(FIND_VCS_CLAUSE) $(PRUNE_CHECKER) -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \; + find . $(FIND_VCS_CLAUSE) \( -name \*.o -o -name \*.a -o -name \*.cmxs \) -exec cp --parents {} $(FULLCOQLIB) \; + find . $(FIND_VCS_CLAUSE) -name \*.cmi -exec cp --parents {} $(FULLCOQLIB) \; # csdpcert is not meant to be directly called by the user; we install # it with libraries -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega diff --git a/Makefile.common b/Makefile.common index 63740d086..c2f3e305b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -1,3 +1,4 @@ + ####################################################################### # v # The Coq Proof Assistant / The Coq Development Team # # <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # @@ -130,7 +131,7 @@ CONFIG:=\ 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 \ - lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \ + lib/envars.cmo lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \ lib/tlm.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \ lib/predicate.cmo lib/rtree.cmo lib/heap.cmo lib/option.cmo # Rem: Cygwin already uses variable LIB @@ -391,11 +392,14 @@ COQIDECMO:=ide/utils/okey.cmo ide/utils/config_file.cmo \ COQIDECMX:=$(COQIDECMO:.cmo=.cmx) -COQMKTOPCMO:=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo +COQENVCMO:=$(CONFIG) lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ + lib/util.cmo lib/system.cmo lib/envars.cmo + +COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo +COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx) -COQMKTOPCMX:=config/coq_config.cmx scripts/tolink.cmx scripts/coqmktop.cmx -COQCCMO:=$(CONFIG) toplevel/usage.cmo lib/pp_control.cmo lib/pp.cmo scripts/coqc.cmo -COQCCMX:=config/coq_config.cmx toplevel/usage.cmx lib/pp_control.cmx lib/pp.cmx scripts/coqc.cmx +COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo +COQCCMX:=$(COQCCMO:.cmo=.cmx) INTERFACE:=\ contrib/interface/vtp.cmo contrib/interface/xlate.cmo \ @@ -433,7 +437,7 @@ CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx) DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma -COQDEPCMO:=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo +COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep.cmo GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \ tools/coqdoc/index.cmo tools/coqdoc/output.cmo \ @@ -446,7 +450,7 @@ MCHECKER:=\ 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/system.cmo lib/envars.cmo \ lib/predicate.cmo lib/rtree.cmo \ kernel/names.cmo kernel/univ.cmo \ kernel/esubst.cmo checker/term.cmo \ diff --git a/Makefile.doc b/Makefile.doc index 10550da3a..9f98cc2b5 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -153,12 +153,12 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html doc/stdlib/index-body.html: | $(COQDOC) $(THEORIESVO) - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -d doc/stdlib/html --multi-index --html \ + $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html doc/stdlib/index-list.html: doc/stdlib/index-list.html.template - COQTOP=$(COQSRC) ./doc/stdlib/make-library-index doc/stdlib/index-list.html + ./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html cat doc/stdlib/index-list.html > $@ @@ -168,7 +168,7 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm ### Standard library (light version, full version is definitely too big) doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) - $(COQSRC)/$(COQDOC) -q --gallina --body-only --latex --stdout \ + $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex diff --git a/checker/checker.ml b/checker/checker.ml index 1ed094cf2..9c1802cab 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -43,7 +43,7 @@ let (/) = Filename.concat let get_version_date () = try - let ch = open_in (Coq_config.coqlib^"/revision") in + let ch = open_in (Coq_config.coqsrc ^ "/revision") in let ver = input_line ch in let rev = input_line ch in (ver,rev) @@ -108,13 +108,9 @@ let set_rec_include d p = check_coq_overwriting p; push_rec_include(d,p) -(* Initializes the LoadPath according to COQLIB and Coq_config *) +(* Initializes the LoadPath *) let init_load_path () = - let coqlib = - (* variable COQLIB overrides the default library *) - getenv_else "COQLIB" - (if Coq_config.local || !Flags.boot then Coq_config.coqtop - else Coq_config.coqlib) in + let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let contrib = coqlib/"contrib" in (* first user-contrib *) @@ -323,7 +319,7 @@ let parse_args() = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 + print_endline (Envars.coqlib ()); exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () diff --git a/config/coq_config.mli b/config/coq_config.mli index e5a32708d..1eff9c38d 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -10,15 +10,14 @@ val local : bool (* local use (no installation) *) -val bindir : string (* where the binaries are installed *) val coqlib : string (* where the std library is installed *) +val coqsrc : string (* where are the sources *) -val coqtop : string (* where are the sources *) - -val camldir : string (* base directory of OCaml binaries *) +val camlbin : string (* base directory of OCaml binaries *) val camllib : string (* for Dynlink *) val camlp4 : string (* exact name of camlp4: either "camlp4" ou "camlp5" *) +val camlp4bin : string (* base directory for Camlp4/5 binaries *) val camlp4lib : string (* where is the library of Camlp4 *) val best : string (* byte/opt *) @@ -862,6 +862,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'` ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'` ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'` @@ -876,6 +877,7 @@ case $ARCH in *) ESCCOQTOP="$COQTOP" ESCBINDIR="$BINDIR" + ESCSRCDIR="$COQSRC" ESCLIBDIR="$LIBDIR" ESCCAMLDIR="$CAMLBIN" ESCCAMLLIB="$CAMLLIB" @@ -896,12 +898,12 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file let local = $local let coqrunbyteflags = "$COQRUNBYTEFLAGS" -let bindir = try Sys.getenv "COQBIN" with Not_found -> "$ESCBINDIR" -let coqlib = try Sys.getenv "COQLIB" with Not_found -> "$ESCLIBDIR" -let coqtop = try Sys.getenv "COQTOP" with Not_found -> "$ESCCOQTOP" -let camldir = "$ESCCAMLDIR" +let coqlib = "$ESCLIBDIR" +let coqsrc = "$ESCSRCDIR" +let camlbin = "$ESCCAMLDIR" let camllib = "$ESCCAMLLIB" let camlp4 = "$CAMLP4" +let camlp4bin = "$ESCCAMLP4BIN" let camlp4lib = "$ESCCAMLP4LIB" let best = "$best_compiler" let arch = "$ARCH" diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml index f77f1a5c4..9c035aa85 100644 --- a/contrib/dp/dp_gappa.ml +++ b/contrib/dp/dp_gappa.ml @@ -153,7 +153,7 @@ let call_gappa hl p = let gappa_out2 = temp_file "gappa2" in patch_gappa_proof gappa_out gappa_out2; remove_file gappa_out; - let cmd = sprintf "%s/coqc %s" Coq_config.bindir gappa_out2 in + let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out2 in let out = Sys.command cmd in if out <> 0 then raise GappaProofFailed; let gappa_out3 = temp_file "gappa3" in @@ -164,7 +164,7 @@ let call_gappa hl p = (Filename.chop_suffix gappa_out2 ".v") gappa2; close_out c; let lambda = temp_file "gappa_lambda" in - let cmd = sprintf "%s/coqc %s > %s" Coq_config.bindir gappa_out3 lambda in + let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out3 ^ " > " ^ lambda in let out = Sys.command cmd in if out <> 0 then raise GappaProofFailed; remove_file gappa_out2; remove_file gappa_out3; diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index b551b143c..5de6060f0 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -370,7 +370,7 @@ Libobject.relax true; (let coqdir = try Sys.getenv "COQDIR" with Not_found -> - let coqdir = Coq_config.coqlib in + let coqdir = Envars.coqlib () in if Sys.file_exists coqdir then coqdir else diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml index 890671ab5..e9a8a0e3b 100644 --- a/contrib/micromega/coq_micromega.ml +++ b/contrib/micromega/coq_micromega.ml @@ -1294,7 +1294,7 @@ let call_csdpcert provername poly = output_value ch_to (provername,poly : provername * micromega_polys); close_out ch_to; let cmdname = - List.fold_left Filename.concat Coq_config.coqlib + List.fold_left Filename.concat (Envars.coqlib ()) ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in (try Sys.remove tmp_to with _ -> ()); diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 3c4b01f5b..4ee97813b 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -691,7 +691,7 @@ let _ = end ; Option.iter (fun fn -> - let coqdoc = Coq_config.bindir^"/coqdoc" in + let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let dir = Option.get xml_library_root in let command cmd = diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files index add14a13b..9516a19ff 100755 --- a/doc/stdlib/make-library-files +++ b/doc/stdlib/make-library-files @@ -1,6 +1,6 @@ #!/bin/sh -# Needs COQTOP and GALLINA set +# Needs COQSRC and GALLINA set # On garde la liste de tous les *.v avec dates dans library.files.ls # Si elle a change depuis la derniere fois ou library.files n'existe pas @@ -13,12 +13,12 @@ LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes" rm -f library.files.ls.tmp -(cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp +(cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then mv -f library.files.ls.tmp library.files.ls rm -f library.files; touch library.files ABSOLUTE=`pwd`/library.files - cd $COQTOP/theories + cd $COQSRC/theories echo $LIBDIRS for rep in $LIBDIRS ; do (cd $rep diff --git a/ide/coq.ml b/ide/coq.ml index 809c502e7..c60507251 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -58,7 +58,7 @@ let get_version_date () = then Coq_config.date else "<date not printable>" in try - let ch = open_in (Coq_config.coqtop^"/revision") in + let ch = open_in (Coq_config.coqsrc^"/revision") in let ver = input_line ch in let rev = input_line ch in (ver,rev) @@ -88,7 +88,7 @@ let is_in_coq_lib dir = List.exists (fun s -> let fdir = - Filename.concat Coq_config.coqlib (Filename.concat "theories" s) in + Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in prerr_endline (" Comparing to: "^fdir); if is_same_file fdir then (prerr_endline " YES";true) else (prerr_endline"NO";false)) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 5295f273e..be765922c 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -33,10 +33,7 @@ let prerr_string s = if !debug then (prerr_string s;flush stderr) let lib_ide_file f = - let coqlib = - System.getenv_else "COQLIB" - (if Coq_config.local || !Flags.boot then Coq_config.coqtop - else Coq_config.coqlib) in + let coqlib = Envars.coqlib () in Filename.concat (Filename.concat coqlib "ide") f let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT diff --git a/lib/envars.ml b/lib/envars.ml new file mode 100644 index 000000000..82e0d3162 --- /dev/null +++ b/lib/envars.ml @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This file gathers environment variables needed by Coq to run (such + as coqlib) *) + +let coqbin () = + if !Flags.boot || Coq_config.local + then Filename.concat Coq_config.coqsrc "bin" + else Filename.dirname Sys.executable_name + +let guess_coqlib () = + let file = "states/initial.coq" in + if Sys.file_exists (Filename.concat Coq_config.coqlib file) + then Coq_config.coqlib + else + let prefix = Filename.dirname (Filename.dirname Sys.executable_name) in + let coqlib = if Coq_config.local then prefix else + List.fold_left Filename.concat prefix ["lib";"coq"] in + if Sys.file_exists (Filename.concat coqlib file) then coqlib else + Util.error "cannot guess a path for Coq libraries; please use -coqlib option" + +let coqlib () = + if !Flags.coqlib_spec then !Flags.coqlib else + (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ()) + +let path_to_list p = + let sep = Str.regexp_string (if Sys.os_type = "Win32" then ";" else ":") in + Str.split sep p + +let rec which l f = + match l with + | [] -> raise Not_found + | p :: tl -> + if Sys.file_exists (Filename.concat p f) + then p + else which tl f + +let guess_camlbin () = + let path = try Sys.getenv "PATH" with _ -> raise Not_found in + let lpath = path_to_list path in + which lpath "ocamlc" + +let guess_camlp4bin () = + let path = try Sys.getenv "PATH" with _ -> raise Not_found in + let lpath = path_to_list path in + which lpath Coq_config.camlp4 + +let camlbin () = + if !Flags.camlbin_spec then !Flags.camlbin else + if !Flags.boot then Coq_config.camlbin else + try guess_camlbin () with _ -> Coq_config.camlbin + +let camllib () = + if !Flags.boot + then Coq_config.camllib + else + let camlbin = camlbin () in + let com = (Filename.concat camlbin "ocamlc") ^ " -where" in + let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in + res + +(* TODO : essayer aussi camlbin *) +let camlp4bin () = + if !Flags.camlp4bin_spec then !Flags.camlp4bin else + if !Flags.boot then Coq_config.camlp4bin else + try guess_camlp4bin () with _ -> Coq_config.camlp4bin + +let camlp4lib () = + if !Flags.boot + then Coq_config.camlp4lib + else + let camlp4bin = camlp4bin () in + let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in + let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in + res + + diff --git a/lib/envars.mli b/lib/envars.mli new file mode 100644 index 000000000..62d0cb61d --- /dev/null +++ b/lib/envars.mli @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val coqlib : unit -> string +val coqbin : unit -> string + +val camlbin : unit -> string +val camlp4bin : unit -> string +val camllib : unit -> string +val camlp4lib : unit -> string diff --git a/lib/flags.ml b/lib/flags.ml index f4b36c6c3..c3033c4b5 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -104,3 +104,16 @@ let browser_cmd_fmt = Sys.getenv coq_netscape_remote_var with Not_found -> Coq_config.browser + +(* Options for changing coqlib *) +let coqlib_spec = ref false +let coqlib = ref Coq_config.coqlib + +(* Options for changing camlbin (used by coqmktop) *) +let camlbin_spec = ref false +let camlbin = ref Coq_config.camlbin + +(* Options for changing camlp4bin (used by coqmktop) *) +let camlp4bin_spec = ref false +let camlp4bin = ref Coq_config.camlp4bin + diff --git a/lib/flags.mli b/lib/flags.mli index db472cccb..f0e4103f6 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -68,3 +68,13 @@ val browser_cmd_fmt : string (* Substitute %s in the first chain by the second chain *) val subst_command_placeholder : string -> string -> string + +(* Options for specifying where coq librairies reside *) +val coqlib_spec : bool ref +val coqlib : string ref + +(* Options for specifying where OCaml binaries reside *) +val camlbin_spec : bool ref +val camlbin : string ref +val camlp4bin_spec : bool ref +val camlp4bin : string ref diff --git a/scripts/coqc.ml b/scripts/coqc.ml index bee9e7b32..f2cf2025d 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -24,17 +24,9 @@ let environment = Unix.environment () -let bindir = ref Coq_config.bindir let binary = ref ("coqtop." ^ Coq_config.best) let image = ref "" -(* the $COQBIN environment variable has priority over the Coq_config value *) -let _ = - try - let c = Sys.getenv "COQBIN" in - if c <> "" then bindir := c - with Not_found -> () - (* coqc options *) let specification = ref false @@ -116,12 +108,8 @@ let parse_args () = | ("-verbose" | "--verbose") :: rem -> verbose := true ; parse (cfiles,args) rem | "-boot" :: rem -> - bindir:= Filename.concat Coq_config.coqtop "bin"; + Flags.boot := true; parse (cfiles, "-boot"::args) rem - | "-bindir" :: d :: rem -> - bindir := d ; parse (cfiles,args) rem - | "-bindir" :: [] -> - usage () | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem | "-opt" :: rem -> @@ -141,7 +129,7 @@ let parse_args () = | ("-I"|"-include"|"-outputstate" |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" - |"-init-file" | "-dump-glob" as o) :: rem -> + |"-init-file" | "-dump-glob" | "-coqlib" as o) :: rem -> begin match rem with | s :: rem' -> parse (cfiles,s::o::args) rem' @@ -158,12 +146,11 @@ let parse_args () = |"-unboxed-values"|"-unboxed-definitions"|"-draw-vm-instr" |"-no-glob"|"-noglob" as o) :: rem -> parse (cfiles,o::args) rem - - | "-where" :: _ -> - let coqlib = - try Sys.getenv "COQLIB" with Not_found -> Coq_config.coqlib - in - print_endline coqlib; exit 0 + + | ("-where") :: _ -> + (try print_endline (Envars.coqlib ()) + with Util.UserError(_,pps) -> Pp.msgerrnl (Pp.hov 0 pps)); + exit 0 | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0 @@ -188,14 +175,15 @@ let parse_args () = let main () = let cfiles, args = parse_args () in - if cfiles = [] then begin - prerr_endline "coqc: too few arguments" ; - usage () - end; - let coqtopname = - if !image <> "" then !image else Filename.concat !bindir (!binary ^ Coq_config.exec_extension) - in -(* List.iter (compile coqtopname args) cfiles*) - Unix.handle_unix_error (compile coqtopname args) cfiles + if cfiles = [] then begin + prerr_endline "coqc: too few arguments" ; + usage () + end; + let coqtopname = + if !image <> "" then !image + else Filename.concat (Envars.coqbin ()) (!binary ^ Coq_config.exec_extension) + in + (* List.iter (compile coqtopname args) cfiles*) + Unix.handle_unix_error (compile coqtopname args) cfiles let _ = Printexc.print main (); exit 0 diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 1b9247616..0bd9d0402 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -17,7 +17,7 @@ open Unix (* Objects to link *) (* 1. Core objects *) -let ocamlobjs = ["unix.cma";"nums.cma"] +let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"] let dynobjs = ["dynlink.cma"] let camlp4objs = ["gramlib.cma"] let libobjs = ocamlobjs @ camlp4objs @@ -44,7 +44,6 @@ let notopobjs = gramobjs (* 4. High-level tactics objects *) (* environment *) -let src_coqtop = ref Coq_config.coqtop let opt = ref false let full = ref false let top = ref false @@ -57,11 +56,13 @@ let src_dirs () = if !coqide then [[ "ide" ]] else [] let includes () = - List.fold_right - (fun d l -> "-I" :: List.fold_left Filename.concat !src_coqtop d :: l) - (src_dirs ()) - (["-I"; "\"" ^ Coq_config.camlp4lib ^ "\""] @ - (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else [])) + let coqlib = Envars.coqlib () in + List.fold_right + (fun d l -> "-I" :: List.fold_left Filename.concat coqlib d :: l) + (src_dirs ()) + (["-I"; "\"" ^ Coq_config.camlp4lib ^ "\""] @ + ["-I"; "\"" ^ coqlib ^ "\""] @ + (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else [])) (* Transform bytecode object file names in native object file names *) let native_suffix f = @@ -88,11 +89,11 @@ let files_to_link userfiles = let toplevel_objs = if !top then topobjs else if !opt then notopobjs else [] in let ide_objs = if !coqide then - "str.cma"::"threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide + "threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide else [] in let ide_libs = if !coqide then - ["str.cma" ; "threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; + ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; "ide/ide.cma" ] else [] in @@ -136,22 +137,33 @@ let all_subdirs dir = let usage () = prerr_endline "Usage: coqmktop <options> <ocaml options> files Flags.are: - -srcdir dir Specify where the Coq source files are - -o exec-file Specify the name of the resulting toplevel - -opt Compile in native code - -full Link high level tactics - -top Build Coq on a ocaml toplevel (incompatible with -opt) - -searchisos Build a toplevel for SearchIsos - -ide Build a toplevel for the Coq IDE - -R dir Specify recursively directories for Ocaml\n"; + -coqlib dir Specify where the Coq object files are + -camlbin dir Specify where the OCaml binaries are + -camlp4bin dir Specify where the CAmp4/5 binaries are + -o exec-file Specify the name of the resulting toplevel + -boot Run in boot mode + -opt Compile in native code + -full Link high level tactics + -top Build Coq on a ocaml toplevel (incompatible with -opt) + -searchisos Build a toplevel for SearchIsos + -ide Build a toplevel for the Coq IDE + -R dir Specify recursively directories for Ocaml\n"; exit 1 (* parsing of the command line *) let parse_args () = let rec parse (op,fl) = function | [] -> List.rev op, List.rev fl - | "-srcdir" :: d :: rem -> src_coqtop := d ; parse (op,fl) rem - | "-srcdir" :: _ -> usage () + | "-coqlib" :: d :: rem -> + Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem + | "-coqlib" :: _ -> usage () + | "-camlbin" :: d :: rem -> + Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem + | "-camlbin" :: _ -> usage () + | "-camlp4bin" :: d :: rem -> + Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem + | "-camlp4bin" :: _ -> usage () + | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem | "-opt" :: rem -> opt := true ; parse (op,fl) rem | "-full" :: rem -> full := true ; parse (op,fl) rem | "-top" :: rem -> top := true ; parse (op,fl) rem @@ -254,16 +266,17 @@ let create_tmp_main_file modules = let main () = let (options, userfiles) = parse_args () in (* which ocaml command to invoke *) + let camlbin = Envars.camlbin () in let prog = if !opt then begin (* native code *) if !top then failwith "no custom toplevel in native code !"; - let ocamloptexec = Filename.concat Coq_config.camldir "ocamlopt" in + let ocamloptexec = Filename.concat camlbin "ocamlopt" in ocamloptexec^" -linkall" end else (* bytecode (we shunt ocamlmktop script which fails on win32) *) let ocamlmktoplib = " toplevellib.cma" in - let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in + let ocamlcexec = Filename.concat camlbin "ocamlc" in let ocamlccustom = Printf.sprintf "%s %s -linkall " ocamlcexec Coq_config.coqrunbyteflags in (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom) @@ -282,22 +295,22 @@ let main () = try let args = options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in - (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *) + (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *) let args = if !top then args @ [ "topstart.cmo" ] else args in - (* Now, with the .cma, we MUST use the -linkall option *) + (* Now, with the .cma, we MUST use the -linkall option *) let command = String.concat " " (prog::"-rectypes"::args) in - if !echo then - begin - print_endline command; - print_endline - ("(command length is " ^ - (string_of_int (String.length command)) ^ " characters)"); - flush Pervasives.stdout - end; - let retcode = Sys.command command in - clean main_file; - (* command gives the exit code in HSB, and signal in LSB !!! *) - if retcode > 255 then retcode lsr 8 else retcode + if !echo then + begin + print_endline command; + print_endline + ("(command length is " ^ + (string_of_int (String.length command)) ^ " characters)"); + flush Pervasives.stdout + end; + let retcode = Sys.command command in + clean main_file; + (* command gives the exit code in HSB, and signal in LSB !!! *) + if retcode > 255 then retcode lsr 8 else retcode with e -> clean main_file; raise e diff --git a/test-suite/check b/test-suite/check index 68a4b0e38..a73654bcd 100755 --- a/test-suite/check +++ b/test-suite/check @@ -3,9 +3,9 @@ # Automatic test of Coq if [ "$1" = -byte ]; then - coqtop="../bin/coqtop.byte -q -batch" + coqtop="../bin/coqtop.byte -boot -q -batch" else - coqtop="../bin/coqtop -q -batch" + coqtop="../bin/coqtop -boot -q -batch" fi command="$coqtop -top Top -load-vernac-source" diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 52923ad4e..77fdffb0d 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -89,8 +89,6 @@ let is_genrule r = Str.string_match genrule r 0 let standard sds sps = - print "Makefile.config:\n"; - print "\t$(COQBIN)coqtop -config > $@\n\n"; print "byte:\n"; print "\t$(MAKE) all \"OPT:=-byte\"\n\n"; print "opt:\n"; @@ -121,7 +119,7 @@ let standard sds sps = print "clean:\n"; print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n"; print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ - $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d) Makefile.config\n"; + $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n"; if !some_mlfile then print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n"; print "\t- rm -rf html\n"; @@ -139,10 +137,11 @@ let standard sds sps = List.iter (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") sds; - print "\n\n" + print "\n\n"; + print "printenv: \n\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n"; + print "\t@echo CAMLP4LIB =\t$(CAMLP4LIB)\n\n" -let header_includes () = - print "include Makefile.config\n.PHONY: Makefile.config\n" +let header_includes () = () let footer_includes () = if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n"; @@ -187,10 +186,12 @@ let variables l = if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n"; (* Coq executables and relative variables *) print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; + print "ifdef CAMLBIN\n COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)\nendif\n"; print "COQC:=$(COQBIN)coqc\n"; print "COQDEP:=$(COQBIN)coqdep -c\n"; print "GALLINA:=$(COQBIN)gallina\n"; print "COQDOC:=$(COQBIN)coqdoc\n"; + print "COQMKTOP:=$(COQBIN)coqmktop\n"; (* Caml executables and relative variables *) printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; @@ -228,11 +229,13 @@ let dir_of_target t = let parameters () = print "# \n"; - print "# This Makefile looks for coqtop in PATH and in COQBIN to create Makefile.config\n"; - print "# Once created, Make refers to this file to determine the important paths for Coq\n"; - print "# and Caml binaries. To change which Coq is used to compile your contribution,\n"; - print "# delete Makefile.config, and set COQBIN to the desired value.\n"; - print "# \n\n" + print "# This Makefile may take 3 arguments passed as environment variables:\n"; + print "# - COQBIN to specify the directory where Coq binaries resides;\n"; + print "# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.\n"; + print "COQLIB:=$(shell $(COQBIN)coqtop -where)\n"; + print "CAMLP4:=$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')\n"; + print "ifndef CAMLP4BIN\n CAMLP4BIN:=$(CAMLBIN)\nendif\n\n"; + print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\n\n" let include_dirs l = let rec split_includes l = @@ -263,22 +266,18 @@ let include_dirs l = let str_r = parse_includes inc_r in section "Libraries definitions."; print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n " str_i; print "\n"; - print "ifneq ($(LOCAL),0) # set COQTOP for compiling from Coq sources\n"; - print " COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ - -I $(COQTOP)/library -I $(COQTOP)/parsing \\ - -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\ - -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\ - -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc -I $(COQTOP)/contrib/dp \\ - -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\ - -I $(COQTOP)/contrib/firstorder -I $(COQTOP)/contrib/fourier \\ - -I $(COQTOP)/contrib/funind -I $(COQTOP)/contrib/interface \\ - -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\ - -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\ - -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\ - -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml\n"; - print "else\n"; - print " COQSRCLIBS:=-I $(COQLIB)\n"; - print "endif\n"; + print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\ + -I $(COQLIB)/library -I $(COQLIB)/parsing \\ + -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\ + -I $(COQLIB)/proofs -I $(COQLIB)/tactics \\ + -I $(COQLIB)/toplevel -I $(COQLIB)/contrib/cc -I $(COQLIB)/contrib/dp \\ + -I $(COQLIB)/contrib/extraction -I $(COQLIB)/contrib/field \\ + -I $(COQLIB)/contrib/firstorder -I $(COQLIB)/contrib/fourier \\ + -I $(COQLIB)/contrib/funind -I $(COQLIB)/contrib/interface \\ + -I $(COQLIB)/contrib/micromega -I $(COQLIB)/contrib/omega \\ + -I $(COQLIB)/contrib/ring -I $(COQLIB)/contrib/romega \\ + -I $(COQLIB)/contrib/rtauto -I $(COQLIB)/contrib/setoid_ring \\ + -I $(COQLIB)/contrib/subtac -I $(COQLIB)/contrib/xml\n"; print "COQLIBS:="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n"; print "COQDOCLIBS:="; print_list "\\\n " str_r; print "\n\n" diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 3d93c8a90..393554568 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -15,8 +15,6 @@ open Unix let stderr = Pervasives.stderr let stdout = Pervasives.stdout -let coqlib = ref Coq_config.coqlib - let option_c = ref false let option_D = ref false let option_w = ref false @@ -24,7 +22,6 @@ let option_i = ref false let option_sort = ref false let option_noglob = ref false let option_slash = ref false -let option_boot = ref false let suffixe = ref ".vo" let suffixe_spec = ref ".vi" @@ -516,14 +513,14 @@ let rec parse = function | "-D" :: ll -> option_D := true; parse ll | "-w" :: ll -> option_w := true; parse ll | "-i" :: ll -> option_i := true; parse ll - | "-boot" :: ll -> option_boot := true; parse ll + | "-boot" :: ll -> Flags.boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | "-noglob" :: ll | "-no-glob" :: ll -> option_noglob := true; parse ll | "-I" :: r :: ll -> add_dir add_known r []; parse ll | "-I" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll | "-R" :: ([] | [_]) -> usage () - | "-coqlib" :: (r :: ll) -> coqlib := r; parse ll + | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll | "-suffix" :: [] -> usage () @@ -534,13 +531,14 @@ let rec parse = function let coqdep () = if Array.length Sys.argv < 2 then usage (); parse (List.tl (Array.to_list Sys.argv)); - if !option_boot then begin + if !Flags.boot then begin add_rec_dir add_known "theories" ["Coq"]; add_rec_dir add_known "contrib" ["Coq"] - end else begin - add_rec_dir add_coqlib_known (!coqlib//"theories") ["Coq"]; - add_rec_dir add_coqlib_known (!coqlib//"contrib") ["Coq"]; - add_dir add_coqlib_known (!coqlib//"user-contrib") [] + end else begin + let coqlib = Envars.coqlib () in + add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; + add_rec_dir add_coqlib_known (coqlib//"contrib") ["Coq"]; + add_dir add_coqlib_known (coqlib//"user-contrib") [] end; List.iter (fun (f,_,d) -> Hashtbl.add mliKnown f d) !mliAccu; List.iter (fun (f,_,d) -> Hashtbl.add mlKnown f d) !mlAccu; diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index e6c3e5c07..864b2718e 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -57,6 +57,7 @@ let usage () = prerr_endline " --no-externals no links to Coq standard library"; prerr_endline " --coqlib <url> set URL for Coq standard library"; prerr_endline " (default is http://coq.inria.fr/library/)"; + prerr_endline " --boot run in boot mode"; prerr_endline " --coqlib_path <dir> set the path where Coq files are installed"; prerr_endline " -R <dir> <coqdir> map physical dir to Coq dir"; prerr_endline " --latin1 set ISO-8859-1 input language"; @@ -318,6 +319,8 @@ let parse () = Cdglobals.coqlib := u; parse_rec rem | ("--coqlib" | "-coqlib") :: [] -> usage () + | ("--boot" | "-boot") :: rem -> + Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: d :: rem -> Cdglobals.coqlib_path := d; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: [] -> diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index daae9b94e..a21e33c87 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -93,16 +93,12 @@ let theories_dirs_map = [ "theories/Init", "Init" ] -(* Initializes the LoadPath according to COQLIB and Coq_config *) +(* Initializes the LoadPath *) let init_load_path () = - let coqlib = - (* variable COQLIB overrides the default library *) - getenv_else "COQLIB" - (if Coq_config.local || !Flags.boot then Coq_config.coqtop - else Coq_config.coqlib) in + let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let dirs = "states" :: ["contrib"] in - let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in + let camlp4 = Envars.camlp4lib () in (* first user-contrib *) if Sys.file_exists user_contrib then Mltop.add_rec_path user_contrib Nameops.default_root_prefix; @@ -129,13 +125,13 @@ let init_library_roots () = (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) -(* We only assume that the variable COQTOP is set *) let init_ocaml_path () = - let coqtop = getenv_else "COQTOP" Coq_config.coqtop in + let coqsrc = Coq_config.coqsrc in let add_subdir dl = - Mltop.add_ml_dir (List.fold_left (/) coqtop dl) + Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) in - List.iter add_subdir - [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; - [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; - [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ] + Mltop.add_ml_dir (Envars.coqlib ()); + List.iter add_subdir + [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; + [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; + [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ] diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index dd92ccfc2..fec6b0740 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -21,7 +21,7 @@ open Coqinit let get_version_date () = try - let ch = open_in (Coq_config.coqlib^"/revision") in + let ch = open_in (Coq_config.coqsrc^"/revision") in let ver = input_line ch in let rev = input_line ch in (ver,rev) @@ -274,7 +274,10 @@ let parse_args is_ide = | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem - | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 + | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem + | "-coqlib" :: [] -> usage () + + | "-where" :: _ -> print_endline (Envars.coqlib ()); exit 0 | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0 diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 02fa69142..cdb3b6f02 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -82,7 +82,6 @@ let print_usage_coqc () = print_usage "Usage: coqc <options> <Coq options> file...\n options are: -verbose compile verbosely - -bindir override the default directory where coqc looks for coqtop -image f specify an alternative executable for Coq -t keep temporary files\n\n" @@ -90,11 +89,12 @@ options are: let print_config () = if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; - Printf.printf "COQBIN=%s/\n" Coq_config.bindir; Printf.printf "COQLIB=%s/\n" Coq_config.coqlib; - Printf.printf "COQTOP=%s/\n" Coq_config.coqtop; - Printf.printf "CAMLBIN=%s/\n" Coq_config.camldir; + Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc; + Printf.printf "CAMLBIN=%s/\n" Coq_config.camlbin; + Printf.printf "CAMLLIB=%s/\n" Coq_config.camllib; Printf.printf "CAMLP4=%s\n" Coq_config.camlp4; + Printf.printf "CAMLP4BIN=%s\n" Coq_config.camlp4bin; Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib |