Closed CudraniaTrec closed 11 months ago
Hello!
Thank you for opening an issue and for finding this library useful :slightly_smiling_face: This library is very recent and we are still doing major changes, so it might be a bit unstable for now. We are only testing it on Linux, but we would be very happy to support MacOS as well!
Since I don't have the chance to test it on a MacOS environment, could you try to change this line: https://github.com/sr-lab/coq-lsp-pyclient/blob/eb98ddc851b6b4b685b72f646ef46632daf49f38/coqlspclient/coq_lsp_client.py#L59
To this:
f"ulimit -v {memory_limit} ; coq-lsp",
It's just an extra space after the }
.
If that does not work, please try to change the ;
to &&
.
I'm suspecting that the way the MacOS shell is parsing the command is different from the way the shells we use on Linux parse it (it's a wild guess, but let's see). And so, what happens is that the argument sent to ulimit
is 2097152;
instead of 2097152
.
Hello!
Thank you for opening an issue and for finding this library useful 🙂 This library is very recent and we are still doing major changes, so it might be a bit unstable for now. We are only testing it on Linux, but we would be very happy to support MacOS as well!
Since I don't have the chance to test it on a MacOS environment, could you try to change this line:
To this:
f"ulimit -v {memory_limit} ; coq-lsp",
It's just an extra space after the
}
. If that does not work, please try to change the;
to&&
.I'm suspecting that the way the MacOS shell is parsing the command is different from the way the shells we use on Linux parse it (it's a wild guess, but let's see). And so, what happens is that the argument sent to
ulimit
is2097152;
instead of2097152
.
It seems this change doesn't work... I just guess macos's ulimit command supports different argument formats, since neither google nor ChatGPT can give me a clear answer.
Again, thans for your project, it helps me a lot in interacting with Coq.
Hello! Thank you for opening an issue and for finding this library useful 🙂 This library is very recent and we are still doing major changes, so it might be a bit unstable for now. We are only testing it on Linux, but we would be very happy to support MacOS as well! Since I don't have the chance to test it on a MacOS environment, could you try to change this line: https://github.com/sr-lab/coq-lsp-pyclient/blob/eb98ddc851b6b4b685b72f646ef46632daf49f38/coqlspclient/coq_lsp_client.py#L59
To this:
f"ulimit -v {memory_limit} ; coq-lsp",
It's just an extra space after the
}
. If that does not work, please try to change the;
to&&
. I'm suspecting that the way the MacOS shell is parsing the command is different from the way the shells we use on Linux parse it (it's a wild guess, but let's see). And so, what happens is that the argument sent toulimit
is2097152;
instead of2097152
.It seems this change doesn't work... I just guess macos's ulimit command supports different argument formats, since neither google nor ChatGPT can give me a clear answer.
Again, thans for your project, it helps me a lot in interacting with Coq.
I created a VM with MacOS catalina (I wasn't able to create a VM for newer versions) and I was able to run all the tests without changes to the code. I was trying to replicate your problem but apparently it might be specific to newer versions of MacOS. What version are you using?
I'm using MacOS Ventura 13.0.
I'm using MacOS Ventura 13.0.
Apparently newer versions of MacOS do not support the usage of ulimit to limit RAM usage. I removed the call to ulimit
in MacOS.
I'm trying to run the tests on my macmini, but each time the program prints a lot of
" /bin/sh: line 0: ulimit: virtual memory: cannot modify limit: Invalid argument /bin/sh: line 0: ulimit: virtual memory: cannot modify limit: Invalid argument ..."
after looking up the code, I changed the 60 line of coqlspclient/coq_lsp_client.py, turning the "ulimit -v {memory_limit};" into "ulimit -v unlimited;" then the annoying messages disappeared.
I'm not sure whether it's the fault of the ulimit command or macos...