diff options
| -rw-r--r-- | Makefile.build | 16 | ||||
| -rw-r--r-- | lib/minisys.ml | 14 | ||||
| -rw-r--r-- | lib/segmenttree.ml | 8 | ||||
| -rw-r--r-- | lib/segmenttree.mli | 8 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 7 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 3 |
6 files changed, 43 insertions, 13 deletions
diff --git a/Makefile.build b/Makefile.build index 63aa41c6c5..991942bf0a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -430,14 +430,18 @@ tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) # Remember to update the dependencies below when you add files! -COQDEPBOOTSRC := lib/minisys.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo \ +COQDEPBOOTSRC := \ + lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \ tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep_boot.cmo lib/segmenttree.cmo : lib/segmenttree.cmi lib/segmenttree.cmx : lib/segmenttree.cmi -lib/unicode.cmo : lib/unicodetable.cmo lib/segmenttree.cmi lib/unicode.cmi -lib/unicode.cmx : lib/unicodetable.cmx lib/segmenttree.cmx lib/unicode.cmi +lib/unicodetable.cmo : lib/segmenttree.cmo +lib/unicodetable.cmx : lib/segmenttree.cmx +lib/unicode.cmo : lib/unicodetable.cmo lib/unicode.cmi +lib/unicode.cmx : lib/unicodetable.cmx lib/unicode.cmi +lib/minisys.cmo : lib/unicode.cmo +lib/minisys.cmx : lib/unicode.cmx tools/coqdep_lexer.cmo : lib/unicode.cmi tools/coqdep_lexer.cmi tools/coqdep_lexer.cmx : lib/unicode.cmx tools/coqdep_lexer.cmi tools/coqdep_common.cmo : lib/minisys.cmo tools/coqdep_lexer.cmi tools/coqdep_common.cmi @@ -455,8 +459,8 @@ $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) # The full coqdep (unused by this build, but distributed by make install) -COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo lib/minisys.cmo \ - lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo \ +COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \ + lib/segmenttree.cmo lib/unicodetable.cmo lib/unicode.cmo lib/minisys.cmo \ lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo \ tools/coqdep.cmo diff --git a/lib/minisys.ml b/lib/minisys.ml index 706f0430c3..389b18ad4e 100644 --- a/lib/minisys.ml +++ b/lib/minisys.ml @@ -36,10 +36,15 @@ let skipped_dirnames = ref ["CVS"; "_darcs"] let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames +(* Note: this test is possibly used for Coq module/file names but also for + OCaml filenames, whose syntax as of today is more restrictive for + module names (only initial letter then letter, digits, _ or quote), + but more permissive (though disadvised) for file names *) + let ok_dirname f = not (f = "") && f.[0] != '.' && - not (List.mem f !skipped_dirnames) (*&& - (match Unicode.ident_refutation f with None -> true | _ -> false)*) + not (List.mem f !skipped_dirnames) && + match Unicode.ident_refutation f with None -> true | _ -> false (* Check directory can be opened *) @@ -55,10 +60,11 @@ let exists_dir dir = 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 base = try Filename.chop_extension name with Invalid_argument _ -> name in + if ok_dirname base 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_DIR when name = base -> f (FileDir (path,name)) | Unix.S_REG -> f (FileRegular name) | _ -> () diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml index 9ce348a0bd..d0ded4cb59 100644 --- a/lib/segmenttree.ml +++ b/lib/segmenttree.ml @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + (** This module is a very simple implementation of "segment trees". A segment tree of type ['a t] represents a mapping from a union of diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli index 3258537b99..e274a6fdc8 100644 --- a/lib/segmenttree.mli +++ b/lib/segmenttree.mli @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + (** This module is a very simple implementation of "segment trees". A segment tree of type ['a t] represents a mapping from a union of diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index cfa5526025..8f79f8a669 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -179,8 +179,6 @@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) -CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) - # FIXME This should be generated by Coq GRAMMARS:=grammar.cma ifeq ($(CAMLP4),camlp5) @@ -189,7 +187,12 @@ else CAMLP4EXTEND= endif +CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) +ifeq (,$(CAMLLIB)) +PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") +else PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +endif ifneq (,$(TIMING)) TIMING_ARG=-time diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4a9d871fd3..2feaaa04cd 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -122,7 +122,8 @@ let generate_makefile oc conf_file local_file args project = Envars.coqlib () ^ template in let s = read_whole_file makefile_template in let s = List.fold_left - (fun s (k,v) -> Str.global_replace (Str.regexp_string k) v s) s + (* We use global_substitute to avoid running into backslash issues due to \1 etc. *) + (fun s (k,v) -> Str.global_substitute (Str.regexp_string k) (fun _ -> v) s) s [ "@CONF_FILE@", conf_file; "@LOCAL_FILE@", local_file; "@COQ_VERSION@", Coq_config.version; |