From 2def58217686b5083da38778a5ebffb451b1d4d6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 22:12:02 +0200 Subject: [flags] Remove XML output flag. This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied. --- Makefile.build | 12 +++--------- doc/tools/Translator.tex | 2 +- interp/declare.ml | 15 +-------------- interp/declare.mli | 5 ----- lib/flags.ml | 3 --- lib/flags.mli | 5 ----- library/declaremods.ml | 17 ----------------- library/declaremods.mli | 8 -------- library/lib.ml | 7 ------- library/lib.mli | 6 +----- library/library.ml | 3 --- library/library.mli | 3 --- man/coqide.1 | 7 ------- man/coqtop.1 | 6 ------ parsing/cLexer.ml4 | 6 ------ parsing/cLexer.mli | 3 --- test-suite/bugs/closed/HoTT_coq_032.v | 1 - tools/beautify-archive | 2 +- tools/check-translate | 2 +- tools/coqc.ml | 2 +- toplevel/coqtop.ml | 1 - toplevel/usage.ml | 3 --- toplevel/vernac.ml | 6 ------ toplevel/vernac.mli | 4 ---- 24 files changed, 9 insertions(+), 120 deletions(-) diff --git a/Makefile.build b/Makefile.build index b45c6427a..1c31f6c81 100644 --- a/Makefile.build +++ b/Makefile.build @@ -46,9 +46,6 @@ NO_RECALC_DEPS ?= # Non-empty runs the checker on all produced .vo files: VALIDATE ?= -# Is "-xml" when building XML library: -COQ_XML ?= - # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -189,7 +186,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # the output format of the unix command time. For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) +COQOPTS=$(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) @@ -273,9 +270,6 @@ $(error This Makefile needs GNU Make 3.81 or later (that is a version that suppo endif VO_TOOLS_DEP := $(COQTOPBEST) -ifdef COQ_XML - VO_TOOLS_DEP += $(COQDOC) -endif ifdef VALIDATE VO_TOOLS_DEP += $(CHICKEN) endif @@ -707,9 +701,9 @@ TIMING_EXTRA = endif theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) - $(SHOW)'COQC $(COQ_XML) -noinit $<' + $(SHOW)'COQC -noinit $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) # MExtraction.v generates the ml core file of the micromega tactic. # We check that this generated code is still in sync with the version diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index ed1d336d9..3ee65d6f2 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -614,7 +614,7 @@ is compiled by a Makefile with the following constraints: \begin{itemize} \item compilation is achieved by invoking make without specifying a target \item options are passed to Coq with make variable COQFLAGS that - includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML. + includes variables OPT, COQLIBS, and OTHERFLAGS. \end{itemize} These constraints are met by the makefiles produced by {\tt coq\_makefile} diff --git a/interp/declare.ml b/interp/declare.ml index 70f422b51..7fcb38296 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -32,14 +32,6 @@ type internal_flag = | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) -(** XML output hooks *) - -let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore () -let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore () -let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore () - -let if_xml f x = if !Flags.xml_export then f x else () - (** Declaration of section variables and local definitions *) type section_variable_entry = @@ -95,7 +87,6 @@ let declare_variable id obj = declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); Heads.declare_head (EvalVarRef id); - if_xml (Hook.get f_xml_declare_variable) oname; oname @@ -256,7 +247,6 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let id = Label.to_id (pi3 (Constant.repr3 c)) in ignore(add_leaf id o); update_tables c; - let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in match role with | Safe_typing.Subproof -> () | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] @@ -268,9 +258,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e cst_kind = kind; cst_locl = local; } in - let kn = declare_constant_common id cst in - let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in - kn + declare_constant_common id cst let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) @@ -410,7 +398,6 @@ let declare_mind mie = let isrecord,isprim = declare_projections mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; - if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname); oname, isprim (* Declaration messages *) diff --git a/interp/declare.mli b/interp/declare.mli index 6a0943464..ccd7d28bb 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -69,11 +69,6 @@ val set_declare_scheme : the whole block and a boolean indicating if it is a primitive record. *) val declare_mind : mutual_inductive_entry -> object_name * bool -(** Hooks for XML output *) -val xml_declare_variable : (object_name -> unit) Hook.t -val xml_declare_constant : (internal_flag * constant -> unit) Hook.t -val xml_declare_inductive : (bool * object_name -> unit) Hook.t - (** Declaration messages *) val definition_message : Id.t -> unit diff --git a/lib/flags.ml b/lib/flags.ml index 0bce22f58..40bad9035 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -87,8 +87,6 @@ let in_toplevel = ref false let profile = false -let xml_export = ref false - let ide_slave = ref false let ideslave_coqtop_flags = ref None @@ -96,7 +94,6 @@ let time = ref false let raw_print = ref false - let univ_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index eb4c37a54..388a3ff55 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -56,11 +56,6 @@ val stm_debug : bool ref val profile : bool -(* Legacy flags *) - -(* -xml option: xml hooks will be called *) -val xml_export : bool ref - (* -ide_slave: printing will be more verbose, will affect stm caching *) val ide_slave : bool ref val ideslave_coqtop_flags : string option ref diff --git a/library/declaremods.ml b/library/declaremods.ml index e7aa5bd0d..6d9295bde 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -557,17 +557,6 @@ let openmodtype_info = Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" -(** XML output hooks *) - -let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore () -let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore () -let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore () -let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore () -let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore () -let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore () - -let if_xml f x = if !Flags.xml_export then f x else () - (** {6 Modules : start, end, declare} *) module RawModOps = struct @@ -589,7 +578,6 @@ let start_module interp_modast export id args res fs = openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - if_xml (Hook.get f_xml_start_module) mp; mp let end_module () = @@ -628,7 +616,6 @@ let end_module () = assert (eq_full_path (fst newoname) (fst oldoname)); assert (ModPath.equal (mp_of_kn (snd newoname)) mp); - if_xml (Hook.get f_xml_end_module) mp; mp let declare_module interp_modast id args res mexpr_o fs = @@ -682,7 +669,6 @@ let declare_module interp_modast id args res mexpr_o fs = let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in ignore (Lib.add_leaf id (in_module sobjs)); - if_xml (Hook.get f_xml_declare_module) mp; mp end @@ -699,7 +685,6 @@ let start_modtype interp_modast id args mtys fs = openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - if_xml (Hook.get f_xml_start_module_type) mp; mp let end_modtype () = @@ -716,7 +701,6 @@ let end_modtype () = assert (eq_full_path (fst oname) (fst oldoname)); assert (ModPath.equal (mp_of_kn (snd oname)) mp); - if_xml (Hook.get f_xml_end_module_type) mp; mp let declare_modtype interp_modast id args mtys (mty,ann) fs = @@ -750,7 +734,6 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = check_subtypes_mt mp sub_mty_l; ignore (Lib.add_leaf id (in_modtype sobjs)); - if_xml (Hook.get f_xml_declare_module_type) mp; mp end diff --git a/library/declaremods.mli b/library/declaremods.mli index 005594b8d..9d750b616 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -63,14 +63,6 @@ val start_modtype : val end_modtype : unit -> module_path -(** Hooks for XML output *) -val xml_declare_module : (module_path -> unit) Hook.t -val xml_start_module : (module_path -> unit) Hook.t -val xml_end_module : (module_path -> unit) Hook.t -val xml_declare_module_type : (module_path -> unit) Hook.t -val xml_start_module_type : (module_path -> unit) Hook.t -val xml_end_module_type : (module_path -> unit) Hook.t - (** {6 Libraries i.e. modules on disk } *) type library_name = DirPath.t diff --git a/library/lib.ml b/library/lib.ml index a24d20c68..c6a0253b3 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -512,11 +512,6 @@ let is_in_section ref = (*************) (* Sections. *) - -(* XML output hooks *) -let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore () -let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore () - let open_section id = let olddir,(mp,oldsec) = !lib_state.path_prefix in let dir = add_dirpath_suffix olddir id in @@ -528,7 +523,6 @@ let open_section id = (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); lib_state := { !lib_state with path_prefix = prefix }; - if !Flags.xml_export then Hook.get f_xml_open_section id; add_section () @@ -556,7 +550,6 @@ let close_section () = let full_olddir = fst !lib_state.path_prefix in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); - if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname)); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; diff --git a/library/lib.mli b/library/lib.mli index f1c9bfca2..3dcec1d53 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -150,10 +150,6 @@ val unfreeze : frozen -> unit val init : unit -> unit -(** XML output hooks *) -val xml_open_section : (Names.Id.t -> unit) Hook.t -val xml_close_section : (Names.Id.t -> unit) Hook.t - (** {6 Section management for discharge } *) type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list @@ -165,7 +161,7 @@ val named_of_variable_context : variable_context -> Context.Named.t val section_segment_of_constant : Names.constant -> abstr_info val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info val variable_section_segment_of_reference : Globnames.global_reference -> variable_context - + val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool diff --git a/library/library.ml b/library/library.ml index 20ecc2c22..28afa054e 100644 --- a/library/library.ml +++ b/library/library.ml @@ -551,8 +551,6 @@ let in_require : require_obj -> obj = (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) -let (f_xml_require, xml_require) = Hook.make ~default:ignore () - let warn_require_in_module = CWarnings.create ~name:"require-in-module" ~category:"deprecated" (fun () -> strbrk "Require inside a module is" ++ @@ -574,7 +572,6 @@ let require_library_from_dirpath modrefl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); - if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl; () (* the function called by Vernacentries.vernac_import *) diff --git a/library/library.mli b/library/library.mli index 604167804..6c624ce52 100644 --- a/library/library.mli +++ b/library/library.mli @@ -67,9 +67,6 @@ val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit -(** {6 Hook for the xml exportation of libraries } *) -val xml_require : (DirPath.t -> unit) Hook.t - (** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound diff --git a/man/coqide.1 b/man/coqide.1 index f82bf2ad4..3592f6e4e 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -123,13 +123,6 @@ Set sort Set impredicative. .TP .B \-dont\-load\-proofs Don't load opaque proofs in memory. -.TP -.B \-xml -Export XML files either to the hierarchy rooted in -the directory -.B COQ_XML_LIBRARY_ROOT -(if set) or to stdout (if unset). - .SH SEE ALSO diff --git a/man/coqtop.1 b/man/coqtop.1 index feee7fd8b..62d17aa67 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -153,12 +153,6 @@ set sort Set impredicative .B \-dont\-load\-proofs don't load opaque proofs in memory -.TP -.B \-xml -export XML files either to the hierarchy rooted in -the directory $COQ_XML_LIBRARY_ROOT (if set) or to -stdout (if unset) - .SH SEE ALSO .BR coqc (1), diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 5fcbb43b6..636027f9b 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -368,9 +368,6 @@ let rec string loc ~comm_level bp len = parser let loc = set_loc_pos loc bp ep in err loc Unterminated_string -(* Hook for exporting comment into xml theory files *) -let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () - (* To associate locations to a file name *) let current_file = ref None @@ -432,9 +429,6 @@ let null_comment s = let comment_stop ep = let current_s = Buffer.contents current_comment in - if !Flags.xml_export && Buffer.length current_comment > 0 && - (!between_commands || not(null_comment current_s)) then - Hook.get f_xml_output_comment current_s; (if !Flags.beautify && Buffer.length current_comment > 0 && (!between_commands || not(null_comment current_s)) then let bp = match !comment_begin with diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 09c9d8ee4..77d652b18 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -19,9 +19,6 @@ val get_keyword_state : unit -> keyword_state val check_ident : string -> unit val is_ident : string -> bool val check_keyword : string -> unit - -val xml_output_comment : (string -> unit) Hook.t - val terminal : string -> Tok.t (** The lexer of Coq: *) diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v index 39a7103d1..40abb215e 100644 --- a/test-suite/bugs/closed/HoTT_coq_032.v +++ b/test-suite/bugs/closed/HoTT_coq_032.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-xml") -*- *) Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. diff --git a/tools/beautify-archive b/tools/beautify-archive index 6bfa974a5..a327ea44e 100755 --- a/tools/beautify-archive +++ b/tools/beautify-archive @@ -23,7 +23,7 @@ cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE cd $NEWARCHIVE rm description || true make clean -make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ +make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS)' || \ { echo ---- Failed to beautify; exit 1; } echo -------- Upgrading files in the beautification directory -------------- beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX` diff --git a/tools/check-translate b/tools/check-translate index 3dd824053..acb6f4590 100755 --- a/tools/check-translate +++ b/tools/check-translate @@ -2,7 +2,7 @@ echo -------------- Producing translated files --------------------- rm */*/*.v8 >& /dev/null -make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; } +make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; } if [ -e translated ]; then rm -r translated; fi if [ -e successful-translation ]; then rm -r successful-translation; fi if [ -e failed-translation ]; then rm -r failed-translation; fi diff --git a/tools/coqc.ml b/tools/coqc.ml index 4595af6e8..862225d3d 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -94,7 +94,7 @@ let parse_args () = | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet" - |"-silent"|"-m"|"-xml"|"-beautify"|"-strict-implicit" + |"-silent"|"-m"|"-beautify"|"-strict-implicit" |"-impredicative-set"|"-vm"|"-native-compiler" |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8fe27b3b9..ba6d4b05b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -585,7 +585,6 @@ let parse_args arglist = |"-v"|"--version" -> Usage.version (exitcode ()) |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ()) |"-where" -> print_where := true - |"-xml" -> Flags.xml_export := true (* Unknown option *) | s -> extras := s :: !extras diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 962bb4302..d596e36f3 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -78,9 +78,6 @@ let print_usage_channel co command = \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ -\n -xml export XML files either to the hierarchy rooted in\ -\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ -\n stdout (if unset)\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index fe853c093..bfab44770 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -243,10 +243,6 @@ let process_expr sid loc_ast = checknav_deep loc_ast; interp_vernac sid loc_ast -(* XML output hooks *) -let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () -let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore () - let warn_file_no_extension = CWarnings.create ~name:"file-no-extension" ~category:"filesystem" (fun (f,ext) -> @@ -308,7 +304,6 @@ let compile verbosely f = ~v_file:long_f_dot_v); Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); - if !Flags.xml_export then Hook.get f_xml_start_library (); let wall_clock1 = Unix.gettimeofday () in let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.join (); @@ -318,7 +313,6 @@ let compile verbosely f = Aux_file.record_in_aux_at "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); - if !Flags.xml_export then Hook.get f_xml_end_library (); Dumpglob.end_dump_glob () | BuildVio -> let long_f_dot_v = ensure_v f in diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 77c4f44e1..bccf560e1 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -21,7 +21,3 @@ val load_vernac : bool -> Stateid.t -> string -> Stateid.t (** Compile a vernac file, (f is assumed without .v suffix) *) val compile : bool -> string -> unit - -(** Set XML hooks *) -val xml_start_library : (unit -> unit) Hook.t -val xml_end_library : (unit -> unit) Hook.t -- cgit v1.2.3