Working idris2 error detection

Idris 2 doesn't have a failing exit code in this context when it fails
to compile an expr given at the command line, we need to check for an
error message in the output
This commit is contained in:
Nathan McCarty 2025-01-02 00:00:13 -05:00
parent a0ba82ab38
commit b28b91d5d2
2 changed files with 11 additions and 5 deletions

View file

@ -1,9 +1,11 @@
module TestModule.Booleans
import System
-- @@test Boolean Integration passes
passes : IO Bool
passes = pure True
doesWork : IO Bool
doesWork = pure True
-- @@test Boolean Integration fails
fails : IO Bool
fails = pure False
dontWork : IO Bool
dontWork = pure False

View file

@ -51,6 +51,8 @@ class IdrisError is Exception {
qq:to/END/;
Error running idris command: $.command
Command exited with $.exit-code
StdOut:
{$.out.lines.map(*.indent: 2).join("\n")}
END
}
}
@ -75,7 +77,7 @@ sub idris-run(*@cmd) is export {
my $proc = run "idris2", @cmd, :out, :err;
my $out = $proc.out.slurp(:close);
my $err = $proc.err.slurp(:close);
unless $proc {
if !$proc || $out.contains("Error:") {
IdrisError.new(
out => $out, err => $err,
exit-code => $proc.exitcode, command => @cmd.Str)
@ -117,5 +119,7 @@ sub idris-exec($expr, $file, $output-type? = Unit) is export {
exit-code => $proc.exitcode, expr => $expr
).throw;
}
# Remove the output file
'build/exec/iutils_out'.IO.unlink;
return $out;
}