From 6ef8a007e77c61d9f8c2b19b19dc22548f1896ca Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 18 May 2017 04:47:38 +0200 Subject: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520) In non-interactive mode, `edit_at` seems to do very weird things, for instance will try to recompute all the previous states which seems weird. We better avoid that to approximate 8.6 behavior while we investigate more. --- toplevel/coqtop.ml | 3 +++ toplevel/vernac.ml | 4 +++- 2 files changed, 6 insertions(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8f50bfb3d..41d370ea5 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -641,6 +641,9 @@ let init_toplevel arglist = init_library_roots (); load_vernac_obj (); require (); + (* XXX: This is incorrect in batch mode, as we will initialize + the STM before having done Declaremods.start_library, thus + state 1 is invalid. This bug was present in 8.5/8.6. *) Stm.init (); let sid = load_rcfile (Stm.get_current_state ()) in (* XXX: We ignore this for now, but should be threaded to the toplevels *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index eaf685b18..f8378f876 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -153,7 +153,9 @@ let rec interp_vernac sid (loc,com) = let com = if !Flags.time then VernacTime (loc,com) else com in interp com with reraise -> - ignore(Stm.edit_at sid); + (* XXX: In non-interactive mode edit_at seems to do very weird + things, so we better avoid it while we investigate *) + if not !Flags.batch_mode then ignore(Stm.edit_at sid); let (reraise, info) = CErrors.push reraise in let loc' = Option.default Loc.ghost (Loc.get_loc info) in if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) -- cgit v1.2.3