From 592151e323036f0044a0ac285b8b13c964825989 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Sep 2015 14:06:38 +0200 Subject: Fixing bug #4347: Not_found Exception with some Records. A term was reduced in an improper environment. --- pretyping/evarutil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index ee6bbe7fbe..8ebb037c24 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -757,7 +757,7 @@ let define_evar_as_product evd (evk,args) = let define_pure_evar_as_lambda env evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let typ = whd_betadeltaiota env evd (evar_concl evi) in + let typ = whd_betadeltaiota evenv evd (evar_concl evi) in let evd1,(na,dom,rng) = match kind_of_term typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ -- cgit v1.2.3 From 802f3a5c313c8ef98109a3f29c3c862de63bd53c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Sep 2015 14:17:45 +0200 Subject: Test for bug #4347. --- test-suite/bugs/closed/4347.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 test-suite/bugs/closed/4347.v diff --git a/test-suite/bugs/closed/4347.v b/test-suite/bugs/closed/4347.v new file mode 100644 index 0000000000..29686a26c1 --- /dev/null +++ b/test-suite/bugs/closed/4347.v @@ -0,0 +1,17 @@ +Fixpoint demo_recursion(n:nat) := match n with + |0 => Type + |S k => (demo_recursion k) -> Type + end. + +Record Demonstration := mkDemo +{ + demo_law : forall n:nat, demo_recursion n; + demo_stuff : forall n:nat, forall q:(fix demo_recursion (n : nat) : Type := + match n with + | 0 => Type + | S k => demo_recursion k -> Type + end) n, (demo_law (S n)) q +}. + +Theorem DemoError : Demonstration. +Fail apply mkDemo. (*Anomaly: Uncaught exception Not_found. Please report.*) -- cgit v1.2.3 From 5481ff4f6935874ac3798a61f5a2a810006bde37 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Sep 2015 15:00:33 +0200 Subject: Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015. --- doc/refman/coqdoc.tex | 14 ++++++++------ tools/coqdoc/main.ml | 4 ++-- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index ee2b042f4e..30467a5e6e 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -285,7 +285,7 @@ suffix \verb!.tex!. Select a \texmacs\ output. -\item[\texttt{--stdout}] ~\par +\item[\texttt{\mm{}stdout}] ~\par Write output to stdout. @@ -496,14 +496,16 @@ Default behavior is to assume ASCII 7 bits input files. \item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par Select ISO-8859-1 input files. It is equivalent to - \texttt{--inputenc latin1 --charset iso-8859-1}. + \texttt{\mm{}inputenc latin1 \mm{}charset iso-8859-1}. \item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par - Select UTF-8 (Unicode) input files. It is equivalent to - \texttt{--inputenc utf8 --charset utf-8}. - \LaTeX\ UTF-8 support can be found at - \url{http://www.ctan.org/pkg/unicode}. + Set \texttt{\mm{}inputenc utf8x} for \LaTeX\ output and + \texttt{\mm{}charset utf-8} for HTML output. Also use Unicode + replacements for a couple of standard plain ASCII notations such + as $\rightarrow$ for \texttt{->} and $\forall$ for + \texttt{forall}. \LaTeX\ UTF-8 support can be found at + \url{http://www.ctan.org/pkg/unicode}. \item[\texttt{\mm{}inputenc} \textit{string}] ~\par diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 2554ed495b..22febd6a64 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -61,8 +61,8 @@ let usage () = prerr_endline " --coqlib_path set the path where Coq files are installed"; prerr_endline " -R map physical dir to Coq dir"; prerr_endline " -Q map physical dir to Coq dir"; - prerr_endline " --latin1 set ISO-8859-1 input language"; - prerr_endline " --utf8 set UTF-8 input language"; + prerr_endline " --latin1 set ISO-8859-1 mode"; + prerr_endline " --utf8 set UTF-8 mode"; prerr_endline " --charset set HTML charset"; prerr_endline " --inputenc set LaTeX input encoding"; prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module"; -- cgit v1.2.3 From 4b88d774729e0ab7916730e8e6ebedc2033a87f2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 26 Sep 2015 16:31:29 +0200 Subject: Documenting how to support some special unicode characters in coqdoc (thanks to coq-club, Sep 2015). --- doc/refman/coqdoc.tex | 9 +++++++++ tools/coqdoc/output.ml | 7 +++++-- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index 30467a5e6e..26dbd59e76 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -507,6 +507,15 @@ Default behavior is to assume ASCII 7 bits input files. \texttt{forall}. \LaTeX\ UTF-8 support can be found at \url{http://www.ctan.org/pkg/unicode}. + For the interpretation of Unicode characters by \LaTeX, extra + packages which {\coqdoc} does not provide by default might be + required, such as \texttt{textgreek} for some Greek letters or + \texttt{stmaryrd} for some mathematical symbols. If a Unicode + character is missing an interpretation in the \texttt{utf8x} input + encoding, add + \verb=\DeclareUnicodeCharacter{=\textit{code}\verb=}{=\textit{latex-interpretation}\verb=}=. Packages + and declarations can be added with option \texttt{-p}. + \item[\texttt{\mm{}inputenc} \textit{string}] ~\par Give a \LaTeX\ input encoding, as an option to \LaTeX\ package diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 06030c45a6..8589f94a01 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -197,8 +197,11 @@ module Latex = struct printf "\n"; printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n"; printf "%%interpret utf8 characters but extra packages might have to be added\n"; - printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n"; - printf "%%Use coqdoc's option -p to add new packages.\n"; + printf "%%such as \"textgreek\" for Greek letters not already in tipa\n"; + printf "%%or \"stmaryrd\" for mathematical symbols.\n"; + printf "%%Utf8 codes missing a LaTeX interpretation can be defined by using\n"; + printf "%%\\DeclareUnicodeCharacter{code}{interpretation}.\n"; + printf "%%Use coqdoc's option -p to add new packages or declarations.\n"; printf "\\usepackage{tipa}\n"; printf "\n" -- cgit v1.2.3 From b6d5a9f47634371aa18c6e3159c6bc24203d229f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Sep 2015 14:22:29 +0200 Subject: Fixing loss of extra data in Evd. --- pretyping/evd.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fc4f5e040e..6326112912 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1385,7 +1385,7 @@ let set_metas evd metas = { evar_names = evd.evar_names; future_goals = evd.future_goals; principal_future_goal = evd.principal_future_goal; - extras = Store.empty; + extras = evd.extras; } let meta_list evd = metamap_to_list evd.metas -- cgit v1.2.3 From 2cf609c41f7af83d9eaf43308a368fcb7307e6fa Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 28 Sep 2015 11:04:59 +0200 Subject: Make -load-vernac-object respect the loadpath. This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq. --- CHANGES | 5 +++-- doc/refman/RefMan-com.tex | 4 ++-- library/library.ml | 34 ---------------------------------- library/library.mli | 1 - man/coqide.1 | 8 +++++--- man/coqtop.1 | 7 ++++--- toplevel/coqtop.ml | 4 ++-- 7 files changed, 16 insertions(+), 47 deletions(-) diff --git a/CHANGES b/CHANGES index 950f2fab18..16d86c8ff1 100644 --- a/CHANGES +++ b/CHANGES @@ -54,8 +54,9 @@ Tools - The -compile command-line option now takes the full path of the considered file, including the ".v" extension, and outputs a warning if such an extension is lacking. -- The -require command-line option now takes a logical path of a given library - rather than a physical path. +- The -require and -load-vernac-object command-line options now take a logical + path of a given library rather than a physical path, thus they behave like + Require [Import] path. Changes from V8.5beta1 to V8.5beta2 =================================== diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 0f1823a021..9862abb533 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -153,9 +153,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath. Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the standard input. -\item[{\tt -load-vernac-object} {\em file}]\ +\item[{\tt -load-vernac-object} {\em path}]\ - Load \Coq~compiled file {\em file}{\tt .vo} + Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}). \item[{\tt -require} {\em path}]\ diff --git a/library/library.ml b/library/library.ml index a09f91b15a..6d7b0f603a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,33 +488,11 @@ let rec_intern_library libs mref = let _, libs = intern_library libs mref None in libs -let rec_intern_by_filename_only f = - let m = try intern_from_file f with Sys_error s -> error s in - (* We check no other file containing same library is loaded *) - if library_is_loaded m.library_name then - begin - msg_warning - (pr_dirpath m.library_name ++ str " is already loaded from file " ++ - str (library_full_filename m.library_name)); - m.library_name, [] - end - else - let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in - let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in - m.library_name, needed - let native_name_from_filename f = let ch = System.with_magic_number_check raw_intern_library f in let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name -let rec_intern_library_from_file f = - (* A name is specified, we have to check it contains library id *) - let paths = Loadpath.get_paths () in - let _, f = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in - rec_intern_by_filename_only f - (**********************************************************************) (*s [require_library] loads and possibly opens a library. This is a synchronized operation. It is performed as follows: @@ -590,18 +568,6 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library_from_file file export = - let modref,needed = rec_intern_library_from_file file in - let needed = List.rev_map snd needed in - if Lib.is_module_or_modtype () then begin - add_anonymous_leaf (in_require (needed,[modref],None)); - Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp))) - export - end - else - add_anonymous_leaf (in_require (needed,[modref],export)); - add_frozen_state () - (* the function called by Vernacentries.vernac_import *) let safe_locate_module (loc,qid) = diff --git a/library/library.mli b/library/library.mli index 3d96f9a751..d5e610dd67 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,7 +22,6 @@ open Libnames (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit -val require_library_from_file : CUnix.physical_path -> bool option -> unit (** {6 Start the compilation of a library } *) diff --git a/man/coqide.1 b/man/coqide.1 index cfd9c3b4a2..6a3e67ad53 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -63,9 +63,11 @@ Load Coq file (Load Verbose .IR f .). .TP -.BI \-load\-vernac\-object\ f -Load Coq object file -.IR f .vo. +.BI \-load\-vernac\-object\ path +Load Coq library +.IR path +(Require +.IR path .). .TP .BI \-require\ path Load Coq library diff --git a/man/coqtop.1 b/man/coqtop.1 index e079bee39b..62d17aa674 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -73,9 +73,10 @@ load verbosely Coq file (Load Verbose filename.) .TP -.BI \-load\-vernac\-object \ filename -load Coq object file -.I filename.vo +.BI \-load\-vernac\-object \ path +load Coq library +.I path +(Require path.) .TP .BI \-require \ path diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 32ac9a496d..b7f1e4a197 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -171,8 +171,8 @@ let load_vernacular () = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj let load_vernac_obj () = - List.iter (fun f -> Library.require_library_from_file f None) - (List.rev !load_vernacular_obj) + let map dir = Qualid (Loc.ghost, qualid_of_string dir) in + Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj) let require_prelude () = let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in -- cgit v1.2.3 From da4d0b0e3d82621fe8338dd313b788472fc31bb2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 10:26:08 +0200 Subject: Remove some uses of Loadpath.get_paths. The single remaining use is in library/states.ml. This use should be reviewed, as it is most certainly broken. The other uses of Loadpath.get_paths did not disappear by miracle though. They were replaced by a new function Loadpath.locate_file which factors all the uses of the function. This function should not be used as it is as broken as Loadpath.get_paths, by definition. Vernac.load_vernac now takes a complete path rather than looking up for the file. That is the way it was used most of the time, so the lookup was unnecessary. For instance, Vernac.compile was calling Library.start_library which already expected a complete path. Another consequence is that System.find_file_in_path is almost no longer used (except for Loadpath.locate_file, obviously). The two remaining uses are System.intern_state (used by States.intern_state, cf above) and Mltop.dir_ml_load for dynamically loading compiled .ml files. --- library/library.ml | 4 +--- library/loadpath.ml | 6 ++++++ library/loadpath.mli | 4 ++++ stm/vio_checking.ml | 4 +--- toplevel/coqtop.ml | 1 + toplevel/vernac.ml | 13 ++++--------- toplevel/vernacentries.ml | 7 ++----- 7 files changed, 19 insertions(+), 20 deletions(-) diff --git a/library/library.ml b/library/library.ml index 6d7b0f603a..f5c7f63358 100644 --- a/library/library.ml +++ b/library/library.ml @@ -652,9 +652,7 @@ let start_library f = ldir let load_library_todo f = - let paths = Loadpath.get_paths () in - let _, longf = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let longf = Loadpath.locate_file (f^".v") in let f = longf^"io" in let ch = System.with_magic_number_check raw_intern_library f in let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in diff --git a/library/loadpath.ml b/library/loadpath.ml index 26af809e78..d35dca2125 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -112,3 +112,9 @@ let expand_path dir = if DirPath.equal dir lg then (ph, lg) :: aux l else aux l in aux !load_paths + +let locate_file fname = + let paths = get_paths () in + let _,longfname = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + longfname diff --git a/library/loadpath.mli b/library/loadpath.mli index 3251b8c60c..c2c689af70 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -52,3 +52,7 @@ val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list (** As {!expand_path} but uses a filter function instead, and ignores the implicit status of loadpaths. *) + +val locate_file : string -> string +(** Locate a file among the registered paths. Do not use this function, as + it does not respect the visibility of paths. *) diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 4df9603dca..06bf955c82 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -104,9 +104,7 @@ let schedule_vio_compilation j fs = let f = if Filename.check_suffix f ".vio" then Filename.chop_extension f else f in - let paths = Loadpath.get_paths () in - let _, long_f_dot_v = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let long_f_dot_v = Loadpath.locate_file (f^".v") in let aux = Aux_file.load_aux_file_for long_f_dot_v in let eta = try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time") diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b7f1e4a197..4031a161b8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -162,6 +162,7 @@ let add_load_vernacular verb s = let load_vernacular () = List.iter (fun (s,b) -> + let s = Loadpath.locate_file s in if Flags.do_beautify () then with_option beautify_file (Vernac.load_vernac b) s else diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 14d2bcea41..a0cd618e99 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -97,10 +97,7 @@ let user_error loc s = Errors.user_err_loc (loc,"_",str s) Note: we could use only one thanks to seek_in, but seeking on and on in the file we parse seems a bit risky to me. B.B. *) -let open_file_twice_if verbosely fname = - let paths = Loadpath.get_paths () in - let _,longfname = - find_file_in_path ~warn:(Flags.is_verbose()) paths fname in +let open_file_twice_if verbosely longfname = let in_chan = open_utf8_file_in longfname in let verb_ch = if verbosely then Some (open_utf8_file_in longfname) else None in @@ -206,19 +203,17 @@ let rec vernac_com verbose checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in + let fname = CUnix.make_suffix fname ".v" in + let f = Loadpath.locate_file fname in let st = save_translator_coqdoc () in if !Flags.beautify_file then begin - let paths = Loadpath.get_paths () in - let _,f = find_file_in_path ~warn:(Flags.is_verbose()) - paths - (CUnix.make_suffix fname ".v") in chan_beautify := open_out (f^beautify_suffix); Pp.comments := [] end; begin try - read_vernac_file verbosely (CUnix.make_suffix fname ".v"); + read_vernac_file verbosely f; restore_translator_coqdoc st; with reraise -> let reraise = Errors.push reraise in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8efcccaaae..ec81a3f1ae 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -365,8 +365,7 @@ let dump_universes sorted s = (* "Locate" commands *) let locate_file f = - let paths = Loadpath.get_paths () in - let _, file = System.find_file_in_path ~warn:false paths f in + let file = Flags.silently Loadpath.locate_file f in str file let msg_found_library = function @@ -1845,9 +1844,7 @@ let vernac_load interp fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let input = - let paths = Loadpath.get_paths () in - let _,longfname = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in Pcoq.Gram.parsable (Stream.of_channel in_chan) in try while true do interp (snd (parse_sentence input)) done -- cgit v1.2.3 From 82a618e8a4945752698a7900c8af7a51091f7b1b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:05:45 +0200 Subject: Prevent States.intern_state and System.extern_intern from looking up files in the loadpath. This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner. --- lib/system.ml | 11 +++++------ lib/system.mli | 6 +++--- library/library.ml | 6 ++++-- library/states.ml | 6 +----- toplevel/coqtop.ml | 10 ++++++++-- toplevel/vernacentries.ml | 2 ++ 6 files changed, 23 insertions(+), 18 deletions(-) diff --git a/lib/system.ml b/lib/system.ml index d1cdd8efc9..139effd9fa 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -178,7 +178,7 @@ let raw_extern_intern magic = let extern_state filename = let channel = open_trapping_failure filename in output_binary_int channel magic; - filename, channel + channel and intern_state filename = try let channel = open_in_bin filename in @@ -191,11 +191,11 @@ let raw_extern_intern magic = in (extern_state,intern_state) -let extern_intern ?(warn=true) magic = +let extern_intern magic = let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state name val_0 = + let extern_state filename val_0 = try - let (filename,channel) = raw_extern name in + let channel = raw_extern filename in try marshal_out channel val_0; close_out channel @@ -205,9 +205,8 @@ let extern_intern ?(warn=true) magic = iraise reraise with Sys_error s -> errorlabstrm "System.extern_state" (str "System error: " ++ str s) - and intern_state paths name = + and intern_state filename = try - let _,filename = find_file_in_path ~warn paths name in let channel = raw_intern filename in let v = marshal_in filename channel in close_in channel; diff --git a/lib/system.mli b/lib/system.mli index a3d66d577a..5797502e9f 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -37,10 +37,10 @@ val find_file_in_path : exception Bad_magic_number of string val raw_extern_intern : int -> - (string -> string * out_channel) * (string -> in_channel) + (string -> out_channel) * (string -> in_channel) -val extern_intern : ?warn:bool -> int -> - (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a) +val extern_intern : int -> + (string -> 'a -> unit) * (string -> 'a) val with_magic_number_check : ('a -> 'b) -> 'a -> 'b diff --git a/library/library.ml b/library/library.ml index f5c7f63358..0fb938e9b6 100644 --- a/library/library.ml +++ b/library/library.ml @@ -742,7 +742,8 @@ let save_library_to ?todo dir f otab = if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then error_recursively_dependent_library dir; (* Open the vo file and write the magic number *) - let (f',ch) = raw_extern_library f in + let f' = f in + let ch = raw_extern_library f' in try (* Writing vo payload *) System.marshal_out_segment f' ch (sd : seg_sum); @@ -765,7 +766,8 @@ let save_library_to ?todo dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let (f',ch) = raw_extern_library (f^"o") in + let f' = f^".o" in + let ch = raw_extern_library f' in System.marshal_out_segment f' ch (sum : seg_sum); System.marshal_out_segment f' ch (lib : seg_lib); System.marshal_out_segment f' ch (Some univs : seg_univ option); diff --git a/library/states.ml b/library/states.ml index 96a487b160..4e55f0cdc6 100644 --- a/library/states.ml +++ b/library/states.ml @@ -22,16 +22,12 @@ let unfreeze (fl,fs) = Summary.unfreeze_summaries fs let (extern_state,intern_state) = - let ensure_suffix f = CUnix.make_suffix f ".coq" in let (raw_extern, raw_intern) = extern_intern Coq_config.state_magic_number in (fun s -> - let s = ensure_suffix s in raw_extern s (freeze ~marshallable:`Yes)), (fun s -> - let s = ensure_suffix s in - let paths = Loadpath.get_paths () in - unfreeze (with_magic_number_check (raw_intern paths) s); + unfreeze (with_magic_number_check raw_intern s); Library.overwrite_library_filenames s) (* Rollback. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4031a161b8..7562c29f70 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -144,13 +144,19 @@ let inputstate = ref "" let set_inputstate s = let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in inputstate:=s -let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate +let inputstate () = + if not (String.is_empty !inputstate) then + let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in + intern_state fname let outputstate = ref "" let set_outputstate s = let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in outputstate:=s -let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate +let outputstate () = + if not (String.is_empty !outputstate) then + let fname = CUnix.make_suffix !outputstate ".coq" in + extern_state fname let set_include d p implicit = let p = dirpath_of_string p in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index ec81a3f1ae..8ae6ac2bc3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -929,10 +929,12 @@ let vernac_chdir = function let vernac_write_state file = Pfedit.delete_all_proofs (); + let file = CUnix.make_suffix file ".coq" in States.extern_state file let vernac_restore_state file = Pfedit.delete_all_proofs (); + let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in States.intern_state file (************) -- cgit v1.2.3 From 05ab666a1283de5500dbc0520d18bdb05d95f286 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:45:27 +0200 Subject: Make the interface of System.raw_extern_intern much saner. There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures. --- checker/check.ml | 18 +++----------- lib/system.ml | 71 +++++++++++++++++++++++++----------------------------- lib/system.mli | 10 +++++--- library/library.ml | 16 ++++++------ library/states.ml | 14 +++++------ 5 files changed, 58 insertions(+), 71 deletions(-) diff --git a/checker/check.ml b/checker/check.ml index c835cec824..2bc470aead 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -271,20 +271,10 @@ let try_locate_qualified_library qid = | LibNotFound -> error_lib_not_found qid (************************************************************************) -(*s Low-level interning/externing of libraries to files *) +(*s Low-level interning of libraries from files *) -(*s Loading from disk to cache (preparation phase) *) - -let raw_intern_library = - snd (System.raw_extern_intern Coq_config.vo_magic_number) - -let with_magic_number_check f a = - try f a - with System.Bad_magic_number fname -> - errorlabstrm "with_magic_number_check" - (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ - spc () ++ str"It is corrupted" ++ spc () ++ - str"or was compiled with another version of Coq.") +let raw_intern_library f = + System.raw_intern_state Coq_config.vo_magic_number f (************************************************************************) (* Internalise libraries *) @@ -312,7 +302,7 @@ let intern_from_file (dir, f) = Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); let (sd,md,table,opaque_csts,digest) = try - let ch = with_magic_number_check raw_intern_library f in + let ch = System.with_magic_number_check raw_intern_library f in let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in diff --git a/lib/system.ml b/lib/system.ml index 139effd9fa..ddc56956c5 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -174,47 +174,42 @@ let skip_in_segment f ch = exception Bad_magic_number of string -let raw_extern_intern magic = - let extern_state filename = - let channel = open_trapping_failure filename in - output_binary_int channel magic; +let raw_extern_state magic filename = + let channel = open_trapping_failure filename in + output_binary_int channel magic; + channel + +let raw_intern_state magic filename = + try + let channel = open_in_bin filename in + if not (Int.equal (input_binary_int filename channel) magic) then + raise (Bad_magic_number filename); channel - and intern_state filename = - try - let channel = open_in_bin filename in - if not (Int.equal (input_binary_int filename channel) magic) then - raise (Bad_magic_number filename); - channel - with - | End_of_file -> error_corrupted filename "premature end of file" - | Failure s | Sys_error s -> error_corrupted filename s - in - (extern_state,intern_state) + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s | Sys_error s -> error_corrupted filename s -let extern_intern magic = - let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state filename val_0 = - try - let channel = raw_extern filename in - try - marshal_out channel val_0; - close_out channel - with reraise -> - let reraise = Errors.push reraise in - let () = try_remove filename in - iraise reraise - with Sys_error s -> - errorlabstrm "System.extern_state" (str "System error: " ++ str s) - and intern_state filename = +let extern_state magic filename val_0 = + try + let channel = raw_extern_state magic filename in try - let channel = raw_intern filename in - let v = marshal_in filename channel in - close_in channel; - v - with Sys_error s -> - errorlabstrm "System.intern_state" (str "System error: " ++ str s) - in - (extern_state,intern_state) + marshal_out channel val_0; + close_out channel + with reraise -> + let reraise = Errors.push reraise in + let () = try_remove filename in + iraise reraise + with Sys_error s -> + errorlabstrm "System.extern_state" (str "System error: " ++ str s) + +let intern_state magic filename = + try + let channel = raw_intern_state magic filename in + let v = marshal_in filename channel in + close_in channel; + v + with Sys_error s -> + errorlabstrm "System.intern_state" (str "System error: " ++ str s) let with_magic_number_check f a = try f a diff --git a/lib/system.mli b/lib/system.mli index 5797502e9f..247d528b97 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -36,11 +36,13 @@ val find_file_in_path : exception Bad_magic_number of string -val raw_extern_intern : int -> - (string -> out_channel) * (string -> in_channel) +val raw_extern_state : int -> string -> out_channel -val extern_intern : int -> - (string -> 'a -> unit) * (string -> 'a) +val raw_intern_state : int -> string -> in_channel + +val extern_state : int -> string -> 'a -> unit + +val intern_state : int -> string -> 'a val with_magic_number_check : ('a -> 'b) -> 'a -> 'b diff --git a/library/library.ml b/library/library.ml index 0fb938e9b6..6da9ccf68b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -19,10 +19,12 @@ open Lib (************************************************************************) (*s Low-level interning/externing of libraries to files *) -(*s Loading from disk to cache (preparation phase) *) +let raw_extern_library f = + System.raw_extern_state Coq_config.vo_magic_number f -let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern Coq_config.vo_magic_number +let raw_intern_library f = + System.with_magic_number_check + (System.raw_intern_state Coq_config.vo_magic_number) f (************************************************************************) (** Serialized objects loaded on-the-fly *) @@ -56,7 +58,7 @@ let in_delayed f ch = let fetch_delayed del = let { del_digest = digest; del_file = f; del_off = pos; } = del in try - let ch = System.with_magic_number_check raw_intern_library f in + let ch = raw_intern_library f in let () = seek_in ch pos in let obj, _, digest' = System.marshal_in_segment f ch in let () = close_in ch in @@ -434,7 +436,7 @@ let mk_summary m = { } let intern_from_file f = - let ch = System.with_magic_number_check raw_intern_library f in + let ch = raw_intern_library f in let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in let (lmd : seg_lib delayed) = in_delayed f ch in let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in @@ -489,7 +491,7 @@ let rec_intern_library libs mref = libs let native_name_from_filename f = - let ch = System.with_magic_number_check raw_intern_library f in + let ch = raw_intern_library f in let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name @@ -654,7 +656,7 @@ let start_library f = let load_library_todo f = let longf = Loadpath.locate_file (f^".v") in let f = longf^"io" in - let ch = System.with_magic_number_check raw_intern_library f in + let ch = raw_intern_library f in let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in diff --git a/library/states.ml b/library/states.ml index 4e55f0cdc6..3cb6da12ec 100644 --- a/library/states.ml +++ b/library/states.ml @@ -21,14 +21,12 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let (extern_state,intern_state) = - let (raw_extern, raw_intern) = - extern_intern Coq_config.state_magic_number in - (fun s -> - raw_extern s (freeze ~marshallable:`Yes)), - (fun s -> - unfreeze (with_magic_number_check raw_intern s); - Library.overwrite_library_filenames s) +let extern_state s = + System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes) + +let intern_state s = + unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); + Library.overwrite_library_filenames s (* Rollback. *) -- cgit v1.2.3 From 99918c8a8cfb4285798a70351673be2679a6e819 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 21:27:26 +0200 Subject: Fix dumb typo. --- library/library.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/library.ml b/library/library.ml index 6da9ccf68b..024ac9e6fa 100644 --- a/library/library.ml +++ b/library/library.ml @@ -768,7 +768,7 @@ let save_library_to ?todo dir f otab = iraise reraise let save_library_raw f sum lib univs proofs = - let f' = f^".o" in + let f' = f^"o" in let ch = raw_extern_library f' in System.marshal_out_segment f' ch (sum : seg_sum); System.marshal_out_segment f' ch (lib : seg_lib); -- cgit v1.2.3 From b248c23b84a96ef692e4a3ded6668733820e1a77 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 30 Sep 2015 06:52:01 +0200 Subject: Unexport Loadpath.get_paths. --- library/loadpath.ml | 4 +--- library/loadpath.mli | 3 --- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/library/loadpath.ml b/library/loadpath.ml index d35dca2125..622d390a2c 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -28,8 +28,6 @@ let physical p = p.path_physical let get_load_paths () = !load_paths -let get_paths () = List.map physical !load_paths - let anomaly_too_many_paths path = anomaly (str "Several logical paths are associated to" ++ spc () ++ str path) @@ -114,7 +112,7 @@ let expand_path dir = aux !load_paths let locate_file fname = - let paths = get_paths () in + let paths = List.map physical !load_paths in let _,longfname = System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in longfname diff --git a/library/loadpath.mli b/library/loadpath.mli index c2c689af70..269e28e0b5 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -27,9 +27,6 @@ val logical : t -> DirPath.t val get_load_paths : unit -> t list (** Get the current loadpath association. *) -val get_paths : unit -> CUnix.physical_path list -(** Same as [get_load_paths] but only get the physical part. *) - val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit (** [add_load_path phys log type] adds the binding [phys := log] to the current loadpaths. *) -- cgit v1.2.3 From a478947e33bcca34291ec36487876443a694c6bf Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 14 Sep 2015 17:46:52 -0400 Subject: Add compatibility files (feature 4319) --- theories/Compat/Coq84.v | 56 ++++++++++++++++++++++++++++++++++++++++++++++ theories/Compat/Coq85.v | 9 ++++++++ theories/Compat/vo.itarget | 2 ++ theories/theories.itarget | 1 + 4 files changed, 68 insertions(+) create mode 100644 theories/Compat/Coq84.v create mode 100644 theories/Compat/Coq85.v create mode 100644 theories/Compat/vo.itarget diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v new file mode 100644 index 0000000000..83016976e8 --- /dev/null +++ b/theories/Compat/Coq84.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* \textbackslash"). You can now execute CoqIDE with the following commands (assuming +Control-\textbackslash). You can now execute CoqIDE with the following commands (assuming you use a Bourne-style shell): \begin{verbatim} @@ -268,7 +271,7 @@ $ export GTK_IM_MODULE=uim $ coqide \end{verbatim} -Activate the ELatin Input Method with Ctrl-\textbackslash, then type the +Activate the ELatin Input Method with Control-\textbackslash, then type the sequence "\verb=\Gamma=". You will see the sequence being replaced by $\Gamma$ as soon as you type the second "a". @@ -286,7 +289,7 @@ detect its character encoding.) If you choose something else than UTF-8, then missing characters will be written encoded by \verb|\x{....}| or \verb|\x{........}| where each dot is an hexadecimal digit: the number between braces is the -hexadecimal UNICODE index for the missing character. +hexadecimal Unicode index for the missing character. %%% Local Variables: -- cgit v1.2.3 From 832ef36c5b066f5cb50a85b9a1450eaf7dcb9e44 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 2 Oct 2015 14:41:29 +0200 Subject: emacs output mode: Added tag to debug messages. So that they display in response buffer. --- lib/pp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/pp.ml b/lib/pp.ml index 30bc30a9ad..1711008ead 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -424,7 +424,7 @@ type logger = message_level -> std_ppcmds -> unit let make_body info s = emacs_quote (hov 0 (info ++ spc () ++ s)) -let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm) +let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm)) let warnbody strm = make_body (str "Warning:") strm let errorbody strm = make_body (str "Error:") strm let infobody strm = emacs_quote_info strm -- cgit v1.2.3 From 88abc50ece70405d71777d5350ca2fa70c1ff437 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 2 Oct 2015 14:41:57 +0200 Subject: Changed status of Info messages from notice to info. This fixes a bug in proofgeneral. PG will now diplay this message eagerly. Otherwise since they appear before the goal, they are considered outdated and not displayed. --- proofs/pfedit.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index ceb4facc1e..05a2975458 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr = let () = match info_lvl with | None -> () - | Some i -> Pp.msg_notice (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) + | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) in (p,status) with -- cgit v1.2.3