From f5abd069a86b85829ab49141d27ef7633f4b84a1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 11 Dec 2017 23:26:10 +0100
Subject: [toplevel] [vernac] Remove Load hack and check supported scenarios.

Parsing in `VernacLoad` was broken for a while, but the situation has
improved by miscellaneous refactoring.

However, we still cannot support `Load` properly when proofs are
crossing file boundaries. So in this patch we do two things:

- We check for supported scenarios [no proofs open at `Load` entry/exit]

- Remove the hack in `toplevel` so the behavior of `Load` is
  consistent between `coqide`/`coqc`.

We close #5053 as its main bug was fixed by the main toplevel
refactoring and the remaining cases are documented now.
---
 vernac/vernacentries.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'vernac')

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... *)
-- 
cgit v1.2.3