Add debug switch to verification process.

src/autodetection.ml

@@ -16,7 +16,7 @@ let rec lookup_file dirs filename =
     let file = Caml.Filename.concat dir filename in
     if Sys.file_exists file then file else lookup_file dirs filename
 
-let autodetect ~debug () =
+let autodetect ?(debug = false) () =
   let open Why3 in
   if debug then Debug.set_flag Autodetection.debug;
   let caisar_conf =

src/autodetection.mli

@@ -4,7 +4,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val autodetect : debug:bool -> unit -> Why3.Whyconf.config
+val autodetect : ?debug:bool -> unit -> Why3.Whyconf.config
 (** Perform the autodetection of provers.
 
     @param debug activates debug information. *)

src/main.ml

@@ -66,7 +66,10 @@ let config detect () =
         provers))
 
 let verify format loadpath memlimit prover files =
-  List.iter ~f:(Verification.verify format loadpath ?memlimit ~prover) files
+  let debug = match Logs.level () with Some Debug -> true | _ -> false in
+  List.iter
+    ~f:(Verification.verify ~debug format loadpath ?memlimit ~prover)
+    files
 
 let exec_cmd cmdname cmd =
   Logs.debug (fun m -> m "Command `%s'." cmdname);
@@ -141,11 +144,11 @@ let verify_cmd =
   let man = [ `S Manpage.s_description; `P doc ] in
   ( Term.(
       ret
-        (const (fun format loadpath memlimit prover files ->
+        (const (fun format loadpath memlimit prover files _ ->
            `Ok
              (exec_cmd cmdname (fun () ->
                 verify format loadpath memlimit prover files)))
-        $ format $ loadpath $ memlimit $ prover $ files)),
+        $ format $ loadpath $ memlimit $ prover $ files $ setup_logs)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
 
 let default_cmd =

src/verification.ml

@@ -7,9 +7,9 @@
 open Base
 module Filename = Caml.Filename
 
-let () = Language.register_nnet_support ()
-
-let () = Language.register_onnx_support ()
+let () =
+  Language.register_nnet_support ();
+  Language.register_onnx_support ()
 
 let create_env loadpath =
   let config = Autodetection.autodetect ~debug:true () in
@@ -73,9 +73,9 @@ let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
   Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
     Call_provers.print_prover_answer answer
 
-let verify format loadpath ?memlimit ~prover file =
+let verify ?(debug = false) format loadpath ?memlimit ~prover file =
   let open Why3 in
-  (* Debug.(set_flag (lookup_flag "call_prover")); *)
+  if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env loadpath in
   let steplimit = None in
   let timeout = None in

src/verification.mli

@@ -5,15 +5,17 @@
 (**************************************************************************)
 
 val verify :
+  ?debug:bool ->
   string option ->
   string list ->
   ?memlimit:int ->
   prover:string ->
   string ->
   unit
-(** [verify format loadpath memlimit prover file] launches a verification of the
-    given [file] with the provided [prover].
+(** [verify debug format loadpath memlimit prover file] launches a verification
+    of the given [file] with the provided [prover].
 
+    @param debug when set, enables debug information.
     @param format is the [file] format.
     @param loadpath is the additional loadpath.
     @param memlimit