Andreas Abel

Thanks! So it seems that it is not the case that `canonicalizePath` can violate `isAbsolute`, or at least it is not easily reproducible. Adding a test for this issue will...

If we want to get rid of `canonicalizePath` (other than its uses for canonicalizing a path for use in our index structures), then we have to find an alternative implementation...

Testing `canonicalizePath` on UNC paths shows some gliches: ```haskell import System.Directory import System.FilePath list :: FilePath -> IO () list dir = do putStrLn $ replicate 66 '-' putStrLn dir...

Suggestion (Agda dev 2025-10-15), @plt-amy) : Make a "known issues" section in the CHANGELOG / docs and describe it here.

> Cornelis is essentially the only client that communicates with Agda over json. Ah, good to know, I thought `--interaction-json` didn't have any users anymore. > Agda formats constraints on...

`--guardedness` is an infective option, but those warnings _should_ be filtered out: https://github.com/agda/agda/blob/822e0aee235ba787b7ac50cc7ab19fca20be5924/src/full/Agda/Interaction/BuildLibrary.hs#L95-L104 Not sure why this does not work in all situations yet.

`--agda` is just one of the options of the Haskell backend: ``` Special options for the Haskell backend -p NAMESPACE --name-space=NAMESPACE Prepend NAMESPACE to the package/module name -d Put Haskell...

Yeah, `--build-library` is quite buggy still. This is probably the same issue as: - #8005

@jneira wrote: > iirc you can install tarballs with `cabal install path/to/package.tar.gz`, is it not suitable for your workflow? You cannot with `v2-install`, at least in 2025.

This issue comes with a detailed description and plan how to fix so it could be assigned to copilot or someone who wants to learn about the Agda code base....