Skip to content

Commit

Permalink
add optional JSON output of error messages for LSP integration
Browse files Browse the repository at this point in the history
  • Loading branch information
wies committed Nov 21, 2024
1 parent d9d4578 commit 1af4ae6
Show file tree
Hide file tree
Showing 3 changed files with 45 additions and 13 deletions.
35 changes: 22 additions & 13 deletions bin/raven.ml
Original file line number Diff line number Diff line change
Expand Up @@ -283,32 +283,41 @@ let typecheck_only =
let doc = "Only type-check input program but do not verify it." in
Arg.(value & flag & info [ "typeonly" ] ~doc)

let lsp_mode =
let doc = "Format error messages for LSP integration." in
Arg.(value & flag & info [ "lsp-mode" ] ~doc)

let smt_timeout =
let doc = "Timeout for SMT solver in ms." in
Arg.(value & opt int 10000 & info [ "smt-timeout" ] ~doc)

let greeting = "Raven version " ^ Config.version

let main () input_files no_greeting no_library typecheck_only prog_stats smt_timeout smt_diagnostics =
let print_errors lsp_mode errs =
if lsp_mode then begin
Stdlib.print_endline (Error.errors_to_lsp_string errs);
Stdlib.exit 0
end
else begin
List.iter errs ~f:(fun e -> Logs.err (fun m -> m !"%{Error}" e));
Logs.debug (fun m ->
m "\n---------\n%s"
@@ Backtrace.to_string (Backtrace.Exn.most_recent ()));
Stdlib.exit 1 (* duplicates error output: `Error (false, "") *)
end

let main () input_files no_greeting no_library typecheck_only lsp_mode prog_stats smt_timeout smt_diagnostics =
if not no_greeting then Logs.app (fun m -> m "%s" greeting) else ();
try `Ok (parse_and_check_all typecheck_only smt_timeout smt_diagnostics no_library prog_stats input_files) with
| Sys_error s | Failure s | Invalid_argument s ->
Logs.err (fun m -> m "%s" s);
Logs.debug (fun m ->
m "\n---------\n%s"
@@ Backtrace.to_string (Backtrace.Exn.most_recent ()));
Stdlib.exit 1 (* `Error (false, s) <- duplicates error output *)
print_errors lsp_mode [Internal, Loc.dummy, s]
| Error.Msg es ->
List.iter es ~f:(fun e -> Logs.err (fun m -> m !"%{Error}" e));
Logs.debug (fun m ->
m "\n---------\n%s"
@@ Backtrace.to_string (Backtrace.Exn.most_recent ()));
Stdlib.exit 1 (* duplicates error output: `Error (false, "") *)

print_errors lsp_mode es

let main_cmd =
let info = Cmd.info "raven" ~version:Config.version in
Cmd.v info
Term.(
ret (const main $ setup_config $ input_file $ no_greeting $ no_library $ typecheck_only $ prog_stats $ smt_timeout $ smt_diagnostics))
ret (const main $ setup_config $ input_file $ no_greeting $ no_library $ typecheck_only $ lsp_mode $ prog_stats $ smt_timeout $ smt_diagnostics))

let () = Stdlib.exit (Cmd.eval main_cmd)
19 changes: 19 additions & 0 deletions lib/util/error.ml
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,17 @@ type error_kind =
| Verification
| RelatedLoc

let error_kind_to_lsp_string = function
| Generic -> "Generic"
| Lexical -> "Lexical"
| Syntax -> "Syntax"
| Type -> "Type"
| Internal -> "Internal"
| Unsupported -> "Unsupported"
| Verification -> "Verification"
| RelatedLoc -> "RelatedLoc"


let error_kind_to_string = function
| Generic -> "Error"
| Lexical -> "Lexical Error"
Expand Down Expand Up @@ -44,6 +55,14 @@ let to_string (kind, (loc : Loc.t), msg) =
then Printf.sprintf "%s:%s" (flycheck_string_of_src_pos pos) msg*)
Printf.sprintf !"%{Loc}%{String}%{String}." loc label msg

let to_lsp_string ppf (kind, (loc : Loc.t), msg) =
Stdlib.Format.fprintf ppf !"@\n{ \"file\": \"%{String}\", \"start_line\": %d, \"start_col\": %d, \"end_line\": %d, \"end_col\": %d, \"kind\": \"%s\", \"message\": \"%s\" }"
(Loc.file_name loc) (Loc.start_line loc) (Loc.start_col loc) (Loc.end_line loc) (Loc.end_col loc) (error_kind_to_lsp_string kind) msg

let errors_to_lsp_string errs =
let print_list ppf errs = Stdlib.Format.fprintf ppf "[@[<2>%a@]]" (Print.pr_list_comma to_lsp_string) errs in
Print.string_of_format print_list errs

(** Predefined error messags *)

let internal_error loc msg = fail loc ~lbl:Internal msg
Expand Down
4 changes: 4 additions & 0 deletions lib/util/loc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,10 @@ let file_name loc = loc.loc_start.pos_fname
let to_end loc = { loc with loc_start = loc.loc_end }
let to_start loc = { loc with loc_end = loc.loc_start }

let start_index loc = loc.loc_start.pos_cnum
let end_index loc = loc.loc_end.pos_cnum


let merge l1 l2 =
assert (String.equal (file_name l1) (file_name l2));
let spos =
Expand Down

0 comments on commit 1af4ae6

Please sign in to comment.