aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES5
-rw-r--r--Makefile33
-rw-r--r--Makefile.build2
-rw-r--r--Makefile.dev16
-rw-r--r--doc/sphinx/language/cic.rst2
-rw-r--r--test-suite/coq-makefile/timing/after/time-of-build-both.log.desired6
-rw-r--r--test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired18
-rwxr-xr-xtest-suite/coq-makefile/timing/run.sh4
-rw-r--r--tools/CoqMakefile.in8
-rw-r--r--tools/coq_makefile.ml34
-rw-r--r--toplevel/coqtop.ml2
11 files changed, 66 insertions, 64 deletions
diff --git a/CHANGES b/CHANGES
index a704f8047b..9bc2d2b369 100644
--- a/CHANGES
+++ b/CHANGES
@@ -82,6 +82,11 @@ Tools
please open an issue. We can help set up external maintenance as part
of Proof-General, or independently as part of coq-community.
+- The targets `print-pretty-timed`, `print-pretty-timed-diff`, and
+ `print-pretty-single-time-diff` now correctly label the "before" and
+ "after" columns, rather than swapping them.
+
+
Vernacular Commands
- Removed deprecated commands Arguments Scope and Implicit Arguments
diff --git a/Makefile b/Makefile
index 636093d7a5..344f2ee972 100644
--- a/Makefile
+++ b/Makefile
@@ -81,7 +81,7 @@ export ML4FILES := $(call find, '*.ml4')
export MLGFILES := $(call find, '*.mlg')
export CFILES := $(call findindir, 'kernel/byterun', '*.c')
-export MERLININFILES := $(call find, '.merlin.in')
+MERLININFILES := $(call find, '.merlin.in')
export MERLINFILES := $(MERLININFILES:.in=)
# NB: The lists of currently existing .ml and .mli files will change
@@ -116,7 +116,7 @@ include Makefile.common
NOARG: world
-.PHONY: NOARG help noconfig submake
+.PHONY: NOARG help noconfig submake camldevfiles
help:
@echo "Please use either:"
@@ -143,12 +143,13 @@ Then, you may want to consider whether you want to restore the autosaves)
#run.
endif
-# Apart from clean and tags, everything will be done in a sub-call to make
-# on Makefile.build. This way, we avoid doing here the -include of .d :
-# since they trigger some compilations, we do not want them for a mere clean.
-# Moreover, we regroup this sub-call in a common target named 'submake'.
-# This way, multiple user-given goals (cf the MAKECMDGOALS variable) won't
-# trigger multiple (possibly parallel) make sub-calls
+# Apart from clean and a few misc files, everything will be done in a
+# sub-call to make on Makefile.build. This way, we avoid doing here
+# the -include of .d : since they trigger some compilations, we do not
+# want them for a mere clean. Moreover, we regroup this sub-call in a
+# common target named 'submake'. This way, multiple user-given goals
+# (cf the MAKECMDGOALS variable) won't trigger multiple (possibly
+# parallel) make sub-calls
ifdef COQ_CONFIGURED
%:: submake ;
@@ -161,7 +162,7 @@ MAKE_OPTS := --warn-undefined-variable --no-builtin-rules
bin:
mkdir bin
-submake: alienclean | bin
+submake: alienclean camldevfiles | bin
$(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS)
noconfig:
@@ -172,6 +173,20 @@ noconfig:
Makefile $(wildcard Makefile.*) config/Makefile : ;
###########################################################################
+# OCaml dev files
+###########################################################################
+camldevfiles: $(MERLINFILES) META.coq
+
+.merlin: .merlin.in
+ cp -a "$<" "$@"
+
+%/.merlin: %/.merlin.in
+ cp -a "$<" "$@"
+
+META.coq: META.coq.in
+ cp -a "$<" "$@"
+
+###########################################################################
# Cleaning
###########################################################################
diff --git a/Makefile.build b/Makefile.build
index 05633cecc8..c100eda400 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -64,7 +64,7 @@ AFTER ?=
# build the different subsystems:
-world: camldevfiles coq coqide documentation revision
+world: coq coqide documentation revision
coq: coqlib coqbinaries tools
diff --git a/Makefile.dev b/Makefile.dev
index ea1a3d40a2..68e96a57b7 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -15,7 +15,7 @@
# Debug printers in dev/
#########################
-.PHONY: devel printers camldevfiles
+.PHONY: devel printers
DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo
@@ -85,20 +85,6 @@ endif
# But these partial targets could be quite handy for quick builds
# of specific components of Coq.
-###########################################################################
-# OCaml dev files
-###########################################################################
-camldevfiles: $(MERLINFILES) META.coq
-
-.merlin: .merlin.in
- cp -a "$<" "$@"
-
-%/.merlin: %/.merlin.in
- cp -a "$<" "$@"
-
-META.coq: META.coq.in
- cp -a "$<" "$@"
-
###############################
### 1) general-purpose targets
###############################
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index a63400103f..b0ba2bcc31 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -781,7 +781,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is
.. coqtop:: in
- Inductive even : nat -> prop :=
+ Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, odd n -> even (S n)
with odd : nat -> prop :=
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired
index 56815d241e..72c520218c 100644
--- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired
+++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired
@@ -1,6 +1,6 @@
After | File Name | Before || Change | % Change
--------------------------------------------------------
-0m00.38s | Total | 0m00.39s || -0m00.01s | -2.56%
+0m00.34s | Total | 0m00.49s || -0m00.14s | -30.61%
--------------------------------------------------------
-0m00.35s | Slow | 0m00.02s || +0m00.32s | +1649.99%
-0m00.03s | Fast | 0m00.37s || -0m00.34s | -91.89% \ No newline at end of file
+0m00.32s | Fast | 0m00.02s || +0m00.30s | +1500.00%
+0m00.02s | Slow | 0m00.47s || -0m00.44s | -95.74% \ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired
index 18f0f34b28..74dad73332 100644
--- a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired
+++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired
@@ -1,9 +1,9 @@
-After | Code | Before || Change | % Change
----------------------------------------------------------------------------------------------------
-0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96%
----------------------------------------------------------------------------------------------------
-0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47%
-0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88%
- N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A
-0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A
-0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% \ No newline at end of file
+After | Code | Before || Change | % Change
+----------------------------------------------------------------------------------------------------
+0m04.35s | Total | 0m00.58s || +0m03.77s | +649.05%
+----------------------------------------------------------------------------------------------------
+0m03.87s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.246s || +0m03.62s | +1473.17%
+0m00.322s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.189s || +0m00.13s | +70.37%
+0m00.16s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.146s || +0m00.01s | +9.58%
+0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | N/A || +0m00.00s | N/A
+ N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | 0m00.s || +0m00.00s | N/A \ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 6737197ee4..78a3f7c63a 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -5,6 +5,10 @@ set -e
. ../template/path-init.sh
+# reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues
+
+MAKEFLAGS=
+
cd precomputed-time-tests
./run.sh || exit $?
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 8b6822a4ed..403ad61798 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -343,19 +343,19 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
print-pretty-timed::
$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
print-pretty-timed-diff::
- $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
ifeq (,$(BEFORE))
print-pretty-single-time-diff::
- @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+ @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
$(HIDE)false
else
ifeq (,$(AFTER))
print-pretty-single-time-diff::
- @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+ @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
$(HIDE)false
else
print-pretty-single-time-diff::
- $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
endif
endif
pretty-timed:
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ad489da822..c3bdf656d1 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -31,8 +31,19 @@ let rec print_prefix_list sep = function
| x :: l -> print sep; print x; print_prefix_list sep l
| [] -> ()
-let usage_common () =
+let usage_coq_makefile () =
+ output_string stderr "Usage summary:\
+\n\
+\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
+\n ... [any] ... [-extra[-phony] result dependencies command]\
+\n ... [-I dir] ... [-R physicalpath logicalpath]\
+\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
+\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
+\n [-h] [--help]\
+\n";
output_string stderr "\
+\nFull list of options:\
+\n\
\n[file.v]: Coq file to be compiled\
\n[file.ml[i4]?]: Objective Caml file to be compiled\
\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\
@@ -61,25 +72,6 @@ let usage_common () =
\n[-install opt]: where opt is \"user\" to force install into user directory,\
\n \"none\" to build a makefile with no install target or\
\n \"global\" to force install in $COQLIB directory\
-\n"
-
-let usage_coq_project () =
- output_string stderr "Available arguments:";
- usage_common ();
- exit 1
-
-let usage_coq_makefile () =
- output_string stderr "Usage summary:\
-\n\
-\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
-\n ... [any] ... [-extra[-phony] result dependencies command]\
-\n ... [-I dir] ... [-R physicalpath logicalpath]\
-\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
-\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
-\n [-h] [--help]\
-\n";
- usage_common ();
- output_string stderr "\
\n[-f file]: take the contents of file as arguments\
\n[-o file]: output should go in file file (recommended)\
\n Output file outside the current directory is forbidden.\
@@ -405,7 +397,7 @@ let _ =
let project =
try cmdline_args_to_project ~curdir:Filename.current_dir_name args
- with Parsing_error s -> prerr_endline s; usage_coq_project () in
+ with Parsing_error s -> prerr_endline s; usage_coq_makefile () in
if only_destination <> None then begin
destination_of project (Option.get only_destination);
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9b68f303a6..bdd33e10ef 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -384,7 +384,7 @@ let print_style_tags opts =
(** GC tweaking *)
(** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
- minor heap is heavily sollicited. Unfortunately, the default size is far too
+ minor heap is heavily solicited. Unfortunately, the default size is far too
small, so we enlarge it a lot (128 times larger).
To better handle huge memory consumers, we also augment the default major
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 02:52:14 +0000