Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[memo] Cache control and eviction improvements #662

Merged
merged 1 commit into from
Apr 3, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,9 @@
(@bhaktishh, @ejgallego, #642, #643, #644)
- new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
goals from a document (@ejgallego @gbdrt, #619)
- new trim command (both in the server and in VSCode) to liberate
space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236
#348)

# coq-lsp 0.1.8.1: Spring fix
-----------------------------
Expand Down
8 changes: 4 additions & 4 deletions controller/coq_lsp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ open Lsp_core
(* Do cleanup here if necessary *)
let exit_message () =
let message = "server exiting" in
LIO.logMessage ~lvl:1 ~message
LIO.logMessage ~lvl:Error ~message

let lsp_cleanup () = exit_message ()

Expand Down Expand Up @@ -63,7 +63,7 @@ let concise_cb ofn =
let lsp_cb ofn =
let message ~lvl ~message =
let lvl = Fleche.Io.Level.to_int lvl in
LIO.logMessage ~lvl ~message
LIO.logMessageInt ~lvl ~message
in
Fleche.Io.CallBack.
{ trace = LIO.trace
Expand Down Expand Up @@ -165,7 +165,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
with
| Lsp_exit ->
let message = "[LSP shutdown] EOF\n" in
LIO.logMessage ~lvl:1 ~message
LIO.logMessage ~lvl:Error ~message
| exn ->
let bt = Printexc.get_backtrace () in
let exn, info = Exninfo.capture exn in
Expand All @@ -175,7 +175,7 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
Pp.(string_of_ppcmds CErrors.(iprint (exn, info)));
LIO.trace "server crash" (exn_msg ^ bt);
let message = "[uncontrolled LSP shutdown] server crash\n" ^ exn_msg in
LIO.logMessage ~lvl:1 ~message
LIO.logMessage ~lvl:Error ~message

(* Arguments handling *)
open Cmdliner
Expand Down
16 changes: 10 additions & 6 deletions controller/lsp_core.ml
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ module Helpers = struct
| Error err ->
(* ppx_deriving_yojson error messages leave a lot to be desired *)
let message = Format.asprintf "json parsing failed: %s" err in
LIO.logMessage ~lvl:1 ~message;
LIO.logMessage ~lvl:Error ~message;
(* XXX Fixme *)
CErrors.user_err (Pp.str "failed to parse uri")
in
Expand Down Expand Up @@ -133,10 +133,10 @@ module State = struct
let file = Lang.LUri.File.to_string_file uri in
match List.find_opt (fun (dir, _) -> is_in_dir ~dir ~file) workspaces with
| None ->
LIO.logMessage ~lvl:1 ~message:("file not in workspace: " ^ file);
LIO.logMessage ~lvl:Error ~message:("file not in workspace: " ^ file);
(root_state, default_workspace)
| Some (_, Error _) ->
LIO.logMessage ~lvl:1 ~message:("file in errored workspace: " ^ file);
LIO.logMessage ~lvl:Error ~message:("file in errored workspace: " ^ file);
(root_state, default_workspace)
| Some (_, Ok workspace) -> (root_state, workspace)
end
Expand Down Expand Up @@ -393,6 +393,8 @@ let do_cancel ~ofn ~params =
let message = "Cancelled by client" in
Rq.cancel ~ofn ~code ~message id

let do_cache_trim () = Nt_cache_trim.notification ()

(***********************************************************************)

(** LSP Init routine *)
Expand All @@ -401,7 +403,7 @@ exception Lsp_exit
let log_workspace (dir, w) =
let message, extra = Coq.Workspace.describe_guess w in
LIO.trace "workspace" ("initialized " ^ dir) ~extra;
LIO.logMessage ~lvl:3 ~message
LIO.logMessage ~lvl:Info ~message

let version () =
let dev_version =
Expand All @@ -426,12 +428,12 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
let message =
Format.asprintf "Initializing coq-lsp server %s" (version ())
in
LIO.logMessage ~lvl:3 ~message;
LIO.logMessage ~lvl:Info ~message;
let result, dirs = Rq_init.do_initialize ~params in
(* We don't need to interrupt this *)
let token = Coq.Limits.Token.create () in
Rq.Action.now (Ok result) |> Rq.serve ~ofn ~token ~id;
LIO.logMessage ~lvl:3 ~message:"Server initialized";
LIO.logMessage ~lvl:Info ~message:"Server initialized";
(* Workspace initialization *)
let debug = debug || !Fleche.Config.v.debug in
let workspaces =
Expand Down Expand Up @@ -463,6 +465,8 @@ let dispatch_notification ~io ~ofn ~token ~state ~method_ ~params : unit =
| "textDocument/didChange" -> do_change ~io ~ofn ~token params
| "textDocument/didClose" -> do_close ~ofn params
| "textDocument/didSave" -> Cache.save_to_disk ()
(* Specific to coq-lsp *)
| "coq/trimCaches" -> do_cache_trim ()
(* Cancel Request *)
| "$/cancelRequest" -> do_cancel ~ofn ~params
(* NOOPs *)
Expand Down
95 changes: 95 additions & 0 deletions controller/nt_cache_trim.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
module OCaml = struct
(* Version using formatter instead of out_channel *)
open Gc
open Format

let _print_stat c () =
let st = stat () in
fprintf c "minor_collections: %d\n" st.minor_collections;
fprintf c "major_collections: %d\n" st.major_collections;
fprintf c "compactions: %d\n" st.compactions;
fprintf c "forced_major_collections: %d\n" st.forced_major_collections;
fprintf c "\n";
let l1 = String.length (sprintf "%.0f" st.minor_words) in
fprintf c "minor_words: %*.0f\n" l1 st.minor_words;
fprintf c "promoted_words: %*.0f\n" l1 st.promoted_words;
fprintf c "major_words: %*.0f\n" l1 st.major_words;
fprintf c "\n";
let l2 = String.length (sprintf "%d" st.top_heap_words) in
fprintf c "top_heap_words: %*d\n" l2 st.top_heap_words;
fprintf c "heap_words: %*d\n" l2 st.heap_words;
fprintf c "live_words: %*d\n" l2 st.live_words;
fprintf c "free_words: %*d\n" l2 st.free_words;
fprintf c "largest_free: %*d\n" l2 st.largest_free;
fprintf c "fragments: %*d\n" l2 st.fragments;
fprintf c "\n";
fprintf c "live_blocks: %d\n" st.live_blocks;
fprintf c "free_blocks: %d\n" st.free_blocks;
fprintf c "heap_chunks: %d\n" st.heap_chunks

let print_stat_simple c () =
let st = stat () in
let l2 = String.length (sprintf "%d" st.top_heap_words) in
fprintf c "live: %*d\n" l2 st.live_words;
fprintf c "free: %*d\n" l2 st.free_words;
fprintf c "----------\n";
()
end

module M = Fleche.Memo
module LIO = Lsp.Io

let caches () =
[ ("interp", M.Interp.all_freqs ())
; ("admit", M.Admit.all_freqs ())
; ("init", M.Init.all_freqs ())
; ("require", M.Require.all_freqs ())
]

let pp_cache fmt (name, freqs) =
let zsum = List.filter (Int.equal 0) freqs in
let pp_zsum fmt l = Format.fprintf fmt "{ 0-entries: %d }" (List.length l) in
let fsum = Base.List.take freqs 20 in
let pp_sep fmt () = Format.fprintf fmt ",@," in
let pp_fsum = Format.(pp_print_list ~pp_sep pp_print_int) in
Format.fprintf fmt "@[%s: %d | %a @[(%a)@]@]" name (List.length freqs) pp_zsum
zsum pp_fsum fsum

let build_message () =
let caches = caches () in
Format.asprintf "@[Cache trim requested:@\n @[<v>%a@]@]"
(Format.pp_print_list pp_cache)
caches

let cache_trim () =
let () = M.Interp.clear () in
let () = M.Admit.clear () in
let () = M.Init.clear () in
let () = M.Require.clear () in
()

let gc_stats hd msg =
let message =
Format.asprintf "[%s] %s:@\n%a" hd msg OCaml.print_stat_simple ()
in
LIO.logMessage ~lvl:Info ~message

let full_major hd =
gc_stats hd "before full major";
Gc.full_major ();
gc_stats hd "after full major";
()

let do_trim () =
full_major "pre ";
cache_trim ();
let message = Format.asprintf "%s@\n---------@\n" "trimming" in
LIO.logMessage ~lvl:Info ~message;
full_major "post";
()

let notification () =
let message = build_message () in
LIO.logMessage ~lvl:Info ~message;
do_trim ();
()
1 change: 1 addition & 0 deletions controller/nt_cache_trim.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
val notification : unit -> unit
2 changes: 1 addition & 1 deletion controller/rq_goals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ let parse_and_execute_in ~token ~loc tac st =
let open Coq.Protect.E.O in
let* ast = parse ~token ~loc tac st in
match ast with
| Some ast -> (Fleche.Memo.Interp.eval ~token (st, ast)).res
| Some ast -> Fleche.Memo.Interp.eval ~token (st, ast)
(* On EOF we return the previous state, the command was the empty string or a
comment *)
| None -> Coq.Protect.E.ok st
Expand Down
4 changes: 2 additions & 2 deletions controller/rq_init.ml
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ let check_client_version client_version : unit =
Format.asprintf "Incorrect client version: %s , expected %s."
client_version server_version
in
LIO.logMessage ~lvl:1 ~message
LIO.(logMessage ~lvl:Lvl.Error ~message)

(* Maybe this should be [cwd] ? *)
let default_workspace_root = "."
Expand All @@ -54,7 +54,7 @@ let parse_fpath x =
"rootPath is not absolute: " ^ path
^ " . This is not robust, please use absolute paths or rootURI"
in
LIO.logMessage ~lvl:2 ~message);
LIO.logMessage ~lvl:LIO.Lvl.Warning ~message);
Lang.LUri.of_string ("file:///" ^ path) |> Lang.LUri.File.of_uri

let parse_null_or f = function
Expand Down
4 changes: 4 additions & 0 deletions editor/code/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,10 @@
{
"command": "coq-lsp.save",
"title": "Coq LSP: Save .vo file for the current buffer"
},
{
"command": "coq-lsp.trim",
"title": "Coq LSP: Request the server to trim caches and compact memory (useful to try reduce memory comsumption)"
}
],
"keybindings": [
Expand Down
8 changes: 8 additions & 0 deletions editor/code/src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ import {
import {
BaseLanguageClient,
LanguageClientOptions,
NotificationType,
RequestType,
RevealOutputChannelOn,
VersionedTextDocumentIdentifier,
Expand Down Expand Up @@ -259,6 +260,12 @@ export function activateCoqLSP(
client.sendRequest(docReq, params).then((fd) => console.log(fd));
};

const trimNot = new NotificationType<{}>("coq/trimCaches");

const cacheTrim = () => {
client.sendNotification(trimNot, {});
};

const saveReq = new RequestType<FlecheDocumentParams, void, void>(
"coq/saveVo"
);
Expand Down Expand Up @@ -325,6 +332,7 @@ export function activateCoqLSP(

coqCommand("restart", restart);
coqCommand("toggle", toggle);
coqCommand("trim", cacheTrim);

coqEditorCommand("goals", goals);
coqEditorCommand("document", getDocument);
Expand Down
5 changes: 5 additions & 0 deletions etc/doc/PROTOCOL.md
Original file line number Diff line number Diff line change
Expand Up @@ -303,3 +303,8 @@ export interface DocumentPerfParams {
#### Changelog

- v0.1.7: Initial version

### Trim cache notification

The `coq/trimCaches` notification from client to server tells the
server to free memory. It has no parameters.
2 changes: 2 additions & 0 deletions examples/Rtrigo1.v
Original file line number Diff line number Diff line change
Expand Up @@ -571,6 +571,8 @@ Proof.
intro x; rewrite sin_plus; rewrite sin_PI2; rewrite cos_PI2; ring.
Qed.

(* We do what we can; it is what it is... *)

Lemma PI2_RGT_0 : 0 < PI / 2.
Proof.
unfold Rdiv in |- *; apply Rmult_lt_0_compat;
Expand Down
4 changes: 2 additions & 2 deletions fleche/doc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -637,8 +637,8 @@ end

let interp_and_info ~st ~files ast =
match Coq.Ast.Require.extract ast with
| None -> Memo.Interp.eval (st, ast)
| Some ast -> Memo.Require.eval (st, files, ast)
| None -> Memo.Interp.evalS (st, ast)
| Some ast -> Memo.Require.evalS (st, files, ast)

let interp_and_info ~token ~parsing_time ~st ~files ast =
let { Gc.major_words = mw_prev; _ } = Gc.quick_stat () in
Expand Down
2 changes: 1 addition & 1 deletion fleche/io.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ end
module CallBack = struct
type t =
{ trace : string -> ?extra:string -> string -> unit
; message : lvl:int -> message:string -> unit
; message : lvl:Level.t -> message:string -> unit
; diagnostics :
uri:Lang.LUri.File.t -> version:int -> Lang.Diagnostic.t list -> unit
; fileProgress :
Expand Down
Loading
Loading