From 59c9403ceb09a35ed219b522e9f5abdb50615d76 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 12 Apr 2012 20:49:01 +0000 Subject: 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 --- Makefile | 4 +- Makefile.build | 48 ++-- Makefile.common | 33 +-- _tags | 6 +- build | 8 +- checker/check.ml | 4 +- checker/check.mllib | 1 + checker/checker.ml | 9 +- checker/safe_typing.mli | 4 +- configure | 5 +- dev/base_include | 2 +- dev/db | 1 + dev/printers.mllib | 1 + doc/refman/RefMan-com.tex | 4 +- ide/coq.ml | 24 +- lib/cUnix.ml | 108 +++++++++ lib/cUnix.mli | 32 +++ lib/clib.mllib | 8 + lib/envars.ml | 72 ++++-- lib/envars.mli | 9 +- lib/interface.mli | 93 ++++++++ lib/lib.mllib | 5 - lib/serialize.ml | 447 +++++++++++++++++++++++++++++++++++++ lib/serialize.mli | 89 ++++++++ lib/system.ml | 153 +------------ lib/system.mli | 36 +-- lib/xml_parser.ml | 2 +- lib/xml_parser.mli | 4 +- lib/xml_utils.ml | 2 +- library/goptions.ml | 4 +- library/goptions.mli | 4 +- library/goptionstyp.mli | 26 --- library/library.ml | 10 +- library/library.mli | 16 +- myocamlbuild.ml | 10 +- plugins/micromega/coq_micromega.ml | 2 +- scripts/coqc.ml | 3 +- scripts/coqmktop.ml | 2 +- tools/coqdep.ml | 5 +- tools/fake_ide.ml | 32 +-- toplevel/coqinit.ml | 18 +- toplevel/coqtop.ml | 6 +- toplevel/ide_intf.ml | 446 ------------------------------------ toplevel/ide_intf.mli | 87 -------- toplevel/ide_slave.ml | 16 +- toplevel/interface.mli | 93 -------- toplevel/mltop.ml4 | 2 +- toplevel/toplevel.mllib | 1 - toplevel/usage.ml | 2 +- toplevel/vernac.ml | 8 +- toplevel/vernacentries.ml | 14 +- toplevel/vernacexpr.ml | 2 +- toplevel/whelp.ml4 | 2 +- 53 files changed, 1000 insertions(+), 1025 deletions(-) create mode 100644 lib/cUnix.ml create mode 100644 lib/cUnix.mli create mode 100644 lib/clib.mllib create mode 100644 lib/interface.mli create mode 100644 lib/serialize.ml create mode 100644 lib/serialize.mli delete mode 100644 library/goptionstyp.mli delete mode 100644 toplevel/ide_intf.ml delete mode 100644 toplevel/ide_intf.mli delete mode 100644 toplevel/interface.mli diff --git a/Makefile b/Makefile index b0d243e21..695de0c53 100644 --- a/Makefile +++ b/Makefile @@ -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 ) ########################################################################### diff --git a/_tags b/_tags index 6c69011b8..b714aa93d 100644 --- a/_tags +++ b/_tags @@ -2,9 +2,9 @@ ## tags for binaries : use_str, use_unix, use_dynlink, use_camlpX - : use_unix, use_dynlink, use_camlpX + : use_str, use_unix, use_dynlink, use_camlpX : use_unix - : use_unix, use_dynlink, use_camlpX + : use_str, use_unix, use_dynlink, use_camlpX : use_str : use_str, use_unix : 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 diff --git a/build b/build index c4b90d86c..da3efdca3 100755 --- a/build +++ b/build @@ -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. diff --git a/configure b/configure index 0fe91b9dc..00938f40f 100755 --- a/configure +++ b/configure @@ -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;; diff --git a/dev/db b/dev/db index 63c98bb6b..e7346c6b4 100644 --- a/dev/db +++ b/dev/db @@ -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 *) +(* 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 *) +(* 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 + 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/lib/interface.mli b/lib/interface.mli new file mode 100644 index 000000000..f2aba72e9 --- /dev/null +++ b/lib/interface.mli @@ -0,0 +1,93 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string; + rewind : int -> int; + goals : unit -> goals option; + evars : unit -> evar list option; + hints : unit -> (hint list * hint) option; + status : unit -> status; + get_options : unit -> (option_name * option_state) list; + set_options : (option_name * option_value) list -> unit; + inloadpath : string -> bool; + mkcases : string -> string list list; + handle_exn : exn -> location * string; +} 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/lib/serialize.ml b/lib/serialize.ml new file mode 100644 index 000000000..96cdc6c2c --- /dev/null +++ b/lib/serialize.ml @@ -0,0 +1,447 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Obj.magic (handler.interp (r,b,s) : string) + | Rewind i -> Obj.magic (handler.rewind i : int) + | Goal -> Obj.magic (handler.goals () : goals option) + | Evars -> Obj.magic (handler.evars () : evar list option) + | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) + | Status -> Obj.magic (handler.status () : status) + | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) + | SetOptions opts -> Obj.magic (handler.set_options opts : unit) + | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) + | MkCases s -> Obj.magic (handler.mkcases s : string list list) + in Good res + with e -> + let (l, str) = handler.handle_exn e in + Fail (l,str) + +(** * XML data marshalling *) + +exception Marshal_error + +(** Utility functions *) + +let massoc x l = + try List.assoc x l + with Not_found -> raise Marshal_error + +let constructor t c args = Element (t, ["val", c], args) + +let do_match constr t mf = match constr with +| Element (s, attrs, args) -> + if s = t then + let c = massoc "val" attrs in + mf c args + else raise Marshal_error +| _ -> raise Marshal_error + +let pcdata = function +| PCData s -> s +| _ -> raise Marshal_error + +let singleton = function +| [x] -> x +| _ -> raise Marshal_error + +let raw_string = function +| [] -> "" +| [PCData s] -> s +| _ -> raise Marshal_error + +let bool_arg tag b = if b then [tag, ""] else [] + +(** Base types *) + +let of_bool b = + if b then constructor "bool" "true" [] + else constructor "bool" "false" [] + +let to_bool xml = do_match xml "bool" + (fun s _ -> match s with + | "true" -> true + | "false" -> false + | _ -> raise Marshal_error) + +let of_list f l = + Element ("list", [], List.map f l) + +let to_list f = function +| Element ("list", [], l) -> + List.map f l +| _ -> raise Marshal_error + +let of_option f = function +| None -> Element ("option", ["val", "none"], []) +| Some x -> Element ("option", ["val", "some"], [f x]) + +let to_option f = function +| Element ("option", ["val", "none"], []) -> None +| Element ("option", ["val", "some"], [x]) -> Some (f x) +| _ -> raise Marshal_error + +let of_string s = Element ("string", [], [PCData s]) + +let to_string = function +| Element ("string", [], l) -> raw_string l +| _ -> raise Marshal_error + +let of_int i = Element ("int", [], [PCData (string_of_int i)]) + +let to_int = function +| Element ("int", [], [PCData s]) -> int_of_string s +| _ -> raise Marshal_error + +let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) + +let to_pair f g = function +| Element ("pair", [], [x; y]) -> (f x, g y) +| _ -> raise Marshal_error + +(** More elaborate types *) + +let of_option_value = function +| IntValue i -> + constructor "option_value" "intvalue" [of_option of_int i] +| BoolValue b -> + constructor "option_value" "boolvalue" [of_bool b] +| StringValue s -> + constructor "option_value" "stringvalue" [of_string s] + +let to_option_value xml = do_match xml "option_value" + (fun s args -> match s with + | "intvalue" -> IntValue (to_option to_int (singleton args)) + | "boolvalue" -> BoolValue (to_bool (singleton args)) + | "stringvalue" -> StringValue (to_string (singleton args)) + | _ -> raise Marshal_error + ) + +let of_option_state s = + Element ("option_state", [], [ + of_bool s.opt_sync; + of_bool s.opt_depr; + of_string s.opt_name; + of_option_value s.opt_value] + ) + +let to_option_state = function +| Element ("option_state", [], [sync; depr; name; value]) -> + { + opt_sync = to_bool sync; + opt_depr = to_bool depr; + opt_name = to_string name; + opt_value = to_option_value value; + } +| _ -> raise Marshal_error + +let of_value f = function +| Good x -> Element ("value", ["val", "good"], [f x]) +| Fail (loc, msg) -> + let loc = match loc with + | None -> [] + | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] + in + Element ("value", ["val", "fail"] @ loc, [PCData msg]) + +let to_value f = function +| Element ("value", attrs, l) -> + let ans = massoc "val" attrs in + if ans = "good" then Good (f (singleton l)) + else if ans = "fail" then + let loc = + try + let loc_s = int_of_string (List.assoc "loc_s" attrs) in + let loc_e = int_of_string (List.assoc "loc_e" attrs) in + Some (loc_s, loc_e) + with _ -> None + in + let msg = raw_string l in + Fail (loc, msg) + else raise Marshal_error +| _ -> raise Marshal_error + +let of_call = function +| Interp (raw, vrb, cmd) -> + let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in + Element ("call", ("val", "interp") :: flags, [PCData cmd]) +| Rewind n -> + Element ("call", ("val", "rewind") :: ["steps", string_of_int n], []) +| Goal -> + Element ("call", ["val", "goal"], []) +| Evars -> + Element ("call", ["val", "evars"], []) +| Hints -> + Element ("call", ["val", "hints"], []) +| Status -> + Element ("call", ["val", "status"], []) +| GetOptions -> + Element ("call", ["val", "getoptions"], []) +| SetOptions opts -> + let args = List.map (of_pair (of_list of_string) of_option_value) opts in + Element ("call", ["val", "setoptions"], args) +| InLoadPath file -> + Element ("call", ["val", "inloadpath"], [PCData file]) +| MkCases ind -> + Element ("call", ["val", "mkcases"], [PCData ind]) + +let to_call = function +| Element ("call", attrs, l) -> + let ans = massoc "val" attrs in + begin match ans with + | "interp" -> + let raw = List.mem_assoc "raw" attrs in + let vrb = List.mem_assoc "verbose" attrs in + Interp (raw, vrb, raw_string l) + | "rewind" -> + let steps = int_of_string (massoc "steps" attrs) in + Rewind steps + | "goal" -> Goal + | "evars" -> Evars + | "status" -> Status + | "getoptions" -> GetOptions + | "setoptions" -> + let args = List.map (to_pair (to_list to_string) to_option_value) l in + SetOptions args + | "inloadpath" -> InLoadPath (raw_string l) + | "mkcases" -> MkCases (raw_string l) + | "hints" -> Hints + | _ -> raise Marshal_error + end +| _ -> raise Marshal_error + +let of_status s = + let of_so = of_option of_string in + let of_sl = of_list of_string in + Element ("status", [], + [ + of_sl s.status_path; + of_so s.status_proofname; + of_sl s.status_allproofs; + of_int s.status_statenum; + of_int s.status_proofnum; + ] + ) + +let to_status = function +| Element ("status", [], [path; name; prfs; snum; pnum]) -> + { + status_path = to_list to_string path; + status_proofname = to_option to_string name; + status_allproofs = to_list to_string prfs; + status_statenum = to_int snum; + status_proofnum = to_int pnum; + } +| _ -> raise Marshal_error + +let of_evar s = + Element ("evar", [], [PCData s.evar_info]) + +let to_evar = function +| Element ("evar", [], data) -> { evar_info = raw_string data; } +| _ -> raise Marshal_error + +let of_goal g = + let hyp = of_list of_string g.goal_hyp in + let ccl = of_string g.goal_ccl in + Element ("goal", [], [hyp; ccl]) + +let to_goal = function +| Element ("goal", [], [hyp; ccl]) -> + let hyp = to_list to_string hyp in + let ccl = to_string ccl in + { goal_hyp = hyp; goal_ccl = ccl } +| _ -> raise Marshal_error + +let of_goals g = + let fg = of_list of_goal g.fg_goals in + let bg = of_list of_goal g.bg_goals in + Element ("goals", [], [fg; bg]) + +let to_goals = function +| Element ("goals", [], [fg; bg]) -> + let fg = to_list to_goal fg in + let bg = to_list to_goal bg in + { fg_goals = fg; bg_goals = bg; } +| _ -> raise Marshal_error + +let of_hints = + let of_hint = of_list (of_pair of_string of_string) in + of_option (of_pair (of_list of_hint) of_hint) + +let of_answer (q : 'a call) (r : 'a value) = + let convert = match q with + | Interp _ -> Obj.magic (of_string : string -> xml) + | Rewind _ -> Obj.magic (of_int : int -> xml) + | Goal -> Obj.magic (of_option of_goals : goals option -> xml) + | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml) + | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml) + | Status -> Obj.magic (of_status : status -> xml) + | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml) + | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], [])) + | InLoadPath _ -> Obj.magic (of_bool : bool -> xml) + | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml) + in + of_value convert r + +let to_answer xml = + let rec convert elt = match elt with + | Element (tpe, attrs, l) -> + begin match tpe with + | "unit" -> Obj.magic () + | "string" -> Obj.magic (to_string elt : string) + | "int" -> Obj.magic (to_int elt : int) + | "status" -> Obj.magic (to_status elt : status) + | "bool" -> Obj.magic (to_bool elt : bool) + | "list" -> Obj.magic (to_list convert elt : 'a list) + | "option" -> Obj.magic (to_option convert elt : 'a option) + | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b)) + | "goals" -> Obj.magic (to_goals elt : goals) + | "evar" -> Obj.magic (to_evar elt : evar) + | "option_value" -> Obj.magic (to_option_value elt : option_value) + | "option_state" -> Obj.magic (to_option_state elt : option_state) + | _ -> raise Marshal_error + end + | _ -> raise Marshal_error + in + to_value convert xml + +(** * Debug printing *) + +let pr_option_value = function +| IntValue None -> "none" +| IntValue (Some i) -> string_of_int i +| StringValue s -> s +| BoolValue b -> if b then "true" else "false" + +let rec pr_setoptions opts = + let map (key, v) = + let key = String.concat " " key in + key ^ " := " ^ (pr_option_value v) + in + String.concat "; " (List.map map opts) + +let pr_getoptions opts = + let map (key, s) = + let key = String.concat " " key in + Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n" + key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) + in + "\n" ^ String.concat "" (List.map map opts) + +let pr_call = function + | Interp (r,b,s) -> + let raw = if r then "RAW" else "" in + let verb = if b then "" else "SILENT" in + "INTERP"^raw^verb^" ["^s^"]" + | Rewind i -> "REWIND "^(string_of_int i) + | Goal -> "GOALS" + | Evars -> "EVARS" + | Hints -> "HINTS" + | Status -> "STATUS" + | GetOptions -> "GETOPTIONS" + | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]" + | InLoadPath s -> "INLOADPATH "^s + | MkCases s -> "MKCASES "^s + +let pr_value_gen pr = function + | Good v -> "GOOD " ^ pr v + | Fail (_,str) -> "FAIL ["^str^"]" + +let pr_value v = pr_value_gen (fun _ -> "") v + +let pr_string s = "["^s^"]" +let pr_bool b = if b then "true" else "false" + +let pr_status s = + let path = + let l = String.concat "." s.status_path in + "path=" ^ l ^ ";" + in + let name = match s.status_proofname with + | None -> "no proof;" + | Some n -> "proof = " ^ n ^ ";" + in + "Status: " ^ path ^ name + +let pr_mkcases l = + let l = List.map (String.concat " ") l in + "[" ^ String.concat " | " l ^ "]" + +let pr_goals_aux g = + if g.fg_goals = [] then + if g.bg_goals = [] then "Proof completed." + else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals) + else + let pr_menu s = s in + let pr_goal { goal_hyp = hyps; goal_ccl = goal } = + "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]" + in + String.concat " " (List.map pr_goal g.fg_goals) + +let pr_goals = function +| None -> "No proof in progress." +| Some g -> pr_goals_aux g + +let pr_evar ev = "[" ^ ev.evar_info ^ "]" + +let pr_evars = function +| None -> "No proof in progress." +| Some evars -> String.concat " " (List.map pr_evar evars) + +let pr_full_value call value = + match call with + | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value) + | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value) + | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option value) + | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value) + | Hints -> pr_value value + | Status -> pr_value_gen pr_status (Obj.magic value : status value) + | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value) + | SetOptions _ -> pr_value value + | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value) + | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value) diff --git a/lib/serialize.mli b/lib/serialize.mli new file mode 100644 index 000000000..2ab557c53 --- /dev/null +++ b/lib/serialize.mli @@ -0,0 +1,89 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string call + +(** Backtracking by at least a certain number of phrases. + No finished proofs will be re-opened. Instead, + we continue backtracking until before these proofs, + and answer the amount of extra backtracking performed. + Backtracking by more than the number of phrases already + interpreted successfully (and not yet undone) will fail. *) +val rewind : int -> int call + +(** Fetching the list of current goals. Return [None] if no proof is in + progress, [Some gl] otherwise. *) +val goals : goals option call + +(** Retrieving the tactics applicable to the current goal. [None] if there is + no proof in progress. *) +val hints : (hint list * hint) option call + +(** The status, for instance "Ready in SomeSection, proving Foo" *) +val status : status call + +(** Is a directory part of Coq's loadpath ? *) +val inloadpath : string -> bool call + +(** Create a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. *) +val mkcases : string -> string list list call + +(** Retrieve the list of unintantiated evars in the current proof. [None] if no + proof is in progress. *) +val evars : evar list option call + +(** Retrieve the list of options of the current toplevel, together with their + state. *) +val get_options : (option_name * option_state) list call + +(** Set the options to the given value. Warning: this is not atomic, so whenever + the call fails, the option state can be messed up... This is the caller duty + to check that everything is correct. *) +val set_options : (option_name * option_value) list -> unit call + +val abstract_eval_call : handler -> 'a call -> 'a value + +(** * XML data marshalling *) + +exception Marshal_error + +val of_value : ('a -> xml) -> 'a value -> xml +val to_value : (xml -> 'a) -> xml -> 'a value + +val of_call : 'a call -> xml +val to_call : xml -> 'a call + +val of_answer : 'a call -> 'a value -> xml +val to_answer : xml -> 'a value + +(** * Debug printing *) + +val pr_call : 'a call -> string +val pr_value : 'a value -> string +val pr_full_value : 'a call -> 'a value -> string 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 - 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 *) -(* 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_intf.ml b/toplevel/ide_intf.ml deleted file mode 100644 index d36e46624..000000000 --- a/toplevel/ide_intf.ml +++ /dev/null @@ -1,446 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Obj.magic (handler.interp (r,b,s) : string) - | Rewind i -> Obj.magic (handler.rewind i : int) - | Goal -> Obj.magic (handler.goals () : goals option) - | Evars -> Obj.magic (handler.evars () : evar list option) - | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) - | Status -> Obj.magic (handler.status () : status) - | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) - | SetOptions opts -> Obj.magic (handler.set_options opts : unit) - | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) - | MkCases s -> Obj.magic (handler.mkcases s : string list list) - in Good res - with e -> - let (l, str) = handler.handle_exn e in - Fail (l,str) - -(** * XML data marshalling *) - -exception Marshal_error - -(** Utility functions *) - -let massoc x l = - try List.assoc x l - with Not_found -> raise Marshal_error - -let constructor t c args = Element (t, ["val", c], args) - -let do_match constr t mf = match constr with -| Element (s, attrs, args) -> - if s = t then - let c = massoc "val" attrs in - mf c args - else raise Marshal_error -| _ -> raise Marshal_error - -let pcdata = function -| PCData s -> s -| _ -> raise Marshal_error - -let singleton = function -| [x] -> x -| _ -> raise Marshal_error - -let raw_string = function -| [] -> "" -| [PCData s] -> s -| _ -> raise Marshal_error - -let bool_arg tag b = if b then [tag, ""] else [] - -(** Base types *) - -let of_bool b = - if b then constructor "bool" "true" [] - else constructor "bool" "false" [] - -let to_bool xml = do_match xml "bool" - (fun s _ -> match s with - | "true" -> true - | "false" -> false - | _ -> raise Marshal_error) - -let of_list f l = - Element ("list", [], List.map f l) - -let to_list f = function -| Element ("list", [], l) -> - List.map f l -| _ -> raise Marshal_error - -let of_option f = function -| None -> Element ("option", ["val", "none"], []) -| Some x -> Element ("option", ["val", "some"], [f x]) - -let to_option f = function -| Element ("option", ["val", "none"], []) -> None -| Element ("option", ["val", "some"], [x]) -> Some (f x) -| _ -> raise Marshal_error - -let of_string s = Element ("string", [], [PCData s]) - -let to_string = function -| Element ("string", [], l) -> raw_string l -| _ -> raise Marshal_error - -let of_int i = Element ("int", [], [PCData (string_of_int i)]) - -let to_int = function -| Element ("int", [], [PCData s]) -> int_of_string s -| _ -> raise Marshal_error - -let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) - -let to_pair f g = function -| Element ("pair", [], [x; y]) -> (f x, g y) -| _ -> raise Marshal_error - -(** More elaborate types *) - -let of_option_value = function -| IntValue i -> - constructor "option_value" "intvalue" [of_option of_int i] -| BoolValue b -> - constructor "option_value" "boolvalue" [of_bool b] -| StringValue s -> - constructor "option_value" "stringvalue" [of_string s] - -let to_option_value xml = do_match xml "option_value" - (fun s args -> match s with - | "intvalue" -> IntValue (to_option to_int (singleton args)) - | "boolvalue" -> BoolValue (to_bool (singleton args)) - | "stringvalue" -> StringValue (to_string (singleton args)) - | _ -> raise Marshal_error - ) - -let of_option_state s = - Element ("option_state", [], [ - of_bool s.opt_sync; - of_bool s.opt_depr; - of_string s.opt_name; - of_option_value s.opt_value] - ) - -let to_option_state = function -| Element ("option_state", [], [sync; depr; name; value]) -> - { - opt_sync = to_bool sync; - opt_depr = to_bool depr; - opt_name = to_string name; - opt_value = to_option_value value; - } -| _ -> raise Marshal_error - -let of_value f = function -| Good x -> Element ("value", ["val", "good"], [f x]) -| Fail (loc, msg) -> - let loc = match loc with - | None -> [] - | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] - in - Element ("value", ["val", "fail"] @ loc, [PCData msg]) - -let to_value f = function -| Element ("value", attrs, l) -> - let ans = massoc "val" attrs in - if ans = "good" then Good (f (singleton l)) - else if ans = "fail" then - let loc = - try - let loc_s = int_of_string (List.assoc "loc_s" attrs) in - let loc_e = int_of_string (List.assoc "loc_e" attrs) in - Some (loc_s, loc_e) - with _ -> None - in - let msg = raw_string l in - Fail (loc, msg) - else raise Marshal_error -| _ -> raise Marshal_error - -let of_call = function -| Interp (raw, vrb, cmd) -> - let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in - Element ("call", ("val", "interp") :: flags, [PCData cmd]) -| Rewind n -> - Element ("call", ("val", "rewind") :: ["steps", string_of_int n], []) -| Goal -> - Element ("call", ["val", "goal"], []) -| Evars -> - Element ("call", ["val", "evars"], []) -| Hints -> - Element ("call", ["val", "hints"], []) -| Status -> - Element ("call", ["val", "status"], []) -| GetOptions -> - Element ("call", ["val", "getoptions"], []) -| SetOptions opts -> - let args = List.map (of_pair (of_list of_string) of_option_value) opts in - Element ("call", ["val", "setoptions"], args) -| InLoadPath file -> - Element ("call", ["val", "inloadpath"], [PCData file]) -| MkCases ind -> - Element ("call", ["val", "mkcases"], [PCData ind]) - -let to_call = function -| Element ("call", attrs, l) -> - let ans = massoc "val" attrs in - begin match ans with - | "interp" -> - let raw = List.mem_assoc "raw" attrs in - let vrb = List.mem_assoc "verbose" attrs in - Interp (raw, vrb, raw_string l) - | "rewind" -> - let steps = int_of_string (massoc "steps" attrs) in - Rewind steps - | "goal" -> Goal - | "evars" -> Evars - | "status" -> Status - | "getoptions" -> GetOptions - | "setoptions" -> - let args = List.map (to_pair (to_list to_string) to_option_value) l in - SetOptions args - | "inloadpath" -> InLoadPath (raw_string l) - | "mkcases" -> MkCases (raw_string l) - | "hints" -> Hints - | _ -> raise Marshal_error - end -| _ -> raise Marshal_error - -let of_status s = - let of_so = of_option of_string in - let of_sl = of_list of_string in - Element ("status", [], - [ - of_sl s.status_path; - of_so s.status_proofname; - of_sl s.status_allproofs; - of_int s.status_statenum; - of_int s.status_proofnum; - ] - ) - -let to_status = function -| Element ("status", [], [path; name; prfs; snum; pnum]) -> - { - status_path = to_list to_string path; - status_proofname = to_option to_string name; - status_allproofs = to_list to_string prfs; - status_statenum = to_int snum; - status_proofnum = to_int pnum; - } -| _ -> raise Marshal_error - -let of_evar s = - Element ("evar", [], [PCData s.evar_info]) - -let to_evar = function -| Element ("evar", [], data) -> { evar_info = raw_string data; } -| _ -> raise Marshal_error - -let of_goal g = - let hyp = of_list of_string g.goal_hyp in - let ccl = of_string g.goal_ccl in - Element ("goal", [], [hyp; ccl]) - -let to_goal = function -| Element ("goal", [], [hyp; ccl]) -> - let hyp = to_list to_string hyp in - let ccl = to_string ccl in - { goal_hyp = hyp; goal_ccl = ccl } -| _ -> raise Marshal_error - -let of_goals g = - let fg = of_list of_goal g.fg_goals in - let bg = of_list of_goal g.bg_goals in - Element ("goals", [], [fg; bg]) - -let to_goals = function -| Element ("goals", [], [fg; bg]) -> - let fg = to_list to_goal fg in - let bg = to_list to_goal bg in - { fg_goals = fg; bg_goals = bg; } -| _ -> raise Marshal_error - -let of_hints = - let of_hint = of_list (of_pair of_string of_string) in - of_option (of_pair (of_list of_hint) of_hint) - -let of_answer (q : 'a call) (r : 'a value) = - let convert = match q with - | Interp _ -> Obj.magic (of_string : string -> xml) - | Rewind _ -> Obj.magic (of_int : int -> xml) - | Goal -> Obj.magic (of_option of_goals : goals option -> xml) - | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml) - | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml) - | Status -> Obj.magic (of_status : status -> xml) - | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml) - | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], [])) - | InLoadPath _ -> Obj.magic (of_bool : bool -> xml) - | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml) - in - of_value convert r - -let to_answer xml = - let rec convert elt = match elt with - | Element (tpe, attrs, l) -> - begin match tpe with - | "unit" -> Obj.magic () - | "string" -> Obj.magic (to_string elt : string) - | "int" -> Obj.magic (to_int elt : int) - | "status" -> Obj.magic (to_status elt : status) - | "bool" -> Obj.magic (to_bool elt : bool) - | "list" -> Obj.magic (to_list convert elt : 'a list) - | "option" -> Obj.magic (to_option convert elt : 'a option) - | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b)) - | "goals" -> Obj.magic (to_goals elt : goals) - | "evar" -> Obj.magic (to_evar elt : evar) - | "option_value" -> Obj.magic (to_option_value elt : option_value) - | "option_state" -> Obj.magic (to_option_state elt : option_state) - | _ -> raise Marshal_error - end - | _ -> raise Marshal_error - in - to_value convert xml - -(** * Debug printing *) - -let pr_option_value = function -| IntValue None -> "none" -| IntValue (Some i) -> string_of_int i -| StringValue s -> s -| BoolValue b -> if b then "true" else "false" - -let rec pr_setoptions opts = - let map (key, v) = - let key = String.concat " " key in - key ^ " := " ^ (pr_option_value v) - in - String.concat "; " (List.map map opts) - -let pr_getoptions opts = - let map (key, s) = - let key = String.concat " " key in - Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n" - key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) - in - "\n" ^ String.concat "" (List.map map opts) - -let pr_call = function - | Interp (r,b,s) -> - let raw = if r then "RAW" else "" in - let verb = if b then "" else "SILENT" in - "INTERP"^raw^verb^" ["^s^"]" - | Rewind i -> "REWIND "^(string_of_int i) - | Goal -> "GOALS" - | Evars -> "EVARS" - | Hints -> "HINTS" - | Status -> "STATUS" - | GetOptions -> "GETOPTIONS" - | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]" - | InLoadPath s -> "INLOADPATH "^s - | MkCases s -> "MKCASES "^s - -let pr_value_gen pr = function - | Good v -> "GOOD " ^ pr v - | Fail (_,str) -> "FAIL ["^str^"]" - -let pr_value v = pr_value_gen (fun _ -> "") v - -let pr_string s = "["^s^"]" -let pr_bool b = if b then "true" else "false" - -let pr_status s = - let path = - let l = String.concat "." s.status_path in - "path=" ^ l ^ ";" - in - let name = match s.status_proofname with - | None -> "no proof;" - | Some n -> "proof = " ^ n ^ ";" - in - "Status: " ^ path ^ name - -let pr_mkcases l = - let l = List.map (String.concat " ") l in - "[" ^ String.concat " | " l ^ "]" - -let pr_goals_aux g = - if g.fg_goals = [] then - if g.bg_goals = [] then "Proof completed." - else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals) - else - let pr_menu s = s in - let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]" - in - String.concat " " (List.map pr_goal g.fg_goals) - -let pr_goals = function -| None -> "No proof in progress." -| Some g -> pr_goals_aux g - -let pr_evar ev = "[" ^ ev.evar_info ^ "]" - -let pr_evars = function -| None -> "No proof in progress." -| Some evars -> String.concat " " (List.map pr_evar evars) - -let pr_full_value call value = - match call with - | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value) - | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value) - | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option value) - | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value) - | Hints -> pr_value value - | Status -> pr_value_gen pr_status (Obj.magic value : status value) - | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value) - | SetOptions _ -> pr_value value - | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value) - | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value) diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli deleted file mode 100644 index 69204da16..000000000 --- a/toplevel/ide_intf.mli +++ /dev/null @@ -1,87 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string call - -(** Backtracking by at least a certain number of phrases. - No finished proofs will be re-opened. Instead, - we continue backtracking until before these proofs, - and answer the amount of extra backtracking performed. - Backtracking by more than the number of phrases already - interpreted successfully (and not yet undone) will fail. *) -val rewind : int -> int call - -(** Fetching the list of current goals. Return [None] if no proof is in - progress, [Some gl] otherwise. *) -val goals : goals option call - -(** Retrieving the tactics applicable to the current goal. [None] if there is - no proof in progress. *) -val hints : (hint list * hint) option call - -(** The status, for instance "Ready in SomeSection, proving Foo" *) -val status : status call - -(** Is a directory part of Coq's loadpath ? *) -val inloadpath : string -> bool call - -(** Create a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. *) -val mkcases : string -> string list list call - -(** Retrieve the list of unintantiated evars in the current proof. [None] if no - proof is in progress. *) -val evars : evar list option call - -(** Retrieve the list of options of the current toplevel, together with their - state. *) -val get_options : (option_name * option_state) list call - -(** Set the options to the given value. Warning: this is not atomic, so whenever - the call fails, the option state can be messed up... This is the caller duty - to check that everything is correct. *) -val set_options : (option_name * option_value) list -> unit call - -val abstract_eval_call : handler -> 'a call -> 'a value - -(** * XML data marshalling *) - -exception Marshal_error - -val of_value : ('a -> xml) -> 'a value -> xml -val to_value : (xml -> 'a) -> xml -> 'a value - -val of_call : 'a call -> xml -val to_call : xml -> 'a call - -val of_answer : 'a call -> 'a value -> xml -val to_answer : xml -> 'a value - -(** * Debug printing *) - -val pr_call : 'a call -> string -val pr_value : 'a value -> string -val pr_full_value : 'a call -> 'a value -> string 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/interface.mli b/toplevel/interface.mli deleted file mode 100644 index 604060550..000000000 --- a/toplevel/interface.mli +++ /dev/null @@ -1,93 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string; - rewind : int -> int; - goals : unit -> goals option; - evars : unit -> evar list option; - hints : unit -> (hint list * hint) option; - status : unit -> status; - get_options : unit -> (option_name * option_state) list; - set_options : (option_name * option_value) list -> unit; - inloadpath : string -> bool; - mkcases : string -> string list list; - handle_exn : exn -> location * string; -} 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 -- cgit v1.2.3