Wojciech Nawrocki

@tydeu thank you for looking into this! The two feature requests you point out roughly correspond to my two messages above, which are indeed different. For widgets, specifying dependencies *before*...

> I am sorry, but I do not understand what you are saying here at all. In short, I'd like to tell Lake somehow that the target for `CommDiag.lean` is...

@liberninja unfortunately not. This seriously messes up my graphs, so I will try to submit a fix when time allows.

@jul1u5 thanks for your interest! For generalizing to different kinds of diagrams, there are at least two mostly unrelated tasks. - One is just about the widget implementation. There is...

Something that works for me (or at least seems to work, so far) is that `cached` can be used to store (well, cache) partial compilation results. For example, pandoc compilation...

Hm, it looks like the CI build actually [sets `CMAKE_C_COMPILER` to a custom LLVM under `stage1/bin`](https://github.com/leanprover/lean4/actions/runs/7232967915/job/19707731194#step:11:53). Before this PR, the stage0 build was still [using the system compiler](https://github.com/leanprover/lean4/actions/runs/7228723799/job/19698609546?pr=3078#step:11:79) instead of...

Work from coco is currently in the process of being merged into crossbeam, so in the foreseeable future this crate should be able to use `Atomic` with destructors.

Can [`assoc_rewrite`](https://github.com/leanprover-community/mathlib/blob/c9cfafc922927c4fc157a4acc2e8df984d3e74bd/src/tactic/rewrite.lean#L198) do it?

Hi! One thing you could try would be to run `Developer: Toggle Developer Tools` from the command panel and paste the contents of the `Console` tab here (using `` to...

@mhuisi that is a valid concern, but I have not found it to be that much of an issue, at least when edits sufficiently low-frequency. This is often the case...