From 313a84780011f0bbf153bd79bbccaf97109d62f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 11 Feb 2025 19:53:20 -0800 Subject: [PATCH 1/4] Main: nits in error messages --- src/fstar/FStarC.Main.fst | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index d4d97f522d4..c0f9ff64763 100644 --- a/src/fstar/FStarC.Main.fst +++ b/src/fstar/FStarC.Main.fst @@ -69,6 +69,7 @@ let report_errors fmods = end let load_native_tactics () = + let open FStarC.Errors.Msg in let modules_to_load = Options.load() |> List.map Ident.lid_of_str in let cmxs_to_load = Options.load_cmxs () |> List.map Ident.lid_of_str in let ml_module_name m = FStarC.Extraction.ML.Util.ml_module_name_of_lid m in @@ -83,15 +84,19 @@ let load_native_tactics () = else //else try to find and compile the ml file match Find.find_file_odir (ml_file m) with | None -> - E.raise_error0 E.Fatal_FailToCompileNativeTactic - (Util.format1 "Failed to compile native tactic; extracted module %s not found" (ml_file m)) + E.raise_error0 E.Fatal_FailToCompileNativeTactic [ + text "Failed to compile native tactic."; + text (format1 "Extracted module %s not found." (ml_file m)) + ] | Some ml -> let dir = Util.dirname ml in Plugins.compile_modules dir [ml_module_name m]; begin match Find.find_file_odir cmxs with | None -> - E.raise_error0 E.Fatal_FailToCompileNativeTactic - (Util.format1 "Failed to compile native tactic; compiled object %s not found" cmxs) + E.raise_error0 E.Fatal_FailToCompileNativeTactic [ + text "Failed to compile native tactic."; + text (format1 "Compilation seemingly succeeded, but compiled object %s not found." cmxs); + ] | Some f -> f end in From 9dbaa4101d748c8e9614b582c4aac8b04c68998c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 11 Feb 2025 19:08:59 -0800 Subject: [PATCH 2/4] PrintML: nit --- src/extraction/FStarC.Extraction.ML.PrintML.fsti | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/extraction/FStarC.Extraction.ML.PrintML.fsti b/src/extraction/FStarC.Extraction.ML.PrintML.fsti index 78c4b3054ef..e5af849b555 100644 --- a/src/extraction/FStarC.Extraction.ML.PrintML.fsti +++ b/src/extraction/FStarC.Extraction.ML.PrintML.fsti @@ -17,4 +17,8 @@ module FStarC.Extraction.ML.PrintML open FStarC.Extraction.ML.Syntax -val print: option string -> string -> mllib -> unit +val print + (odir : option string) + (extension : string) + (defs : mllib) + : unit From c9388fe214f0e879fb76416ddbdd5deb57f97dc4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 11 Feb 2025 13:52:57 -0800 Subject: [PATCH 3/4] IDE: nit, show instances --- src/interactive/FStarC.Interactive.Ide.Types.fst | 16 ++++++++-------- .../FStarC.Interactive.Ide.Types.fsti | 2 ++ src/interactive/FStarC.Interactive.Ide.fst | 2 ++ 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/interactive/FStarC.Interactive.Ide.Types.fst b/src/interactive/FStarC.Interactive.Ide.Types.fst index ce0a22a29d8..b9603313f3b 100644 --- a/src/interactive/FStarC.Interactive.Ide.Types.fst +++ b/src/interactive/FStarC.Interactive.Ide.Types.fst @@ -38,6 +38,13 @@ module SS = FStarC.Syntax.Syntax let initial_range = Range.mk_range "" (Range.mk_pos 1 0) (Range.mk_pos 1 0) +instance showable_push_kind : showable push_kind = { + show = (function + | SyntaxCheck -> "SyntaxCheck" + | LaxCheck -> "LaxCheck" + | FullCheck -> "FullCheck"); +} + (*************************) (* REPL tasks and states *) (*************************) @@ -98,14 +105,7 @@ let repl_state_to_string (r:repl_state) | Some m -> Ident.string_of_lid m.name); string_of_repl_stack r.repl_deps_stack] - let push_query_to_string pq = - let pk = - match pq.push_kind with - | SyntaxCheck -> "SyntaxCheck" - | LaxCheck -> "LaxCheck" - | FullCheck -> "FullCheck" - in let code_or_decl = match pq.push_code_or_decl with | Inl code -> code @@ -113,7 +113,7 @@ let push_query_to_string pq = in FStarC.Util.format "{ push_kind = %s; push_line = %s; \ push_column = %s; push_peek_only = %s; push_code_or_decl = %s }" - [pk; string_of_int pq.push_line; + [show pq.push_kind; string_of_int pq.push_line; string_of_int pq.push_column; string_of_bool pq.push_peek_only; code_or_decl] diff --git a/src/interactive/FStarC.Interactive.Ide.Types.fsti b/src/interactive/FStarC.Interactive.Ide.Types.fsti index 471a740eb8b..6f0a3a73d7d 100644 --- a/src/interactive/FStarC.Interactive.Ide.Types.fsti +++ b/src/interactive/FStarC.Interactive.Ide.Types.fsti @@ -36,6 +36,8 @@ val initial_range : range type push_kind = | SyntaxCheck | LaxCheck | FullCheck +instance val showable_push_kind : Class.Show.showable push_kind + type completion_context = | CKCode | CKOption of bool (* #set-options (false) or #reset-options (true) *) diff --git a/src/interactive/FStarC.Interactive.Ide.fst b/src/interactive/FStarC.Interactive.Ide.fst index 3d4ad6bf2ca..06be3bbda19 100644 --- a/src/interactive/FStarC.Interactive.Ide.fst +++ b/src/interactive/FStarC.Interactive.Ide.fst @@ -29,6 +29,8 @@ open FStarC.Interactive.PushHelper open FStarC.Interactive.Ide.Types module BU = FStarC.Util +open FStarC.Class.Show + let dbg = Debug.get_toggle "IDE" open FStarC.Universal From 83a859d73bb95b05c59187c4d50b8982dae45ecc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 11 Feb 2025 19:37:38 -0800 Subject: [PATCH 4/4] Parser.Dep: nits --- src/parser/FStarC.Parser.Dep.fst | 8 ++------ src/parser/FStarC.Parser.Dep.fsti | 1 - 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index 4e6e3a962fb..6a24c38533a 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -25,12 +25,8 @@ module FStarC.Parser.Dep open FStarC open FStarC.Effect //for ref, failwith etc open FStarC.List -open FStarC.Parser open FStarC.Parser.AST -open FStarC.Util open FStarC.Const -open FStar.String -open FStarC.Ident open FStarC.Errors open FStarC.Class.Show @@ -142,10 +138,10 @@ let module_name_of_file f = let lowercase_module_name f = String.lowercase (module_name_of_file f) let namespace_of_module f = - let lid = FStarC.Ident.lid_of_path (FStarC.Ident.path_of_text f) Range.dummyRange in + let lid = Ident.lid_of_path (Ident.path_of_text f) Range.dummyRange in match ns_of_lid lid with | [] -> None - | ns -> Some (FStarC.Ident.lid_of_ids ns) + | ns -> Some (Ident.lid_of_ids ns) type file_name = string type dependence = diff --git a/src/parser/FStarC.Parser.Dep.fsti b/src/parser/FStarC.Parser.Dep.fsti index dd9749ef59b..086e10c15c7 100644 --- a/src/parser/FStarC.Parser.Dep.fsti +++ b/src/parser/FStarC.Parser.Dep.fsti @@ -17,7 +17,6 @@ module FStarC.Parser.Dep open FStarC open FStarC.Effect -open FStarC.Parser.AST open FStarC.Util open FStarC.Ident