How to compile lean without MULTI_THREAD?

Stream: general

[Jason Rute]

I'm going to preface this with the fact that I really have no experience with C++ development, even compiling C++ code. Having said that, I'd like to try to compile Lean with MULTI_THREAD off (where MULTI_THREAD is from this file.) That will make sure we don't set the LEAN_MULTI_THREAD flag, which forces some delays in the server. I'd like to try running the lean server (from Python) without this flag so that I can see how it behaves. Is it significantly faster, but still reliable?

Anyway, how would I go about doing that? Should I just clone lean, set option(MULTI_THREAD "MULTI_THREAD" ON) to OFF, and then compile from sources as normal?

[Sebastian Ullrich]

Append -DMULTI_THREAD=OFF to your cmake cmdline

[Sebastian Ullrich]

But I don't recall how the server will behave with that flag turned off

[Gabriel Ebner]

Probably like the javascript version.

[Sebastian Ullrich]

Right, that would make sense :)

[Jason Rute]

Thanks! Anything I should look out for when running it?