Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom

Successful exit code after error in --exec #3427

Open
spcfox opened this issue Nov 28, 2024 · 3 comments · May be fixed by #3434
Open

Successful exit code after error in --exec #3427

spcfox opened this issue Nov 28, 2024 · 3 comments · May be fixed by #3434
Labels
backend: chez good first issue Good for newcomers

Comments

@spcfox
Copy link
Contributor

spcfox commented Nov 28, 2024 •
edited
Loading

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
Copy link
Contributor Author

spcfox commented Nov 29, 2024 •
edited
Loading

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
Copy link
Contributor Author

spcfox commented Nov 29, 2024 •
edited
Loading

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
Copy link
Collaborator

buzden commented Nov 29, 2024

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.

This was referenced Dec 2, 2024
Merged
Open
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
backend: chez good first issue Good for newcomers
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[ refactor ] Improve error handling in Core spcfox/Idris2
3 participants
@buzden @andrevidela @spcfox