search

agda / agda

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

Testsuite: heads up: with GHC 9.10, `throw` will print a callstack #7299

Closed andreasabel closed 2 months ago

andreasabel commented 4 months ago

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 ...
  toExceptionWithBacktrace, called at libraries/ghc-internal/src/GHC/Internal/Exception.hs:84:32 in ...
  throw, called at src/full/Agda/Utils/IO/UTF8.hs:70:16 in ....

I recall discussing with @nad the choice or error reporting here, we might want to return Nothing here instead and let Agda handle it further up, or catch this exception and print it without a stack trace.

andreasabel commented 2 months ago

Now biting:

andreasabel commented 2 months ago

The problem could be that the parser only catches IOErrors, but readFile throws a custom exception DecodingError :: ReadException. https://github.com/agda/agda/blob/20ad6b5d02f7a647e83cc493d8b4e11e22cac8c9/src/full/Agda/Syntax/Parser.hs#L86-L96 We could simply throw a userError rather than our hand-rolled DecodingError, since we never catch the latter.

andreasabel commented 2 months ago

We are also suffering from this regression in base-4.20 concerning exception printing:

andreasabel commented 2 months ago

We could simply throw a userError rather than our hand-rolled DecodingError, since we never catch the latter.

This is actually how it used to be in 8d75579c41308fc33671a96235a83f72add316c2 but it was changed in 71ad0f1de7aaaa4296364d7cef1d0e153e987bcf. Maybe better not going back... I noticed we can use the backtraceDesired feature to turn off the backtrace for the DecodingError exception. (It will still add some annoying trailing whitespace, see my report of GHC issue 25052.)