aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in27
-rw-r--r--tools/coq_dune.ml2
-rw-r--r--tools/coqc.ml39
3 files changed, 49 insertions, 19 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 4372ac72ae..f8f10b34ae 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -126,6 +126,8 @@ TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log
TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log
TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
+TGTS ?=
+
########## End of parameters ##################################################
# What follows may be relevant to you only if you need to
# extend this Makefile. If so, look for 'Extension point' here and
@@ -237,6 +239,11 @@ vo_to_obj = $(addsuffix .o,\
$(filter-out Warning: Error:,\
$(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1))))
strip_dotslash = $(patsubst ./%,%,$(1))
+
+# without this we get undefined variables in the expansion for the
+# targets of the [deprecated,use-mllib-or-mlpack] rule
+with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1)))
+
VO = vo
VOFILES = $(VFILES:.v=.$(VO))
@@ -269,14 +276,14 @@ CMXSFILES = \
PACKEDFILES = \
$(call strip_dotslash, \
$(foreach lib, \
- $(call strip_dotslash, \
- $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib))))
+ $(call strip_dotslash, \
+ $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib))))
# files that are archived into a .cma (mllib)
LIBEDFILES = \
$(call strip_dotslash, \
$(foreach lib, \
- $(call strip_dotslash, \
- $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib))))
+ $(call strip_dotslash, \
+ $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib))))
CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES))
CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
OBJFILES = $(call vo_to_obj,$(VOFILES))
@@ -681,11 +688,11 @@ $(GHTMLFILES): %.g.html: %.v %.glob
# Dependency files ############################################################
-ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),)
- -include $(ALLDFILES)
-else
- ifeq ($(MAKECMDGOALS),)
+ifndef MAKECMDGOALS
-include $(ALLDFILES)
+else
+ ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),)
+ -include $(ALLDFILES)
endif
endif
@@ -784,3 +791,7 @@ debug:
.PHONY: debug
.DEFAULT_GOAL := all
+
+# Local Variables:
+# mode: makefile-gmake
+# End:
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 9ecd8f19ce..8f6c4c0968 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -186,7 +186,7 @@ let pp_vo_dep dir fmt vo =
(* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *)
let libflag = "-coqlib %{project_root}" in
(* The final build rule *)
- let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in
+ let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -w -deprecate-compile-arg -compile %s))" libflag eflag cflag source in
let all_targets = gen_coqc_targets vo in
pp_rule fmt all_targets deps action
diff --git a/tools/coqc.ml b/tools/coqc.ml
index ae841212a7..0f65823740 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -32,8 +32,9 @@ let verbose = ref false
let rec make_compilation_args = function
| [] -> []
| file :: fl ->
- (if !verbose then "-compile-verbose" else "-compile")
- :: file :: (make_compilation_args fl)
+ "-w" :: "-deprecate-compile-arg"
+ :: (if !verbose then "-compile-verbose" else "-compile")
+ :: file :: (make_compilation_args fl)
(* compilation of files [files] with command [command] and args [args] *)
@@ -61,16 +62,28 @@ let usage () =
(* parsing of the command line *)
let extra_arg_needed = ref true
+let deprecated_coqc_warning = CWarnings.(create
+ ~name:"deprecate-compile-arg"
+ ~category:"toplevel"
+ ~default:Enabled
+ (fun opt_name -> Pp.(seq [str "The option "; str opt_name; str" is deprecated."])))
+
let parse_args () =
let rec parse (cfiles,args) = function
| [] ->
List.rev cfiles, List.rev args
| ("-verbose" | "--verbose") :: rem ->
verbose := true ; parse (cfiles,args) rem
- | "-image" :: f :: rem -> image := f; parse (cfiles,args) rem
+ | "-image" :: f :: rem ->
+ deprecated_coqc_warning "-image";
+ image := f; parse (cfiles,args) rem
| "-image" :: [] -> usage ()
- | "-byte" :: rem -> use_bytecode := true; parse (cfiles,args) rem
- | "-opt" :: rem -> use_bytecode := false; parse (cfiles,args) rem
+ | "-byte" :: rem ->
+ deprecated_coqc_warning "-byte";
+ use_bytecode := true; parse (cfiles,args) rem
+ | "-opt" :: rem ->
+ deprecated_coqc_warning "-opt";
+ use_bytecode := false; parse (cfiles,args) rem
(* Informative options *)
@@ -87,7 +100,7 @@ let parse_args () =
Envars.set_coqlib ~fail:(fun x -> x);
Envars.print_config stdout Coq_config.all_src_dirs;
exit 0
-
+
| ("-print-version" | "--print-version") :: _ ->
Usage.machine_readable_version 0
@@ -97,7 +110,7 @@ let parse_args () =
|"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
|"-q"|"-profile"|"-echo" |"-quiet"
|"-silent"|"-m"|"-beautify"|"-strict-implicit"
- |"-impredicative-set"|"-vm"
+ |"-impredicative-set"|"-vm"|"-test-mode"|"-emacs"
|"-indices-matter"|"-quick"|"-type-in-type"
|"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
|"-stm-debug"
@@ -108,22 +121,28 @@ let parse_args () =
| ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color"
|"-load-vernac-source"|"-l"|"-load-vernac-object"
- |"-load-ml-source"|"-require"|"-load-ml-object"
+ |"-load-ml-source"|"-require"|"-load-ml-object"|"-async-proofs-cache"
|"-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"
+ |"-profile-ltac-cutoff"|"-mangle-names"|"-bytecode-compiler"|"-native-compiler"
as o) :: rem ->
begin
match rem with
| s :: rem' -> parse (cfiles,s::o::args) rem'
| [] -> usage ()
end
+ | "-o" :: rem->
+ begin
+ match rem with
+ | s :: rem' -> parse (cfiles,s::"-o"::args) rem'
+ | [] -> usage ()
+ end
| ("-I"|"-include" as o) :: s :: rem -> parse (cfiles,s::o::args) rem
(* Options for coqtop : c) options with 1 argument and possibly more *)
| ("-R"|"-Q" as o) :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem
- | ("-schedule-vio-checking"
+ | ("-schedule-vio-checking"|"-vio2vo"
|"-check-vio-tasks" | "-schedule-vio2vo" as o) :: s :: rem ->
let nodash, rem =
CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 19:32:42 +0000