From bd24ca3093b314b348c63826f7a868e6433b6acc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 2 Apr 2025 12:10:46 +0200 Subject: [PATCH] test: re-elaboration benchmarks (#7784) Tests language server memory use by repeatedly re-elaborate a given file --- script/benchReelabRss.lean | 70 ++++++++++++++++++++++++ src/Init/System/IO.lean | 6 +- src/runtime/process.cpp | 11 ++++ src/util/shell.cpp | 6 +- tests/bench/speedcenter.exec.velcom.yaml | 28 ++++++++-- 5 files changed, 113 insertions(+), 8 deletions(-) create mode 100644 script/benchReelabRss.lean diff --git a/script/benchReelabRss.lean b/script/benchReelabRss.lean new file mode 100644 index 0000000000..1475679c28 --- /dev/null +++ b/script/benchReelabRss.lean @@ -0,0 +1,70 @@ +import Lean.Data.Lsp +open Lean +open Lean.Lsp +open Lean.JsonRpc + +/-! +Tests language server memory use by repeatedly re-elaborate a given file. + +NOTE: only works on Linux for now. + +HACK: The line that is to be prepended with a space is hard-coded below to be sufficiently far down +not to touch the imports for usual files. +-/ + +def main (args : List String) : IO Unit := do + let leanCmd :: file :: iters :: args := args | panic! "usage: script <#iterations> ..." + let uri := s!"file:///{file}" + Ipc.runWith leanCmd (#["--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do + -- for use with heaptrack: + --Ipc.runWith "heaptrack" (#[leanCmd, "--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do + -- -- heaptrack has no quiet mode?? + -- let _ ← (← Ipc.stdout).getLine + -- let _ ← (← Ipc.stdout).getLine + let capabilities := { + textDocument? := some { + completion? := some { + completionItem? := some { + insertReplaceSupport? := true + } + } + } + } + Ipc.writeRequest ⟨0, "initialize", { capabilities : InitializeParams }⟩ + + let text ← IO.FS.readFile file + let mut requestNo : Nat := 1 + let mut versionNo : Nat := 1 + Ipc.writeNotification ⟨"textDocument/didOpen", { + textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }⟩ + for i in [0:iters.toNat!] do + if i > 0 then + versionNo := versionNo + 1 + let pos := { line := 19, character := 0 } + let params : DidChangeTextDocumentParams := { + textDocument := { + uri := uri + version? := versionNo + } + contentChanges := #[TextDocumentContentChangeEvent.rangeChange { + start := pos + «end» := pos + } " "] + } + let params := toJson params + Ipc.writeNotification ⟨"textDocument/didChange", params⟩ + requestNo := requestNo + 1 + + let diags ← Ipc.collectDiagnostics requestNo uri versionNo + if let some diags := diags then + for diag in diags.param.diagnostics do + IO.eprintln diag.message + requestNo := requestNo + 1 + + let status ← IO.FS.readFile s!"/proc/{(← read).pid}/status" + for line in status.splitOn "\n" |>.filter (·.startsWith "RssAnon") do + IO.eprintln line + + let _ ← Ipc.collectDiagnostics requestNo uri versionNo + (← Ipc.stdin).writeLspMessage (Message.notification "exit" none) + discard <| Ipc.waitForExit diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 7eae7c1d23..5666a25d8f 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -1367,8 +1367,7 @@ A child process that was spawned with configuration `cfg`. The configuration determines whether the child process's standard input, standard output, and standard error are `IO.FS.Handle`s or `Unit`. -/ --- TODO(Sebastian): constructor must be private -structure Child (cfg : StdioConfig) where +structure Child (cfg : StdioConfig) where private mk :: /-- The child process's standard input handle, if it was configured as `IO.Process.Stdio.piped`, or `()` otherwise. @@ -1428,6 +1427,9 @@ standard input is exhausted. @[extern "lean_io_process_child_take_stdin"] opaque Child.takeStdin {cfg : @& StdioConfig} : Child cfg → IO (cfg.stdin.toHandleType × Child { cfg with stdin := Stdio.null }) +/-- Returns the operating system process id of the child process. -/ +@[extern "lean_io_process_child_pid"] opaque Child.pid {cfg : @& StdioConfig} : Child cfg → UInt32 + /-- The result of running a process to completion. -/ diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp index 13c3c30d40..50b8bc3907 100644 --- a/src/runtime/process.cpp +++ b/src/runtime/process.cpp @@ -124,6 +124,11 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg c return lean_io_result_mk_ok(box(0)); } +extern "C" LEAN_EXPORT uint32_t lean_io_process_child_pid(b_obj_arg, b_obj_arg child) { + HANDLE h = static_cast(lean_get_external_data(cnstr_get(child, 3))); + return GetProcessId(h); +} + static FILE * from_win_handle(HANDLE handle, char const * mode) { int fd = _open_osfhandle(reinterpret_cast(handle), _O_APPEND); return fdopen(fd, mode); @@ -386,6 +391,12 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg c return lean_io_result_mk_ok(box(0)); } +extern "C" LEAN_EXPORT uint32_t lean_io_process_child_pid(b_obj_arg, b_obj_arg child) { + static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT + pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *)); + return pid; +} + struct pipe { int m_read_fd; int m_write_fd; }; static optional setup_stdio(stdio cfg) { diff --git a/src/util/shell.cpp b/src/util/shell.cpp index ba106b5349..1b2d0ef2fe 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -514,7 +514,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { buffer forwarded_args; buffer error_kinds; - while (true) { + while (!run) { // stop consuming arguments after `--run` int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL); if (c == -1) break; // end of command line @@ -561,6 +561,10 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { break; case 'r': run = true; + // apparently this call is necessary for `--run` to be permuted in front of any + // preceding file name arguments (we shouldn't permute *after* `--run` because those + // arguments are not ours) + getopt_long(argc, argv, g_opt_str, g_long_options, NULL); break; case 'o': olean_fn = optarg; diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 5784829b39..bf706fb9f4 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -59,25 +59,43 @@ tags: [fast] run_config: <<: *time - cmd: lean ../../src/Init/Prelude.lean -DElab.async=true + cmd: lean ../../src/Init/Prelude.lean - attributes: description: Init.Data.List.Sublist async tags: [fast] run_config: <<: *time - cmd: lean ../../src/Init/Data/List/Sublist.lean -DElab.async=true + cmd: lean ../../src/Init/Data/List/Sublist.lean - attributes: description: Std.Data.Internal.List.Associative tags: [fast] run_config: <<: *time - cmd: lean ../../src/Std/Data/Internal/List/Associative.lean -DElab.async=true + cmd: lean ../../src/Std/Data/Internal/List/Associative.lean - attributes: description: Std.Data.DHashMap.Internal.RawLemmas tags: [fast] run_config: <<: *time - cmd: lean ../../src/Std/Data/DHashMap/Internal/RawLemmas.lean -DElab.async=true + cmd: lean ../../src/Std/Data/DHashMap/Internal/RawLemmas.lean +- attributes: + description: Init.Data.BitVec.Lemmas + tags: [fast] + run_config: + <<: *time + cmd: lean ../../src/Init/Data/BitVec/Lemmas.lean +- attributes: + description: Init.Data.List.Sublist re-elab -j4 + run_config: + <<: *time + cmd: lean --run ../../script/benchReelabRss.lean lean ../../src/Init/Data/List/Sublist.lean 10 -j4 + max_runs: 2 +- attributes: + description: Init.Data.BitVec.Lemmas re-elab + run_config: + <<: *time + cmd: lean --run ../../script/benchReelabRss.lean lean ../../src/Init/Data/BitVec/Lemmas.lean 2 -j4 + max_runs: 2 - attributes: description: import Lean tags: [fast] @@ -428,4 +446,4 @@ tags: [fast] run_config: <<: *time - cmd: lean omega_stress.lean -DElab.async=true + cmd: lean omega_stress.lean