Some rework and plug config command in with autodection.

src/detection.ml → src/autodetection.ml

@@ -16,9 +16,9 @@ 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 detect () =
+let autodetect ~debug () =
   let open Why3 in
-  Debug.set_flag Why3.Autodetection.debug;
+  if debug then Debug.set_flag Autodetection.debug;
   let caisar_conf = lookup_file Dirs.Sites.config "caisar.conf" in
   let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
   let config = Whyconf.init_config (Some null) in

src/language.ml

@@ -6,18 +6,20 @@
 
 open Base
 
-(* Register neural network formats. *)
+(* -- Register neural network format. *)
 
 let nnet_parser env _ filename _ =
   let open Why3 in
-  let nnet = Pmodule.read_module env [ "caisar" ] "NNet" in
-  let nnet_input_type =
-    Ty.ty_app Theory.(ns_find_ts nnet.mod_theory.th_export [ "input_type" ]) []
-  in
   let header = Nnet.parse filename in
   match header with
   | Error s -> Loc.errorm "%s" s
   | Ok header ->
+    let nnet = Pmodule.read_module env [ "caisar" ] "NNet" in
+    let nnet_input_type =
+      Ty.ty_app
+        Theory.(ns_find_ts nnet.mod_theory.th_export [ "input_type" ])
+        []
+    in
     let id_as_tuple = Ident.id_fresh "AsTuple" in
     let th_uc = Pmodule.create_module env id_as_tuple in
     let th_uc = Pmodule.use_export th_uc nnet in

src/main.ml

@@ -10,7 +10,7 @@ module Format = Caml.Format
 
 let caisar = "caisar"
 
-(* Logs. *)
+(* -- Logs. *)
 
 let pp_header =
   let x =
@@ -40,13 +40,30 @@ let setup_logs =
   in
   Term.(const setup_log $ Logs_cli.level ())
 
-(* Commands. *)
+(* -- Commands. *)
 
-let config cmd detect () =
-  Logs.debug (fun m -> m "Command `%s'." cmd);
-  if detect then Logs.app (fun m -> m "Automatic detection.")
+let config detect () =
+  if detect
+  then begin
+    Logs.debug (fun m -> m "Automatic detection.");
+    let config = Autodetection.autodetect ~debug:false () in
+    let open Why3 in
+    let provers = Whyconf.get_provers config in
+    Logs.app (fun m ->
+      m "@[<v>%a@]"
+        (Pp.print_iter2 Whyconf.Mprover.iter Pp.newline Pp.nothing
+           Whyconf.print_prover Pp.nothing)
+        provers)
+  end
 
-(* Command line. *)
+let verify format loadpath files =
+  List.iter ~f:(Verification.verify format loadpath) files
+
+let exec_cmd cmdname cmd =
+  Logs.debug (fun m -> m "Command `%s'." cmdname);
+  cmd ()
+
+(* -- Command line. *)
 
 let config_cmd =
   let cmdname = "config" in
@@ -83,7 +100,7 @@ let config_cmd =
            else
              (* TODO: Do not only check for [detect], and enable it by
                 default, as soon as other options are available. *)
-             `Ok (config cmdname true ()))
+             `Ok (exec_cmd cmdname (fun () -> config true ())))
         $ const cmdname $ detect $ setup_logs)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man )
 
@@ -111,7 +128,7 @@ let verify_cmd =
   ( Term.(
       ret
         (const (fun format loadpath files ->
-           `Ok (List.iter ~f:(Verify.do_verify format loadpath) files))
+           `Ok (exec_cmd cmdname (fun () -> verify format loadpath files)))
         $ format $ loadpath $ files)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
 

src/verify.ml → src/verification.ml

@@ -10,7 +10,7 @@ module Format = Caml.Format
 let () = Language.register ()
 
 let create_env loadpath =
-  let config = Detection.detect () in
+  let config = Autodetection.autodetect ~debug:true () in
   let stdlib = Dirs.Sites.stdlib in
 
   let open Why3 in
@@ -20,7 +20,7 @@ let create_env loadpath =
 
 let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
 
-let do_verify format loadpath file =
+let verify format loadpath file =
   let open Why3 in
   let env, config = create_env loadpath in
   let _, mstr_theory =

tests/autodetect.t

+Test verify
+  $ caisar config -d
+  [caisar] Alt-Ergo 2.4.0

tests/simple.t

-Test help
+Test verify
   $ caisar verify -L . --format whyml - <<EOF
   > theory T
   >   use TestNetwork.AsTuple