feat: thread initialization for reverse FFI

[Kha]

Makes it possible to properly allocate and free thread-local runtime resources for threads not started by Lean itself

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6af7a01af643e82e1deeb6b7523b8099d177b159 --onto 611b1746896bbadf459c00cc218fa31cf51b4e08. (2024-03-07 14:02:33)

[digama0]

Wondering if you noticed #2464 ...

[Kha]

@digama0 Oh no, I didn't remember that one... I'd like to start small driven by practical needs, e.g. lean_finalize* seems unobjectionable to me but thread finalizers are a bit more fringe and I don't even know whether post finalizers will stay around

[digama0]

There is more info on the Zulip thread. The basic motivation is that FFI should be able to do all the same lifecycle things that lean does so that it can correctly initialize lean code when lean is not running the show. This has in fact stopped some FFI projects of mine with no recourse. As an example where thread finalizers are needed, suppose there is a lean object stored in some thread local state which is not managed by lean. This object will not be cleaned up properly when the thread goes down and may corrupt lean if the same CPU is reused for another thread.

If we get rid of post_finalize then they would also disappear from this interface; I don't think there is any stability promised in that regard.