Andreas Abel

Inner `.agda-lib` takes precedence over outer `.agda-lib` used for `--build-library`

1

It seems that an additional `.agda-lib` file in a sub-directory silently takes over even when type checking was started with `agda --build-library` from the project root. Reproducer: - `/Main.agda-lib` with...

Non-normalized level printed for interactive "show constraints" and "solve"

2

```agda open import Agda.Primitive postulate Rel : ∀{a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ) Lex : ∀{a ℓ₁ ℓ₂} {A : Set a}...

`Normalise` does not normalize `Level` (anymore ?)

4

When investigating double checking, I got weird `NotLeqLevel` errors for `Set1` and `Set (lsuc lzero)` (which should be clearly equal). It seems Agda does not normalize levels correctly anymore: https://github.com/agda/agda/blob/94ff685b05db59874cb118acc223c4dc13945285/src/full/Agda/TypeChecking/Reduce.hs#L1294-L1298...

Missing test that `--caching` actually does the caching

3

The testsuite has tests that make sure that `--caching` does not break anything, but no tests yet that `--caching` does anything.

Build with Agda 2.6.3

1

- **Remove trailing whitespace** (Just for one module which I touched.) The following commits make `all.agda` build with Agda 2.6.3 (if I comment out `OEIS-A000001.agda` which exceeded my patience). -...

Nix workflow broken on macos-latest (macos-15-arm64)

1

https://github.com/haskell/hackage-server/actions/runs/17315560040/job/49157667263#step:3:97 > mv: fastcopy: open() failed (to): /usr/bin/rmz: Read-only file system Upstream issue: - https://github.com/wimpysworld/nothing-but-nix/issues/39 CC @peterbecich

Possible race condition when creating `.cabal/store/ghc-....`

2

After a fresh install of GHC 9.14 rc3: ``` $ cabal build Resolving dependencies... Build profile: -w ghc-9.14.0.20251128 -O1 In order, the following will be built (use -v for more...

`cabal v2-install` silently ignores `--run-tests`, but docs suggests it should work

5

https://github.com/haskell/cabal/blob/8365cec87198fce066bc8389604e285eddfe1d9a/doc/cabal-project-description-file.rst?plain=1#L1050-L1068 > Run package test suite during installation. I understand this sentence as `cabal v2-install --run-tests` should run the tests. It doesn't. It also does not alert the user that...

`cabal v2-install`ed executables should be resilient against (partial) deletion of `.cabal/store`

9

According to #6506, the default `--install-method` _on Windows_ is `copy` instead of `symlink`. I think this is the more sensible default _in general_. From `v1-install` I am used to get...

Missing top command `CornelisShowConstraints` (Emacs `C-c C-=`)

4

Feature request: add `CornelisShowConstraints`, equivalent of Emacs `C-c C-=`. This displays the solution for the interaction metas that have been found by unification (if any). It is the command `Cmd_constraints`...