[feature request] Option for pickling imported environment completely, not just diff from imports - so that they can be recovered fast in one command without re-doing the fully-fledged imports

[vadimkantorov]

This is needed because Lean issues ~100K I/O syscalls when processing mathlib imports. This can stall the whole server, when there are a hundred of parallel REPL processes.

So being able to quickly pre-load the environment instead of waiting for import Mathlib would simplify a lot the operation of REPL servers.

In https://github.com/leanprover-community/repl?tab=readme-ov-file#pickling is written: we don't record full Environments, only the changes relative to imports. The other side of trade-off is also useful: large pickled files, but no need to process import Mathlib (and its I/O syscalls)