Stream: general

Topic: How to compile lean without MULTI_THREAD?

Jason Rute (Oct 02 2020 at 12:27):

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 (Oct 02 2020 at 12:29):

Append -DMULTI_THREAD=OFF to your cmake cmdline

Sebastian Ullrich (Oct 02 2020 at 12:29):

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

Gabriel Ebner (Oct 02 2020 at 12:30):

Probably like the javascript version.

Sebastian Ullrich (Oct 02 2020 at 12:30):

Right, that would make sense :)

Jason Rute (Oct 02 2020 at 12:31):

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

Last updated: May 13 2021 at 22:15 UTC