Nils Anders Danielsson

> I'm building Agda with cabal 3.0.0.0 for weeks. It always work Then perhaps the makefile could be updated to use `install` instead of `v1-install`. (Just dropping the `v1-` prefix...

One issue with Nix-style builds is that the `agda` binary is stored in a [new location](https://www.haskell.org/cabal/users-guide/nix-local-build.html#where-are-my-build-products), which varies depending on things like the OS and the version of GHC. Our...

I have read up on and tested some of the `v2-` commands. The new Nix-style builds are sort of like Cabal sandboxes with a global cache. This sounds good, and...

> Perhaps we could use something like `cabal v2-run` instead. That seems to make `agda --help` quite a bit slower (more than 0.1 s on my machine), and the test...

> I noticed that `cabal v2-install` rebuilds the package from scratch if it isn't built already. However, `cabal v2-build` seems to reuse earlier results. Unfortunately it seems as if `v2-install`...

One possible drawback of `v2-install` is that all data files (like the Emacs mode) are installed in the Cabal tree (in my case under `~/.cabal/`), and as far as I...

It seems as if we can build Agda without optimisations, in a separate build directory, by running `cabal v2-build --project-file=Agda-quick.project --builddir=dist-quick -fenable-cluster-counting`, where `Agda-quick.project` contains the following text: ``` packages:...

It seems as if Cabal 3 uses separate build directories automatically, one component of the build path is called `noopt`: ``` [369 of 369] Compiling Agda.Main ( src/full/Agda/Main.hs, […]/dist-quick/build/i386-linux/ghc-8.8.3/Agda-2.6.1/noopt/build/Agda/Main.o )...

> Would anything break if we allow a reduction rule to be enabled and disabled? Subject reduction?

I think it would suffice to set the fifth argument of `read-string` to a non-nil value in the implementation of `string-rectangle` (and similar procedures). The value of this argument could...