Elektrine lite

← Feed

@julesh@mathstodon.xyz

Post #2103463

2026-05-06 17:01 UTC

Attempted to result to using Debug.trace for debugging in idris; discovered that unsafePerformIO is actually broken in idris; found the issue opened by @gallais 4 years ago https://github.com/idris-lang/Idris2/issues/2306

Replies (3)

  • @constantine@types.pl 2026-05-06 17:11

    @julesh@mathstodon.xyz @gallais@mamot.fr > unsafeDestroyWorld I know Idris is powerful etc but this is too far..

    Open ##2278871

  • @gallais@mamot.fr 2026-05-06 17:56

    @julesh@mathstodon.xyz you just need to execute your code rather than normalising it in the REPL

    Open ##2278872

  • @Andrev@types.pl 2026-05-06 18:15

    @julesh@mathstodon.xyz isn't that expected? This displays the IO value rather than the result of running the IO computation

    Open ##2278873