From 682528d73e0b4aaf57e7bf23775376a3a7cf8296 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Mon, 5 May 2025 15:30:45 +0100 Subject: [PATCH 1/2] Fix #128: avoid Marshal-ing exn value via closure This commit fixes an observed discrepancy between running a TeX filter straight after parsing an Ott file, or after caching it and reading the cache. I believe the issue is that the code for the exception handler inside the Marshal'd closure captures a value for the exception which is not guaranteed to be preserved: https://ocaml.org/manual/5.3/api/Marshal.html#:~:text=Values%20of%20extensible,work%20as%20expected https://stackoverflow.com/a/54872172 One can observe this by debug-printing the tags associated with the exception using the diff mentioned in [this comment](https://github.com/ott-lang/ott/issues/128#issuecomment-2851186496). --- src/glr.ml | 6 ++---- src/new_term_parser.ml | 3 --- src/term_parser.ml | 2 -- src/types.ml | 4 ++++ 4 files changed, 6 insertions(+), 9 deletions(-) diff --git a/src/glr.ml b/src/glr.ml index 43d4e9d..8cd4a1e 100644 --- a/src/glr.ml +++ b/src/glr.ml @@ -65,8 +65,6 @@ module type IN = sig include Parse_table.S val debug : bool - exception Reject_parse - exception Reject_all_parses end;; module Make (Pt : IN) : S with @@ -538,7 +536,7 @@ struct (rn.rule_nt.reduce_action rl, idx::injection_children, NTset.add rn.rule_nt.reduce_left loop)::res - with Reject_parse -> + with Types.Reject_parse -> res) (process_t_or_s_nodes idx rn.outgoing rn.rule_nt.reduce_transparent) [] @@ -602,7 +600,7 @@ struct try sn.started <- true; List.flatten (List.map process_rule_node sn.possibilities) - with Reject_all_parses -> + with Types.Reject_all_parses -> [] in sn.finished <- true; diff --git a/src/new_term_parser.ml b/src/new_term_parser.ml index c8219cb..6b1802f 100644 --- a/src/new_term_parser.ml +++ b/src/new_term_parser.ml @@ -245,9 +245,6 @@ module Nt = Nonterminal;; module GramTypes = Parse_table.MakeTypes (Gtp);; open GramTypes;; -exception Reject_parse -exception Reject_all_parses - let rec split l n = if n = 0 then ([], l) diff --git a/src/term_parser.ml b/src/term_parser.ml index 6c2d407..28058d3 100644 --- a/src/term_parser.ml +++ b/src/term_parser.ml @@ -1191,8 +1191,6 @@ let make_parser xd : made_parser = let module Pt2 = struct include Pt - exception Reject_parse = New_term_parser.Reject_parse;; - exception Reject_all_parses = New_term_parser.Reject_all_parses;; let debug = false end in diff --git a/src/types.ml b/src/types.ml index f770b73..5ad1f73 100644 --- a/src/types.ml +++ b/src/types.ml @@ -39,6 +39,10 @@ exception LemTODO;; exception DE1 of string;; +exception Reject_parse;; + +exception Reject_all_parses;; + open Location;; (** ************************ *) From 0105f02f8e7a9d4308137731da02daada51bb3c1 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Mon, 5 May 2025 15:36:59 +0100 Subject: [PATCH 2/2] Use type synonym for Marshal'd parser --- src/main.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main.ml b/src/main.ml index 0c67e50..c5ac87b 100644 --- a/src/main.ml +++ b/src/main.ml @@ -697,7 +697,7 @@ let read_systemdefn read_systemdefn_filename = let fd = open_in_bin read_systemdefn_filename in let sd,lookup ,sd_unquotiented, sd_quotiented_unaux = try (Marshal.from_channel fd : - (Types.systemdefn * (string -> bool -> string -> Types.symterm list) * Types.systemdefn * Types.systemdefn)) + (Types.systemdefn * Types.made_parser * Types.systemdefn * Types.systemdefn)) with Failure s -> Auxl.error None ("Cannot read dumped systemdefn\n " ^ s ^"\n") in close_in fd; @@ -712,7 +712,7 @@ let output_stage (sd,lookup,sd_unquotiented,sd_quotiented_unaux) = let fd = open_out_bin s in Marshal.to_channel fd ( (sd,lookup,sd_unquotiented,sd_quotiented_unaux) : - (Types.systemdefn * (string -> bool -> string -> Types.symterm list) * Types.systemdefn * Types.systemdefn)) + (Types.systemdefn * Types.made_parser * Types.systemdefn * Types.systemdefn)) [Marshal.Closures]; close_out fd; print_string ("system definition in file: " ^ s ^ "\n") );