From 0168f040e29c3bbaeb666f0b793f41627f154e12 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 28 Nov 2017 18:05:44 +0100 Subject: Adding an interface file for checker/check.ml. --- checker/check.ml | 6 ------ checker/check.mli | 26 ++++++++++++++++++++++++++ 2 files changed, 26 insertions(+), 6 deletions(-) create mode 100644 checker/check.mli diff --git a/checker/check.ml b/checker/check.ml index 180ca1ece1..525c84c2f3 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -412,9 +412,3 @@ let recheck_library ~norec ~admit ~check = (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); List.iter (check_one_lib nochk) needed; Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked") - -open Printf - -let mem s = - let m = try_find_library s in - h 0 (str (sprintf "%dk" (CObj.size_kb m))) diff --git a/checker/check.mli b/checker/check.mli new file mode 100644 index 0000000000..ef87e3efa2 --- /dev/null +++ b/checker/check.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +val recheck_library : + norec:section_path list -> + admit:section_path list -> + check:section_path list -> unit -- cgit v1.2.3 From 45192ccb907349f0ec51c3d2ac577920c4016119 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 28 Nov 2017 20:23:54 +0100 Subject: Allow to pass physical files to coqchk. --- checker/check.ml | 22 ++++++++++++++++------ checker/check.mli | 10 +++++++--- checker/checker.ml | 11 ++++++----- 3 files changed, 29 insertions(+), 14 deletions(-) diff --git a/checker/check.ml b/checker/check.ml index 525c84c2f3..21fdba1faf 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -22,6 +22,11 @@ let extend_dirpath p id = DirPath.make (id :: DirPath.repr p) type section_path = { dirpath : string list ; basename : string } + +type object_file = +| PhysicalFile of CUnix.physical_path +| LogicalFile of section_path + let dir_of_path p = DirPath.make (List.map Id.of_string p.dirpath) let path_of_dirpath dir = @@ -69,11 +74,6 @@ let libraries_table = ref LibraryMap.empty let find_library dir = LibraryMap.find dir !libraries_table -let try_find_library dir = - try find_library dir - with Not_found -> - user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir))) - let library_full_filename dir = (find_library dir).library_filename (* If a library is loaded several time, then the first occurrence must @@ -263,7 +263,17 @@ let try_locate_absolute_library dir = | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir) | LibNotFound -> error_lib_not_found (path_of_dirpath dir) -let try_locate_qualified_library qid = +let try_locate_qualified_library lib = match lib with +| PhysicalFile f -> + let () = + if not (System.file_exists_respecting_case "" f) then + error_lib_not_found { dirpath = []; basename = f; } + in + let dir = Filename.dirname f in + let base = Filename.chop_extension (Filename.basename f) in + let dir = extend_dirpath (find_logical_path dir) (Id.of_string base) in + (dir, f) +| LogicalFile qid -> try locate_qualified_library qid with diff --git a/checker/check.mli b/checker/check.mli index ef87e3efa2..28ae385b5b 100644 --- a/checker/check.mli +++ b/checker/check.mli @@ -14,6 +14,10 @@ type section_path = { basename : string; } +type object_file = +| PhysicalFile of physical_path +| LogicalFile of section_path + type logical_path = DirPath.t val default_root_prefix : DirPath.t @@ -21,6 +25,6 @@ val default_root_prefix : DirPath.t val add_load_path : physical_path * logical_path -> unit val recheck_library : - norec:section_path list -> - admit:section_path list -> - check:section_path list -> unit + norec:object_file list -> + admit:object_file list -> + check:object_file list -> unit diff --git a/checker/checker.ml b/checker/checker.ml index e960a55fd2..b2433ee364 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -40,9 +40,10 @@ let dirpath_of_string s = [] -> Check.default_root_prefix | dir -> DirPath.make (List.map Id.of_string dir) let path_of_string s = - match parse_dir s with + if Filename.check_suffix s ".vo" then PhysicalFile s + else match parse_dir s with [] -> invalid_arg "path_of_string" - | l::dir -> {dirpath=dir; basename=l} + | l::dir -> LogicalFile {dirpath=dir; basename=l} let ( / ) = Filename.concat @@ -144,15 +145,15 @@ let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet let engage () = Safe_typing.set_engagement (!impredicative_set) -let admit_list = ref ([] : section_path list) +let admit_list = ref ([] : object_file list) let add_admit s = admit_list := path_of_string s :: !admit_list -let norec_list = ref ([] : section_path list) +let norec_list = ref ([] : object_file list) let add_norec s = norec_list := path_of_string s :: !norec_list -let compile_list = ref ([] : section_path list) +let compile_list = ref ([] : object_file list) let add_compile s = compile_list := path_of_string s :: !compile_list -- cgit v1.2.3 From 1207d5d018436e70a2ee386cb5644493c02cd983 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 29 Nov 2017 10:58:40 +0100 Subject: Documenting the possibility to pass filenames to coqchk. --- CHANGES | 4 ++++ doc/refman/RefMan-com.tex | 5 +++-- man/coqchk.1 | 2 +- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/CHANGES b/CHANGES index 7a326c589a..f2a46bd24b 100644 --- a/CHANGES +++ b/CHANGES @@ -21,6 +21,10 @@ Tactics - Tactic "decide equality" now able to manage constructors which contain proofs. +Checker + +- The checker now accepts filenames in addition to logical paths. + Changes from 8.7+beta2 to 8.7.0 =============================== diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 8b1fc7c8f3..b4d9f60ebc 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -299,8 +299,9 @@ The following command-line options are recognized by the commands {\tt \section{Compiled libraries checker ({\tt coqchk})} -The {\tt coqchk} command takes a list of library paths as argument. -The corresponding compiled libraries (.vo files) are searched in the +The {\tt coqchk} command takes a list of library paths as argument, described +either by their logical name or by their physical filename, which must end in +{\tt .vo}. The corresponding compiled libraries (.vo files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type-checked. The effect of {\tt coqchk} is only to return with normal exit code in case of success, diff --git a/man/coqchk.1 b/man/coqchk.1 index 76a7cfc5d2..a00914eab8 100644 --- a/man/coqchk.1 +++ b/man/coqchk.1 @@ -23,7 +23,7 @@ library was not found, corrupted content, type-checking failure, etc. .IR modules \& is a list of modules to be checked. Modules can be referred to by a -short or qualified name. +short or qualified logical name, or by their filename. .SH OPTIONS -- cgit v1.2.3 From bbe7b785787ff3f13e5c2809a67241981b06e1db Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 29 Nov 2017 12:05:01 +0100 Subject: coq_makefile: pass filenames to coqchk --- tools/CoqMakefile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 4ee6efec0c..87783350a2 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -392,7 +392,7 @@ checkproofs: .PHONY: checkproofs validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $^ .PHONY: validate only: $(TGTS) -- cgit v1.2.3