Andreas Abel

Reproduce errors in createMissingHCompClause

2

These errors are not covered by our testsuite: https://github.com/agda/agda/blob/a7edb851ddbd2eff62fab399542a22fdb68b909e/src/full/Agda/TypeChecking/Coverage/Cubical.hs#L1169-L1170 https://github.com/agda/agda/blob/a7edb851ddbd2eff62fab399542a22fdb68b909e/src/full/Agda/TypeChecking/Coverage/Cubical.hs#L1189-L1196 Any experts that can trigger them? @plt-amy @Saizan

Allow entries `name = path` in the `executables` file.

8

This is mainly motivated by the testsuite where make AGDA_BIN=agda-quicker succeed would error because `execTC` wants to invoke `agda` but the `executables` file will naturally allow invocation of `agda-quicker`. A...

https://github.com/agda/agda/blob/3a9d3893737b3a47c57e1c997f588931d592b0b6/doc/user-manual/language/safe-agda.lagda.rst?plain=1#L11-L15 In the list following here, only postulates and certain options are mentioned, but not the pragmas ruled out by `--safe`, e.g. `TERMINATING`, `NO_UNIVERSE_CHECK` etc.

See https://github.com/agda/agda/pull/7336/files#r1676781758 https://github.com/agda/agda/blob/a381060cdd040ce7511626cbe2223e8301c65b02/src/full/Agda/Compiler/MAlonzo/Compiler.hs#L440-L444

Irrefutable matching in binders does not deliver expected results for non-eta patterns

13

```agda module _ (A : Set) (P : A → Set) (p : (a : A) → P a) where module Eta where record Wrap : Set where constructor wrap...

Making `@tactic` arguments visible leads to unsolved constraints

14

This is `test/Succeed/TacticModality.agda`, but with explicit tactic arguments. ```agda open import Agda.Builtin.Reflection open import Agda.Builtin.Unit open import Agda.Builtin.Nat open import Agda.Builtin.Equality variable A : Set super-tac : Term → TC...

Restrict pattern matching in binding position to eta-equality records (#6845 reopened)

4

This reverts commit b38093ef713158fb01aac1880f035ee183602372, reopening this PR by @plt-amy : - #6845 Closes #6825.

Regression in 3.12: package system-filepath (with custom Setup) cannot be installed with GHC 8.0

8

With cabal-install-3.12.1.0, I can trigger this bug - by `cabal install -w ghc-8.0.2 system-filepath-0.4.14` (latest version of `system-filepath`) - by getting `system-filepath`and do a `cabal install --lib -w ghc-8.0.2` -...

Custom setup: Can't use Cabal-3.14 released with GHC 9.12

4

> [__1] rejecting: Agda:setup.Cabal; 3.14.0.0/installed-17a5, 3.14.0.0 (constraint from maximum version of Cabal used by Setup.hs requires

v1-install fails with internal libraries

1

Lifted from: - https://github.com/haskell/hackage-server/issues/1173 `cabal v1-install` chokes on the `hackage-cli` executable in the linking phase. @gbaz suspects it is because `hackage-cli` defines an internal library (`cabal-revisions`): ``` $ cabal get...