diff options
| -rw-r--r-- | Makefile.build | 14 | ||||
| -rw-r--r-- | Makefile.common | 3 | ||||
| -rw-r--r-- | checker/check.mllib | 1 | ||||
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 | ||||
| -rw-r--r-- | lib/minisys.ml | 74 | ||||
| -rw-r--r-- | lib/system.ml | 60 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 6 |
8 files changed, 95 insertions, 65 deletions
diff --git a/Makefile.build b/Makefile.build index 190a62d00..dbf60afb7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -611,6 +611,16 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP) # to avoid using implicit rules and hence .ml.d files that would need # coqdep_boot. +COQDEPBOOTSRC := \ + lib/minisys.ml \ + tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ + tools/coqdep_common.mli tools/coqdep_common.ml \ + tools/coqdep_boot.ml + +$(COQDEPBOOT): $(COQDEPBOOTSRC) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml, -I tools, unix) + OCAMLLIBDEPSRC:= tools/ocamllibdep.ml $(OCAMLLIBDEP): $(OCAMLLIBDEPSRC) @@ -1093,9 +1103,9 @@ dev/%.mllib.d: $(D_DEPEND_BEFORE_SRC) dev/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLL $(SHOW)'OCAMLLIBDEP $<' $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES) +%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) -boot $(DEPNATDYN) "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) $(SHOW)'CCDEP $<' diff --git a/Makefile.common b/Makefile.common index e7d092876..2244e6867 100644 --- a/Makefile.common +++ b/Makefile.common @@ -85,6 +85,7 @@ CHKSRCDIRS:= config lib checker ########################################################################### COQDEP:=bin/coqdep$(EXE) +COQDEPBOOT:=bin/coqdep_boot$(EXE) OCAMLLIBDEP:=bin/ocamllibdep$(EXE) COQMAKEFILE:=bin/coq_makefile$(EXE) GALLINA:=bin/gallina$(EXE) @@ -258,7 +259,7 @@ CSDPCERTCMO:=$(addprefix plugins/micromega/, \ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma -COQDEPCMO:=$(COQENVCMO) lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo +COQDEPCMO:=$(COQENVCMO) lib/minisys.cmo lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) diff --git a/checker/check.mllib b/checker/check.mllib index 900cfe0c8..49de5e87f 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -37,6 +37,7 @@ CEphemeron Future CUnix +Minisys System Profile RemoteCounter diff --git a/dev/printers.mllib b/dev/printers.mllib index aa74cb508..022d06e3e 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -39,6 +39,7 @@ Ppstyle Errors Bigint CUnix +Minisys System Envars Aux_file diff --git a/lib/lib.mllib b/lib/lib.mllib index 2be435f6f..a6c09058d 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -3,6 +3,7 @@ Bigint Segmenttree Unicodetable Unicode +Minisys System CThread Spawn diff --git a/lib/minisys.ml b/lib/minisys.ml new file mode 100644 index 000000000..25e4d79c4 --- /dev/null +++ b/lib/minisys.ml @@ -0,0 +1,74 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Minisys regroups some code that used to be in System. + Unlike System, this module has no dependency and could + be used for initial compilation target such as coqdep_boot. + The functions here are still available in System thanks to + an include. For the signature, look at the top of system.mli +*) + +(** Dealing with directories *) + +type unix_path = string (* path in unix-style, with '/' separator *) + +type file_kind = + | FileDir of unix_path * (* basename of path: *) string + | FileRegular of string (* basename of file *) + +(* Copy of Filename.concat but assuming paths to always be POSIX *) + +let (//) dirname filename = + let l = String.length dirname in + if l = 0 || dirname.[l-1] = '/' + then dirname ^ filename + else dirname ^ "/" ^ filename + +(* Excluding directories; We avoid directories starting with . as well + as CVS and _darcs and any subdirs given via -exclude-dir *) + +let skipped_dirnames = ref ["CVS"; "_darcs"] + +let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames + +let ok_dirname f = + not (f = "") && f.[0] != '.' && + not (List.mem f !skipped_dirnames) (*&& + (match Unicode.ident_refutation f with None -> true | _ -> false)*) + +(* Check directory can be opened *) + +let exists_dir dir = + try Sys.is_directory dir with Sys_error _ -> false + +let check_unix_dir warn dir = + if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") && + (String.length dir > 2 && dir.[1] = ':' || + String.contains dir '\\' || + String.contains dir ';') + then warn ("assuming " ^ dir ^ + " to be a Unix path even if looking like a Win32 path.") + +let apply_subdir f path name = + (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) + (* as well as skipped files like CVS, ... *) + if ok_dirname name then + let path = if path = "." then name else path//name in + match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with + | Unix.S_DIR -> f (FileDir (path,name)) + | Unix.S_REG -> f (FileRegular name) + | _ -> () + +let readdir dir = try Sys.readdir dir with any -> [||] + +let process_directory f path = + Array.iter (apply_subdir f path) (readdir path) + +let process_subdirectories f path = + let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in + process_directory f path diff --git a/lib/system.ml b/lib/system.ml index e54109a2f..ffb4459d7 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -12,65 +12,7 @@ open Pp open Errors open Util -(** Dealing with directories *) - -type unix_path = string (* path in unix-style, with '/' separator *) - -type file_kind = - | FileDir of unix_path * (* basename of path: *) string - | FileRegular of string (* basename of file *) - -(* Copy of Filename.concat but assuming paths to always be POSIX *) - -let (//) dirname filename = - let l = String.length dirname in - if l = 0 || dirname.[l-1] = '/' - then dirname ^ filename - else dirname ^ "/" ^ filename - -(* Excluding directories; We avoid directories starting with . as well - as CVS and _darcs and any subdirs given via -exclude-dir *) - -let skipped_dirnames = ref ["CVS"; "_darcs"] - -let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames - -let ok_dirname f = - not (f = "") && f.[0] != '.' && - not (List.mem f !skipped_dirnames) (*&& - (match Unicode.ident_refutation f with None -> true | _ -> false)*) - -(* Check directory can be opened *) - -let exists_dir dir = - try Sys.is_directory dir with Sys_error _ -> false - -let check_unix_dir warn dir = - if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") && - (String.length dir > 2 && dir.[1] = ':' || - String.contains dir '\\' || - String.contains dir ';') - then warn ("assuming " ^ dir ^ - " to be a Unix path even if looking like a Win32 path.") - -let apply_subdir f path name = - (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) - (* as well as skipped files like CVS, ... *) - if ok_dirname name then - let path = if path = "." then name else path//name in - match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with - | Unix.S_DIR -> f (FileDir (path,name)) - | Unix.S_REG -> f (FileRegular name) - | _ -> () - -let readdir dir = try Sys.readdir dir with any -> [||] - -let process_directory f path = - Array.iter (apply_subdir f path) (readdir path) - -let process_subdirectories f path = - let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in - process_directory f path +include Minisys (** Returns the list of all recursive subdirectories of [root] in depth-first search, with sons ordered as on the file system; diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index c63e4aaa6..0f7937d72 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -9,11 +9,11 @@ open Printf open Coqdep_lexer open Unix -open System +open Minisys (** [coqdep_boot] is a stripped-down version of [coqdep], whose behavior is the one of [coqdep -boot]. Its only dependencies - are [Coqdep_lexer] and [Unix], and it should stay so. + are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so. If it need someday some additional information, pass it via options (see for instance [option_natdynlk] below). *) @@ -526,7 +526,7 @@ let rec add_directory recur add_file phys_dir log_dir = | FileRegular f -> add_file phys_dir log_dir f in - System.check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir; + check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir; if exists_dir phys_dir then process_directory f phys_dir else |