aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml16
-rw-r--r--Makefile.doc8
-rw-r--r--doc/refman/RefMan-oth.tex5
-rw-r--r--doc/refman/RefMan-tac.tex2
-rw-r--r--lib/system.ml3
-rw-r--r--parsing/doc.tex9
-rw-r--r--test-suite/output/Load.out6
-rw-r--r--test-suite/output/Load.v7
-rw-r--r--test-suite/output/load/Load_noproof.v1
-rw-r--r--test-suite/output/load/Load_openproof.v1
-rw-r--r--test-suite/output/load/Load_proof.v2
-rw-r--r--toplevel/coqargs.ml2
-rw-r--r--toplevel/vernac.ml28
-rw-r--r--vernac/vernacentries.ml12
14 files changed, 58 insertions, 44 deletions
diff --git a/.travis.yml b/.travis.yml
index f4f01d2f02..9ec936b0c9 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -40,10 +40,10 @@ env:
# system is == 4.02.3
- COMPILER="system"
- COMPILER_BE="4.06.0"
- - CAMLP5_VER="6.14"
- - CAMLP5_VER_BE="7.03"
- - FINDLIB_VER="1.4.1"
- - FINDLIB_VER_BE="1.7.3"
+ - CAMLP5_VER=".6.14"
+ - CAMLP5_VER_BE=".7.03"
+ - FINDLIB_VER=".1.4.1"
+ - FINDLIB_VER_BE=".1.7.3"
- LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6"
- LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6"
- NATIVE_COMP="yes"
@@ -76,6 +76,8 @@ matrix:
- TEST_TARGET="ci-coquelicot"
- if: NOT (type = pull_request)
env:
+ # ppx_tools_versioned requires a specific version findlib
+ - FINDLIB_VER=""
- TEST_TARGET="ci-elpi" EXTRA_OPAM="ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree"
- if: NOT (type = pull_request)
env:
@@ -221,7 +223,7 @@ matrix:
env:
- TEST_TARGET="test-suite"
- COMPILER="4.02.3"
- - CAMLP5_VER="6.17"
+ - CAMLP5_VER=".6.17"
- NATIVE_COMP="no"
- COQ_DEST="-local"
before_install:
@@ -234,7 +236,7 @@ matrix:
env:
- TEST_TARGET=""
- COMPILER="4.02.3"
- - CAMLP5_VER="6.17"
+ - CAMLP5_VER=".6.17"
- NATIVE_COMP="no"
- COQ_DEST="-prefix ${PWD}/_install"
- EXTRA_CONF="-coqide opt -warn-error"
@@ -264,7 +266,7 @@ install:
- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
- eval $(opam config env)
- opam config list
-- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind.${FINDLIB_VER} ${EXTRA_OPAM}
+- opam install -j ${NJOBS} -y camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM}
- opam list
script:
diff --git a/Makefile.doc b/Makefile.doc
index 8cb9c9f0fa..3385e4951d 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -400,7 +400,7 @@ source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
$(SHOW)'OCAMLDOC -latex -o $@'
- $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+ $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP5LIB) $(MLINCLUDES)\
$(DOCMLIS) -noheader -t "Coq mlis documentation" \
-intro $(OCAMLDOCDIR)/docintro -o $@.tmp
$(SHOW)'OCAMLDOC utf8 fix'
@@ -410,13 +410,13 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
mli-doc: $(DOCMLIS:.mli=.cmi)
$(SHOW)'OCAMLDOC -html'
- $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
+ $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP5LIB) $(MLINCLUDES) \
$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-css-style style.css
ml-dot: $(MLFILES)
- $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \
+ $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP5LIB) $(MLINCLUDES) \
$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
%_dep.png: %.dot
@@ -449,7 +449,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d
$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
$(SHOW)'PDFLATEX $*.tex'
$(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex)
- $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log)
+ $(HIDE)(cd doc/tools/; ./show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log)
###########################################################################
# local web server
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 1cd23c9297..bef31d3fa5 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -513,6 +513,9 @@ This command loads the file named {\ident}{\tt .v}, searching
successively in each of the directories specified in the {\em
loadpath}. (see Section~\ref{loadpath})
+Files loaded this way cannot leave proofs open, and neither the {\tt
+ Load} command can be use inside a proof.
+
\begin{Variants}
\item {\tt Load {\str}.}\label{Load-str}\\
Loads the file denoted by the string {\str}, where {\str} is any
@@ -530,6 +533,8 @@ successively in each of the directories specified in the {\em
\begin{ErrMsgs}
\item \errindex{Can't find file {\ident} on loadpath}
+\item \errindex{Load is not supported inside proofs}
+\item \errindex{Files processed by Load cannot leave open proofs}
\end{ErrMsgs}
\section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index bf30a30517..6dca314b4a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3611,7 +3611,7 @@ $\beta$-expansion (the inverse of $\bt$-reduction) of the current goal
\item applying the abstracted goal to {\term}
\end{enumerate}
-For instance, if the current goal $T$ is expressible has $\phi(t)$
+For instance, if the current goal $T$ is expressible as $\phi(t)$
where the notation captures all the instances of $t$ in $\phi(t)$,
then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt
x}$)$) $t$}. This command can be used, for instance, when the tactic
diff --git a/lib/system.ml b/lib/system.ml
index e56736eb15..0ad86c73ff 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -54,7 +54,8 @@ let make_dir_table dir =
let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
-let trust_file_cache = ref true
+(** Don't trust in interactive mode (the default) *)
+let trust_file_cache = ref false
let exists_in_dir_respecting_case dir bf =
let cache_dir dir =
diff --git a/parsing/doc.tex b/parsing/doc.tex
deleted file mode 100644
index 68ab601cc1..0000000000
--- a/parsing/doc.tex
+++ /dev/null
@@ -1,9 +0,0 @@
-
-\newpage
-\section*{The Coq parsers and printers}
-
-\ocwsection \label{parsing}
-This chapter describes the implementation of the \Coq\ parsers and printers.
-
-\bigskip
-\begin{center}\epsfig{file=parsing.dep.ps}\end{center}
diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out
new file mode 100644
index 0000000000..0904d5540b
--- /dev/null
+++ b/test-suite/output/Load.out
@@ -0,0 +1,6 @@
+f = 2
+ : nat
+u = I
+ : True
+The command has indeed failed with message:
+Files processed by Load cannot leave open proofs.
diff --git a/test-suite/output/Load.v b/test-suite/output/Load.v
new file mode 100644
index 0000000000..967507415a
--- /dev/null
+++ b/test-suite/output/Load.v
@@ -0,0 +1,7 @@
+Load "output/load/Load_noproof.v".
+Print f.
+
+Load "output/load/Load_proof.v".
+Print u.
+
+Fail Load "output/load/Load_openproof.v".
diff --git a/test-suite/output/load/Load_noproof.v b/test-suite/output/load/Load_noproof.v
new file mode 100644
index 0000000000..aaf1ffe26d
--- /dev/null
+++ b/test-suite/output/load/Load_noproof.v
@@ -0,0 +1 @@
+Definition f := 2.
diff --git a/test-suite/output/load/Load_openproof.v b/test-suite/output/load/Load_openproof.v
new file mode 100644
index 0000000000..204d4ecbfe
--- /dev/null
+++ b/test-suite/output/load/Load_openproof.v
@@ -0,0 +1 @@
+Lemma k : True.
diff --git a/test-suite/output/load/Load_proof.v b/test-suite/output/load/Load_proof.v
new file mode 100644
index 0000000000..e47f66a193
--- /dev/null
+++ b/test-suite/output/load/Load_proof.v
@@ -0,0 +1,2 @@
+Lemma u : True.
+Proof. exact I. Qed.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 5b73471c59..a7065c0315 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -153,7 +153,7 @@ let add_compat_require opts v =
let set_batch_mode opts =
Flags.quiet := true;
- System.trust_file_cache := false;
+ System.trust_file_cache := true;
{ opts with batch_mode = true }
let add_compile opts verbose s =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 92dee84f32..a84990f919 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -120,16 +120,9 @@ module State = struct
end
-let rec interp_vernac ~time ~check ~interactive ~state (loc,com) =
+let interp_vernac ~time ~check ~interactive ~state (loc,com) =
let open State in
- let interp v =
- match under_control v with
- | VernacLoad (verbosely, fname) ->
- let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
- let fname = CUnix.make_suffix fname ".v" in
- let f = Loadpath.locate_file fname in
- load_vernac ~time ~verbosely ~check ~interactive ~state f
- | _ ->
+ try
(* XXX: We need to run this before add as the classification is
highly dynamic and depends on the structure of the
document. Hopefully this is fixed when VtMeta can be removed
@@ -139,13 +132,17 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) =
against that... *)
let wflags = CWarnings.get_flags () in
CWarnings.set_flags "none";
- let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
+ let is_proof_step = match fst (Vernac_classifier.classify_vernac com) with
| VtProofStep _ | VtMeta | VtStartProof _ -> true
| _ -> false
in
CWarnings.set_flags wflags;
- let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,v) in
+ (* The -time option is only supported from console-based
+ clients due to the way it prints. *)
+ if time then print_cmd_header ?loc com;
+ let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in
+ let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in
(* Main STM interaction *)
if ntip <> `NewTip then
@@ -165,13 +162,6 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) =
if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
let new_proof = Proof_global.give_me_the_proof_opt () in
{ doc = ndoc; sid = nsid; proof = new_proof }
- in
- try
- (* The -time option is only supported from console-based
- clients due to the way it prints. *)
- if time then print_cmd_header ?loc com;
- let com = if time then VernacTime(time, CAst.make ?loc com) else com in
- interp com
with reraise ->
(* XXX: In non-interactive mode edit_at seems to do very weird
things, so we better avoid it while we investigate *)
@@ -184,7 +174,7 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) =
end in iraise (reraise, info)
(* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac ~time ~verbosely ~check ~interactive ~state file =
+let load_vernac ~time ~verbosely ~check ~interactive ~state file =
let ft_beautify, close_beautify =
if !Flags.beautify_file then
let chan_beautify = open_out (file^beautify_suffix) in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4613100fc3..89fd2b6416 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1926,6 +1926,8 @@ exception End_of_input
without a considerable amount of refactoring.
*)
let vernac_load interp fname =
+ if Proof_global.there_are_pending_proofs () then
+ CErrors.user_err Pp.(str "Load is not supported inside proofs.");
let interp x =
let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in
Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
@@ -1942,8 +1944,13 @@ let vernac_load interp fname =
let longfname = Loadpath.locate_file fname in
let in_chan = open_utf8_file_in longfname in
Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
- try while true do interp (snd (parse_sentence input)) done
- with End_of_input -> ()
+ begin
+ try while true do interp (snd (parse_sentence input)) done
+ with End_of_input -> ()
+ end;
+ (* If Load left a proof open, we fail too. *)
+ if Proof_global.there_are_pending_proofs () then
+ CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.")
(* "locality" is the prefix "Local" attribute, while the "local" component
* is the outdated/deprecated "Local" attribute of some vernacular commands
@@ -1954,6 +1961,7 @@ let interp ?proof ~atts ~st c =
vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
match c with
+ (* Loading a file requires access to the control interpreter *)
| VernacLoad _ -> assert false
(* The STM should handle that, but LOAD bypasses the STM... *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 12:06:18 +0000