Andreas Abel
Andreas Abel
Rather than first extracting pattern variables from target, directly calculate whether they make a constructor argument forced. This refactoring uses a custom Monoid and is similar to the structure of...
In the dev meeting today (2023-09-13) we touched upon the subject of dropping further GHCs after releasing 2.6.4. As developers, what can we gain from raising the lower bound from...
TBT accepts a non-productive definition, which we can exploit to make the Agda loop: ```agda {-# OPTIONS --type-based-termination #-} {-# OPTIONS --size-preservation #-} -- default -- {-# OPTIONS -v term.tbt:50...
This passes without warning: ```agda open import Agda.Builtin.Nat open import Agda.Builtin.Bool isZero : Nat → Bool isZero 0 = true {-# CATCHALL #-} -- This pragma is useless! isZero (suc...
Investigating #6685 I noticed that PR #5319 introduced a semantics change introduced which we did not document explicitly: ```agda private module A where module B where module B' = B...
This is the current specification of `-i`: https://github.com/agda/agda/blob/3c239ef6eddf3f0502c5fe42f81f2b038b76717f/doc/user-manual/tools/command-line-options.rst?plain=1#L184-L186 Rather sad, I'd expect to be informed about the following there: - [x] `-i` is monoidal, i.e., can be supplied many times,...
Since recently, I noticed that `git pull` usually pulls in around 8MB. (Of course, not consecutive pulls, but whenever I return to Agda development the next day or a couple...
Observed the following behavior: - edited `src/data/MAlonzo/src/MAlonzo/RTE.hs` - ran `make install-bin` - ran `make compiler-test` It used the old, existing `MALonzo/RTE.hs` (dating 2021), giving `-Werror=star-is-type` errors with GHC 9.6.1. I...
E.g.: https://github.com/agda/agda/actions/runs/4506148531/jobs/7932946851#step:10:42 ``` +ret > ExitFailure 42 +out > { compiling Issue2908.foo +out > Issue2908.foo = λ a → let b = a + a in seq b 0 +out...