diff --git a/dune-project b/dune-project index 85f142616..435605d30 100644 --- a/dune-project +++ b/dune-project @@ -19,6 +19,10 @@ dune dune-build-info dune-site + fmt + logs + lsp + lwt markdown (pcre2 (>= 8)) (why3 (and (>= 1.8.0) (< 1.9))) diff --git a/easycrypt.opam b/easycrypt.opam index 08bdb40ea..92b556b97 100644 --- a/easycrypt.opam +++ b/easycrypt.opam @@ -7,6 +7,10 @@ depends: [ "dune" {>= "3.13"} "dune-build-info" "dune-site" + "fmt" + "logs" + "lsp" + "lwt" "markdown" "pcre2" {>= "8"} "why3" {>= "1.8.0" & < "1.9"} diff --git a/src/dune b/src/dune index 487e9cfcf..53c3a9b40 100644 --- a/src/dune +++ b/src/dune @@ -16,7 +16,7 @@ (public_name easycrypt.ecLib) (foreign_stubs (language c) (names eunix)) (modules :standard \ ec) - (libraries batteries camlp-streams dune-build-info dune-site inifiles markdown markdown.html pcre2 tyxml why3 yojson zarith) + (libraries batteries camlp-streams dune-build-info dune-site inifiles logs logs.fmt lsp lwt lwt.unix markdown markdown.html pcre2 tyxml why3 yojson zarith) ) (executable @@ -24,7 +24,8 @@ (name ec) (modules ec) (promote (until-clean)) - (libraries batteries camlp-streams dune-build-info dune-site inifiles pcre2 why3 yojson zarith ecLib)) + (libraries batteries ecLib) +) (ocamllex ecLexer) diff --git a/src/ec.ml b/src/ec.ml index 627d25b81..6820fcf17 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -214,6 +214,9 @@ let main () = (* Execution of eager commands *) begin match options.o_command with + | `Lsp -> + EcLsp.run (); + exit 0 | `Runtest input -> begin let root = match EcRelocate.sourceroot with @@ -535,6 +538,9 @@ let main () = | `Runtest _ -> (* Eagerly executed *) assert false + | `Lsp -> + (* Eagerly executed *) + assert false | `DocGen docopts -> begin let name = docopts.doco_input in diff --git a/src/ecIo.ml b/src/ecIo.ml index 016545d85..d6fd6f498 100644 --- a/src/ecIo.ml +++ b/src/ecIo.ml @@ -96,14 +96,15 @@ let from_string data = let finalize (ecreader : ecreader) = Disposable.dispose ecreader +(* -------------------------------------------------------------------- *) +let isfinal_token = function + | EcParser.FINAL _ -> true + | _ -> false + (* -------------------------------------------------------------------- *) let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) = let lexbuf = ecreader.ecr_lexbuf in - let isfinal = function - | EcParser.FINAL _ -> true - | _ -> false in - if ecreader.ecr_atstart then ecreader.ecr_trim <- ecreader.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum; @@ -134,7 +135,7 @@ let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) = ecreader.ecr_tokens <- prequeue @ queue; - if isfinal token then + if isfinal_token token then ecreader.ecr_atstart <- true else ecreader.ecr_atstart <- ecreader.ecr_atstart && ( @@ -177,6 +178,42 @@ let parse (ecreader : ecreader) : EcParsetree.prog = in parse (EcParser.Incremental.prog ecreader.ecr_lexbuf.lex_curr_p) +(* -------------------------------------------------------------------- *) +let next_sentence_from (text : string) (start : int) : (string * int * int) option = + let len = String.length text in + if start < 0 || start >= len then + None + else + let sub = String.sub text start (len - start) in + let reader = from_string sub in + let ecr = Disposable.get reader in + + let exception EOF in + + Fun.protect + ~finally:(fun () -> finalize reader) + (fun () -> + try + begin + let exception Done in + + try + while true do + match proj3_1 (lexer ecr) with + | EcParser.FINAL _ -> raise Done + | EcParser.EOF -> raise EOF + | _ -> () + done + with Done -> () + end; + + let p = ecr.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum - 1 in + let s = String.sub sub 0 p in + + Some (s, start, start + p) + with + | EcLexer.LexicalError _ | EOF -> None) + (* -------------------------------------------------------------------- *) let xparse (ecreader : ecreader) : string * EcParsetree.prog = let ecr = Disposable.get ecreader in diff --git a/src/ecIo.mli b/src/ecIo.mli index 42d28ba74..f69a371b6 100644 --- a/src/ecIo.mli +++ b/src/ecIo.mli @@ -13,6 +13,7 @@ val parse : ecreader -> EcParsetree.prog val parseall : ecreader -> EcParsetree.global list val drain : ecreader -> unit val lexbuf : ecreader -> Lexing.lexbuf +val next_sentence_from : string -> int -> (string * int * int) option (* -------------------------------------------------------------------- *) val lex_single_token : string -> EcParser.token option diff --git a/src/ecLsp.ml b/src/ecLsp.ml new file mode 100644 index 000000000..1057b9a11 --- /dev/null +++ b/src/ecLsp.ml @@ -0,0 +1,631 @@ +open Lwt.Syntax + +module Json = Yojson.Safe +module J = Yojson.Safe.Util + +module Lsp_io = + Lsp.Io.Make + (struct + type 'a t = 'a + + let return x = x + let raise = Stdlib.raise + + module O = struct + let ( let+ ) x f = f x + let ( let* ) x f = f x + end + end) + (struct + type input = in_channel + type output = out_channel + + let read_line ic = + try Some (input_line ic) with End_of_file -> None + + let read_exactly ic len = + try Some (really_input_string ic len) with End_of_file -> None + + let write oc chunks = + List.iter (output_string oc) chunks; + flush oc + end) + +let setup_logging () : unit = + let reporter = + match Sys.getenv_opt "EASYCRYPT_LSP_LOG" with + | None -> Logs_fmt.reporter () + | Some path -> ( + try + let oc = + open_out_gen [ Open_creat; Open_text; Open_append ] 0o644 path + in + Logs_fmt.reporter ~dst:(Format.formatter_of_out_channel oc) () + with e -> + prerr_endline ("[easycrypt-lsp] failed to open log file: " ^ Printexc.to_string e); + Logs_fmt.reporter ()) + in + Logs.set_reporter reporter; + Logs.set_level (Some Logs.Info) + +let log (fmt : ('a, Format.formatter, unit, unit) format4) = + Format.kasprintf (fun msg -> Logs.info (fun m -> m "%s" msg)) fmt + +module Easycrypt_cli = struct + type session = { + proc : Lwt_process.process; + mutable uuid : int; + mutable mode : string; + mutable last_output : string; + root_uuid : int; + } + + type config = { + mutable cli_path : string; + mutable cli_args : string list; + } + + let prompt_re : Pcre2.regexp = + Pcre2.regexp "\\[([0-9]+)\\|([^\\]]+)\\]>" + + let parse_prompt (line : string) : (int * string) option = + try + let subs = Pcre2.exec ~rex:prompt_re line in + let uuid_str = Pcre2.get_substring subs 1 in + let mode = Pcre2.get_substring subs 2 in + Some (int_of_string uuid_str, mode) + with + | Not_found -> None + | Pcre2.Error _ -> None + + let default_cli_path () : string = + if Sys.file_exists "ec.native" then + "./ec.native" + else + "easycrypt" + + let read_until_prompt (sess : session) : string Lwt.t = + let buf = Buffer.create 256 in + let rec loop () = + let* line_opt = Lwt_io.read_line_opt sess.proc#stdout in + match line_opt with + | None -> Lwt.return (Buffer.contents buf) + | Some line -> + log "cli + sess.uuid <- uuid; + sess.mode <- mode; + Lwt.return (Buffer.contents buf) + | None -> + Buffer.add_string buf line; + Buffer.add_char buf '\n'; + loop ()) + in + loop () + + let start_session_lwt (cfg : config) : session Lwt.t = + let argv = + let args = "cli" :: "-emacs" :: cfg.cli_args in + Array.of_list (cfg.cli_path :: args) + in + let proc = Lwt_process.open_process (cfg.cli_path, argv) in + let sess = + { proc + ; uuid = 0 + ; mode = "" + ; last_output = "" + ; root_uuid = 0 + } + in + let* _initial_output = read_until_prompt sess in + Lwt.return { sess with root_uuid = sess.uuid } + + let start_session (cfg : config) : session = + Lwt_main.run (start_session_lwt cfg) + + let send_command_lwt (sess : session) (text : string) : string Lwt.t = + log "cli> %s" (String.trim text); + let write = + if String.ends_with ~suffix:"\n" text then + Lwt_io.write sess.proc#stdin text + else + Lwt_io.write_line sess.proc#stdin text + in + let* () = write in + let* () = Lwt_io.flush sess.proc#stdin in + let* output = read_until_prompt sess in + sess.last_output <- output; + let preview = + if String.length output = 0 then "" + else if String.length output <= 200 then String.escaped output + else String.escaped (String.sub output 0 200) ^ "..." + in + log "cli< (%d bytes) %s" (String.length output) preview; + Lwt.return output + + let send_command (sess : session) (text : string) : string = + Lwt_main.run (send_command_lwt sess text) + + let send_undo_lwt (sess : session) (target_uuid : int) : string Lwt.t = + let cmd = Printf.sprintf "undo %d." target_uuid in + send_command_lwt sess cmd + + let send_undo (sess : session) (target_uuid : int) : string = + Lwt_main.run (send_undo_lwt sess target_uuid) + + let stop_session_lwt (sess : session) : unit Lwt.t = + let close_chan ch = Lwt.catch (fun () -> Lwt_io.close ch) (fun _ -> Lwt.return_unit) in + let* () = close_chan sess.proc#stdin in + let* () = close_chan sess.proc#stdout in + sess.proc#terminate; + let* _status = sess.proc#status in + Lwt.return_unit + + let stop_session (sess : session) : unit = + Lwt_main.run (stop_session_lwt sess) +end + +type doc_state = { + mutable text : BatText.t; + mutable last_offset : int; + mutable history : (int * int) list; + mutable session : Easycrypt_cli.session option; +} + +let doc_states : (string, doc_state) Hashtbl.t = Hashtbl.create 16 + +let get_doc_state (uri : string) : doc_state = + match Hashtbl.find_opt doc_states uri with + | Some state -> state + | None -> + let created = { text = BatText.empty; last_offset = 0; history = []; session = None } in + Hashtbl.add doc_states uri created; + created + +let error_tag_re : Pcre2.regexp = + Pcre2.regexp "\\[error-\\d+-\\d+\\]" + +let output_has_error (output : string) : bool = + Pcre2.pmatch ~rex:error_tag_re output + +let find_next_sentence + (text : BatText.t) + (start : int) : (string * int * int) option = + EcIo.next_sentence_from (BatText.to_string text) start + +let position_to_offset (text : BatText.t) (pos : Lsp.Types.Position.t) : int = + let len = BatText.length text in + let target_line = pos.Lsp.Types.Position.line in + let target_col = pos.Lsp.Types.Position.character in + let newline = BatUChar.of_char '\n' in + let rec find_line_start line current = + if line <= 0 then + current + else + try + let idx = BatText.index_from text current newline in + find_line_start (line - 1) (min (idx + 1) len) + with + | Not_found -> len + | BatText.Out_of_bounds -> len + in + let line_start = find_line_start target_line 0 in + if line_start >= len then + len + else + let offset = line_start + target_col in + if offset > len then len else offset + +let apply_change + (text : BatText.t) + (change : Lsp.Types.TextDocumentContentChangeEvent.t) : BatText.t * int = + match change.Lsp.Types.TextDocumentContentChangeEvent.range with + | None -> + BatText.of_string change.Lsp.Types.TextDocumentContentChangeEvent.text, 0 + | Some range -> + let start_offset = position_to_offset text range.Lsp.Types.Range.start in + let end_offset = position_to_offset text range.Lsp.Types.Range.end_ in + let len = BatText.length text in + let start_offset = max 0 (min start_offset len) in + let end_offset = max start_offset (min end_offset len) in + let removed = BatText.remove start_offset (end_offset - start_offset) text in + let inserted = BatText.of_string change.Lsp.Types.TextDocumentContentChangeEvent.text in + (BatText.insert start_offset inserted removed, start_offset) + +let json_of_proof_response + ~(sess : Easycrypt_cli.session) + ~(doc : doc_state) + ?sentence + (output : string) : Json.t = + let sentence_start, sentence_end = + match sentence with + | None -> (`Null, `Null) + | Some (start, end_) -> (`Int start, `Int end_) + in + `Assoc + [ ("output", `String output) + ; ("uuid", `Int sess.uuid) + ; ("mode", `String sess.mode) + ; ("processedEnd", `Int doc.last_offset) + ; ("sentenceStart", sentence_start) + ; ("sentenceEnd", sentence_end) + ] + +type proof_command_kind = + | Proof_next + | Proof_step + | Proof_jump_to of int + | Proof_back + | Proof_restart + | Proof_goals + +type proof_command = + { uri : string + ; cmd : proof_command_kind + } + +let proof_command_of_request (meth : string) (params : Json.t option) : + (proof_command, string) result = + let get_uri json = + match J.member "uri" json with + | `String uri -> uri + | _ -> "" + in + match meth, params with + | "easycrypt/proof/next", Some (`Assoc _ as json) -> + let uri = get_uri json in + if uri = "" then Error "missing uri" else Ok { uri; cmd = Proof_next } + | "easycrypt/proof/step", Some (`Assoc _ as json) -> + let uri = get_uri json in + if uri = "" then Error "missing uri" else Ok { uri; cmd = Proof_step } + | "easycrypt/proof/jumpTo", Some (`Assoc _ as json) -> + let uri = get_uri json in + let target = + try J.member "target" json |> J.to_int with _ -> -1 + in + if uri = "" || target < 0 then + Error "missing uri or target" + else + Ok { uri; cmd = Proof_jump_to target } + | "easycrypt/proof/back", Some (`Assoc _ as json) -> + let uri = get_uri json in + if uri = "" then Error "missing uri" else Ok { uri; cmd = Proof_back } + | "easycrypt/proof/restart", Some (`Assoc _ as json) -> + let uri = get_uri json in + if uri = "" then Error "missing uri" else Ok { uri; cmd = Proof_restart } + | "easycrypt/proof/goals", Some (`Assoc _ as json) -> + let uri = get_uri json in + if uri = "" then Error "missing uri" else Ok { uri; cmd = Proof_goals } + | _ -> Error "Method not found" + +let rewind_to_offset + (doc : doc_state) + (sess : Easycrypt_cli.session) + (target : int) : string option = + if target >= doc.last_offset then + None + else + let rec last_before acc = function + | [] -> acc + | (offset, uuid) :: rest -> + let acc = if offset <= target then Some (offset, uuid) else acc in + last_before acc rest + in + let target_entry = last_before None doc.history in + let target_uuid, new_offset = + match target_entry with + | None -> sess.root_uuid, 0 + | Some (offset, uuid) -> uuid, offset + in + doc.history <- List.filter (fun (offset, _) -> offset <= new_offset) doc.history; + doc.last_offset <- new_offset; + Some (Easycrypt_cli.send_undo sess target_uuid) + +let send_packet (oc : out_channel) (packet : Jsonrpc.Packet.t) = + Lsp_io.write oc packet + +let send_response (oc : out_channel) (id : Jsonrpc.Id.t) (result : Jsonrpc.Json.t) = + let response = Jsonrpc.Response.ok id result in + send_packet oc (Jsonrpc.Packet.Response response) + +let send_typed_response + (oc : out_channel) + (id : Jsonrpc.Id.t) + (req : 'a Lsp.Client_request.t) + (result : 'a) = + let payload = Lsp.Client_request.yojson_of_result req result in + send_response oc id payload + +let send_error + (oc : out_channel) + (id : Jsonrpc.Id.t) + (code : Jsonrpc.Response.Error.Code.t) + (message : string) = + let error = + Jsonrpc.Response.Error.make + ~code + ~message + () + in + let response = Jsonrpc.Response.error id error in + send_packet oc (Jsonrpc.Packet.Response response) + +let send_notification (oc : out_channel) (method_ : string) (params : Jsonrpc.Json.t) = + let params_struct = Jsonrpc.Structured.t_of_yojson params in + let notif = Jsonrpc.Notification.create ~params:params_struct ~method_ () in + send_packet oc (Jsonrpc.Packet.Notification notif) + +let run () : unit = + Sys.set_signal Sys.sigpipe Sys.Signal_ignore; + setup_logging (); + log "argv=%s" (String.concat " " (Array.to_list Sys.argv)); + log "server start"; + let argv = Array.to_list Sys.argv in + let cli_path = + match argv with + | prog :: _ -> prog + | [] -> Easycrypt_cli.default_cli_path () + in + let cfg : Easycrypt_cli.config = { cli_path; cli_args = []; } in + let ic = stdin in + let oc = stdout in + let shutdown = ref false in + + let get_session_for_doc (doc : doc_state) : Easycrypt_cli.session = + match doc.session with + | Some sess -> sess + | None -> + let sess = Easycrypt_cli.start_session cfg in + doc.session <- Some sess; + sess + in + + let handle_initialize id (params : Lsp.Types.InitializeParams.t) = + log "initialize"; + let capabilities = + Lsp.Types.ServerCapabilities.create + ~textDocumentSync:(`TextDocumentSyncKind Lsp.Types.TextDocumentSyncKind.Incremental) + () + in + let result = Lsp.Types.InitializeResult.create ~capabilities () in + send_typed_response oc id (Lsp.Client_request.Initialize params) result + in + + let handle_proof_next id uri = + log "proof next"; + let doc = get_doc_state uri in + let sess = get_session_for_doc doc in + match find_next_sentence doc.text doc.last_offset with + | None -> + send_response oc id (json_of_proof_response ~sess ~doc sess.last_output) + | Some (_text, start, end_) -> + send_response oc id (json_of_proof_response ~sess ~doc ~sentence:(start, end_) sess.last_output) + in + + let handle_proof_exec id uri = + log "proof exec"; + let doc = get_doc_state uri in + match find_next_sentence doc.text doc.last_offset with + | None -> + let sess = get_session_for_doc doc in + send_response oc id (json_of_proof_response ~sess ~doc sess.last_output) + | Some (text, start, end_) -> ( + let previous_offset = doc.last_offset in + try + let rec run ~retry = + let sess = get_session_for_doc doc in + try (sess, Easycrypt_cli.send_command sess text) with + | Sys_error msg when retry && String.lowercase_ascii msg = "broken pipe" -> + log "cli broken pipe; restarting session"; + doc.session <- None; + run ~retry:false + in + let sess, output = run ~retry:true in + if output_has_error output then ( + doc.last_offset <- previous_offset; + send_response oc id + (json_of_proof_response ~sess ~doc ~sentence:(start, end_) output)) + else ( + doc.last_offset <- end_; + doc.history <- doc.history @ [ (doc.last_offset, sess.uuid) ]; + send_response oc id + (json_of_proof_response ~sess ~doc ~sentence:(start, end_) output)) + with e -> + log "proof exec error: %s" (Printexc.to_string e); + send_error oc id Jsonrpc.Response.Error.Code.InternalError "proof exec failed") + in + + let handle_proof_jump id uri target = + log "proof jump"; + let doc = get_doc_state uri in + let sess = get_session_for_doc doc in + let text_len = BatText.length doc.text in + let target = max 0 (min target text_len) in + let respond ?sentence output = + send_response oc id (json_of_proof_response ~sess ~doc ?sentence output) + in + if target < doc.last_offset then ( + let rec last_before acc = function + | [] -> acc + | (offset, uuid) :: rest -> + let acc = if offset <= target then Some (offset, uuid) else acc in + last_before acc rest + in + let target_entry = last_before None doc.history in + let target_uuid, new_offset = + match target_entry with + | None -> sess.root_uuid, 0 + | Some (offset, uuid) -> uuid, offset + in + doc.history <- List.filter (fun (offset, _) -> offset <= new_offset) doc.history; + doc.last_offset <- new_offset; + let output = Easycrypt_cli.send_undo sess target_uuid in + respond output) + else if target = doc.last_offset then + respond sess.last_output + else ( + let rec loop last_output = + if doc.last_offset >= target then + respond last_output + else + match find_next_sentence doc.text doc.last_offset with + | None -> respond last_output + | Some (text, start, end_) -> + if end_ > target then + respond last_output + else + let previous_offset = doc.last_offset in + let output = Easycrypt_cli.send_command sess text in + if output_has_error output then ( + doc.last_offset <- previous_offset; + respond ~sentence:(start, end_) output) + else ( + doc.last_offset <- end_; + doc.history <- doc.history @ [ (doc.last_offset, sess.uuid) ]; + loop output) + in + loop sess.last_output) + in + + let handle_proof_back id uri = + log "proof back"; + let doc = get_doc_state uri in + let sess = get_session_for_doc doc in + match List.rev doc.history with + | [] -> + send_response oc id (json_of_proof_response ~sess ~doc sess.last_output) + | _last :: rest_rev -> + let target_uuid, new_offset = + match rest_rev with + | [] -> sess.root_uuid, 0 + | (offset, uuid) :: _ -> uuid, offset + in + let output = Easycrypt_cli.send_undo sess target_uuid in + doc.history <- List.rev rest_rev; + doc.last_offset <- new_offset; + send_response oc id (json_of_proof_response ~sess ~doc output) + in + + let handle_proof_restart id uri = + log "proof restart"; + let doc = get_doc_state uri in + let sess = get_session_for_doc doc in + let output = Easycrypt_cli.send_undo sess sess.root_uuid in + doc.history <- []; + doc.last_offset <- 0; + send_response oc id (json_of_proof_response ~sess ~doc output) + in + + let handle_proof_goals id uri = + log "proof goals"; + let doc = get_doc_state uri in + let sess = get_session_for_doc doc in + send_response oc id (json_of_proof_response ~sess ~doc sess.last_output) + in + + let execute_proof_command (id : Jsonrpc.Id.t) (cmd : proof_command) = + match cmd.cmd with + | Proof_next -> handle_proof_next id cmd.uri + | Proof_step -> handle_proof_exec id cmd.uri + | Proof_jump_to target -> handle_proof_jump id cmd.uri target + | Proof_back -> handle_proof_back id cmd.uri + | Proof_restart -> handle_proof_restart id cmd.uri + | Proof_goals -> handle_proof_goals id cmd.uri + in + + let handle_request req = + match Lsp.Client_request.of_jsonrpc req with + | Error message -> + send_error oc req.id Jsonrpc.Response.Error.Code.InvalidParams message + | Ok (Lsp.Client_request.E r) -> ( + match r with + | Lsp.Client_request.Initialize params -> + handle_initialize req.id params + | Lsp.Client_request.Shutdown -> + shutdown := true; + send_typed_response oc req.id r () + | Lsp.Client_request.UnknownRequest { meth; params } -> ( + let params = Option.map Jsonrpc.Structured.yojson_of_t params in + match proof_command_of_request meth params with + | Ok cmd -> execute_proof_command req.id cmd + | Error "Method not found" -> + send_error oc req.id Jsonrpc.Response.Error.Code.MethodNotFound "Method not found" + | Error message -> + send_error oc req.id Jsonrpc.Response.Error.Code.InvalidParams message) + | _ -> + send_error oc req.id Jsonrpc.Response.Error.Code.MethodNotFound "Method not found") + in + + let handle_notification_packet notif = + match Lsp.Client_notification.of_jsonrpc notif with + | Error _ -> () + | Ok notification -> ( + match notification with + | Lsp.Client_notification.Initialized -> () + | Lsp.Client_notification.Exit -> shutdown := true + | Lsp.Client_notification.TextDocumentDidOpen params -> + let uri = + Lsp.Types.DocumentUri.to_string + params.Lsp.Types.DidOpenTextDocumentParams.textDocument.uri + in + let doc = get_doc_state uri in + doc.text <- BatText.of_string params.Lsp.Types.DidOpenTextDocumentParams.textDocument.text; + doc.last_offset <- 0; + doc.history <- []; + doc.session <- None + | Lsp.Client_notification.TextDocumentDidChange params -> + let uri = + Lsp.Types.DocumentUri.to_string + params.Lsp.Types.DidChangeTextDocumentParams.textDocument.uri + in + let doc = get_doc_state uri in + let earliest = ref max_int in + let updated = ref doc.text in + List.iter + (fun change -> + let text, start_offset = apply_change !updated change in + updated := text; + if start_offset < !earliest then earliest := start_offset) + params.Lsp.Types.DidChangeTextDocumentParams.contentChanges; + doc.text <- !updated; + if !earliest < doc.last_offset then + let sess = get_session_for_doc doc in + ignore (rewind_to_offset doc sess !earliest) + | Lsp.Client_notification.TextDocumentDidClose params -> + let uri = + Lsp.Types.DocumentUri.to_string + params.Lsp.Types.DidCloseTextDocumentParams.textDocument.uri + in + (match Hashtbl.find_opt doc_states uri with + | Some doc -> Option.iter Easycrypt_cli.stop_session doc.session + | None -> ()); + Hashtbl.remove doc_states uri + | _ -> ()) + in + + while not !shutdown do + match Lsp_io.read ic with + | None -> + log "stdin closed"; + shutdown := true + | Some packet -> + (try + match packet with + | Jsonrpc.Packet.Request req -> + log "recv request %s" req.Jsonrpc.Request.method_; + handle_request req + | Jsonrpc.Packet.Notification notif -> + log "recv notification %s" notif.Jsonrpc.Notification.method_; + handle_notification_packet notif + | Jsonrpc.Packet.Batch_call calls -> + List.iter + (function + | `Request req -> handle_request req + | `Notification notif -> handle_notification_packet notif) + calls + | Jsonrpc.Packet.Response _ -> () + | Jsonrpc.Packet.Batch_response _ -> () + with e -> + log "error: %s" (Printexc.to_string e)) + done diff --git a/src/ecLsp.mli b/src/ecLsp.mli new file mode 100644 index 000000000..733b2a323 --- /dev/null +++ b/src/ecLsp.mli @@ -0,0 +1 @@ +val run : unit -> unit diff --git a/src/ecOptions.ml b/src/ecOptions.ml index f012e8e8d..c9b54139f 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -6,10 +6,12 @@ open EcMaps type command = [ | `Compile of cmp_option | `Cli of cli_option + | `Lsp | `Config | `Runtest of run_option | `Why3Config | `DocGen of doc_option + | `Lsp ] and options = { @@ -356,6 +358,9 @@ let specs = { `Group "provers"; `Spec ("emacs", `Flag, "Output format set to ")]); + ("lsp", "Run EasyCrypt LSP server", [ + `Spec ("-stdio" , `Flag , "")]); + ("config", "Print EasyCrypt configuration", []); ("runtest", "Run a test-suite", [ @@ -604,6 +609,15 @@ let parse getini argv = raise (Arg.Bad "this command takes a single input file as argument") end + | "lsp" -> + if not (List.is_empty anons) then + raise (Arg.Bad "this command does not take arguments"); + + let ini = getini None in + let cmd = `Lsp in + + (cmd, ini, true) + | _ -> assert false in { diff --git a/src/ecOptions.mli b/src/ecOptions.mli index 59009718a..c6aaa4d14 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -2,6 +2,7 @@ type command = [ | `Compile of cmp_option | `Cli of cli_option + | `Lsp | `Config | `Runtest of run_option | `Why3Config diff --git a/src/ecTerminal.ml b/src/ecTerminal.ml index 94f7c048e..f680719f1 100644 --- a/src/ecTerminal.ml +++ b/src/ecTerminal.ml @@ -90,7 +90,7 @@ object(self) | EcScope.TopError (loc, e) -> (loc, e) | _ -> (LC._dummy, e) in - Format.fprintf Format.err_formatter + Format.fprintf Format.std_formatter "[error-%d-%d]%s\n%!" (max 0 (loc.LC.loc_bchar - startpos)) (max 0 (loc.LC.loc_echar - startpos)) diff --git a/vscode/.gitignore b/vscode/.gitignore new file mode 100644 index 000000000..82abfab5c --- /dev/null +++ b/vscode/.gitignore @@ -0,0 +1,2 @@ +/node_modules/ +/out/ diff --git a/vscode/README.md b/vscode/README.md new file mode 100644 index 000000000..0c3ac44c8 --- /dev/null +++ b/vscode/README.md @@ -0,0 +1,46 @@ +# EasyCrypt VSCode Extension (local) + +This folder contains a local VSCode extension for EasyCrypt. + +## Build the EasyCrypt binary (with LSP) + +From the repository root: + +``` +$ dune build src/ec.exe +``` + +The binary will be at `_build/default/src/ec.exe` and provides `easycrypt lsp`. + +## Build the extension + +From this `vscode/` folder: + +``` +$ npm install +$ npm run compile +``` + +Then use "Developer: Install Extension from Location..." and select this folder. + +## Configuration + +- `easycrypt.cli.path`: path to the EasyCrypt CLI (e.g. `ec.native` or `easycrypt`). + +## TextMate colors + +This extension uses TextMate scopes for syntax highlighting. To customize colors without changing a theme, add rules to your VSCode settings: + +```jsonc +"editor.tokenColorCustomizations": { + "textMateRules": [ + { "scope": "keyword.other.easycrypt.bytac", "settings": { "foreground": "#6C71C4" } }, + { "scope": "keyword.other.easycrypt.dangerous", "settings": { "foreground": "#DC322F", "fontStyle": "bold" } }, + { "scope": "keyword.control.easycrypt.global", "settings": { "foreground": "#268BD2" } }, + { "scope": "keyword.other.easycrypt.internal", "settings": { "foreground": "#B58900" } }, + { "scope": "keyword.operator.easycrypt.prog", "settings": { "foreground": "#2AA198" } }, + { "scope": "keyword.control.easycrypt.tactic", "settings": { "foreground": "#859900" } }, + { "scope": "keyword.control.easycrypt.tactical", "settings": { "foreground": "#CB4B16" } } + ] +} +``` diff --git a/vscode/assets/back.svg b/vscode/assets/back.svg new file mode 100644 index 000000000..63fa27643 --- /dev/null +++ b/vscode/assets/back.svg @@ -0,0 +1,3 @@ + + + diff --git a/vscode/assets/easycrypt.svg b/vscode/assets/easycrypt.svg new file mode 100644 index 000000000..f18030d31 --- /dev/null +++ b/vscode/assets/easycrypt.svg @@ -0,0 +1,5 @@ + + + + + diff --git a/vscode/assets/goals.svg b/vscode/assets/goals.svg new file mode 100644 index 000000000..fe6bd5048 --- /dev/null +++ b/vscode/assets/goals.svg @@ -0,0 +1,4 @@ + + + + diff --git a/vscode/assets/jump.svg b/vscode/assets/jump.svg new file mode 100644 index 000000000..daeb25d59 --- /dev/null +++ b/vscode/assets/jump.svg @@ -0,0 +1,3 @@ + + + diff --git a/vscode/assets/refresh.svg b/vscode/assets/refresh.svg new file mode 100644 index 000000000..d124bdd5c --- /dev/null +++ b/vscode/assets/refresh.svg @@ -0,0 +1,3 @@ + + + diff --git a/vscode/assets/step.svg b/vscode/assets/step.svg new file mode 100644 index 000000000..dd77f646a --- /dev/null +++ b/vscode/assets/step.svg @@ -0,0 +1,3 @@ + + + diff --git a/vscode/language-configuration.json b/vscode/language-configuration.json new file mode 100644 index 000000000..163424eeb --- /dev/null +++ b/vscode/language-configuration.json @@ -0,0 +1,23 @@ +{ + "comments": { + "lineComment": "//", + "blockComment": ["(*", "*)"] + }, + "brackets": [ + ["{", "}"], + ["[", "]"], + ["(", ")"] + ], + "autoClosingPairs": [ + {"open": "{", "close": "}"}, + {"open": "[", "close": "]"}, + {"open": "(", "close": ")"}, + {"open": "\"", "close": "\""} + ], + "surroundingPairs": [ + ["{", "}"], + ["[", "]"], + ["(", ")"], + ["\"", "\""] + ] +} diff --git a/vscode/package-lock.json b/vscode/package-lock.json new file mode 100644 index 000000000..7070c5862 --- /dev/null +++ b/vscode/package-lock.json @@ -0,0 +1,139 @@ +{ + "name": "easycrypt-vscode", + "version": "0.0.1", + "lockfileVersion": 3, + "requires": true, + "packages": { + "": { + "name": "easycrypt-vscode", + "version": "0.0.1", + "dependencies": { + "vscode-languageclient": "^9.0.1" + }, + "devDependencies": { + "@types/node": "^20.11.0", + "@types/vscode": "^1.85.0", + "typescript": "^5.3.3" + }, + "engines": { + "vscode": "^1.85.0" + } + }, + "node_modules/@types/node": { + "version": "20.19.30", + "resolved": "https://registry.npmjs.org/@types/node/-/node-20.19.30.tgz", + "integrity": "sha512-WJtwWJu7UdlvzEAUm484QNg5eAoq5QR08KDNx7g45Usrs2NtOPiX8ugDqmKdXkyL03rBqU5dYNYVQetEpBHq2g==", + "dev": true, + "license": "MIT", + "dependencies": { + "undici-types": "~6.21.0" + } + }, + "node_modules/@types/vscode": { + "version": "1.108.1", + "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.108.1.tgz", + "integrity": "sha512-DerV0BbSzt87TbrqmZ7lRDIYaMiqvP8tmJTzW2p49ZBVtGUnGAu2RGQd1Wv4XMzEVUpaHbsemVM5nfuQJj7H6w==", + "dev": true, + "license": "MIT" + }, + "node_modules/balanced-match": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.2.tgz", + "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw==", + "license": "MIT" + }, + "node_modules/brace-expansion": { + "version": "2.0.2", + "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-2.0.2.tgz", + "integrity": "sha512-Jt0vHyM+jmUBqojB7E1NIYadt0vI0Qxjxd2TErW94wDz+E2LAm5vKMXXwg6ZZBTHPuUlDgQHKXvjGBdfcF1ZDQ==", + "license": "MIT", + "dependencies": { + "balanced-match": "^1.0.0" + } + }, + "node_modules/minimatch": { + "version": "5.1.6", + "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-5.1.6.tgz", + "integrity": "sha512-lKwV/1brpG6mBUFHtb7NUmtABCb2WZZmm2wNiOA5hAb8VdCS4B3dtMWyvcoViccwAW/COERjXLt0zP1zXUN26g==", + "license": "ISC", + "dependencies": { + "brace-expansion": "^2.0.1" + }, + "engines": { + "node": ">=10" + } + }, + "node_modules/semver": { + "version": "7.7.3", + "resolved": "https://registry.npmjs.org/semver/-/semver-7.7.3.tgz", + "integrity": "sha512-SdsKMrI9TdgjdweUSR9MweHA4EJ8YxHn8DFaDisvhVlUOe4BF1tLD7GAj0lIqWVl+dPb/rExr0Btby5loQm20Q==", + "license": "ISC", + "bin": { + "semver": "bin/semver.js" + }, + "engines": { + "node": ">=10" + } + }, + "node_modules/typescript": { + "version": "5.9.3", + "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.9.3.tgz", + "integrity": "sha512-jl1vZzPDinLr9eUt3J/t7V6FgNEw9QjvBPdysz9KfQDD41fQrC2Y4vKQdiaUpFT4bXlb1RHhLpp8wtm6M5TgSw==", + "dev": true, + "license": "Apache-2.0", + "bin": { + "tsc": "bin/tsc", + "tsserver": "bin/tsserver" + }, + "engines": { + "node": ">=14.17" + } + }, + "node_modules/undici-types": { + "version": "6.21.0", + "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-6.21.0.tgz", + "integrity": "sha512-iwDZqg0QAGrg9Rav5H4n0M64c3mkR59cJ6wQp+7C4nI0gsmExaedaYLNO44eT4AtBBwjbTiGPMlt2Md0T9H9JQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/vscode-jsonrpc": { + "version": "8.2.0", + "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-8.2.0.tgz", + "integrity": "sha512-C+r0eKJUIfiDIfwJhria30+TYWPtuHJXHtI7J0YlOmKAo7ogxP20T0zxB7HZQIFhIyvoBPwWskjxrvAtfjyZfA==", + "license": "MIT", + "engines": { + "node": ">=14.0.0" + } + }, + "node_modules/vscode-languageclient": { + "version": "9.0.1", + "resolved": "https://registry.npmjs.org/vscode-languageclient/-/vscode-languageclient-9.0.1.tgz", + "integrity": "sha512-JZiimVdvimEuHh5olxhxkht09m3JzUGwggb5eRUkzzJhZ2KjCN0nh55VfiED9oez9DyF8/fz1g1iBV3h+0Z2EA==", + "license": "MIT", + "dependencies": { + "minimatch": "^5.1.0", + "semver": "^7.3.7", + "vscode-languageserver-protocol": "3.17.5" + }, + "engines": { + "vscode": "^1.82.0" + } + }, + "node_modules/vscode-languageserver-protocol": { + "version": "3.17.5", + "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.17.5.tgz", + "integrity": "sha512-mb1bvRJN8SVznADSGWM9u/b07H7Ecg0I3OgXDuLdn307rl/J3A9YD6/eYOssqhecL27hK1IPZAsaqh00i/Jljg==", + "license": "MIT", + "dependencies": { + "vscode-jsonrpc": "8.2.0", + "vscode-languageserver-types": "3.17.5" + } + }, + "node_modules/vscode-languageserver-types": { + "version": "3.17.5", + "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.17.5.tgz", + "integrity": "sha512-Ld1VelNuX9pdF39h2Hgaeb5hEZM2Z3jUrrMgWQAu82jMtZp7p3vJT3BzToKtZI7NgQssZje5o0zryOrhQvzQAg==", + "license": "MIT" + } + } +} diff --git a/vscode/package.json b/vscode/package.json new file mode 100644 index 000000000..4c1031c20 --- /dev/null +++ b/vscode/package.json @@ -0,0 +1,178 @@ +{ + "name": "easycrypt-vscode", + "displayName": "EasyCrypt", + "publisher": "easycrypt", + "version": "0.0.1", + "engines": { + "vscode": "^1.85.0" + }, + "categories": ["Programming Languages"], + "activationEvents": [ + "onLanguage:easycrypt", + "onCommand:easycrypt.proof.step", + "onCommand:easycrypt.proof.back", + "onCommand:easycrypt.proof.restart", + "onCommand:easycrypt.proof.jumpToCursor", + "onCommand:easycrypt.proof.goals", + "onCommand:easycrypt.lsp.restart" + ], + "main": "./out/extension.js", + "contributes": { + "languages": [ + { + "id": "easycrypt", + "aliases": ["EasyCrypt", "easycrypt"], + "extensions": [".ec"], + "configuration": "./language-configuration.json" + } + ], + "grammars": [ + { + "language": "easycrypt", + "scopeName": "source.easycrypt", + "path": "./syntaxes/easycrypt.tmLanguage.json" + } + ], + "commands": [ + { + "command": "easycrypt.proof.step", + "title": "Step", + "icon": { "light": "assets/step.svg", "dark": "assets/step.svg" } + }, + { + "command": "easycrypt.proof.back", + "title": "Back", + "icon": { "light": "assets/back.svg", "dark": "assets/back.svg" } + }, + { + "command": "easycrypt.proof.restart", + "title": "Restart", + "icon": { "light": "assets/refresh.svg", "dark": "assets/refresh.svg" } + }, + { + "command": "easycrypt.proof.jumpToCursor", + "title": "Jump To Cursor", + "icon": { "light": "assets/jump.svg", "dark": "assets/jump.svg" } + }, + { + "command": "easycrypt.proof.goals", + "title": "Show Goals", + "icon": { "light": "assets/goals.svg", "dark": "assets/goals.svg" } + }, + { + "command": "easycrypt.lsp.restart", + "title": "Restart LSP" + } + ], + "menus": { + "editor/title": [ + { + "command": "easycrypt.proof.step", + "when": "resourceLangId == easycrypt && config.easycrypt.ui.editorToolbarGroup == 'navigation'", + "group": "navigation.easycrypt@3" + }, + { + "command": "easycrypt.proof.step", + "when": "resourceLangId == easycrypt && config.easycrypt.ui.editorToolbarGroup == 'inline'", + "group": "inline.easycrypt@3" + }, + { + "command": "easycrypt.proof.back", + "when": "resourceLangId == easycrypt && config.easycrypt.ui.editorToolbarGroup == 'navigation'", + "group": "navigation.easycrypt@1" + }, + { + "command": "easycrypt.proof.back", + "when": "resourceLangId == easycrypt && config.easycrypt.ui.editorToolbarGroup == 'inline'", + "group": "inline.easycrypt@1" + }, + { + "command": "easycrypt.proof.jumpToCursor", + "when": "resourceLangId == easycrypt && config.easycrypt.ui.editorToolbarGroup == 'navigation'", + "group": "navigation.easycrypt@2" + }, + { + "command": "easycrypt.proof.jumpToCursor", + "when": "resourceLangId == easycrypt && config.easycrypt.ui.editorToolbarGroup == 'inline'", + "group": "inline.easycrypt@2" + }, + { + "command": "easycrypt.proof.goals", + "when": "resourceLangId == easycrypt && config.easycrypt.ui.editorToolbarGroup == 'navigation'", + "group": "navigation.easycrypt@4" + }, + { + "command": "easycrypt.proof.goals", + "when": "resourceLangId == easycrypt && config.easycrypt.ui.editorToolbarGroup == 'inline'", + "group": "inline.easycrypt@4" + } + ] + }, + "keybindings": [ + { + "command": "easycrypt.proof.step", + "key": "ctrl+alt+down", + "mac": "cmd+alt+down", + "when": "editorLangId == easycrypt" + }, + { + "command": "easycrypt.proof.back", + "key": "ctrl+alt+up", + "mac": "cmd+alt+up", + "when": "editorLangId == easycrypt" + }, + { + "command": "easycrypt.proof.jumpToCursor", + "key": "ctrl+alt+enter", + "mac": "cmd+alt+enter", + "when": "editorLangId == easycrypt" + }, + { + "command": "easycrypt.proof.goals", + "key": "ctrl+alt+g", + "mac": "cmd+alt+g", + "when": "editorLangId == easycrypt" + } + ], + "configuration": { + "title": "EasyCrypt", + "properties": { + "easycrypt.cli.path": { + "type": "string", + "default": "", + "description": "Path to the EasyCrypt CLI (easycrypt or ec.native)." + }, + "easycrypt.cli.args": { + "type": "array", + "items": { "type": "string" }, + "default": [], + "description": "Extra arguments passed to the EasyCrypt CLI when running in proof mode." + }, + "easycrypt.trace.server": { + "type": "string", + "enum": ["off", "messages", "verbose"], + "default": "off", + "description": "Trace LSP communication to the Output panel." + }, + "easycrypt.ui.editorToolbarGroup": { + "type": "string", + "enum": ["navigation", "inline"], + "default": "navigation", + "description": "Editor title toolbar group for EasyCrypt buttons." + } + } + } + }, + "scripts": { + "compile": "tsc -p ./", + "watch": "tsc -w -p ./" + }, + "dependencies": { + "vscode-languageclient": "^9.0.1" + }, + "devDependencies": { + "@types/node": "^20.11.0", + "@types/vscode": "^1.85.0", + "typescript": "^5.3.3" + } +} diff --git a/vscode/package.nls.json b/vscode/package.nls.json new file mode 100644 index 000000000..2da004d97 --- /dev/null +++ b/vscode/package.nls.json @@ -0,0 +1,3 @@ +{ + "easycrypt.ui.editorToolbarGroup": "Editor title toolbar group for EasyCrypt buttons." +} diff --git a/vscode/src/extension.ts b/vscode/src/extension.ts new file mode 100644 index 000000000..6c976a03f --- /dev/null +++ b/vscode/src/extension.ts @@ -0,0 +1,696 @@ +import * as fs from 'fs'; +import * as path from 'path'; +import * as vscode from 'vscode'; +import { + LanguageClient, + LanguageClientOptions, + ServerOptions, + TransportKind, + Trace +} from 'vscode-languageclient/node'; + +type ProofResponse = { + output: string; + uuid: number; + mode: string; + processedEnd: number; + sentenceStart?: number | null; + sentenceEnd?: number | null; +}; + +type DocState = { + lastOffset: number; +}; + +let client: LanguageClient | undefined; +let clientReady: Promise | undefined; +let clientOptions: LanguageClientOptions | undefined; +let serverOptions: ServerOptions | undefined; +let goalsPanel: vscode.WebviewPanel | undefined; +let outputChannel: vscode.OutputChannel | undefined; +let traceLevel: Trace = Trace.Off; +let lspCommand: string | undefined; +let lspArgs: string[] = []; +let processedDecoration: vscode.TextEditorDecorationType | undefined; +let processingDecoration: vscode.TextEditorDecorationType | undefined; +let errorDecoration: vscode.TextEditorDecorationType | undefined; +let lastEasyCryptEditor: vscode.TextEditor | undefined; +const docStates = new Map(); +let suppressProcessedEdits = false; +let suppressProcessingEdits = false; +let processingDocUri: string | undefined; +let processingSnapshot: string | undefined; +let diagnostics: vscode.DiagnosticCollection | undefined; + +function getDocState(doc: vscode.TextDocument): DocState { + const key = doc.uri.toString(); + const state = docStates.get(key); + if (state) { + return state; + } + const created = { lastOffset: 0 }; + docStates.set(key, created); + return created; +} + +function escapeHtml(value: string): string { + return value + .replace(/&/g, '&') + .replace(//g, '>'); +} + +function showGoals(output: string): void { + if (!goalsPanel) { + goalsPanel = vscode.window.createWebviewPanel( + 'easycryptGoals', + 'EasyCrypt Goals', + { viewColumn: vscode.ViewColumn.Beside, preserveFocus: true }, + { enableFindWidget: true } + ); + goalsPanel.onDidDispose(() => { + goalsPanel = undefined; + }); + } else { + goalsPanel.reveal(goalsPanel.viewColumn, true); + } + + goalsPanel.webview.html = ` + + + + + + + +
${escapeHtml(output)}
+ +`; +} + +function updateProcessedDecoration(editor: vscode.TextEditor | undefined): void { + if (!editor || !processedDecoration) { + return; + } + const state = getDocState(editor.document); + const endOffset = state.lastOffset; + const endPos = editor.document.positionAt(endOffset); + const startPos = new vscode.Position(0, 0); + const anchor = new vscode.Range(startPos, startPos); + const fixed = new vscode.Range(startPos, endPos); + editor.setDecorations(processedDecoration, [anchor, fixed]); +} + +function setProcessingDecoration(editor: vscode.TextEditor | undefined, range: vscode.Range): void { + if (!editor || !processingDecoration) { + return; + } + editor.setDecorations(processingDecoration, [range]); +} + +function clearProcessingDecoration(editor: vscode.TextEditor | undefined): void { + if (!editor || !processingDecoration) { + return; + } + editor.setDecorations(processingDecoration, []); +} + +function setProcessingLock(doc: vscode.TextDocument): void { + processingDocUri = doc.uri.toString(); + processingSnapshot = doc.getText(); +} + +function clearProcessingLock(): void { + processingDocUri = undefined; + processingSnapshot = undefined; +} + +async function restoreProcessingSnapshot(doc: vscode.TextDocument): Promise { + if (!processingSnapshot) { + return; + } + const lastLine = doc.lineAt(doc.lineCount - 1); + const fullRange = new vscode.Range(new vscode.Position(0, 0), lastLine.range.end); + const edit = new vscode.WorkspaceEdit(); + edit.replace(doc.uri, fullRange, processingSnapshot); + await vscode.workspace.applyEdit(edit); +} + +function outputHasError(output: string): boolean { + return /\[error-\d+-\d+\]/.test(output); +} + +function summarizeErrorOutput(output: string): string { + const line = output.split(/\r?\n/).find((entry) => entry.trim().length > 0); + if (!line) { + return 'EasyCrypt reported an error.'; + } + const cleaned = line.replace(/\[error-\d+-\d+\]/g, '').trim(); + return cleaned.length > 0 ? cleaned : 'EasyCrypt reported an error.'; +} + +function showGoalsOrError(output: string): void { + if (output.trim().length > 0) { + showGoals(output); + } else { + showGoals('EasyCrypt reported an error.'); + } +} + +function parseErrorTag(output: string): { start: number; end: number; message: string } | undefined { + const match = output.match(/\[error-(\d+)-(\d+)\]/); + if (!match) { + return undefined; + } + const start = Number(match[1]); + const end = Number(match[2]); + if (!Number.isFinite(start) || !Number.isFinite(end)) { + return undefined; + } + const message = output.replace(match[0], '').trim(); + return { start, end, message: message.length > 0 ? message : 'EasyCrypt reported an error.' }; +} + +function clearErrorDecoration(editor: vscode.TextEditor | undefined): void { + if (!editor || !errorDecoration) { + return; + } + editor.setDecorations(errorDecoration, []); +} + +function clearDiagnostics(doc: vscode.TextDocument): void { + diagnostics?.delete(doc.uri); +} + +function showErrorDecoration( + editor: vscode.TextEditor | undefined, + sentenceOffset: number, + errorStart: number, + errorEnd: number +): void { + if (!editor || !errorDecoration) { + return; + } + const start = editor.document.positionAt(sentenceOffset + errorStart); + const end = editor.document.positionAt(sentenceOffset + Math.max(errorStart + 1, errorEnd)); + editor.setDecorations(errorDecoration, [new vscode.Range(start, end)]); +} + +function handleProofError( + output: string, + editor: vscode.TextEditor | undefined, + sentenceOffset?: number +): void { + const parsed = parseErrorTag(output); + if (parsed && sentenceOffset !== undefined) { + showErrorDecoration(editor, sentenceOffset, parsed.start, parsed.end); + showGoals(parsed.message); + if (editor && diagnostics) { + const doc = editor.document; + const start = doc.positionAt(sentenceOffset + parsed.start); + const end = doc.positionAt(sentenceOffset + Math.max(parsed.start + 1, parsed.end)); + const range = new vscode.Range(start, end); + const diag = new vscode.Diagnostic(range, parsed.message, vscode.DiagnosticSeverity.Error); + diagnostics.set(doc.uri, [diag]); + } + } else { + showGoalsOrError(output.replace(/\[error-\d+-\d+\]/g, '').trim()); + } +} + +function getEditorForCommand(): vscode.TextEditor | undefined { + const active = vscode.window.activeTextEditor; + if (active && active.document.languageId === 'easycrypt') { + return active; + } + return lastEasyCryptEditor; +} + +async function requestProof(method: string, params: Record): Promise { + if (!client) { + throw new Error('EasyCrypt language client is not running.'); + } + if (clientReady) { + await clientReady; + } + const start = Date.now(); + outputChannel?.appendLine(`[proof] request ${method}`); + const timeout = setTimeout(() => { + outputChannel?.appendLine(`[proof] waiting ${method} >3s`); + }, 3000); + try { + const result = await client.sendRequest(method, params); + const elapsed = Date.now() - start; + outputChannel?.appendLine(`[proof] response ${method} ${elapsed}ms`); + return result; + } catch (err) { + const elapsed = Date.now() - start; + outputChannel?.appendLine(`[proof] error ${method} ${elapsed}ms ${String(err)}`); + throw err; + } finally { + clearTimeout(timeout); + } +} + +async function handleStep(): Promise { + const editor = getEditorForCommand(); + if (!editor) { + vscode.window.showInformationMessage('EasyCrypt: no active EasyCrypt editor.'); + return; + } + + const doc = editor.document; + const state = getDocState(doc); + const previousOffset = state.lastOffset; + let sentenceStart: number | null | undefined; + let sentenceEnd: number | null | undefined; + let previewProcessedEnd = state.lastOffset; + try { + const preview = await requestProof('easycrypt/proof/next', { uri: doc.uri.toString() }); + sentenceStart = preview.sentenceStart ?? null; + sentenceEnd = preview.sentenceEnd ?? null; + previewProcessedEnd = preview.processedEnd; + } catch (err) { + outputChannel?.appendLine(`[proof] step preview failed ${String(err)}`); + } + + if (sentenceStart == null || sentenceEnd == null) { + state.lastOffset = previewProcessedEnd; + updateProcessedDecoration(editor); + return; + } + + if (sentenceStart != null && sentenceEnd != null) { + const processingRange = new vscode.Range( + doc.positionAt(sentenceStart), + doc.positionAt(sentenceEnd) + ); + setProcessingDecoration(editor, processingRange); + setProcessingLock(doc); + } + + try { + const result = await requestProof('easycrypt/proof/step', { uri: doc.uri.toString() }); + outputChannel?.appendLine(`[proof] step ok uuid=${result.uuid} mode=${result.mode}`); + state.lastOffset = result.processedEnd; + if (outputHasError(result.output)) { + outputChannel?.appendLine(`[proof] step reported error ${result.output}`); + if (result.sentenceStart != null) { + handleProofError(result.output, editor, result.sentenceStart); + } else { + handleProofError(result.output, editor, previousOffset); + } + } else { + showGoals(result.output); + updateProcessedDecoration(editor); + clearErrorDecoration(editor); + clearDiagnostics(editor.document); + } + } catch (err) { + outputChannel?.appendLine(`[proof] step failed ${String(err)}`); + vscode.window.showErrorMessage(`EasyCrypt step failed: ${String(err)}`); + } finally { + clearProcessingDecoration(editor); + clearProcessingLock(); + } +} + +async function handleSendRegion(): Promise { + const editor = getEditorForCommand(); + if (!editor) { + vscode.window.showInformationMessage('EasyCrypt: no active EasyCrypt editor.'); + return; + } + + const doc = editor.document; + const state = getDocState(doc); + const cursorOffset = doc.offsetAt(editor.selection.active); + try { + outputChannel?.appendLine('[proof] jumpToCursor'); + const result = await requestProof('easycrypt/proof/jumpTo', { + uri: doc.uri.toString(), + target: cursorOffset + }); + outputChannel?.appendLine(`[proof] jumpToCursor ok uuid=${result.uuid} mode=${result.mode}`); + state.lastOffset = result.processedEnd; + if (outputHasError(result.output)) { + outputChannel?.appendLine(`[proof] jumpToCursor reported error ${result.output}`); + if (result.sentenceStart != null) { + handleProofError(result.output, editor, result.sentenceStart); + } else { + handleProofError(result.output, editor, state.lastOffset); + } + return; + } + showGoals(result.output); + updateProcessedDecoration(editor); + clearErrorDecoration(editor); + clearDiagnostics(doc); + } catch (err) { + outputChannel?.appendLine(`[proof] jumpToCursor failed ${String(err)}`); + vscode.window.showErrorMessage(`EasyCrypt jump-to-cursor failed: ${String(err)}`); + } finally { + clearProcessingDecoration(editor); + clearProcessingLock(); + } +} + +async function handleBack(): Promise { + const editor = getEditorForCommand(); + if (!editor) { + vscode.window.showInformationMessage('EasyCrypt: no active EasyCrypt editor.'); + return; + } + + const state = getDocState(editor.document); + try { + outputChannel?.appendLine('[proof] back'); + const result = await requestProof('easycrypt/proof/back', { + uri: editor.document.uri.toString() + }); + if (outputHasError(result.output)) { + outputChannel?.appendLine(`[proof] back reported error ${result.output}`); + if (result.sentenceStart != null) { + handleProofError(result.output, editor, result.sentenceStart); + } else { + handleProofError(result.output, editor); + } + } else { + state.lastOffset = result.processedEnd; + outputChannel?.appendLine(`[proof] back ok uuid=${result.uuid} mode=${result.mode}`); + showGoals(result.output); + updateProcessedDecoration(editor); + clearErrorDecoration(editor); + clearDiagnostics(editor.document); + } + } catch (err) { + outputChannel?.appendLine(`[proof] back failed ${String(err)}`); + vscode.window.showErrorMessage(`EasyCrypt back failed: ${String(err)}`); + } +} + +async function handleRestart(): Promise { + const editor = getEditorForCommand(); + if (!editor) { + vscode.window.showInformationMessage('EasyCrypt: no active EasyCrypt editor.'); + return; + } + const state = editor ? getDocState(editor.document) : undefined; + const previousOffset = state?.lastOffset ?? 0; + + try { + outputChannel?.appendLine('[proof] restart'); + const result = await requestProof('easycrypt/proof/restart', { + uri: editor.document.uri.toString() + }); + outputChannel?.appendLine(`[proof] restart ok uuid=${result.uuid} mode=${result.mode}`); + if (outputHasError(result.output)) { + outputChannel?.appendLine(`[proof] restart reported error ${result.output}`); + handleProofError(result.output, editor); + if (state) { + state.lastOffset = previousOffset; + } + } else { + if (state) { + state.lastOffset = result.processedEnd; + } + showGoals(result.output); + updateProcessedDecoration(editor ?? vscode.window.activeTextEditor); + clearErrorDecoration(editor ?? vscode.window.activeTextEditor); + if (editor) { + clearDiagnostics(editor.document); + } + } + } catch (err) { + outputChannel?.appendLine(`[proof] restart failed ${String(err)}`); + vscode.window.showErrorMessage(`EasyCrypt restart failed: ${String(err)}`); + } +} + +async function handleGoals(): Promise { + try { + outputChannel?.appendLine('[proof] goals'); + const editor = getEditorForCommand(); + if (!editor) { + vscode.window.showInformationMessage('EasyCrypt: no active EasyCrypt editor.'); + return; + } + const result = await requestProof('easycrypt/proof/goals', { + uri: editor.document.uri.toString() + }); + outputChannel?.appendLine(`[proof] goals ok uuid=${result.uuid} mode=${result.mode}`); + showGoals(result.output); + } catch (err) { + outputChannel?.appendLine(`[proof] goals failed ${String(err)}`); + vscode.window.showErrorMessage(`EasyCrypt goals failed: ${String(err)}`); + } +} + +function resolveServerCommand( + workspaceFolder: string | undefined, + cliPath: string +): string | undefined { + if (cliPath && cliPath.trim().length > 0) { + return cliPath; + } + + if (!workspaceFolder) { + return undefined; + } + + const exeCandidate = path.join(workspaceFolder, '_build', 'default', 'src', 'ec.exe'); + const unixCandidate = path.join(workspaceFolder, '_build', 'default', 'src', 'ec'); + if (fs.existsSync(exeCandidate)) { + return exeCandidate; + } + if (fs.existsSync(unixCandidate)) { + return unixCandidate; + } + + return undefined; +} + +function ensureLspArgs(args: string[]): string[] { + if (args.length > 0 && args[0] === 'lsp') { + return args; + } + return ['lsp', ...args]; +} + +function startClient(): void { + if (!clientOptions || !serverOptions) { + throw new Error('EasyCrypt LSP options are not configured.'); + } + outputChannel?.appendLine(`[lsp] spawn command=${lspCommand ?? ''} args=${lspArgs.join(' ')}`); + client = new LanguageClient('easycryptLsp', 'EasyCrypt LSP', serverOptions, clientOptions); + outputChannel?.appendLine('[lsp] starting client'); + clientReady = client.start(); + void clientReady.then( + () => outputChannel?.appendLine('[lsp] client ready'), + (err) => outputChannel?.appendLine(`[lsp] client start failed ${String(err)}`) + ); + void clientReady.then(() => client?.setTrace(traceLevel)); +} + +async function restartClient(): Promise { + if (!serverOptions || !clientOptions) { + vscode.window.showErrorMessage('EasyCrypt: LSP options are not configured.'); + return; + } + const current = client; + if (current) { + try { + await current.stop(); + } catch (err) { + vscode.window.showWarningMessage(`EasyCrypt: failed to stop LSP (${String(err)}).`); + } + } + startClient(); + outputChannel?.appendLine('[lsp] restarted client'); + vscode.window.showInformationMessage('EasyCrypt: LSP restarted.'); +} + +export function activate(context: vscode.ExtensionContext): void { + outputChannel = vscode.window.createOutputChannel('EasyCrypt'); + context.subscriptions.push(outputChannel); + processedDecoration = vscode.window.createTextEditorDecorationType({ + backgroundColor: 'rgba(120, 140, 180, 0.18)', + isWholeLine: false, + rangeBehavior: vscode.DecorationRangeBehavior.ClosedClosed + }); + context.subscriptions.push(processedDecoration); + processingDecoration = vscode.window.createTextEditorDecorationType({ + backgroundColor: 'rgba(210, 170, 90, 0.28)', + isWholeLine: false + }); + context.subscriptions.push(processingDecoration); + + diagnostics = vscode.languages.createDiagnosticCollection('easycrypt'); + context.subscriptions.push(diagnostics); + + errorDecoration = undefined; + + const workspaceFolder = vscode.workspace.workspaceFolders?.[0]?.uri.fsPath; + const config = vscode.workspace.getConfiguration('easycrypt'); + const cliPath = config.get('cli.path') ?? ''; + const serverCommand = resolveServerCommand(workspaceFolder, cliPath) ?? 'easycrypt'; + const cliArgs = config.get('cli.args') ?? []; + const serverArgs = ensureLspArgs(cliArgs); + lspCommand = serverCommand; + lspArgs = serverArgs; + const traceSetting = config.get('trace.server') ?? 'off'; + traceLevel = + traceSetting === 'verbose' + ? Trace.Verbose + : traceSetting === 'messages' + ? Trace.Messages + : Trace.Off; + + outputChannel.appendLine(`[lsp] serverCommand=${serverCommand}`); + outputChannel.appendLine(`[lsp] cliPath=${cliPath || '(default)'}`); + outputChannel.appendLine(`[lsp] cliArgs=${cliArgs.join(' ')}`); + outputChannel.appendLine(`[lsp] serverArgs=${serverArgs.join(' ')}`); + outputChannel.appendLine(`[lsp] trace=${traceSetting}`); + outputChannel.appendLine( + `[lsp] logFile=${workspaceFolder ? path.join(workspaceFolder, '.easycrypt-lsp.log') : '(inherit)'}` + ); + outputChannel.show(true); + + if (!resolveServerCommand(workspaceFolder, cliPath)) { + vscode.window.showWarningMessage( + "EasyCrypt binary not found in the workspace. Using 'easycrypt' from PATH." + ); + } + + const lspEnv = { + ...process.env, + EASYCRYPT_LSP_LOG: workspaceFolder + ? path.join(workspaceFolder, '.easycrypt-lsp.log') + : process.env.EASYCRYPT_LSP_LOG + }; + const localServerOptions: ServerOptions = { + command: serverCommand, + args: serverArgs, + transport: TransportKind.stdio, + options: { env: lspEnv } + }; + + const localClientOptions: LanguageClientOptions = { + documentSelector: [{ language: 'easycrypt' }], + outputChannel, + traceOutputChannel: outputChannel + }; + + serverOptions = localServerOptions; + clientOptions = localClientOptions; + startClient(); + context.subscriptions.push( + new vscode.Disposable(() => { + outputChannel?.appendLine('[lsp] stopping client'); + void client?.stop(); + }) + ); + if (client) { + client.onDidChangeState((event) => { + outputChannel?.appendLine(`[lsp] state ${event.oldState} -> ${event.newState}`); + }); + } + + context.subscriptions.push( + vscode.commands.registerCommand('easycrypt.proof.step', handleStep), + vscode.commands.registerCommand('easycrypt.proof.back', handleBack), + vscode.commands.registerCommand('easycrypt.proof.restart', handleRestart), + vscode.commands.registerCommand('easycrypt.proof.jumpToCursor', handleSendRegion), + vscode.commands.registerCommand('easycrypt.proof.goals', handleGoals), + vscode.commands.registerCommand('easycrypt.lsp.restart', restartClient) + ); + + context.subscriptions.push( + vscode.workspace.onDidCloseTextDocument((doc) => { + docStates.delete(doc.uri.toString()); + }) + ); + + context.subscriptions.push( + vscode.workspace.onDidChangeTextDocument(async (event) => { + if (suppressProcessedEdits || suppressProcessingEdits) { + return; + } + if (event.contentChanges.length === 0) { + return; + } + const doc = event.document; + if (doc.languageId !== 'easycrypt') { + return; + } + if (processingDocUri && processingDocUri === doc.uri.toString()) { + suppressProcessingEdits = true; + try { + await restoreProcessingSnapshot(doc); + } catch (err) { + outputChannel?.appendLine(`[proof] processing lock restore failed ${String(err)}`); + } finally { + suppressProcessingEdits = false; + } + return; + } + clearErrorDecoration(vscode.window.activeTextEditor); + clearDiagnostics(doc); + const state = getDocState(doc); + const limit = state.lastOffset; + const earliestStart = event.contentChanges.reduce((min, change) => { + const start = change.range ? doc.offsetAt(change.range.start) : 0; + return Math.min(min, start); + }, Number.POSITIVE_INFINITY); + if (!(earliestStart < limit)) { + return; + } + suppressProcessedEdits = true; + try { + try { + const result = await requestProof('easycrypt/proof/jumpTo', { + uri: doc.uri.toString(), + target: earliestStart + }); + state.lastOffset = result.processedEnd; + } catch (err) { + outputChannel?.appendLine(`[proof] auto-rewind failed ${String(err)}`); + vscode.window.showErrorMessage(`EasyCrypt auto-rewind failed: ${String(err)}`); + } + updateProcessedDecoration(vscode.window.activeTextEditor); + } finally { + suppressProcessedEdits = false; + } + return; + }) + ); + + const updateEditorState = (editor: vscode.TextEditor | undefined) => { + if (editor && editor.document.languageId === 'easycrypt') { + lastEasyCryptEditor = editor; + } + updateProcessedDecoration(editor); + clearErrorDecoration(editor); + if (editor) { + clearDiagnostics(editor.document); + } + }; + + updateEditorState(vscode.window.activeTextEditor); + + context.subscriptions.push( + vscode.window.onDidChangeActiveTextEditor((editor) => { + updateEditorState(editor); + }) + ); + +} + +export async function deactivate(): Promise { + if (client) { + await client.stop(); + } +} diff --git a/vscode/syntaxes/easycrypt.tmLanguage.json b/vscode/syntaxes/easycrypt.tmLanguage.json new file mode 100644 index 000000000..af025d0dc --- /dev/null +++ b/vscode/syntaxes/easycrypt.tmLanguage.json @@ -0,0 +1,101 @@ +{ + "$schema": "https://raw.githubusercontent.com/martinring/tmlanguage/master/tmlanguage.json", + "name": "EasyCrypt", + "scopeName": "source.easycrypt", + "patterns": [ + { "include": "#comments" }, + { "include": "#strings" }, + { "include": "#keywords" }, + { "include": "#types" }, + { "include": "#numbers" } + ], + "repository": { + "comments": { + "patterns": [ + { + "name": "comment.block.easycrypt", + "begin": "\\(\\*", + "beginCaptures": { + "0": { "name": "punctuation.definition.comment.easycrypt" } + }, + "end": "\\*\\)", + "endCaptures": { + "0": { "name": "punctuation.definition.comment.easycrypt" } + }, + "patterns": [ + { "include": "#comments" } + ] + } + ] + }, + "strings": { + "patterns": [ + { + "name": "string.quoted.double.easycrypt", + "begin": "\"", + "beginCaptures": { + "0": { "name": "punctuation.definition.string.begin.easycrypt" } + }, + "end": "\"", + "endCaptures": { + "0": { "name": "punctuation.definition.string.end.easycrypt" } + }, + "patterns": [ + { + "name": "constant.character.escape.easycrypt", + "match": "\\\\." + } + ] + } + ] + }, + "keywords": { + "patterns": [ + { + "name": "keyword.other.easycrypt.bytac", + "match": "\\b(assumption|by|check|coq|done|edit|exact|fix|reflexivity|smt|solve)\\b" + }, + { + "name": "keyword.other.easycrypt.dangerous", + "match": "\\b(admit|admitted)\\b" + }, + { + "name": "keyword.control.easycrypt.global", + "match": "\\b(Pr|Self|Top|abbrev|abort|abstract|as|axiom|axiomatized|class|clone|const|declare|dump|end|exit|export|from|global|goal|hint|import|include|inductive|instance|lemma|local|locate|module|notation|of|op|pred|print|proof|prover|qed|realize|remove|rename|require|search|section|subtype|theory|timeout|type|why3|with)\\b" + }, + { + "name": "keyword.other.easycrypt.internal", + "match": "\\b(debug|fail|pragma|time|undo)\\b" + }, + { + "name": "keyword.operator.easycrypt.prog", + "match": "\\b(assert|async|ehoare|elif|else|equiv|exists|for|for|forall|fun|glob|hoare|if|in|is|islossless|let|match|match|phoare|proc|res|return|then|var|while)\\b" + }, + { + "name": "keyword.control.easycrypt.tactic", + "match": "\\b(algebra|alias|apply|auto|beta|byehoare|byequiv|byphoare|bypr|byupto|call|case|cbv|cfold|change|clear|congr|conseq|delta|eager|ecall|elim|eta|exfalso|exlim|fel|field|fieldeq|fission|fusion|gen|have|idassign|idtac|inline|interleave|iota|kill|left|logic|modpath|move|outline|pose|pr_bounded|progress|rcondf|rcondt|replace|rewrite|right|ring|ringeq|rnd|rndsem|rwnormal|seq|sim|simplify|skip|sp|split|splitwhile|subst|suff|swap|symmetry|transitivity|trivial|unroll|weakmem|wlog|wp|zeta)\\b" + }, + { + "name": "keyword.control.easycrypt.tactical", + "match": "\\b(do|expect|first|last|try)\\b" + } + ] + }, + "types": { + "patterns": [ + { + "name": "storage.type.easycrypt", + "match": "\\b(bool|int|real|unit)\\b" + } + ] + }, + "numbers": { + "patterns": [ + { + "name": "constant.numeric.easycrypt", + "match": "\\b\\d+(?:\\.\\d+)?\\b" + } + ] + } + } +} diff --git a/vscode/tsconfig.json b/vscode/tsconfig.json new file mode 100644 index 000000000..6da6eaa6c --- /dev/null +++ b/vscode/tsconfig.json @@ -0,0 +1,13 @@ +{ + "compilerOptions": { + "target": "ES2020", + "module": "commonjs", + "lib": ["ES2020"], + "outDir": "out", + "rootDir": "src", + "sourceMap": true, + "strict": true, + "esModuleInterop": true + }, + "include": ["src"] +}