Elan cgroup hacks

Stream: general

[Anne Baanen]

I got fed up that compiling lean + having a few editors open would consume all my ram even if each individual Lean process uses less than 8GB, and I decided that today would be a nice day for me to learn about cgroups, so here is a hack for elan to run all lean binaries inside the same cgroup:

From a7495a9f372e95c4020989ab9b13ac9988cd776e Mon Sep 17 00:00:00 2001
From: Vierkantor <vierkantor@vierkantor.com>
Date: Tue, 12 Oct 2021 12:44:50 +0000
Subject: [PATCH] feat: (Hackily) run inside a cgroup

---
 src/elan/command.rs | 34 ++++++++++++++++++++++++++++++++--
 1 file changed, 32 insertions(+), 2 deletions(-)

diff --git a/src/elan/command.rs b/src/elan/command.rs
index 0f92775..82b2480 100644
--- a/src/elan/command.rs
+++ b/src/elan/command.rs
@@ -2,6 +2,7 @@ use std::ffi::OsStr;
 use std::fs::File;
 use std::io::{self, Write, BufRead, BufReader, Seek, SeekFrom};
 use std::process::{self, Command, Stdio};
+use std::os::unix::process::CommandExt;
 use std::time::Instant;
 use regex::Regex;
 use tempfile::tempfile;
@@ -12,6 +13,35 @@ use notifications::*;
 use elan_utils;
 use telemetry::{Telemetry, TelemetryEvent};

+#[cfg(unix)]
+pub fn make_cgrouped_command<S: AsRef<OsStr>>(cmd: &Command,
+                                            arg0: &str,
+                                            args: &[S]) -> Command {
+    let mut new_cmd = Command::new("systemd-run");
+    new_cmd.arg0(arg0);
+    new_cmd.arg("--user");
+    new_cmd.arg("--slice=lean.slice");
+    new_cmd.arg("-t");
+    new_cmd.arg("-P");
+    new_cmd.arg("-d");
+    new_cmd.arg("-q");
+    new_cmd.arg("--wait");
+    new_cmd.arg("-G");
+    new_cmd.arg(cmd.get_program());
+    for arg in args {
+        new_cmd.arg(arg);
+    }
+    new_cmd
+}
+
+#[cfg(windows)]
+pub fn make_cgrouped_command<S: AsRef<OsStr>>(cmd: &Command,
+                                            arg0: &str,
+                                            args: &[S]) -> Command {
+    let mut new_cmd = Command::new(cmd.program());
+    new_cmd.args(args);
+    cmd
+}

 pub fn run_command_for_dir<S: AsRef<OsStr>>(cmd: Command,
                                             arg0: &str,
@@ -41,7 +71,7 @@ fn telemetry_lean<S: AsRef<OsStr>>(mut cmd: Command,

     let now = Instant::now();

-    cmd.args(args);
+    cmd = make_cgrouped_command(&mut cmd, arg0, args);

     let has_color_args = args.iter().any(|e| {
         let e = e.as_ref().to_str().unwrap_or("");
@@ -135,7 +165,7 @@ fn telemetry_lean<S: AsRef<OsStr>>(mut cmd: Command,
 fn exec_command_for_dir_without_telemetry<S: AsRef<OsStr>>(
     mut cmd: Command, arg0: &str, args: &[S]) -> Result<()>
 {
-    cmd.args(args);
+    cmd = make_cgrouped_command(&mut cmd, arg0, args);

     // FIXME rust-lang/rust#32254. It's not clear to me
     // when and why this is needed.
--
2.33.0

Configure systemd to limit the memory usage:

# ~/.config/systemd/user/lean.slice
[Slice]
MemoryHigh=12G

This works successfully with Lean 3 on the command line, in Emacs and in Neovim.

[Anne Baanen]

You should probably not actually do this yourself, which is why I used git format-patch output rather than link to a commit on GitHub, to make it slightly more difficult to apply the patch :)

[Julian Berman]

Fun. Another way to "handle" this would be not forking separate lean processes at all, right? As long as they're all using the same Lean version just speaking to one process entirely, even across the different editors? E.g. a very simple "frontend" process (which you run multiple of) which just forwards incoming LSP requests to a common single backend instance of the lean process

[Anne Baanen]

That also sounds reasonable, although I'm not sure how easy it would be forr the different threads to coordinate the memory usage limit. In essence, you'd be re-implementing cgroups from within Lean :)

[Yury G. Kudryashov]

Another solution is to use cgexec in editor settings.

[Yury G. Kudryashov]

(or write a bash wrapper around elan that uses cgexec)