cn: remove --state-file flag

Since CN now generates potentially multiple errors by default, and state files are specialized to exploring a single error, it's harder to control output locations sensibly with a single state file name. `--output-dir` should suffice instead.
rems-project · Aug 8, 2024 · e8bad52 · e8bad52
1 parent ce55642
commit e8bad52
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 41 deletions.
diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml
@@ -190,17 +190,13 @@ let with_well_formedness_check
 
 (** Report an error on [stderr] in an appropriate format: JSON if [json] is
     true, or human-readable if not. *)
-let report_type_error
-  ~(json : bool)
-  ?(state_file : string option)
-  ?(output_dir : string option)
-  (error : TypeErrors.t)
+let report_type_error ~(json : bool) ?(output_dir : string option) (error : TypeErrors.t)
   : unit
   =
   if json then
-    TypeErrors.report_json ?state_file ?output_dir error
+    TypeErrors.report_json ?output_dir error
   else
-    TypeErrors.report_pretty ?state_file ?output_dir error
+    TypeErrors.report_pretty ?output_dir error
 
 
 (** Exit with a code appropriate to the provided error. *)
@@ -209,13 +205,8 @@ let exit_on_type_error (error : TypeErrors.t) : 'a =
 
 
 (** Report the provided error, then exit. *)
-let handle_type_error
-  ~(json : bool)
-  ?(state_file : string option)
-  ?(output_dir : string option)
-  (error : TypeErrors.t)
-  =
-  report_type_error ~json ?state_file ?output_dir error;
+let handle_type_error ~(json : bool) ?(output_dir : string option) (error : TypeErrors.t) =
+  report_type_error ~json ?output_dir error;
   exit_on_type_error error
 
 
@@ -225,7 +216,6 @@ let well_formed
   incl_dirs
   incl_files
   json
-  state_file
   output_dir
   csv_times
   log_times
@@ -245,7 +235,7 @@ let well_formed
     ~use_peval
     ~no_inherit_loc
     ~magic_comment_char_dollar
-    ~handle_error:(handle_type_error ~json ?state_file ?output_dir)
+    ~handle_error:(handle_type_error ~json ?output_dir)
     ~f:(fun ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused:_ -> Resultat.return ())
 
 
@@ -262,7 +252,6 @@ let verify
   slow_smt_dir
   no_timestamps
   json
-  state_file
   output_dir
   diag
   lemmata
@@ -326,15 +315,15 @@ let verify
     ~use_peval
     ~no_inherit_loc
     ~magic_comment_char_dollar (* Callbacks *)
-    ~handle_error:(handle_type_error ~json ?state_file ?output_dir)
+    ~handle_error:(handle_type_error ~json ?output_dir)
     ~f:(fun ~prog5 ~ail_prog ~statement_locs ~paused ->
       match output_decorated with
       | None ->
         let check (functions, lemmas) =
           let open Typing in
           let@ errors = Check.time_check_c_functions functions in
           if not quiet then
-            List.iter (report_type_error ~json ?state_file ?output_dir) errors;
+            List.iter (report_type_error ~json ?output_dir) errors;
           Check.generate_lemmas lemmas lemmata
         in
         Typing.run_from_pause check paused
@@ -565,11 +554,6 @@ module Verify_flags = struct
     Arg.(value & opt (some string) None & info [ "slow-smt-dir" ] ~docv:"FILE" ~doc)
 
 
-  let state_file =
-    let doc = "file in which to output the state" in
-    Arg.(value & opt (some string) None & info [ "state-file" ] ~docv:"FILE" ~doc)
-
-
   let diag =
     let doc = "explore branching diagnostics with key string" in
     Arg.(value & opt (some string) None & info [ "diag" ] ~doc)
@@ -629,7 +613,7 @@ module Verify_flags = struct
 
 
   let output_dir =
-    let doc = "directory in which to output state files (overridden by --state-file)" in
+    let doc = "directory in which to output state files" in
     Arg.(value & opt (some string) None & info [ "output-dir" ] ~docv:"FILE" ~doc)
 end
 
@@ -678,7 +662,6 @@ let wf_cmd =
     $ Common_flags.incl_dirs
     $ Common_flags.incl_files
     $ Verify_flags.json
-    $ Verify_flags.state_file
     $ Verify_flags.output_dir
     $ Common_flags.csv_times
     $ Common_flags.log_times
@@ -715,7 +698,6 @@ let verify_t : unit Term.t =
   $ Verify_flags.slow_smt_dir
   $ Common_flags.no_timestamps
   $ Verify_flags.json
-  $ Verify_flags.state_file
   $ Verify_flags.output_dir
   $ Verify_flags.diag
   $ Lemma_flags.lemmata

diff --git a/backend/cn/lib/typeErrors.ml b/backend/cn/lib/typeErrors.ml
@@ -572,18 +572,13 @@ let mk_state_file_name ?(output_dir : string option) (loc : Cerb_location.t) : s
     error contains enough information to create an HTML state report, generate
     one in [output_dir] (or, failing that, the system temporary directory) and
     print a link to it. *)
-let report_pretty ?state_file:to_ ?output_dir:dir_ { loc; msg } =
+let report_pretty ?output_dir:dir_ { loc; msg } =
   (* stealing some logic from pp_errors *)
   let report = pp_message msg in
   let consider =
     match report.state with
     | Some state ->
-      (* Decide where to write the state *)
-      let state_error_file =
-        match to_ with
-        | Some file -> file
-        | None -> mk_state_file_name ?output_dir:dir_ loc
-      in
+      let state_error_file = mk_state_file_name ?output_dir:dir_ loc in
       let link = Report.make state_error_file (Cerb_location.get_filename loc) state in
       let msg = !^"State file:" ^^^ !^("file://" ^ link) in
       Some msg
@@ -593,17 +588,12 @@ let report_pretty ?state_file:to_ ?output_dir:dir_ { loc; msg } =
 
 
 (* stealing some logic from pp_errors *)
-let report_json ?state_file:to_ ?output_dir:dir_ { loc; msg } =
+let report_json ?output_dir:dir_ { loc; msg } =
   let report = pp_message msg in
   let state_error_file =
     match report.state with
     | Some state ->
-      (* Decide where to write the state *)
-      let file =
-        match to_ with
-        | Some file -> file
-        | None -> mk_state_file_name ?output_dir:dir_ loc
-      in
+      let file = mk_state_file_name ?output_dir:dir_ loc in
       let link = Report.make file (Cerb_location.get_filename loc) state in
       `String link
     | None -> `Null