Nils Anders Danielsson

> If you are worried about _renderings_ of the code, well, I can easily postprocess generated HTML so that I sneak in an `{-# OPTIONS --safe #-}`. There is no...

This makes sense to me. (But I think we should discuss the design as part of issue #5265.)

I don't think we should add new features right before the release.

András [credits](https://github.com/AndrasKovacs/elaboration-zoo/blob/48a31b642745830458fc26cbaecd3628e691457d/GluedEval.hs#L6-L8) the idea to @ollef (see [sixty](https://github.com/ollef/sixty)).

@AndrasKovacs, we discussed glued evaluation during the Agda meeting today. Do you have any concrete, preferably small examples that show that one gets smaller meta-variable solutions if glued evaluation is...

Related: #3094.

> Predates me. My guess is that they _act_ on nullary quantities, i.e. sets, and therefore they live in the nullary module. @nad might be able to confirm or deny?...

Which parts of the output do you think should go to stderr? We have at least three categories: errors, warnings, and other messages corresponding to different verbosity levels.

I have trouble building the code (1309bdb41cc6cc9066f93bd5cc51cf9dfec7c236). I have repeatedly encountered the following internal error (on a 32-bit system): ``` [346 of 400] Compiling Agda.TypeChecking.Rules.LHS ( src/full/Agda/TypeChecking/Rules/LHS.hs, dist-2.6.2-ghc-8.10.4/build/Agda/TypeChecking/Rules/LHS.o, dist-2.6.2-ghc-8.10.4/build/Agda/TypeChecking/Rules/LHS.dyn_o )...

I tried to build using GHC 9.0.1 instead, but it appears as if this branch does not contain the commits related to #4955.