search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

Don't silently ignore `-v` #7190

Closed lawcho closed 1 month ago

lawcho commented 3 months ago

Agda silently ignores the -v option, unless built with the debug cabal flag.

This led me on a merry chase when debugging the test failures in #7165.

Some ways to improve the UX:

Related to #5429 (but -v is not backend-specific)

lawcho commented 3 months ago

Oops, duplicate of #7114

lawcho commented 1 month ago

Wontfix because https://github.com/agda/agda/pull/7256#issuecomment-2110262496