lean-llvm
lean-llvm copied to clipboard
`parseBitcodeFile` error reporting is broken
Calling llvm.ffi.parseBitcodeFile with an invalid file (e.g., an LLVM source assembly file instead of a bitcode file) causes an internal lean assertion to fail, e.g.:
../../bin/../src/runtime/lean.h:634: lean_ctor_num_objs: Assertion `lean_is_ctor(o)' failed.
Presumably there's just something off in how we're using set_io_error
here.
Also, we may want a slightly more explicit return type---e.g. IO (Except String Module)
or similar instead of just IO Module
---to match the underlying LLVM parsing interface (it returns an Except
essentially as well) and leave raising an IO error for unexpected behaviors. This last note about return types also applies to the llvm.ffi.parseAssembly function recently added (at the moment in a branch), which currently just gets the underlying LLVM error message string and calls set_io_error
(here).