test: re-enable re-elab benchmarks and add watchdog re-elab benchmark (#11284)

script/benchReelabRss.lean

@@ -10,6 +10,16 @@ Tests language server memory use by repeatedly re-elaborate a given file.
 NOTE: only works on Linux for now.
 -/
 
+def determineRSS (pid : UInt32) : IO Nat := do
+  let status ← IO.FS.readFile s!"/proc/{pid}/smaps_rollup"
+  let some rssLine := status.splitOn "\n" |>.find? (·.startsWith "Rss:")
+    | throw <| IO.userError "No RSS in proc status"
+  let rssLine := rssLine.dropPrefix "Rss:"
+  let rssLine := rssLine.dropWhile Char.isWhitespace
+  let some rssInKB := rssLine.takeWhile Char.isDigit |>.toNat?
+    | throw <| IO.userError "Cannot parse RSS"
+  return rssInKB
+
 def main (args : List String) : IO Unit := do
   let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
   let file ← IO.FS.realPath file
@@ -34,11 +44,14 @@ def main (args : List String) : IO Unit := do
     let text ← IO.FS.readFile file
     let (_, headerEndPos, _) ← Elab.parseImports text
     let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
+    let n := iters.toNat!
+    let mut lastRSS? : Option Nat := none
+    let mut totalRSSDelta : Int := 0
     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
+    for i in [0:n] do
       if i > 0 then
         versionNo := versionNo + 1
         let params : DidChangeTextDocumentParams := {
@@ -61,9 +74,16 @@ def main (args : List String) : IO Unit := 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 rss ← determineRSS (← read).pid
+      -- The first `didChange` usually results in a significantly higher RSS increase than
+      -- the others, so we ignore it.
+      if i > 1 then
+        if let some lastRSS := lastRSS? then
+          totalRSSDelta := totalRSSDelta + ((rss : Int) - (lastRSS : Int))
+      lastRSS? := some rss
+
+    let avgRSSDelta := totalRSSDelta / (n - 2)
+    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
 
     let _ ← Ipc.collectDiagnostics requestNo uri versionNo
     (← Ipc.stdin).writeLspMessage (Message.notification "exit" none)

script/benchReelabWatchdogRss.lean

@@ -0,0 +1,89 @@
+import Lean.Data.Lsp
+import Lean.Elab.Import
+open Lean
+open Lean.Lsp
+open Lean.JsonRpc
+
+/-!
+Tests watchdog memory use by repeatedly re-elaborate a given file.
+
+NOTE: only works on Linux for now.
+-/
+
+def determineRSS (pid : UInt32) : IO Nat := do
+  let status ← IO.FS.readFile s!"/proc/{pid}/smaps_rollup"
+  let some rssLine := status.splitOn "\n" |>.find? (·.startsWith "Rss:")
+    | throw <| IO.userError "No RSS in proc status"
+  let rssLine := rssLine.dropPrefix "Rss:"
+  let rssLine := rssLine.dropWhile Char.isWhitespace
+  let some rssInKB := rssLine.takeWhile Char.isDigit |>.toNat?
+    | throw <| IO.userError "Cannot parse RSS"
+  return rssInKB
+
+def main (args : List String) : IO Unit := do
+  let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
+  let file ← IO.FS.realPath file
+  let uri := s!"file://{file}"
+  Ipc.runWith leanCmd (#["--server", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do
+    let capabilities := {
+      textDocument? := some {
+        completion? := some {
+          completionItem? := some {
+            insertReplaceSupport? := true
+          }
+        }
+      }
+    }
+    Ipc.writeRequest ⟨0, "initialize", { capabilities : InitializeParams }⟩
+    discard <| Ipc.readResponseAs 0 InitializeResult
+    Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩
+
+    let text ← IO.FS.readFile file
+    let (_, headerEndPos, _) ← Elab.parseImports text
+    let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
+    let n := iters.toNat!
+    let mut lastRSS? : Option Nat := none
+    let mut totalRSSDelta : Int := 0
+    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 params : DidChangeTextDocumentParams := {
+          textDocument := {
+            uri      := uri
+            version? := versionNo
+          }
+          contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
+            start := headerEndPos
+            «end» := headerEndPos
+          } " "]
+        }
+        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
+
+      Ipc.waitForILeans requestNo uri versionNo
+
+      let rss ← determineRSS (← read).pid
+      -- The first `didChange` usually results in a significantly higher RSS increase than
+      -- the others, so we ignore it.
+      if i > 1 then
+        if let some lastRSS := lastRSS? then
+          totalRSSDelta := totalRSSDelta + ((rss : Int) - (lastRSS : Int))
+      lastRSS? := some rss
+
+    let avgRSSDelta := totalRSSDelta / (n - 2)
+    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
+
+    let _ ← Ipc.collectDiagnostics requestNo uri versionNo
+    Ipc.shutdown requestNo
+    discard <| Ipc.waitForExit

tests/bench/speedcenter.exec.velcom.yaml

@@ -116,18 +116,31 @@
     cmd: lean -Dexperimental.module=true Init/Data/BitVec/Lemmas.lean
 - attributes:
     description: Init.Data.List.Sublist re-elab -j4
+    tags: [other]
   run_config:
     <<: *time
     cwd: ../../src
     cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true
     max_runs: 2
+    parse_output: true
 - attributes:
     description: Init.Data.BitVec.Lemmas re-elab
+    tags: [other]
   run_config:
     <<: *time
     cwd: ../../src
-    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/BitVec/Lemmas.lean 2 -j4 -Dexperimental.module=true
+    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/BitVec/Lemmas.lean 3 -j4 -Dexperimental.module=true
     max_runs: 2
+    parse_output: true
+- attributes:
+    description: Init.Data.List.Sublist re-elab -j4 (watchdog rss)
+    tags: [other]
+  run_config:
+    <<: *time
+    cwd: ../../src
+    cmd: lean --run ../script/benchReelabWatchdogRss.lean lean Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true
+    max_runs: 2
+    parse_output: true
 - attributes:
     description: import Lean
     tags: [other]