Christian Doczkal

This problem has the potential to become more severe in the future. When compiling `DFHack` on `gcc-13.2` (specifically version `13.2.1_p20240113-r1` on Gentoo) there are a lot more plugins that have...

What about the following algorithm, which does not seem to be too hard to implement:: 1. When checking/updating the suspend status, also check if there is an item blocking the...

I would opt for a whitelisting rather than a blacklisting approach: 1. Specify a list of (useful) items with materials (i.e., iron bolts). If a mandate matches one of those,...

> The attached PR will make suspendmanager suspend the whole construction in both your cases. I think this is the right way to fix this. I like that it makes...

I am in favor of keeping the "Proof." visible, for the same reason as Fabian. Also, I disagree with calling displaying the existing blank lines in the source code as...

Maybe my proposal for (1) is overkill. It might be enough to just suppress everything except the "Proof." for folded one-line proofs. Here is a sequence of lemmas with short...

I would prefer something unobtrusive. Something that comes to mind is some icon: ```coq Lemma pathp_rev x y p : pathp x y p -> pathp y x (srev p)....

@fakusb @palmskog I'm trying to revive this issue, because I'm trying to update one of my projects and I still find this pretty annoying. I find myself agreeing with Tobias:...

> @chdoc what do you think of the solution we used in Lemma Overloading and some other projects: https://coq-community.org/lemma-overloading/docs/v8.11.0/coqdoc/LemmaOverloading.heaps.html Looks like another reasonable compromise to me, even though the behavior...

> For one part of my defense (FWIW) you are not supposed to unfold `fsetI` ;) Yes, I realized that. Indeed, unfolding the defined operations can cause even more "funny"...