test: re-elaboration benchmarks (#7784)

Tests language server memory use by repeatedly re-elaborate a given file

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 <lean> <file> <#iterations> <server-args>..."
+  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

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.
 -/

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<HANDLE>(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<intptr_t>(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<pipe> setup_stdio(stdio cfg) {

src/util/shell.cpp

@@ -514,7 +514,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
     buffer<string_ref> forwarded_args;
     buffer<name> 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;

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