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

Only warn about unknown warnings, don't fail hard #7219

Closed andreasabel closed 2 months ago

andreasabel commented 2 months ago

https://github.com/andreasabel/agda-automata/actions/runs/8647859406/job/23710306511#step:7:8

Unknown warning flag: DuplicateInterfaceFiles. See --help=warning.

Agda 2.6.4 does not now about this future warning (will enter in 2.7). I think we should only fail softly here. Warn about the unknown warning. This is better for forward compatibility and multi-Agda development.

Since we have --warning=error to turn all warnings into errors, folks who absolutely want to fail when an unknown warning is touched can always do so.