Andreas Abel

Maybe just having or not having a flag is not enough structure to arrive at a satisfactory solution in these question. We might need authority levels. E.g. if I say...

> but I think we should also consider _readers_ of the code. If you are user of someone else's code, you maybe would not pass `--allow-unsolved-metas` on the command line...

@nad: If I understand your position correctly, you want to trust consistency of rendered code if you read `{-# OPTIONS --safe #-}` on top (and you are inclined to trust...

@anuyts: Usually, when I tried to produce a minimal counterexample from my suspicion what the problem is, I could not reproduce the problem. In my experience, one has to go...

> the cubical library is giving me a lot of warnings This is unfortunately the status quo atm, indexed inductive types are still not well-supported by Cubical Agda.

Keeping this issue open until `--allow-newer` becomes obsolete.

Thanks for the report! > Emacs v2.6.1.1-fce01db I see that you are not using the latest version of Agda. This would be either 2.6.2.2 (released) or 2.6.3 (unreleased, from this...

Thanks for reporting. > I don't think `reduce` should ever turn an argument that isn't `unknown` into an `unknown`. Could you add more evidence for your claim? From the bug...

Plain Agda does not produce regular outputs, so I suppose everything should go to `stderr`. Interaction-Agda (`agda --interaction`) does have regular outputs: commands to the client. These should go to...

Welcome to dig around, a starting point could be here: https://github.com/agda/agda/blob/bed2ecf8a9b00711779452e00b78a1a60fa8e542/src/full/Agda/Interaction/InteractionTop.hs#L1015 If I read this correctly Agda does not give `literally` when _refine_ changed something in the expression, like adding...