diff --git a/src/coqOfOCaml.ml b/src/coqOfOCaml.ml index 74bab2eb2..e7db45568 100644 --- a/src/coqOfOCaml.ml +++ b/src/coqOfOCaml.ml @@ -101,13 +101,13 @@ let of_ocaml success_message; } -let exit (context : MonadEval.Context.t) (output : Output.t) : unit = +let get_exit_code (context : MonadEval.Context.t) (output : Output.t) : int = let is_blacklist = Configuration.is_filename_in_error_blacklist context.configuration in if output.has_errors && not is_blacklist then - exit 1 + 1 else - exit 0 + 0 (** The main function. *) let main () = @@ -163,6 +163,7 @@ let main () = let pipeline = Mpipeline.make merlin_config file_source in Mpipeline.with_pipeline pipeline (fun _ -> + try let comments = Mpipeline.reader_comments pipeline in let typing = Mpipeline.typer_result pipeline in let typedtree = Mtyper.get_typedtree typing in @@ -183,6 +184,11 @@ let main () = !output_file_name !json_mode in Output.write !json_mode output; - exit context output) + let exit_code = get_exit_code context output in + exit exit_code + with Failure message -> + prerr_endline message; + exit 1 + ) ;;main () diff --git a/src/error.ml b/src/error.ml index 746277e1d..7c4322d85 100644 --- a/src/error.ml +++ b/src/error.ml @@ -1,4 +1,5 @@ -(** Error messages. *) +(** Error messages. We handle the errors with a monad, and allopw multiple + errors per file. *) open SmartPrint module Category = struct diff --git a/tests/constants.ml b/tests/constants.ml new file mode 100644 index 000000000..c54b379df --- /dev/null +++ b/tests/constants.ml @@ -0,0 +1,13 @@ +let c_int : int = 0 + +let c_char : char = 'c' + +let c_string : string = "c" + +let c_float : float = 1.0 + +let c_int32 : int32 = 0l + +let c_int64 : int64 = 0L + +let c_nativeint : nativeint = 0n diff --git a/tests/constants.v b/tests/constants.v new file mode 100644 index 000000000..6008341e4 --- /dev/null +++ b/tests/constants.v @@ -0,0 +1,24 @@ +Require Import CoqOfOCaml.CoqOfOCaml. +Require Import CoqOfOCaml.Settings. + +Definition c_int : int := 0. + +Definition c_char : ascii := "c" % char. + +Definition c_string : string := "c". + +Definition c_float : float := + (* ❌ Float constant 1.0 is approximated by the integer 1 *) + 1. + +Definition c_int32 : int32 := + (* ❌ Constant of type int32 is converted to int *) + 0. + +Definition c_int64 : int64 := + (* ❌ Constant of type int64 is converted to int *) + 0. + +Definition c_nativeint : nativeint := + (* ❌ Constant of type nativeint is converted to int *) + 0.