diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Main.ml | 26 |
1 files changed, 17 insertions, 9 deletions
diff --git a/compiler/Main.ml b/compiler/Main.ml index e703f1a0..64d8ae2b 100644 --- a/compiler/Main.ml +++ b/compiler/Main.ml @@ -113,7 +113,9 @@ let () = Arg.Clear lean_gen_lakefile, " Generate a default lakefile.lean (Lean only)" ); ("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC"); - ("-k", Arg.Clear fail_hard, " Do not fail hard in case of error"); + ( "-abort-on-error", + Arg.Set fail_hard, + "Abort on the first encountered error" ); ( "-tuple-nested-proj", Arg.Set use_nested_tuple_projectors, " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \ @@ -265,16 +267,22 @@ let () = definitions"; fail ()); - (* Apply the pre-passes *) - let m = Aeneas.PrePasses.apply_passes m in + (* There may be exceptions to catch *) + (try + (* Apply the pre-passes *) + let m = Aeneas.PrePasses.apply_passes m in - (* Some options for the execution *) + (* Test the unit functions with the concrete interpreter *) + if !test_unit_functions then Test.test_unit_functions m; - (* Test the unit functions with the concrete interpreter *) - if !test_unit_functions then Test.test_unit_functions m; - - (* Translate the functions *) - Aeneas.Translate.translate_crate filename dest_dir m; + (* Translate the functions *) + Aeneas.Translate.translate_crate filename dest_dir m + with Errors.CFailure (meta, msg) -> + (* In theory it shouldn't happen, but there may be uncaught errors - + note that we let the [Failure] exceptions go through (they are + send if we use the option [-abort-on-error] *) + log#serror (Errors.format_error_message meta msg); + exit 1); (* Print total elapsed time *) log#linfo |