diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 6a264686f099..fd338e09d76b 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -802,8 +802,11 @@ def run (args : SpawnArgs) : IO String := do end Process -/-- Returns the thread ID of the calling thread. -/ -@[extern "lean_io_get_tid"] opaque getTID : BaseIO UInt32 +/-- +Returns an ID identifying the current thread. May not be identical to the operating system's thread +id. +-/ +@[extern "lean_io_get_thread_id"] opaque getLeanThreadID : BaseIO UInt64 structure AccessRight where read : Bool := false diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 20611d0aa98e..ea7c9330c5ff 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -434,7 +434,7 @@ which is reported in the returned snapshot. -/ def runAsyncAsSnapshot (act : TermElabM Unit) (desc := "") : TermElabM (Task Language.SnapshotTree) := do let t ← runAsync do - let tid ← IO.getTID + let tid ← IO.getLeanThreadID modifyTraceState fun _ => { tid } try withTraceNode `Elab.async (fun _ => return desc) do diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 0618150d618f..745c747bff17 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -65,7 +65,7 @@ structure TraceElem where structure TraceState where /-- Thread ID, used by `trace.profiler.output`. -/ - tid : UInt32 := 0 + tid : UInt64 := 0 traces : PersistentArray TraceElem := {} deriving Inhabited diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp index da7b5f9bea06..04449f579618 100644 --- a/src/runtime/process.cpp +++ b/src/runtime/process.cpp @@ -316,9 +316,17 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) { return lean_io_result_mk_ok(box_uint32(getpid())); } -extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) { - static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT - return lean_io_result_mk_ok(box_uint32(gettid())); +extern "C" LEAN_EXPORT obj_res lean_io_get_thread_id(obj_arg) { + uint64_t tid; +#ifdef LEAN_WINDOWS + tid = GetCurrentThreadId(); +#elif defined(__APPLE__) + pthread_threadid_np(NULL, &tid); +#else + // should use gettid, but that is glibc 2.30+ + tid = static_cast(pthread_self()))); +#endif + return lean_io_result_mk_ok(box_uint64(static_cast(pthread_self()))); } extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {