feat: creation and reporting for asynchronous elaboration tasks

Kha commented 3 days ago

This PR adds core metaprogramming functions for forking off background tasks from elaboration such that their results are visible to reporting and the language server

Kha commented 3 days ago

!bench

leanprover-community-bot commented 3 days ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1126407d9b8358248ccf2f6bdc36787633c40887 --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-22 13:38:10)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5adcd520faae2623be978fab48dcd84aad90440b --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-22 17:17:06)

leanprover-bot commented 3 days ago

Here are the benchmark results for commit b1d6c26a51ba45b2713e744ca4ed9c490afb210f. There were no significant changes against commit 1126407d9b8358248ccf2f6bdc36787633c40887.

leanprover / lean4

feat: creation and reporting for asynchronous elaboration tasks #6170