diff options
| author | Emilio Jesus Gallego Arias | 2017-05-18 04:47:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-05-18 04:48:27 +0200 |
| commit | 6ef8a007e77c61d9f8c2b19b19dc22548f1896ca (patch) | |
| tree | 28b289f8422b435b7ae5ca55c7725f6a1a4a1f45 | |
| parent | 6d770156669dd9868ae7623b8f4302866e2cc8c7 (diff) | |
[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.
| -rw-r--r-- | toplevel/coqtop.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 |
2 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8f50bfb3d8..41d370ea57 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 eaf685b184..f8378f8765 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) |