Richard Copley

`std::coroutines` in INTERFACE_LINK_LIBRARIES breaks cmake packages that consume libunifex

4

The CMake config file installed with unifex (_e.g._, `/usr/local/cmake/lib/unifexConfig.cmake`) contains the following: ``` set_target_properties(unifex::unifex PROPERTIES INTERFACE_COMPILE_FEATURES "cxx_std_17" INTERFACE_INCLUDE_DIRECTORIES "${_IMPORT_PREFIX}/include" INTERFACE_LINK_LIBRARIES "std::coroutines" ) ``` Having std::coroutines in `INTERFACE_LINK_LIBRARIES` means a package...

Fix magit-section usage so the expand/contract functionality works

4

Use named sections so magit-section can track which sections are expanded. Don't use sections for individual diagnostics, since they can't be tracked. Capture data in lexicals for deferred rendering by...

'Building X' diagnostic for every dependency when processing imports

1

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues)....

A lemma of B. H. Neumann.

1

Let the group $G$ be the union of finitely many, let us say $n$, left cosets of subgroups $C₁$, $C₂$, ..., $Cₙ$: $$G = ⋃_{i = 1}^n C_i g_i.$$ Then...