From f6454e7f06decd22b88e43a4010b500cb4e8f778 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Jun 2023 15:31:18 +0200 Subject: [PATCH] [stm] fix regression introduced in de2d782 The finish API is called both by clients and internally by the STM whenever a VtNow command is executed to obtain the new parsing state. Commit de2d782 makes finish cache the state, which is not a problem if do it once, but may increase memory consumption substantially when checking documents containing many commands classified as VtNow. (cherry picked from commit d4881af27a3831d7f8b2eb8a626df6925579d2ef) --- stm/stm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/stm/stm.ml b/stm/stm.ml index 46b5f6fd9331e..5784c3edf2bea 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2687,7 +2687,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) x c = begin match w with | VtNow -> (* We need to execute to get the new parsing state *) - ignore(finish ~doc:dummy_doc); + let () = observe ~doc:dummy_doc (VCS.get_branch_pos (VCS.current_branch ())) in let parsing = Vernacstate.Parser.cur_state () in (* If execution has not been put in cache, we need to save the parsing state *) if (VCS.get_info id).state == EmptyState then VCS.set_parsing_state id parsing;