Nils Anders Danielsson

One dependency was broken. I could fix the problem by unregistering this dependency and removing the local build trees.

Oh, I forgot that I had also commented out the body of the `install-deps` target.

> I wouldn't classify this as `release blocker` since this looks more like a unicorn. Anyway, shouldn't block the release candidate. Hopefully no-one else has this problem.

I may have stumbled over the same error today. Here is my test case: ```agda postulate A : Set variable x : A record R (x : A) : Set₁...

> If we don't have `--save-metas`, then none of `bs`, `sigRewriteRules` and `disp` are instantiated and traversed for reachability. Hence, the metas which only occur in these will be eliminated,...

At first glance this sounds like a good idea, if we disregard the non-negligible implementation cost. Have you evaluated how this would impact the implementation and the user experience? The...

I put this in the icebox for now. If we come to the conclusion that this is a good idea, and someone is willing to actually do the work, then...

We're typically not sending plain strings to Emacs, but rather sexps (serialised as strings).

> The current challenge is that type checking could be slow on large files (4k LOC). *Parsing* can be slow for large files (#5670).

> Checking section applications in `noMutualBlock` seems the right thing to do, because things getting into scope by some module instantiation cannot possibly be mutual with other definition. After all,...