Dummy initial printer.

config/drivers/pyrat.drv

 (* Why3 drivers for PyRAT *)
 
+prelude "(* this is the prelude for PyRAT *)"
+
 (* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
 valid "^Inconsistent assumption$"
 

nnet.opam

@@ -9,7 +9,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst" "--root" "."] {dev}
+  ["dune" "subst"] {dev}
   [
     "dune"
     "build"
@@ -17,8 +17,7 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files"
-    "false"
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}

src/dune

@@ -6,6 +6,8 @@
   (package caisar)
 )
 
+(copy_files printer/*)
+
 (generate_sites_module
   (module dirs)
   (sites caisar))

src/printer/pyrat.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+let print_task args ?old:_ fmt _task =
+  let open Why3 in
+  Printer.print_prelude fmt args.Printer.prelude
+
+let () =
+  Why3.Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
+    print_task

src/verification.ml

@@ -6,6 +6,7 @@
 
 open Base
 module Format = Caml.Format
+module Filename = Caml.Filename
 
 let () = Language.register ()
 
@@ -24,23 +25,23 @@ let verify format loadpath prover file =
     match file with
     | "-" ->
       ("stdin", Env.(read_channel ?format base_language env "stdin" Caml.stdin))
-    | filename ->
-      let mlw_files, _ = Env.(read_file ?format base_language env filename) in
-      (filename, mlw_files)
+    | file ->
+      let mlw_files, _ = Env.(read_file ?format base_language env file) in
+      (file, mlw_files)
   in
   Wstdlib.Mstr.iter
     (fun _ theory ->
       let tasks = Task.split_theory theory None None in
       let prover =
-        Whyconf.filter_one_prover config (Why3.Whyconf.mk_filter_prover prover)
+        Whyconf.(filter_one_prover config (mk_filter_prover prover))
       in
       let driver =
         match String.chop_prefix ~prefix:"caisar_drivers/" prover.driver with
         | None -> Whyconf.(load_driver (get_main config) env prover)
         | Some file ->
           let file =
-            Caml.Filename.concat
-              (Caml.Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
+            Filename.concat
+              (Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
               file
           in
           Driver.load_driver_absolute env file prover.extra_drivers

tests/simple.t

@@ -46,6 +46,7 @@ Test verify
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.0, OK.
   <autodetect>3 prover(s) added
+  (* this is the prelude for PyRAT *)
   (* this is a prelude for Alt-Ergo integer arithmetic *)
   (* this is a prelude for Alt-Ergo real arithmetic *)
   type string