diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-12 20:49:01 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-12 20:49:01 +0000 |
| commit | 59c9403ceb09a35ed219b522e9f5abdb50615d76 (patch) | |
| tree | f7d3e521f6a948defdce70e00c718c6bdc7b696e | |
| parent | 1b9428c4e4ce6f2dbe98d0f753b062ae8634a954 (diff) | |
lib directory is cut in 2 cma.
- Clib that does not depend on camlpX and is made to be shared by all coq
tools/scripts/...
- Lib that is Coqtop specific
As a side effect for the build system :
- Coq_config is in Clib and does not appears in makefiles
- only the BEST version of coqc and coqmktop is made
- ocamlbuild build system fails latter but is still broken
(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
50 files changed, 380 insertions, 405 deletions
@@ -193,7 +193,7 @@ docclean: rm -f doc/coq.tex archclean: clean-ide optclean voclean - rm -rf _build myocamlbuild_config.ml + rm -rf _build rm -f $(ALLSTDLIB).* optclean: @@ -218,7 +218,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 + rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-v7 ide/undo.mli distclean: clean cleanconfig diff --git a/Makefile.build b/Makefile.build index d63558c2b..2eb28265a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -199,14 +199,14 @@ coqlight: theories-light tools coqbinaries states:: states/initial.coq -$(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN) +$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(BESTCOQMKTOP) -boot -opt $(OPTFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(STRIP) $@ -$(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN) +$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(BESTCOQMKTOP) -boot -top $(BYTEFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ $(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP) cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) @@ -228,19 +228,10 @@ $(CHICKENBYTE): checker/check.cma checker/main.ml $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE) -# coqmktop - -$(COQMKTOPBYTE): $(COQMKTOPCMO) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(SYSCMA) $^ $(OSDEPLIBS) - -$(COQMKTOPOPT): $(COQMKTOPCMO:.cmo=.cmx) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(SYSCMXA) $^ $(OSDEPLIBS) - $(STRIP) $@ - -$(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP) - cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE) +# coqmktop +$(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ))) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) scripts/tolink.ml: Makefile.build Makefile.common $(SHOW)"ECHO... >" $@ @@ -249,18 +240,9 @@ scripts/tolink.ml: Makefile.build Makefile.common $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ # coqc - -$(COQCBYTE): $(COQCCMO) | $(COQTOPBYTE) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(SYSCMA) $^ $(OSDEPLIBS) - -$(COQCOPT): $(COQCCMO:.cmo=.cmx) | $(COQTOPOPT) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(SYSCMXA) $^ $(OSDEPLIBS) - $(STRIP) $@ - -$(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC) - cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE) +$(COQC): $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ))) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) # target for libraries @@ -395,7 +377,7 @@ test-suite: world $(ALLSTDLIB).v .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping .PHONY: highparsing toplevel hightactics -lib: lib/lib.cma +lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma byterun: $(BYTERUN) library: library/library.cma @@ -514,7 +496,7 @@ $(COQDEPBOOT): $(COQDEPBOOTSRC) # the full coqdep -$(COQDEP): $(COQDEPCMO:.cmo=$(BESTOBJ)) +$(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) @@ -534,14 +516,14 @@ $(COQWC): tools/coqwc$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -$(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ)) +$(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -$(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BESTOBJ) toplevel/ide_intf$(BESTOBJ) tools/fake_ide$(BESTOBJ) +$(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BESTOBJ) lib/serialize$(BESTOBJ) tools/fake_ide$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,unix) diff --git a/Makefile.common b/Makefile.common index 5f32ee13f..f9da6b5de 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,14 +12,8 @@ # Executables ########################################################################### -COQMKTOPBYTE:=bin/coqmktop.byte$(EXE) -COQMKTOPOPT:=bin/coqmktop.opt$(EXE) -BESTCOQMKTOP:=bin/coqmktop.$(BEST)$(EXE) COQMKTOP:=bin/coqmktop$(EXE) -COQCBYTE:=bin/coqc.byte$(EXE) -COQCOPT:=bin/coqc.opt$(EXE) -BESTCOQC:=bin/coqc.$(BEST)$(EXE) COQC:=bin/coqc$(EXE) COQTOPBYTE:=bin/coqtop.byte$(EXE) @@ -66,6 +60,7 @@ OPT:= endif BESTOBJ:=$(if $(OPT),.cmx,.cmo) +BESTLIB:=$(if $(OPT),.cmxa,.cma) COQBINARIES:= $(COQMKTOP) $(COQC) \ $(COQTOPBYTE) $(if $(OPT),$(COQTOPOPT)) $(COQTOPEXE) \ @@ -152,8 +147,6 @@ COQRUN := coqrun LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT) -CONFIG:=config/coq_config.cmo - BYTERUN:=$(addprefix kernel/byterun/, \ coq_fix_code.o coq_memory.o coq_values.o coq_interp.o ) @@ -162,10 +155,10 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # respecting this order is useful for developers that want to load or link # the libraries directly -CORECMA:=lib/lib.cma kernel/kernel.cma library/library.cma \ +CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ - parsing/highparsing.cma tactics/hightactics.cma + parsing/highparsing.cma tactics/hightactics.cma GRAMMARCMA:=parsing/grammar.cma @@ -218,28 +211,26 @@ endif INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS)) -LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS) -LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) +LINKCMO:=$(CORECMA) $(STATICPLUGINS) +LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) -IDEDEPS:=$(CONFIG) lib/flags.cmo lib/xml_lexer.cmo lib/xml_parser.cmo \ - lib/xml_utils.cmo toplevel/ide_intf.cmo +IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo \ + lib/xml_utils.cmo IDECMA:=ide/ide.cma LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTDEPS) $(IDEDEPS:.cmo=.cmx) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml +LINKIDEOPT:=$(IDEOPTDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml # modules known by the toplevel of Coq -OBJSMOD:=Coq_config $(shell cat $(CORECMA:.cma=.mllib)) +OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib)) IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc -COQENVCMO:=$(CONFIG) \ - lib/pp_control.cmo lib/compat.cmo lib/flags.cmo lib/pp.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/errors.cmo lib/util.cmo lib/system.cmo \ - lib/envars.cmo +COQENVCMO:=lib/clib.cma\ + lib/pp_control.cmo lib/compat.cmo lib/pp.cmo lib/errors.cmo COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo @@ -255,7 +246,7 @@ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo -COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \ +COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) ########################################################################### @@ -2,9 +2,9 @@ ## tags for binaries <scripts/coqmktop.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX -<scripts/coqc.{native,byte}> : use_unix, use_dynlink, use_camlpX +<scripts/coqc.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX <tools/coqdep_boot.{native,byte}> : use_unix -<tools/coqdep.{native,byte}> : use_unix, use_dynlink, use_camlpX +<tools/coqdep.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX <tools/coq_tex.{native,byte}> : use_str <tools/coq_makefile.{native,byte}> : use_str, use_unix <tools/coqdoc/main.{native,byte}> : use_str @@ -27,6 +27,7 @@ "toplevel/mltop.ml4": is_mltop "toplevel/whelp.ml4": use_grammar +"toplevel/g_obligations.ml4": use_grammar "tactics/extraargs.ml4": use_grammar "tactics/extratactics.ml4": use_grammar "tactics/class_tactics.ml4": use_grammar @@ -46,7 +47,6 @@ "parsing/pcoq.ml4": use_compat5 "plugins/decl_mode/g_decl_mode.ml4": use_compat5 "plugins/funind/g_indfun.ml4": use_compat5 -"plugins/subtac/g_subtac.ml4": use_compat5 "parsing/argextend.ml4": use_compat5b "parsing/q_constr.ml4": use_compat5b @@ -1,15 +1,13 @@ #!/bin/sh -FLAGS= +FLAGS="-j 2" OCAMLBUILD=ocamlbuild -CFG=config/coq_config.ml MYCFG=myocamlbuild_config.ml export CAML_LD_LIBRARY_PATH=`pwd`/_build/kernel/byterun check_config() { - [ -f $CFG ] || (echo "please run ./configure first"; exit 1) - [ -L $MYCFG ] || ln -sf $CFG $MYCFG + [ -f $MYCFG ] || (echo "please run ./configure first"; exit 1) } ocb() { $OCAMLBUILD $FLAGS $*; } @@ -17,7 +15,7 @@ ocb() { $OCAMLBUILD $FLAGS $*; } rule() { check_config case $1 in - clean) ocb -clean && rm -rf bin/* && rm -f $MYCFG;; + clean) ocb -clean && rm -rf bin/*;; all) ocb coq.otarget;; win32) ocb coq-win32.otarget;; *) ocb $1;; diff --git a/checker/check.ml b/checker/check.ml index 6f01107f5..3194b2681 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -54,7 +54,7 @@ type library_disk = { type library_t = { library_name : compilation_unit_name; - library_filename : System.physical_path; + library_filename : CUnix.physical_path; library_compiled : Safe_typing.compiled_library; library_deps : (compilation_unit_name * Digest.t) list; library_digest : Digest.t } @@ -114,7 +114,7 @@ let check_one_lib admit (dir,m) = type logical_path = dir_path -let load_paths = ref ([],[] : System.physical_path list * logical_path list) +let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) let get_load_paths () = fst !load_paths diff --git a/checker/check.mllib b/checker/check.mllib index 99b952a38..2cd86355f 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -9,6 +9,7 @@ Errors Util Option Hashcons +CUnix System Envars Predicate diff --git a/checker/checker.ml b/checker/checker.ml index 4da4d14e1..44a77836c 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -43,7 +43,7 @@ let (/) = Filename.concat let get_version_date () = try - let coqlib = Envars.coqlib () in + let coqlib = Envars.coqlib error in let ch = open_in (Filename.concat coqlib "revision") in let ver = input_line ch in let rev = input_line ch in @@ -101,7 +101,7 @@ let set_rec_include d p = (* Initializes the LoadPath *) let init_load_path () = - let coqlib = Envars.coqlib () in + let coqlib = Envars.coqlib error in let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs in let coqpath = Envars.coqpath in @@ -115,7 +115,8 @@ let init_load_path () = if Sys.file_exists user_contrib then add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) - List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) xdg_dirs; + List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) + (xdg_dirs ~warn:(fun x -> msg_warning (str x))); (* then directories in COQPATH *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) @@ -309,7 +310,7 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - print_endline (Envars.coqlib ()); exit 0 + print_endline (Envars.coqlib error); exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index cd2c06d20..b7d7d04cc 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -19,9 +19,9 @@ type compiled_library val set_engagement : Declarations.engagement -> unit val import : - System.physical_path -> compiled_library -> Digest.t -> unit + CUnix.physical_path -> compiled_library -> Digest.t -> unit val unsafe_import : - System.physical_path -> compiled_library -> Digest.t -> unit + CUnix.physical_path -> compiled_library -> Digest.t -> unit (** Store the body of modules' opaque constants inside a table. @@ -1008,6 +1008,7 @@ fi ############################################## mlconfig_file="$COQSRC/config/coq_config.ml" +mymlconfig_file="$COQSRC/myocamlbuild_config.ml" config_file="$COQSRC/config/Makefile" config_template="$COQSRC/config/Makefile.template" @@ -1065,7 +1066,7 @@ esac # Building the $COQTOP/config/coq_config.ml file ##################################################### -rm -f "$mlconfig_file" +rm -f "$mlconfig_file" "$mymlconfig_file" cat << END_OF_COQ_CONFIG > $mlconfig_file (* DO NOT EDIT THIS FILE: automatically generated by ../configure *) @@ -1132,7 +1133,7 @@ subdirs plugins echo "]" >> "$mlconfig_file" chmod a-w "$mlconfig_file" - +ln -sf "$mlconfig_file" "$mymlconfig_file" ############################################### # Building the $COQTOP/config/Makefile file diff --git a/dev/base_include b/dev/base_include index 7dfe234aa..38a5972e9 100644 --- a/dev/base_include +++ b/dev/base_include @@ -32,7 +32,7 @@ #install_printer (* kernel_name *) ppkn;; #install_printer (* constant *) ppcon;; #install_printer (* cl_index *) ppclindex;; -#install_printer (* constr *) print_pure_constr;; +#install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; #install_printer (* values *) ppvalues;; #install_printer (* Idpred.t *) pp_idpred;; @@ -1,4 +1,5 @@ load_printer "gramlib.cma" +load_printer "str.cma" load_printer "printers.cma" install_printer Top_printers.ppid diff --git a/dev/printers.mllib b/dev/printers.mllib index 2d5919d61..f93d01daf 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -11,6 +11,7 @@ Util Bigint Hashcons Dyn +CUnix System Envars Store diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index bcc68c78d..3bf9e7cb5 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -207,7 +207,7 @@ Section~\ref{LongNames}). some standard axioms of classical mathematics such as the functional axiom of choice or the principle of description -\item[{\tt -compat} {\em version}] \null +\item[{\tt -compat} {\em version}] \mbox{} Attempt to maintain some of the incompatible changes in their {\em version} behavior. @@ -239,7 +239,7 @@ Section~\ref{LongNames}). Proofs of opaque theorems are loaded in memory as soon as the corresponding {\tt Require} is done. This used to be Coq's default behavior. -\item[{\tt -no-hash-consing}] \null +\item[{\tt -no-hash-consing}] \mbox{} \item[{\tt -vm}]\ diff --git a/ide/coq.ml b/ide/coq.ml index 16a07b01c..cf73749a8 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -176,19 +176,19 @@ let kill_coqtop coqtop = let p = Xml_parser.make () let () = Xml_parser.check_eof p false -let eval_call coqtop (c:'a Ide_intf.call) = - Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c); +let eval_call coqtop (c:'a Serialize.call) = + Xml_utils.print_xml coqtop.cin (Serialize.of_call c); flush coqtop.cin; let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in - (Ide_intf.to_answer xml : 'a Interface.value) + (Serialize.to_answer xml : 'a Interface.value) let interp coqtop ?(raw=false) ?(verbose=true) s = - eval_call coqtop (Ide_intf.interp (raw,verbose,s)) -let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i) -let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s) -let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s) -let status coqtop = eval_call coqtop Ide_intf.status -let hints coqtop = eval_call coqtop Ide_intf.hints + eval_call coqtop (Serialize.interp (raw,verbose,s)) +let rewind coqtop i = eval_call coqtop (Serialize.rewind i) +let inloadpath coqtop s = eval_call coqtop (Serialize.inloadpath s) +let mkcases coqtop s = eval_call coqtop (Serialize.mkcases s) +let status coqtop = eval_call coqtop Serialize.status +let hints coqtop = eval_call coqtop Serialize.hints module PrintOpt = struct @@ -208,7 +208,7 @@ struct let set coqtop options = let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in - match eval_call coqtop (Ide_intf.set_options options) with + match eval_call coqtop (Serialize.set_options options) with | Interface.Good () -> () | _ -> raise (Failure "Cannot set options.") @@ -220,8 +220,8 @@ end let goals coqtop = let () = PrintOpt.enforce_hack coqtop in - eval_call coqtop Ide_intf.goals + eval_call coqtop Serialize.goals let evars coqtop = let () = PrintOpt.enforce_hack coqtop in - eval_call coqtop Ide_intf.evars + eval_call coqtop Serialize.evars diff --git a/lib/cUnix.ml b/lib/cUnix.ml new file mode 100644 index 000000000..ad5f0587d --- /dev/null +++ b/lib/cUnix.ml @@ -0,0 +1,108 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Files and load path. *) + +type physical_path = string +type load_path = physical_path list + +let physical_path_of_string s = s +let string_of_physical_path p = p + +let path_to_list p = + let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in + Str.split sep p + +(* Hints to partially detects if two paths refer to the same repertory *) +let rec remove_path_dot p = + let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) + let n = String.length curdir in + let l = String.length p in + if l > n && String.sub p 0 n = curdir then + let n' = + let sl = String.length Filename.dir_sep in + let i = ref n in + while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in + remove_path_dot (String.sub p n' (l - n')) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + let l = String.length p in + if l > n && String.sub p 0 n = cwd then + let n' = + let sl = String.length Filename.dir_sep in + let i = ref n in + while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in + remove_path_dot (String.sub p n' (l - n')) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p + +let make_suffix name suffix = + if Filename.check_suffix name suffix then name else (name ^ suffix) + +let correct_path f dir = if Filename.is_relative f then Filename.concat dir f else f + +let file_readable_p name = + try Unix.access name [Unix.R_OK];true with Unix.Unix_error (_, _, _) -> false + +let run_command converter f c = + let result = Buffer.create 127 in + let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in + let buff = String.make 127 ' ' in + let buffe = String.make 127 ' ' in + let n = ref 0 in + let ne = ref 0 in + + while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; + !n+ !ne <> 0 + do + let r = converter (String.sub buff 0 !n) in + f r; + Buffer.add_string result r; + let r = converter (String.sub buffe 0 !ne) in + f r; + Buffer.add_string result r + done; + (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) + +(* + checks if two file names refer to the same (existing) file by + comparing their device and inode. + It seems that under Windows, inode is always 0, so we cannot + accurately check if + +*) +(* Optimised for partial application (in case many candidates must be + compared to f1). *) +let same_file f1 = + try + let s1 = Unix.stat f1 in + (fun f2 -> + try + let s2 = Unix.stat f2 in + s1.Unix.st_dev = s2.Unix.st_dev && + if Sys.os_type = "Win32" then f1 = f2 + else s1.Unix.st_ino = s2.Unix.st_ino + with + Unix.Unix_error _ -> false) + with + Unix.Unix_error _ -> (fun _ -> false) diff --git a/lib/cUnix.mli b/lib/cUnix.mli new file mode 100644 index 000000000..00419bc97 --- /dev/null +++ b/lib/cUnix.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** {5 System utilities} *) + +type physical_path = string +type load_path = physical_path list + +val canonical_path_name : string -> string + +val physical_path_of_string : string -> physical_path +val string_of_physical_path : physical_path -> string + +val path_to_list : string -> string list + +val make_suffix : string -> string -> string +val file_readable_p : string -> bool + +(** {6 Executing commands } *) +(** [run_command converter f com] launches command [com], and returns + the contents of stdout and stderr that have been processed with + [converter]; the processed contents of stdout and stderr is also + passed to [f] *) + +val run_command : (string -> string) -> (string -> unit) -> string -> + Unix.process_status * string + diff --git a/lib/clib.mllib b/lib/clib.mllib new file mode 100644 index 000000000..65d3a1562 --- /dev/null +++ b/lib/clib.mllib @@ -0,0 +1,8 @@ +Coq_config +Segmenttree +Unicodetable +Util +Serialize +Flags +CUnix +Envars diff --git a/lib/envars.ml b/lib/envars.ml index 611b81a7e..4b0f57ada 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -9,8 +9,52 @@ (* This file gathers environment variables needed by Coq to run (such as coqlib) *) +let getenv_else s dft = try Sys.getenv s with Not_found -> dft () + +let safe_getenv warning n = getenv_else n (fun () -> + let () = warning ("Environment variable "^n^" not found: using '$"^n^"' .") + in ("$"^n)) + +(* Expanding shell variables and home-directories *) + +(* On win32, the home directory is probably not in $HOME, but in + some other environment variable *) + +let home ~warn = + getenv_else "HOME" (fun () -> + try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> + getenv_else "USERPROFILE" (fun () -> + warn ("Cannot determine user home directory, using '.' ."); + Filename.current_dir_name)) + +let expand_path_macros ~warn s = + let rec expand_atom s i = + let l = String.length s in + if i<l && (Util.is_digit s.[i] or Util.is_letter s.[i] or s.[i] = '_') + then expand_atom s (i+1) + else i in + let rec expand_macros s i = + let l = String.length s in + if i=l then s else + match s.[i] with + | '$' -> + let n = expand_atom s (i+1) in + let v = safe_getenv warn (String.sub s (i+1) (n-i-1)) in + let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in + expand_macros s (i + String.length v) + | '~' when i = 0 -> + let n = expand_atom s (i+1) in + let v = + if n=i+1 then home ~warn + else (Unix.getpwnam (String.sub s (i+1) (n-i-1))).Unix.pw_dir + in + let s = v^(String.sub s n (l-n)) in + expand_macros s (String.length v) + | c -> expand_macros s (i+1) + in expand_macros s 0 + let coqbin = - System.canonical_path_name (Filename.dirname Sys.executable_name) + CUnix.canonical_path_name (Filename.dirname Sys.executable_name) (* The following only makes sense when executables are running from source tree (e.g. during build or in local mode). *) @@ -21,14 +65,14 @@ let coqroot = Filename.dirname coqbin let _ = if Coq_config.arch = "win32" then - Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "") + Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> "")) let reldir instdir testfile oth = let rpath = if Coq_config.local then [] else instdir in let out = List.fold_left Filename.concat coqroot rpath in if Sys.file_exists (Filename.concat out testfile) then out else oth () -let guess_coqlib () = +let guess_coqlib fail = let file = "states/initial.coq" in reldir (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) file (fun () -> @@ -38,11 +82,11 @@ let guess_coqlib () = in if Sys.file_exists (Filename.concat coqlib file) then coqlib - else Errors.error "cannot guess a path for Coq libraries; please use -coqlib option") + else fail "cannot guess a path for Coq libraries; please use -coqlib option") -let coqlib () = +let coqlib ~fail = if !Flags.coqlib_spec then !Flags.coqlib else - (if !Flags.boot then coqroot else guess_coqlib ()) + (if !Flags.boot then coqroot else guess_coqlib fail) let docdir () = reldir (if Coq_config.arch = "win32" then ["doc"] else ["share";"doc";"coq"]) "html" (fun () -> Coq_config.docdir) @@ -51,14 +95,14 @@ let path_to_list p = let sep = if Sys.os_type = "Win32" then ';' else ':' in Util.split_string_at sep p -let xdg_data_home = +let xdg_data_home warning = Filename.concat - (System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share")) + (getenv_else "XDG_DATA_HOME" (fun () -> Filename.concat (home warning) ".local/share")) "coq" -let xdg_config_home = +let xdg_config_home ~warn = Filename.concat - (System.getenv_else "XDG_CONFIG_HOME" (Filename.concat System.home ".config")) + (getenv_else "XDG_CONFIG_HOME" (fun () -> Filename.concat (home ~warn) ".config")) "coq" let xdg_data_dirs = @@ -67,8 +111,8 @@ let xdg_data_dirs = with Not_found -> "/usr/local/share/coq" :: "/usr/share/coq" :: (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir]) -let xdg_dirs = - let dirs = xdg_data_home :: xdg_data_dirs +let xdg_dirs ~warn = + let dirs = xdg_data_home warn :: xdg_data_dirs in List.rev (List.filter Sys.file_exists dirs) @@ -107,7 +151,7 @@ let 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 + let _,res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in Util.strip res let camlp4bin () = @@ -123,7 +167,7 @@ let 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 + let _,res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in Util.strip res diff --git a/lib/envars.mli b/lib/envars.mli index 0c80492f8..ff4cf4a56 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -9,14 +9,17 @@ (** This file gathers environment variables needed by Coq to run (such as coqlib) *) -val coqlib : unit -> string +val expand_path_macros : warn:(string -> unit) -> string -> string +val home : warn:(string -> unit) -> string + +val coqlib : fail:(string -> string) -> string val docdir : unit -> string val coqbin : string val coqroot : string (* coqpath is stored in reverse order, since that is the order it * gets added to the searc path *) -val xdg_config_home : string -val xdg_dirs : string list +val xdg_config_home : warn:(string -> unit) -> string +val xdg_dirs : warn:(string -> unit) -> string list val coqpath : string list val camlbin : unit -> string diff --git a/toplevel/interface.mli b/lib/interface.mli index 604060550..f2aba72e9 100644 --- a/toplevel/interface.mli +++ b/lib/interface.mli @@ -49,15 +49,15 @@ type goals = { type hint = (string * string) list (** A list of tactics applicable and their appearance *) -type option_name = Goptionstyp.option_name +type option_name = string list -type option_value = Goptionstyp.option_value = +type option_value = | BoolValue of bool | IntValue of int option | StringValue of string (** Summary of an option status *) -type option_state = Goptionstyp.option_state = { +type option_state = { opt_sync : bool; (** Whether an option is synchronous *) opt_depr : bool; diff --git a/lib/lib.mllib b/lib/lib.mllib index eb834af78..77fc4ab09 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -3,17 +3,12 @@ Xml_parser Xml_utils Pp_control Compat -Flags Pp -Segmenttree -Unicodetable Errors -Util Bigint Hashcons Dyn System -Envars Gmap Fset Fmap diff --git a/toplevel/ide_intf.ml b/lib/serialize.ml index d36e46624..96cdc6c2c 100644 --- a/toplevel/ide_intf.ml +++ b/lib/serialize.ml @@ -8,10 +8,11 @@ (** * Interface of calls to Coq by CoqIde *) -open Xml_parser open Interface -type xml = Xml_parser.xml +type xml = + | Element of (string * (string * string) list * xml list) + | PCData of string (** We use phantom types and GADT to protect ourselves against wild casts *) diff --git a/toplevel/ide_intf.mli b/lib/serialize.mli index 69204da16..2ab557c53 100644 --- a/toplevel/ide_intf.mli +++ b/lib/serialize.mli @@ -10,7 +10,9 @@ open Interface -type xml = Xml_parser.xml +type xml = + | Element of (string * (string * string) list * xml list) + | PCData of string type 'a call diff --git a/lib/system.ml b/lib/system.ml index 7e0347530..1537f4892 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -13,123 +13,6 @@ open Errors open Util open Unix -(* Expanding shell variables and home-directories *) - -let safe_getenv_def var def = - try - Sys.getenv var - with Not_found -> - warning ("Environment variable "^var^" not found: using '"^def^"' ."); - flush_all (); - def - -let getenv_else s dft = try Sys.getenv s with Not_found -> dft - -(* On win32, the home directory is probably not in $HOME, but in - some other environment variable *) - -let home = - try Sys.getenv "HOME" with Not_found -> - try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> - try Sys.getenv "USERPROFILE" with Not_found -> - warning ("Cannot determine user home directory, using '.' ."); - flush_all (); - Filename.current_dir_name - -let safe_getenv n = safe_getenv_def n ("$"^n) - -let rec expand_atom s i = - let l = String.length s in - if i<l && (is_digit s.[i] or is_letter s.[i] or s.[i] = '_') - then expand_atom s (i+1) - else i - -let rec expand_macros s i = - let l = String.length s in - if i=l then s else - match s.[i] with - | '$' -> - let n = expand_atom s (i+1) in - let v = safe_getenv (String.sub s (i+1) (n-i-1)) in - let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in - expand_macros s (i + String.length v) - | '~' when i = 0 -> - let n = expand_atom s (i+1) in - let v = - if n=i+1 then home - else (getpwnam (String.sub s (i+1) (n-i-1))).pw_dir - in - let s = v^(String.sub s n (l-n)) in - expand_macros s (String.length v) - | c -> expand_macros s (i+1) - -let expand_path_macros s = expand_macros s 0 - -(* Files and load path. *) - -type physical_path = string -type load_path = physical_path list - -let physical_path_of_string s = s -let string_of_physical_path p = p - -(* - * Split a path into a list of directories. A one-liner with Str, but Coq - * doesn't seem to use this library at all, so here is a slighly longer version. - *) - -let lpath_from_path path path_separator = - let n = String.length path in - let rec aux i l = - if i < n then - let j = - try String.index_from path i path_separator - with Not_found -> n - in - let dir = String.sub path i (j-i) in - aux (j+1) (dir::l) - else - l - in List.rev (aux 0 []) - -(* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = - let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) - let n = String.length curdir in - let l = String.length p in - if l > n && String.sub p 0 n = curdir then - let n' = - let sl = String.length Filename.dir_sep in - let i = ref n in - while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in - remove_path_dot (String.sub p n' (l - n')) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - let l = String.length p in - if l > n && String.sub p 0 n = cwd then - let n' = - let sl = String.length Filename.dir_sep in - let i = ref n in - while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in - remove_path_dot (String.sub p n' (l - n')) - else - remove_path_dot p - -let canonical_path_name p = - let current = Sys.getcwd () in - try - Sys.chdir p; - let p' = Sys.getcwd () in - Sys.chdir current; - p' - with Sys_error _ -> - (* We give up to find a canonical name and just simplify it... *) - strip_path p - (* All subdirectories, recursively *) let exists_dir dir = @@ -212,17 +95,11 @@ let is_in_path lpath filename = let path_separator = if Sys.os_type = "Unix" then ':' else ';' let is_in_system_path filename = - let path = try Sys.getenv "PATH" + let path = try Sys.getenv "PATH" with Not_found -> error "system variable PATH not found" in - let lpath = lpath_from_path path path_separator in + let lpath = CUnix.path_to_list path in is_in_path lpath filename -let make_suffix name suffix = - if Filename.check_suffix name suffix then name else (name ^ suffix) - -let file_readable_p name = - try access name [R_OK];true with Unix_error (_, _, _) -> false - let open_trapping_failure name = try open_out_bin name with _ -> error ("Can't open " ^ name) @@ -240,7 +117,7 @@ exception Bad_magic_number of string let raw_extern_intern magic suffix = let extern_state name = - let filename = make_suffix name suffix in + let filename = CUnix.make_suffix name suffix in let channel = open_trapping_failure filename in output_binary_int channel magic; filename,channel @@ -265,7 +142,7 @@ let extern_intern ?(warn=true) magic suffix = with Sys_error s -> error ("System error: " ^ s) and intern_state paths name = try - let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in + let _,filename = find_file_in_path ~warn paths (CUnix.make_suffix name suffix) in let channel = raw_intern filename in let v = marshal_in channel in close_in channel; @@ -279,7 +156,7 @@ let with_magic_number_check f a = try f a with Bad_magic_number fname -> errorlabstrm "with_magic_number_check" - (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ + (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ strbrk "It is corrupted or was compiled with another version of Coq.") (* Communication through files with another executable *) @@ -318,26 +195,6 @@ let connect writefun readfun com = unlink tmp_to; a -let run_command converter f c = - let result = Buffer.create 127 in - let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in - let buff = String.make 127 ' ' in - let buffe = String.make 127 ' ' in - let n = ref 0 in - let ne = ref 0 in - - while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; - !n+ !ne <> 0 - do - let r = converter (String.sub buff 0 !n) in - f r; - Buffer.add_string result r; - let r = converter (String.sub buffe 0 !ne) in - f r; - Buffer.add_string result r - done; - (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) - (* Time stamps. *) type time = float * float * float diff --git a/lib/system.mli b/lib/system.mli index fae7fd1ed..89fd9df60 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** System utilities *) +(** {5 Coqtop specific system utilities} *) (** {6 Files and load paths} *) @@ -14,32 +14,17 @@ given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) -type physical_path = string -type load_path = physical_path list - -val canonical_path_name : string -> string - val exclude_search_in_dirname : string -> unit -val all_subdirs : unix_path:string -> (physical_path * string list) list -val is_in_path : load_path -> string -> bool +val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list +val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool -val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string - -val physical_path_of_string : string -> physical_path -val string_of_physical_path : physical_path -> string - -val make_suffix : string -> string -> string -val file_readable_p : string -> bool - -val expand_path_macros : string -> string -val getenv_else : string -> string -> string -val home : string +val where_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string val exists_dir : string -> bool val find_file_in_path : - ?warn:bool -> load_path -> string -> physical_path * string + ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number @@ -55,7 +40,7 @@ val raw_extern_intern : int -> string -> (string -> string * out_channel) * (string -> in_channel) val extern_intern : ?warn:bool -> int -> string -> - (string -> 'a -> unit) * (load_path -> string -> 'a) + (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a) val with_magic_number_check : ('a -> 'b) -> 'a -> 'b @@ -63,15 +48,6 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a -(** {6 Executing commands } *) -(** [run_command converter f com] launches command [com], and returns - the contents of stdout and stderr that have been processed with - [converter]; the processed contents of stdout and stderr is also - passed to [f] *) - -val run_command : (string -> string) -> (string -> unit) -> string -> - Unix.process_status * string - (** {6 Time stamps.} *) type time diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml index bf931d75b..014331202 100644 --- a/lib/xml_parser.ml +++ b/lib/xml_parser.ml @@ -20,7 +20,7 @@ open Printf -type xml = +type xml = Serialize.xml = | Element of (string * (string * string) list * xml list) | PCData of string diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli index e3e7ac4dc..2c83eee9d 100644 --- a/lib/xml_parser.mli +++ b/lib/xml_parser.mli @@ -27,9 +27,7 @@ (** An Xml node is either [Element (tag-name, attributes, children)] or [PCData text] *) -type xml = - | Element of (string * (string * string) list * xml list) - | PCData of string +type xml = Serialize.xml (** Abstract type for an Xml parser. *) type t diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml index 310035862..1d09b1723 100644 --- a/lib/xml_utils.ml +++ b/lib/xml_utils.ml @@ -18,7 +18,7 @@ *) open Printf -open Xml_parser +open Serialize exception Not_element of xml exception Not_pcdata of xml diff --git a/library/goptions.ml b/library/goptions.ml index 30804fa5f..1a490c8ce 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -18,9 +18,9 @@ open Term open Nametab open Mod_subst -open Goptionstyp +open Interface -type option_name = Goptionstyp.option_name +type option_name = Interface.option_name (****************************************************************************) (* 0- Common things *) diff --git a/library/goptions.mli b/library/goptions.mli index 979bca2d2..bf894d9c8 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -52,7 +52,7 @@ open Term open Nametab open Mod_subst -type option_name = Goptionstyp.option_name +type option_name = Interface.option_name (** {6 Tables. } *) @@ -165,7 +165,7 @@ val set_string_option_value : option_name -> string -> unit val print_option_value : option_name -> unit -val get_tables : unit -> Goptionstyp.option_state OptionMap.t +val get_tables : unit -> Interface.option_state OptionMap.t val print_tables : unit -> unit val error_undeclared_key : option_name -> 'a diff --git a/library/goptionstyp.mli b/library/goptionstyp.mli deleted file mode 100644 index 541a1470c..000000000 --- a/library/goptionstyp.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Some types used in the generic option mechanism (Goption) *) - -(** Placing them here in a pure interface avoid some dependency issues - when compiling CoqIDE *) - -type option_name = string list - -type option_value = - | BoolValue of bool - | IntValue of int option - | StringValue of string - -type option_state = { - opt_sync : bool; - opt_depr : bool; - opt_name : string; - opt_value : option_value; -} diff --git a/library/library.ml b/library/library.ml index e2adb3fb9..66bca4f1b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -23,19 +23,19 @@ open Nametab type logical_path = dir_path -let load_paths = ref ([] : (System.physical_path * logical_path * bool) list) +let load_paths = ref ([] : (CUnix.physical_path * logical_path * bool) list) let get_load_paths () = List.map pi1 !load_paths let find_logical_path phys_dir = - let phys_dir = System.canonical_path_name phys_dir in + let phys_dir = CUnix.canonical_path_name phys_dir in match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with | [_,dir,_] -> dir | [] -> Nameops.default_root_prefix | l -> anomaly ("Two logical paths are associated to "^phys_dir) let is_in_load_paths phys_dir = - let dir = System.canonical_path_name phys_dir in + let dir = CUnix.canonical_path_name phys_dir in let lp = get_load_paths () in let check_p = fun p -> (String.compare dir p) == 0 in List.exists check_p lp @@ -44,13 +44,13 @@ let remove_load_path dir = load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths let add_load_path isroot (phys_path,coq_path) = - let phys_path = System.canonical_path_name phys_path in + let phys_path = CUnix.canonical_path_name phys_path in match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with | [_,dir,_] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) && not - (phys_path = System.canonical_path_name Filename.current_dir_name + (phys_path = CUnix.canonical_path_name Filename.current_dir_name && coq_path = Nameops.default_root_prefix) then begin diff --git a/library/library.mli b/library/library.mli index c569ff485..95e4a6eb0 100644 --- a/library/library.mli +++ b/library/library.mli @@ -26,7 +26,7 @@ open Libobject val require_library : qualid located list -> bool option -> unit val require_library_from_dirpath : (dir_path * string) list -> bool option -> unit val require_library_from_file : - identifier option -> System.physical_path -> bool option -> unit + identifier option -> CUnix.physical_path -> bool option -> unit (** {6 ... } *) (** Open a module (or a library); if the boolean is true then it's also @@ -63,12 +63,12 @@ val set_xml_require : (dir_path -> unit) -> unit system; to each load path is associated a Coq [dir_path] (the "logical" path of the physical path) *) -val get_load_paths : unit -> System.physical_path list -val get_full_load_paths : unit -> (System.physical_path * dir_path) list -val add_load_path : bool -> System.physical_path * dir_path -> unit -val remove_load_path : System.physical_path -> unit -val find_logical_path : System.physical_path -> dir_path -val is_in_load_paths : System.physical_path -> bool +val get_load_paths : unit -> CUnix.physical_path list +val get_full_load_paths : unit -> (CUnix.physical_path * dir_path) list +val add_load_path : bool -> CUnix.physical_path * dir_path -> unit +val remove_load_path : CUnix.physical_path -> unit +val find_logical_path : CUnix.physical_path -> dir_path +val is_in_load_paths : CUnix.physical_path -> bool (** {6 Locate a library in the load paths } *) exception LibUnmappedDir @@ -76,7 +76,7 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - bool -> qualid -> library_location * dir_path * System.physical_path + bool -> qualid -> library_location * dir_path * CUnix.physical_path val try_locate_qualified_library : qualid located -> dir_path * string (** {6 Statistics: display the memory use of a library. } *) diff --git a/myocamlbuild.ml b/myocamlbuild.ml index bd4d1c345..dc73cf84c 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -104,7 +104,7 @@ let _build = Options.build_dir (** Abbreviations about files *) let core_libs = - ["lib/lib"; "kernel/kernel"; "library/library"; + ["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library"; "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; "parsing/parsing"; "tactics/tactics"; "toplevel/toplevel"; "parsing/highparsing"; "tactics/hightactics"] @@ -381,8 +381,8 @@ let extra_rules () = begin let core_mods = String.concat " " (List.map cat core_mllib) in let core_cmas = String.concat " " core_cma in Echo (["let copts = \"-cclib -lcoqrun\"\n"; - "let core_libs = \"coq_config.cmo "^core_cmas^"\"\n"; - "let core_objs = \"Coq_config "^core_mods^"\"\n"], + "let core_libs = \""^core_cmas^"\"\n"; + "let core_objs = \""^core_mods^"\"\n"], tolink)); (** For windows, building coff object file from a .rc (for the icon) *) @@ -407,8 +407,8 @@ let extra_rules () = begin let () = let fo = coqtop^".native" and fb = coqtop^".byte" in let depsall = (if w32 then [w32ico] else [])@[coqmktop_boot;libcoqrun] in - let depso = "coq_config.cmx" :: core_cmxa in - let depsb = "coq_config.cmo" :: core_cma in + let depso = core_cmxa in + let depsb = core_cma in let w32flag = if not w32 then N else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]) in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 8b7ee55bd..10eaa98b3 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1770,7 +1770,7 @@ let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivste Lazy.force require_csdp; let cmdname = - List.fold_left Filename.concat (Envars.coqlib ()) + List.fold_left Filename.concat (Envars.coqlib Errors.error) ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in match ((command cmdname [|cmdname|] (provername,poly)) : csdp_certificate) with diff --git a/scripts/coqc.ml b/scripts/coqc.ml index ce92b9118..e62a9d2f8 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -150,8 +150,7 @@ let parse_args () = parse (cfiles,o::args) rem | ("-where") :: _ -> - (try print_endline (Envars.coqlib ()) - with Errors.UserError(_,pps) -> Pp.msgerrnl (Pp.hov 0 pps)); + print_endline (Envars.coqlib (fun x -> x)); exit 0 | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0 diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index d0132763a..55e12a30e 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -56,7 +56,7 @@ let src_dirs () = [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] let includes () = - let coqlib = Envars.coqlib () in + let coqlib = Envars.coqlib Errors.error in let camlp4lib = Envars.camlp4lib () in List.fold_right (fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index bc840d2d9..c7e7044df 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -195,12 +195,13 @@ let coqdep () = add_rec_dir add_known "theories" ["Coq"]; add_rec_dir add_known "plugins" ["Coq"] end else begin - let coqlib = Envars.coqlib () in + let coqlib = Envars.coqlib Errors.error in add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in if Sys.file_exists user then add_rec_dir add_coqlib_known user []; - List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.xdg_dirs; + List.iter (fun s -> add_rec_dir add_coqlib_known s []) + (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x))); List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index f2255981a..31303b5ba 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -15,28 +15,28 @@ let coqtop = ref (stdin, stdout) let p = Xml_parser.make () let () = Xml_parser.check_eof p false -let eval_call (call:'a Ide_intf.call) = - prerr_endline (Ide_intf.pr_call call); - let xml_query = Ide_intf.of_call call in +let eval_call (call:'a Serialize.call) = + prerr_endline (Serialize.pr_call call); + let xml_query = Serialize.of_call call in Xml_utils.print_xml (snd !coqtop) xml_query; flush (snd !coqtop); let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in - let res = Ide_intf.to_answer xml_answer in - prerr_endline (Ide_intf.pr_full_value call res); + let res = Serialize.to_answer xml_answer in + prerr_endline (Serialize.pr_full_value call res); match res with Interface.Fail _ -> exit 1 | _ -> () let commands = - [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (true,false,s))); - "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (true,true,s))); - "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (false,false,s))); - "INTERP", (fun s -> eval_call (Ide_intf.interp (false,true,s))); - "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s))); - "GOALS", (fun _ -> eval_call Ide_intf.goals); - "HINTS", (fun _ -> eval_call Ide_intf.hints); - "GETOPTIONS", (fun _ -> eval_call Ide_intf.get_options); - "STATUS", (fun _ -> eval_call Ide_intf.status); - "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s)); - "MKCASES", (fun s -> eval_call (Ide_intf.mkcases s)); + [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (true,false,s))); + "INTERPRAW", (fun s -> eval_call (Serialize.interp (true,true,s))); + "INTERPSILENT", (fun s -> eval_call (Serialize.interp (false,false,s))); + "INTERP", (fun s -> eval_call (Serialize.interp (false,true,s))); + "REWIND", (fun s -> eval_call (Serialize.rewind (int_of_string s))); + "GOALS", (fun _ -> eval_call Serialize.goals); + "HINTS", (fun _ -> eval_call Serialize.hints); + "GETOPTIONS", (fun _ -> eval_call Serialize.get_options); + "STATUS", (fun _ -> eval_call Serialize.status); + "INLOADPATH", (fun s -> eval_call (Serialize.inloadpath s)); + "MKCASES", (fun s -> eval_call (Serialize.mkcases s)); "#", (fun _ -> raise Comment); ] diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index e4cfcb3f7..15916ef8c 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -30,14 +30,14 @@ let load_rcfile() = if !load_rc then try if !rcfile_specified then - if file_readable_p !rcfile then + if CUnix.file_readable_p !rcfile then Vernac.load_vernac false !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) - else try let inferedrc = List.find file_readable_p [ - Envars.xdg_config_home/rcdefaultname^"."^Coq_config.version; - Envars.xdg_config_home/rcdefaultname; - System.home/"."^rcdefaultname^"."^Coq_config.version; - System.home/"."^rcdefaultname; + else try let inferedrc = List.find CUnix.file_readable_p [ + Envars.xdg_config_home (fun x -> msg_warning (str x))/rcdefaultname^"."^Coq_config.version; + Envars.xdg_config_home (fun x -> msg_warning (str x))/rcdefaultname; + Envars.home (fun x -> msg_warning (str x))/"."^rcdefaultname^"."^Coq_config.version; + Envars.home (fun x -> msg_warning (str x))/"."^rcdefaultname; ] in Vernac.load_vernac false inferedrc with Not_found -> () @@ -92,9 +92,9 @@ let theories_dirs_map = [ (* Initializes the LoadPath *) let init_load_path () = - let coqlib = Envars.coqlib () in + let coqlib = Envars.coqlib Errors.error in let user_contrib = coqlib/"user-contrib" in - let xdg_dirs = Envars.xdg_dirs in + let xdg_dirs = Envars.xdg_dirs (fun x -> msg_warning (str x)) in let coqpath = Envars.coqpath in let dirs = ["states";"plugins"] in (* NOTE: These directories are searched from last to first *) @@ -130,7 +130,7 @@ let init_ocaml_path () = let add_subdir dl = Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl) in - Mltop.add_ml_dir (Envars.coqlib ()); + Mltop.add_ml_dir (Envars.coqlib Errors.error); List.iter add_subdir [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index bf5c84e64..fe6e350e6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -20,7 +20,7 @@ open Coqinit let get_version_date () = try - let coqlib = Envars.coqlib () in + let coqlib = Envars.coqlib Errors.error in let ch = open_in (Filename.concat coqlib "revision") in let ver = input_line ch in let rev = input_line ch in @@ -80,7 +80,7 @@ let set_rec_include d p = let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = - load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list + load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list let load_vernacular () = List.iter (fun (s,b) -> @@ -261,7 +261,7 @@ let parse_args arglist = | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem | "-coqlib" :: [] -> usage () - | "-where" :: _ -> print_endline (Envars.coqlib ()); exit (if !filter_opts then 2 else 0) + | "-where" :: _ -> print_endline (Envars.coqlib Errors.error); exit (if !filter_opts then 2 else 0) | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index f8bf9fccb..41a5f48a6 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -219,7 +219,7 @@ let hints () = (** Other API calls *) let inloadpath dir = - Library.is_in_load_paths (System.physical_path_of_string dir) + Library.is_in_load_paths (CUnix.physical_path_of_string dir) let status () = (** We remove the initial part of the current [dir_path] @@ -295,7 +295,7 @@ let eval_call c = in (* If the messages of last command are still there, we remove them *) ignore (read_stdout ()); - Ide_intf.abstract_eval_call handler c + Serialize.abstract_eval_call handler c (** The main loop *) @@ -311,7 +311,7 @@ let pr_debug s = if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s let fail err = - Ide_intf.of_value (fun _ -> assert false) (Interface.Fail (None, err)) + Serialize.of_value (fun _ -> assert false) (Interface.Fail (None, err)) let loop () = let p = Xml_parser.make () in @@ -326,16 +326,16 @@ let loop () = let xml_answer = try let xml_query = Xml_parser.parse p (Xml_parser.SChannel stdin) in - let q = Ide_intf.to_call xml_query in - let () = pr_debug ("<-- " ^ Ide_intf.pr_call q) in + let q = Serialize.to_call xml_query in + let () = pr_debug ("<-- " ^ Serialize.pr_call q) in let r = eval_call q in - let () = pr_debug ("--> " ^ Ide_intf.pr_full_value q r) in - Ide_intf.of_answer q r + let () = pr_debug ("--> " ^ Serialize.pr_full_value q r) in + Serialize.of_answer q r with | Xml_parser.Error (err, loc) -> let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in fail msg - | Ide_intf.Marshal_error -> + | Serialize.Marshal_error -> fail "Incorrect query." in Xml_utils.print_xml !orig_stdout xml_answer; diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index da9575ca6..e02e6329d 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -10,7 +10,7 @@ open Errors open Util open Pp open Flags -open System +open CUnix open Libobject open Library open System diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 599f8e9ff..b46d8fa8a 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -21,7 +21,6 @@ Vernacentries G_obligations Whelp Vernac -Ide_intf Ide_slave Toplevel Usage diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8c9b10786..b4add69ae 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -90,7 +90,7 @@ let print_usage_coqc () = let print_config () = if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; - Printf.printf "COQLIB=%s/\n" (Envars.coqlib ()); + Printf.printf "COQLIB=%s/\n" (Envars.coqlib Errors.error); Printf.printf "DOCDIR=%s/\n" (Envars.docdir ()); Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep; Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc; diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 20b45a2b0..916d213f5 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -172,7 +172,7 @@ let pr_new_syntax loc ocom = let rec vernac_com interpfun checknav (loc,com) = let rec interp = function | VernacLoad (verbosely, fname) -> - let fname = expand_path_macros fname in + let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in (* translator state *) let ch = !chan_beautify in let cs = Lexer.com_state() in @@ -184,13 +184,13 @@ let rec vernac_com interpfun checknav (loc,com) = begin let _,f = find_file_in_path ~warn:(Flags.is_verbose()) (Library.get_load_paths ()) - (make_suffix fname ".v") in + (CUnix.make_suffix fname ".v") in chan_beautify := open_out (f^beautify_suffix); Pp.comments := [] end; begin try - read_vernac_file verbosely (make_suffix fname ".v"); + read_vernac_file verbosely (CUnix.make_suffix fname ".v"); if !Flags.beautify_file then close_out !chan_beautify; chan_beautify := ch; Lexer.restore_com_state cs; @@ -228,7 +228,7 @@ let rec vernac_com interpfun checknav (loc,com) = | VernacTime v -> let tstart = System.get_time() in interp v; - let tend = System.get_time() in + let tend = get_time() in msgnl (str"Finished transaction in " ++ System.fmt_time_difference tstart tend) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 355e69356..538a502ec 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -708,33 +708,35 @@ let vernac_set_used_variables l = let vernac_require_from export filename = Library.require_library_from_file None - (System.expand_path_macros filename) + (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename) export let vernac_add_loadpath isrec pdir ldiropt = - let pdir = System.expand_path_macros pdir in + let pdir = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) pdir in let alias = match ldiropt with | None -> Nameops.default_root_prefix | Some ldir -> ldir in (if isrec then Mltop.add_rec_path else Mltop.add_path) ~unix_path:pdir ~coq_root:alias let vernac_remove_loadpath path = - Library.remove_load_path (System.expand_path_macros path) + Library.remove_load_path (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path) (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) - (System.expand_path_macros path) + (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path) let vernac_declare_ml_module local l = - Mltop.declare_ml_modules local (List.map System.expand_path_macros l) + Mltop.declare_ml_modules local (List.map + (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x))) + l) let vernac_chdir = function | None -> message (Sys.getcwd()) | Some path -> begin - try Sys.chdir (System.expand_path_macros path) + try Sys.chdir (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path) with Sys_error str -> warning ("Cd failed: " ^ str) end; if_verbose message (Sys.getcwd()) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index e9ecc95ec..c8729bfa9 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -134,7 +134,7 @@ type onlyparsing_flag = bool (* true = Parse only; false = Print also *) type infer_flag = bool (* true = try to Infer record; false = nothing *) type full_locality_flag = bool option (* true = Local; false = Global *) -type option_value = Goptionstyp.option_value = +type option_value = Interface.option_value = | BoolValue of bool | IntValue of int option | StringValue of string diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 332d30536..5da85be03 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -177,7 +177,7 @@ let make_string f x = Buffer.reset b; f x; Buffer.contents b let send_whelp req s = let url = make_whelp_request req s in let command = subst_command_placeholder browser_cmd_fmt url in - let _ = run_command (fun x -> x) print_string command in () + let _ = CUnix.run_command (fun x -> x) print_string command in () let whelp_constr req c = let c = detype false [whelm_special] [] c in |