aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build18
-rw-r--r--Makefile.ide1
-rw-r--r--checker/check_stat.ml2
-rw-r--r--doc/refman/Extraction.tex40
-rw-r--r--lib/errors.ml2
-rw-r--r--test-suite/Makefile2
-rw-r--r--tools/coqdep_common.ml4
-rw-r--r--tools/ocamllibdep.mll8
-rw-r--r--toplevel/coqloop.ml12
9 files changed, 57 insertions, 32 deletions
diff --git a/Makefile.build b/Makefile.build
index 4eafe1d619..2a2eb8796d 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -347,7 +347,7 @@ $(COQC): $(call bestobj, $(COQCCMO))
# other tools
###########################################################################
-.PHONY:
+.PHONY: tools
tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT)
# coqdep_boot : a basic version of coqdep, with almost no dependencies.
@@ -567,6 +567,14 @@ plugins/%.cmx: plugins/%.ml
$(SHOW)'OCAMLOPT -shared -o $@'
$(HIDE)$(OCAMLOPT) -shared -o $@ $<
+%.cmxs: %.cmxa
+ $(SHOW)'OCAMLOPT -shared -o $@'
+ifeq ($(HASNATDYNLINK),os5fixme)
+ $(HIDE)dev/ocamlopt_shared_os5fix.sh "$(OCAMLOPT)" $@
+else
+ $(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
+endif
+
%.ml: %.mll
$(SHOW)'OCAMLLEX $<'
$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
@@ -650,6 +658,14 @@ endif
Makefile $(wildcard Makefile.*) config/Makefile : ;
+# Final catch-all rule.
+# Usually, 'make' would display such an error itself.
+# But if the target has some declared dependencies (e.g. in a .d)
+# but no building rule, 'make' succeeds silently (see bug #4812).
+
+%:
+ @echo "Error: no rule to make target $@ (or missing .PHONY)" && false
+
# For emacs:
# Local Variables:
# mode: makefile
diff --git a/Makefile.ide b/Makefile.ide
index 8d6b5de36f..c50e42341e 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -62,6 +62,7 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
###########################################################################
.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
+.PHONY: ide-toploop
# target to build CoqIde
coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index a26c93a30d..a63705adcd 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -18,7 +18,7 @@ let print_memory_stat () =
if !memory_stat then begin
Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ());
Format.print_newline();
- flush_all()
+ Format.print_flush()
end
let output_context = ref false
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index a963662f64..9da23b54ed 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -3,7 +3,7 @@
\aauthor{Jean-Christophe Filliâtre and Pierre Letouzey}
\index{Extraction}
-We present here the \Coq\ extraction commands, used to build certified
+\noindent We present here the \Coq\ extraction commands, used to build certified
and relatively efficient functional programs, extracting them from
either \Coq\ functions or \Coq\ proofs of specifications. The
functional languages available as output are currently \ocaml{},
@@ -30,7 +30,7 @@ The next two commands are meant to be used for rapid preview of
extraction. They both display extracted term(s) inside \Coq.
\begin{description}
-\item {\tt Extraction \qualid.} ~\par
+\item {\tt Extraction \qualid{}.} ~\par
Extraction of a constant or module in the \Coq\ toplevel.
\item {\tt Recursive Extraction} \qualid$_1$ \dots\ \qualid$_n$. ~\par
@@ -40,7 +40,7 @@ extraction. They both display extracted term(s) inside \Coq.
%% TODO error messages
-All the following commands produce real ML files. User can choose to produce
+\noindent All the following commands produce real ML files. User can choose to produce
one monolithic file or one file per \Coq\ library.
\begin{description}
@@ -76,7 +76,7 @@ one monolithic file or one file per \Coq\ library.
using prefixes \verb!coq_! or \verb!Coq_!.
\end{description}
-The list of globals \qualid$_i$ does not need to be
+\noindent The list of globals \qualid$_i$ does not need to be
exhaustive: it is automatically completed into a complete and minimal
environment.
@@ -215,7 +215,7 @@ arguments. In fact, an argument can also be referred by a number
indicating its position, starting from 1.
\end{description}
-When an actual extraction takes place, an error is normally raised if the
+\noindent When an actual extraction takes place, an error is normally raised if the
{\tt Extraction Implicit}
declarations cannot be honored, that is if any of the implicited
variables still occurs in the final code. This behavior can be relaxed
@@ -260,7 +260,7 @@ what ML term corresponds to a given axiom.
be inlined everywhere instead of being declared via a let.
\end{description}
-Note that the {\tt Extract Inlined Constant} command is sugar
+\noindent Note that the {\tt Extract Inlined Constant} command is sugar
for an {\tt Extract Constant} followed by a {\tt Extraction Inline}.
Hence a {\tt Reset Extraction Inline} will have an effect on the
realized and inlined axiom.
@@ -279,7 +279,7 @@ Extract Constant X => "int".
Extract Constant x => "0".
\end{coq_example*}
-Notice that in the case of type scheme axiom (i.e. whose type is an
+\noindent Notice that in the case of type scheme axiom (i.e. whose type is an
arity, that is a sequence of product finished by a sort), then some type
variables have to be given. The syntax is then:
@@ -287,7 +287,7 @@ variables have to be given. The syntax is then:
\item{\tt Extract Constant \qualid\ \str$_1$ \dots\ \str$_n$ => \str.}
\end{description}
-The number of type variables is checked by the system.
+\noindent The number of type variables is checked by the system.
\Example
\begin{coq_example*}
@@ -295,7 +295,7 @@ Axiom Y : Set -> Set -> Set.
Extract Constant Y "'a" "'b" => " 'a*'b ".
\end{coq_example*}
-Realizing an axiom via {\tt Extract Constant} is only useful in the
+\noindent Realizing an axiom via {\tt Extract Constant} is only useful in the
case of an informative axiom (of sort Type or Set). A logical axiom
have no computational content and hence will not appears in extracted
terms. But a warning is nonetheless issued if extraction encounters a
@@ -325,7 +325,7 @@ native boolean type instead of \Coq\ one. The syntax is the following:
pattern-matching of the language will be used.
\end{description}
-For an inductive type with $k$ constructor, the function used to
+\noindent For an inductive type with $k$ constructor, the function used to
emulate the match should expect $(k+1)$ arguments, first the $k$
branches in functional form, and then the inductive element to
destruct. For instance, the match branch \verb$| S n => foo$ gives the
@@ -365,7 +365,7 @@ Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive sumbool => "bool" [ "true" "false" ].
\end{coq_example}
-If an inductive constructor or type has arity 2 and the corresponding
+\noindent If an inductive constructor or type has arity 2 and the corresponding
string is enclosed by parenthesis, then the rest of the string is used
as infix constructor or type.
\begin{coq_example}
@@ -373,7 +373,7 @@ Extract Inductive list => "list" [ "[]" "(::)" ].
Extract Inductive prod => "(*)" [ "(,)" ].
\end{coq_example}
-As an example of translation to a non-inductive datatype, let's turn
+\noindent As an example of translation to a non-inductive datatype, let's turn
{\tt nat} into Ocaml's {\tt int} (see caveat above):
\begin{coq_example}
Extract Inductive nat => int [ "0" "succ" ]
@@ -402,7 +402,7 @@ It is possible to instruct the extraction not to use particular filenames.
Allow the extraction to use any filename.
\end{description}
-For Ocaml, a typical use of these commands is
+\noindent For Ocaml, a typical use of these commands is
{\tt Extraction Blacklist String List}.
\asection{Differences between \Coq\ and ML type systems}
@@ -456,7 +456,7 @@ In Ocaml, we must cast any argument of the constructor dummy.
\end{itemize}
-Even with those unsafe castings, you should never get error like
+\noindent Even with those unsafe castings, you should never get error like
``segmentation fault''. In fact even if your program may seem
ill-typed to the Ocaml type-checker, it can't go wrong: it comes
from a Coq well-typed terms, so for example inductives will always
@@ -489,7 +489,7 @@ Inductive nat : Set :=
| S : nat -> nat.
\end{coq_example*}
-This module contains a theorem {\tt eucl\_dev}, whose type is
+\noindent This module contains a theorem {\tt eucl\_dev}, whose type is
\begin{verbatim}
forall b:nat, b > 0 -> forall a:nat, diveucl a b
\end{verbatim}
@@ -506,7 +506,7 @@ Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2.
Recursive Extraction eucl_dev.
\end{coq_example}
-The inlining of {\tt gt\_wf\_rec} and others is not
+\noindent The inlining of {\tt gt\_wf\_rec} and others is not
mandatory. It only enhances readability of extracted code.
You can then copy-paste the output to a file {\tt euclid.ml} or let
\Coq\ do it for you with the following command:
@@ -515,7 +515,7 @@ You can then copy-paste the output to a file {\tt euclid.ml} or let
Extraction "euclid" eucl_dev.
\end{verbatim}
-Let us play the resulting program:
+\noindent Let us play the resulting program:
\begin{verbatim}
# #use "euclid.ml";;
@@ -543,7 +543,7 @@ val div : int -> int -> int * int = <fun>
- : int * int = (11, 8)
\end{verbatim}
-Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now
+\noindent Note that these {\tt nat\_of\_int} and {\tt int\_of\_nat} are now
available via a mere {\tt Require Import ExtrOcamlIntConv} and then
adding these functions to the list of functions to extract. This file
{\tt ExtrOcamlIntConv.v} and some others in {\tt plugins/extraction/}
@@ -551,7 +551,7 @@ are meant to help building concrete program via extraction.
\asubsection{Extraction's horror museum}
-Some pathological examples of extraction are grouped in the file
+Some pathological examples of extraction are grouped in the file\\
{\tt test-suite/success/extraction.v} of the sources of \Coq.
\asubsection{Users' Contributions}
@@ -579,7 +579,7 @@ extraction test:
\item {\tt stalmarck}
\end{itemize}
-{\tt continuations} and {\tt multiplier} are a bit particular. They are
+\noindent {\tt continuations} and {\tt multiplier} are a bit particular. They are
examples of developments where {\tt Obj.magic} are needed. This is
probably due to an heavy use of impredicativity. After compilation, those
two examples run nonetheless, thanks to the correction of the
diff --git a/lib/errors.ml b/lib/errors.ml
index 8982dde148..1459141d1e 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -144,5 +144,5 @@ let handled e =
let fatal_error info anomaly =
let msg = info ++ fnl () in
pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
- flush_all ();
+ Format.pp_print_flush !Pp_control.err_ft ();
exit (if anomaly then 129 else 1)
diff --git a/test-suite/Makefile b/test-suite/Makefile
index b9c27a2fcf..d779d1f9a4 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -421,7 +421,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
@echo "TEST $<"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-tactic-error-resiliency off -async-proofs-command-error-resiliency off" 2>&1; \
+ $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
if [ $$? = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0f7937d729..cc63c13d7b 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -445,7 +445,7 @@ let mL_dependencies () =
let efullname = escape fullname in
printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep;
printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
- printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname;
+ printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
flush stdout)
(List.rev !mllibAccu);
List.iter
@@ -455,7 +455,7 @@ let mL_dependencies () =
let efullname = escape fullname in
printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep;
printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
- printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname efullname;
+ printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
flush stdout)
(List.rev !mlpackAccu)
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 57fcd5dd21..bf82be09f1 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -176,8 +176,8 @@ let mllib_dependencies () =
printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname sdeps;
printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n"
efullname efullname;
- printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n"
- efullname efullname efullname;
+ printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n"
+ efullname efullname;
flush Pervasives.stdout)
(List.rev !mllibAccu)
@@ -193,8 +193,8 @@ let mlpack_dependencies () =
List.iter (fun d -> printf "%s_FORPACK:= -for-pack %s\n" d modname) deps;
printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n"
efullname efullname;
- printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n"
- efullname efullname efullname;
+ printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n"
+ efullname efullname;
flush Pervasives.stdout)
(List.rev !mlpackAccu)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index c8879963e5..1fe30217dd 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -328,7 +328,7 @@ let do_vernac () =
Format.set_formatter_out_channel stdout;
let msg = print_toplevel_error any ++ fnl () in
pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
- flush_all ()
+ Format.pp_print_flush !Pp_control.std_ft ()
(** Main coq loop : read vernacular expressions until Drop is entered.
Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -345,13 +345,21 @@ let feed_emacs = function
| _ -> ()
*)
+(* Flush in a compatible order with 8.5 *)
+(* This mimics the semantics of the old Pp.flush_all *)
+let loop_flush_all () =
+ Pervasives.flush stderr;
+ Pervasives.flush stdout;
+ Format.pp_print_flush !Pp_control.std_ft ();
+ Format.pp_print_flush !Pp_control.err_ft ()
+
let rec loop () =
Sys.catch_break true;
if !Flags.print_emacs then Vernacentries.qed_display_script := false;
Flags.coqtop_ui := true;
try
reset_input_buffer stdin top_buffer;
- while true do do_vernac(); flush_all() done
+ while true do do_vernac(); loop_flush_all () done
with
| Errors.Drop -> ()
| Errors.Quit -> exit 0
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:01:51 +0000