fix: #include <mutex> in mutex.cpp

[iacore]

succeeds #2091

Before this patch unique_lock refers to lean::unique_lock under certain conditions ( -DLEAN_MULTI_THREAD=OFF).

[gebner]

Before this patch unique_lock refers to lean::unique_lock under certain conditions ( -DLEAN_MULTI_THREAD=OFF).

That's the intended behavior. The LEAN_MULTI_THREAD flag should disable all multi-threading. That flag will also enable optimizations that are only safe if there's only a single thread. So you should never run LEAN_MULTI_THREAD=OFF build with multiple threads.

The actual issue is that Lean no longer builds with LEAN_MULTI_THREAD=OFF because adopt_lock_t doesn't exist, right? If that's the case, then we should add adopt_lock_t to the mutex.h stub. (With have no-op stubs for all threading/mutex operation when multi-threading is disabled.)

[iacore]

The actual issue is that Lean no longer builds with LEAN_MULTI_THREAD=OFF because adopt_lock_t doesn't exist, right?

Correct

If that's the case, then we should add adopt_lock_t to the mutex.h stub. (With have no-op stubs for all threading/mutex operation when multi-threading is disabled.)

I don't know about Lean enough to say either way.

This is the error I got when trying to build stage0 with MULTI_THREAD=OFF (latest master commit)

.../lean4/stage0/src/runtime/mutex.cpp: In function ‘lean::object* lean::lean_io_con
dvar_wait(b_obj_arg, b_obj_arg, obj_arg)’:
.../lean4/stage0/src/runtime/mutex.cpp:54:55: error: ‘adopt_lock_t’ is not a member 
of ‘std’
   54 |     unique_lock<mutex> lock(*basemutex_get(mtx), std::adopt_lock_t());
      |