Andreas Abel

https://github.com/agda/agda/blob/5d30d8e7a25dfced02edefd82699f1f7b6f79316/src/full/Agda/Utils/Lens.hs#L23-L29 Correct is "lens outer inner": https://hackage.haskell.org/package/microlens-0.4.13.0/docs/Lens-Micro-Type.html#t:Lens-39-

Fix #5816: skip generating cubical clauses for Prop stuff

3

Fix #5816: skip generating cubical clauses for Prop stuff TODO: - [ ] disallow `--cubical` and `--prop` together?

Architectural problem: unhygienic import handling, lack of sandboxing

2

This issue points out a general problem in way Agda handles `import`s: The state accumulates the signatures of imported modules in a component `stImports : Signature`. This way information from...

Allow declarations in inner scopes to shadow declarations in outer scopes

6

Agda should allow declarations in inner scopes to shadow declarations in outer scopes, e.g.: ```agda postulate A : Set module M where postulate A : Set ``` This would also...

Cubic slowdown of variable generalization in the presence of instance search or unsolved metas

10

Felix @felixwellen observed slow checking of a longer telescope (https://github.com/agda/cubical/blob/1497d8bfdf817a83a441f57f3bb2a94fcd7c3fdf/Cubical/Algebra/Algebra/Base.agda#L103-L120). This telescope involves one free level variable that is generalized over, and a use of an instance (projecting the carrier...

Race condition in CI workflow `cabal-test`

3

E.g. https://github.com/agda/agda/runs/4013062137?check_suite_focus=true#step:9:725 ```diff Diff between actual and golden value: ======================================== --- a/private/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/Issue496735072-0.golden +++ b/private/var/folders/24/8k48jl6d249_n_qfxwsl6xvm0000gn/T/Issue496735072-1.actual @@ -1,3 +1,7 @@ +Agda.Builtin.Sigma.Σ.fst = + λ a → case a of Agda.Builtin.Sigma._,_ b _...

Caching in the stack.yml CI workflow done correctly?

6

Atm, we are restoring the cache after doing `stack update`: https://github.com/agda/agda/blob/7bda16229ef4728761a9b538f17bb63e20777618/src/github/workflows/stack.yml#L150-L166 A few questions: 1. Is `stack update` actually needed? Cannot find this step in e.g. https://github.com/freckle/stack-action/blob/605917bad6487161de15eea71f03163f9d37399f/action.yml 2. Does `stack...

Switch to `ghc-tags`, retire`hs-tags` ?

4

Switch to `hasktags`, retire our hand-crafted `hTags`.

`interaction` tests using `.hs` script are failing on github actions

13

The `interaction` testsuite started failing on github, see e.g. https://github.com/agda/agda/runs/2028943853?check_suite_focus=true, producing errors like: ``` Issue983.hs:«line»:«col»: error: Could not load module ‘Agda.Version’ It is a member of the package ‘Agda-2.6.2-F2BRXV7od3W7ndov7ntyY4’ which...

Cumulativity breaks invariance of concepts under definitional equality

6

This is rejected, but accepted if the `up A` index is replaced by its definition `A`: ```agda {-# OPTIONS --cumulativity --without-K #-} open import Agda.Primitive up : Set → Set₁...