Running a command last

Stream: lean4

[Damiano Testa]

With the parallel elaboration of Lean files, most command have a chance of finishing their elaboration in a non-sequential order. Is it possible to tell one command (say the last one of a file), to be processed only when everything else has finished processing?

[Sebastian Ullrich]

You can wait on the kernel env for that, Environment.toKernelEnv

[Damiano Testa]

I have been trying to play with docs#Lean.Environment.toKernelEnv, but I am not sure that I know how to use it. Should I simply add

  let env ← getEnv
  let _ := env.toKernelEnv

to my code?

[Damiano Testa]

Also, while investigating this issue, I think that what I actually wanted was to wait for the linters to have finished elaborating. Is there a way to make a command execute after all the previous (from the perspective of command location in the file) linter calls have completed?

[Damiano Testa]

Also, while I would like to have an answer to the above, I was also wondering if it is possible to access the whole syntax tree of a file. E.g. something that has a root node and then every command as a child of this root node, or something similar.

[Damiano Testa]

(Having this "module syntax tree" would bypass for me the need to wait for linter execution, although I would still be curious to know if it is possible to wait for them anyway!)