Nils Anders Danielsson
Nils Anders Danielsson
Perhaps we could avoid the conversions in `canonicalizeAbsolutePath` by using [`OsPath`](https://hackage.haskell.org/package/filepath-1.4.100.0/docs/System-OsPath.html) instead of `FilePath` and `String`. (Note that [`System.Directory.OsPath.canonicalizePath`](https://hackage.haskell.org/package/directory-1.3.8.0/docs/System-Directory-OsPath.html#v:canonicalizePath) supports `OsPath`.)
Imported modules might belong to other libraries with other `.agda-lib` files.
The module `library1/M.agda` might import `library2/N.agda`.
> _My teacher used to say: "don't just toss me a crumb" encouraging us to elaborate our arguments._ Please explain your scenario in more detail, so that we can make...
With recent changes, up to and including 57aa29153db7507e3d677be43b06221faa6dcd28, the number of calls to `stat`/`lstat` for an empty file, with no `~/.agda` directory, is 59: ``` stat("[…]/.agda/executables-2.6.3", 0x4200504660) = -1 ENOENT...
I suspect that some of the tags are default GitHub tags that we never used.
Duplicate of #560.
It [seems](https://github.com/agda/agda/issues/6090#issuecomment-1239916703) as if I had not used `-foptimise-heavily` when creating the [profile](https://github.com/agda/agda/issues/6090#issue-1363705189) which led me to create this issue. Perhaps it would be better to use something like `INLINABLE`...
The use of `workOnTypes` broke one of my tactics. The problem seems to be that `workOnTypes` changes how Agda reduces things: https://github.com/agda/agda/blob/1aa7b2e413f0cc68b1d737ac52e0d34a1fbe85f3/src/full/Agda/TypeChecking/Irrelevance.hs#L117-L126 I used the following code instead, and that...
I replaced `Pi` with a constructor that takes a new kind of telescope, and added a pattern synonym corresponding to the old `Pi` constructor. I also added a variant of...