search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.53k stars 380 forks source link

[ fix ] Report chez failures #3363

Closed dunhamsteve closed 3 months ago

dunhamsteve commented 3 months ago

Description

If chez exits with a status code other than 0 during compilation, Idris ignores the error and completes successfully, leaving a non-working executable. For example, this occurs when an out of memory error occurs during compilation. I've changed Chez.idr to check the return code and throw an InternalError reporting the code if it is not zero.

Before this change, CHEZ=false idris2 -c Hello.idr -o hello would complete successfully, but ./build/exec/hello would report:

./build/exec/hello: line 15: /Users/dunham/code/i2/Idris2/build/exec/hello_app/hello.so: No such file or directory

after the change, the compilation step fails with:

Error: INTERNAL ERROR: Chez exited with return code 1
gallais commented 3 months ago

Can we have the same for the other backends too?

dunhamsteve commented 3 months ago

It looks like the other backends check the return value for compilation. None of them check the return value when running the result of compilation for REPL :exec.

The windows CI failure is for chez/forkjoin001, which produced no output. I believe it's unrelated to this change. It did not fail for me when github ran CI for this commit in my repository. Possibly something timing sensitive?