diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 27 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 5 | ||||
| -rw-r--r-- | tools/coqc.ml | 2 | ||||
| -rw-r--r-- | tools/coqdep.ml | 3 |
4 files changed, 11 insertions, 26 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index e3fa0c24fe..b673225e40 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -20,7 +20,6 @@ include @CONF_FILE@ VFILES := $(COQMF_VFILES) MLIFILES := $(COQMF_MLIFILES) MLFILES := $(COQMF_MLFILES) -ML4FILES := $(COQMF_ML4FILES) MLGFILES := $(COQMF_MLGFILES) MLPACKFILES := $(COQMF_MLPACKFILES) MLLIBFILES := $(COQMF_MLLIBFILES) @@ -37,10 +36,6 @@ LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) -CAMLP5O := $(COQMF_CAMLP5O) -CAMLP5BIN := $(COQMF_CAMLP5BIN) -CAMLP5LIB := $(COQMF_CAMLP5LIB) -CAMLP5OPTIONS := $(COQMF_CAMLP5OPTIONS) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) @@ -99,7 +94,7 @@ BEFORE ?= AFTER ?= # FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=camlp5.gramlib,unix,str +CAMLDONTLINK=unix,str # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c @@ -192,22 +187,11 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) # ocamldoc fails with unknown argument otherwise CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) -# FIXME This should be generated by Coq -GRAMMARS:=grammar.cma -CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo - -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 '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' -endif - ifneq (,$(TIMING)) TIMING_ARG=-time ifeq (after,$(TIMING)) @@ -719,6 +703,9 @@ endif redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) +GENMLFILES:=$(MLGFILES:.mlg=.ml) $(ML4FILES:.ml4=.ml) +$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) + $(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli $(SHOW)'CAMLDEP $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) @@ -771,10 +758,6 @@ printenv:: @echo 'COQLIB = $(COQLIB)' @echo 'DOCDIR = $(DOCDIR)' @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP5O = $(CAMLP5O)' - @echo 'CAMLP5BIN = $(CAMLP5BIN)' - @echo 'CAMLP5LIB = $(CAMLP5LIB)' - @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ca5a232edb..8560bac786 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -396,8 +396,9 @@ let _ = | "-destination-of" :: tgt :: rest -> Some tgt, rest | _ -> None, args in - let project = - try cmdline_args_to_project ~curdir:Filename.current_dir_name args + let project = + let warning_fn x = Format.eprintf "%s@\n%!" x in + try cmdline_args_to_project ~warning_fn ~curdir:Filename.current_dir_name args with Parsing_error s -> prerr_endline s; usage_coq_makefile () in if only_destination <> None then begin diff --git a/tools/coqc.ml b/tools/coqc.ml index ad845470ec..ae841212a7 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -109,7 +109,7 @@ let parse_args () = | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color" |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" - |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" + |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"|"-topfile" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" |"-o"|"-profile-ltac-cutoff"|"-mangle-names"|"-bytecode-compiler"|"-native-compiler" as o) :: rem -> diff --git a/tools/coqdep.ml b/tools/coqdep.ml index ba88069be9..226a19678f 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -473,7 +473,8 @@ let add_r_include path l = add_rec_dir_import add_known path (split_period l) let treat_coqproject f = let open CoqProject_file in let iter_sourced f = List.iter (fun {thing} -> f thing) in - let project = read_project_file f in + let warning_fn x = coqdep_warning "%s" x in + let project = read_project_file ~warning_fn f in iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes; iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes; iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes; |