diff options
| -rw-r--r-- | Makefile.build | 12 | ||||
| -rw-r--r-- | doc/tools/Translator.tex | 2 | ||||
| -rw-r--r-- | interp/declare.ml | 15 | ||||
| -rw-r--r-- | interp/declare.mli | 5 | ||||
| -rw-r--r-- | lib/flags.ml | 3 | ||||
| -rw-r--r-- | lib/flags.mli | 5 | ||||
| -rw-r--r-- | library/declaremods.ml | 17 | ||||
| -rw-r--r-- | library/declaremods.mli | 8 | ||||
| -rw-r--r-- | library/lib.ml | 7 | ||||
| -rw-r--r-- | library/lib.mli | 6 | ||||
| -rw-r--r-- | library/library.ml | 3 | ||||
| -rw-r--r-- | library/library.mli | 3 | ||||
| -rw-r--r-- | man/coqide.1 | 7 | ||||
| -rw-r--r-- | man/coqtop.1 | 6 | ||||
| -rw-r--r-- | parsing/cLexer.ml4 | 6 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_032.v | 1 | ||||
| -rwxr-xr-x | tools/beautify-archive | 2 | ||||
| -rwxr-xr-x | tools/check-translate | 2 | ||||
| -rw-r--r-- | tools/coqc.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 6 | ||||
| -rw-r--r-- | 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 |