Successful exit code after error in --exec

[spcfox]

Steps to Reproduce

This code should not pass typechecking, but it does (see #3416). The result is an error in the generated code. But idris2 --exec returns code 0.

module AutoLazyOff

%auto_lazy off

data X = A

f : Lazy X -> X
f x@A = x

main : IO ()
main = ignore $ pure $ f A

Expected Behavior

The exit code must be non-zero.

Observed Behavior

$ idris2 --codegen chez --exec main AutoLazyOff.idr; echo $?
Exception: attempt to reference unbound identifier pat0C-58-0 at line 648, char 47 of /project/directory/build/exec/_tmpchez_app/_tmpchez.ss
0

$ idris2 --codegen racket --exec main AutoLazyOff.idr; echo $?
build/exec/_tmpracket_app/_tmpracket.rkt:633:46: pat0C-58-0: unbound identifier
  in: pat0C-58-0
  location...:
   build/exec/_tmpracket_app/_tmpracket.rkt:633:46
0

[spcfox]

A simpler example:

main : IO ()
main = printLn $ mod 10 0

$ idris2 --exec main Main.idr; echo $?
ERROR: Unhandled input for Prelude.Num.case block in mod at Prelude.Num:94:3--96:44
0

[spcfox]

Currently --exec can be specified more than once:

$ idris2 --exec hello Main.idr --exec goodbye Main.idr --exec hello Main.idr
Hello!
Goodbye!
Hello!

In this case, it's not clear what exit code should be returned. Maybe only one --exec should be allowed?

[buzden]

In this case, it's not clear what exit code should be returned. Maybe only one --exec should be allowed?

Alternatively, we can pass the last one, or the last non-zero one when there is a non-zero one.