Andreas Abel

Test sum1PrismManualChar === sum1TypePrismChar failing with GHC >= 9.12

2

https://github.com/kcsongor/generic-lens/actions/runs/17205258848/job/48804341052#step:27:142 ``` test/Spec.hs:257:6: sum1PrismManualChar === sum1TypePrismChar failed: inequal terms: join { $j_suPT a1 = Left (pure $dApplicative_ajg1 a1) } in case x of wild_X1E { A i -> Right i;...

Take over HsYAML and HsYAML-aeson ?

3

Dear dhall maintainers, HsYAML(-aeson) does not have any users on Stackage (https://www.stackage.org/nightly-2025-08-30/package/HsYAML-0.2.1.5), but `dhall-yaml` depends on it. I have been maintaining HsYAML for a couple of years but I am...

Simple Bool-contradiction lemma?

13

Would there be a place for this simple lemma in the standard library? ```agda Bool-contradiction : ∀ {ℓ} {A : Set ℓ} {b : Bool} → b ≡ true →...

Previously, a change in an opaque block would invalidate the whole block. Now, cache is only invalidated starting with the first changed declaration in the opaque block. Would be nice...

Update -WUnusedImports to take modules into consideration

2

@copilot Task: Update `-WUnusedImports` to take modules into consideration. PR #8226 introduced a new warning `UnusedImports` with a logic as laid down in the new module `Agda.Syntax.Scope.UnusedImports`: - For every...

RepeatedNamesInImportDirective error too strict

2

This is an error (testcase for #3331): ```agda open import Agda.Builtin.Bool using (true) renaming (true to tt) ``` ``` error: [RepeatedNamesInImportDirective] Repeated name in import directive: true ``` However, I...

```agda -- Andreas, 2025-12-02 -- Weird parse error location with forgotten space at the end of pragma. {-# OPTIONS --universe-polymorphism#-} -- ^ note: forgotten space before # data D {l}...

Premature mangling of import directives

5

Issue description and plan how to fix here: https://github.com/agda/agda/blob/8f59957c43fdf0aa03fb468ab176d57d8d4aff0c/test/Bugs/ManglingOfImportDirectives.lagda.md https://github.com/agda/agda/blob/8f59957c43fdf0aa03fb468ab176d57d8d4aff0c/test/Bugs/ManglingOfImportDirectives.lagda.md?plain=1#L1-L87

1. Build Agda optimized and benchmark e.g. the standard library. 2. Replace `Control.Monad.Writer` (the lazy version) by `Control.Monad.Writer.CPS` everywhere. 3. Again build Agda and benchmark. 4. Report the performance diff....

Ignore forced constructor arguments in termination checker (safe?)

6

This is for our collection of performance issues. Would be interesting to see whether `tog` has the same problem. Since it uses induction-induction, we cannot test it in Coq at...