Andreas Abel

Results 455 issues of Andreas Abel

The `hackage-cli` command `push-candidate` is in the way of `push-cabal` when tab-completing `hackage-cli push` or even `hackage-cli push-ca`. Also, I never use it and I do not see what its...

`cabal upload` asks for the password if not stored in `.cabal/config`. I'd prefer this behaviour for `hackage-cli`, too. That is, if password is missing in `.netrc` then `haskage-cli` should ask...

Currently (2022-01-27) the `--verbose` option has no effect. What should `--verbose` do? (Please extend list.) - [ ] `pull-cabal`: print filename that has just been downloaded. Helpful if hundreds of...

(This is my first attempt to use `sbv`.) I am hitting an _impossible_ in `sbv-10.10` in the internal `sh` function: ``` $ git clone [email protected]:andreasabel/sbv-quarter-circle-puzzle.git $ cd sbv-* $ git...

https://github.com/agda/agda/blob/8c413d4d5cc2db6c7ca309667b4c9fb1c6666bf4/src/full/Agda/Utils/IO/UTF8.hs#L70 This will produce for issue #4506: ``` Failed to read .../test/Fail/Issue4506.agda. Please ensure that this file uses the UTF-8 character encoding. HasCallStack backtrace: collectBacktraces, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:92:13 in ......

ux: error reporting
infra: test suite
unicode
ghc-9.10

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...

performance
forcing
refactor

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...

type: discussion
ghc support

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...

type: bug
false
maculata
type-based-termination

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...

exact split
ux: warnings
catch-all