Nils Anders Danielsson

The following code is rejected: ```agda {-# OPTIONS -Werror #-} open import Agda.Builtin.Nat data ⊥ : Set where record ⊤ : Set where data _⊎_ (A B : Set) :...

I don't think we need to support very old versions of Emacs, and I think it would be great if there was an active maintainer of the Emacs mode. @phikal,...

@phikal, your list contains a number of different suggestions. Please open separate issues for the (larger) items that you actually plan to work on. For minor things like replacing `set-input-method`...

Another option is to restrict the type of `runSpeculative` so that one can only return, say, a boolean. How is `runSpeculative` typically used?

I traced a program containing the call `canonicalizePath "/tmp/A/B/C/D/E/"`, and the trace included the following part: ``` stat64("/tmp/A/B/C/D/E", {st_mode=S_IFDIR|0775, st_size=4096, ...}) = 0 lstat64("/tmp", {st_mode=S_IFDIR|S_ISVTX|0777, st_size=614400, ...}) = 0 lstat64("/tmp/A",...

I replaced the implementation of `findProjectConfig'` with the following code: ```haskell findProjectConfig' dir = do dir >= \case Just conf -> return conf Nothing -> do libFiles return DefaultProjectConfig |...

I switched to [`takeDirectory`](https://hackage.haskell.org/package/filepath-1.4.2.1/docs/System-FilePath-Posix.html#v:takeDirectory). This is a semantic change. I suspect that the new semantics is more in line with what people expect. @jespercockx, what do you think?

> Then the number of calls dropped from 917 to 645. It seems as if I had missed to delete a `.agdai` file. Now I get 823 (but 645 if...

> Are you sure that the new method has the same behaviour under POSIX and Windows? The old method did not, did it? @andreasabel suggested that in some cases one...

The fact that (at least one time profile suggests that) about 10% of the allocations used by Agda when the standard library is type-checked are performed by `canonicalizeAbsolutePath` (see issue...