sqlite3 db for the manager

Makefile.in

@@ -64,8 +64,8 @@ endif
 
 
 INCLUDES = -I src/core -I src/util -I src/driver -I src/parser -I src/printer \
-           -I src/transform -I src/programs -I src 
-BFLAGS   = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cma unix.cma $(DYNLINKBFLAGS)
+           -I src/transform -I src/programs -I src/manager -I src 
+BFLAGS   = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads -I +sqlite3 @OCAMLGRAPHLIB@ str.cma unix.cma $(DYNLINKBFLAGS)
 # no -warn-error because some do not compile all files (e.g. those linked to APRON)
 OFLAGS   = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@ str.cmxa unix.cmxa $(DYNLINKOFLAGS)
 
@@ -116,6 +116,21 @@ include Version
 doc/version.tex src/version.ml: Version version.sh config.status
 	BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) COQVER=$(COQVER) ./version.sh
 
+src/orm/sql_orm_header.ml: src/orm/sql_access.ml src/orm/convert.ml 
+	ocaml src/orm/convert.ml $< $@
+
+
+ORM_CMO := printer_utils.cmo sql_orm_header.cmo sql_orm.cmo
+ORM_CMO := $(addprefix src/orm/,$(ORM_CMO))
+
+src/manager/db.ml: $(ORM_CMO) src/manager/orm_schema.ml
+	ocaml -I src/orm src/manager/orm_schema.ml 
+
+src/orm/%.cmo: src/orm/%.ml
+	ocamlc -c -I src/orm -I +sqlite3 $<
+
+src/manager/orm_schema.ml: $(ORM_CMO)
+
 # why
 #####
 
@@ -163,6 +178,13 @@ bin/why.static: $(CMX) src/why.cmx
 bin/top: $(CMO)
 	ocamlmktop $(BFLAGS) -o $@ nums.cma $^
 
+MANAGER_CMO := db.cmo 
+MANAGER_CMO := $(addprefix src/manager/,$(MANAGER_CMO))
+
+bin/manager.byte: $(MANAGER_CMO)
+	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) \
+		sqlite3.cma -o $@ $^
+
 # test targets
 ##############
 
@@ -413,7 +435,7 @@ doc/main.html: doc/main.tex doc/version.tex
 APIDOCSRC = $(UTIL_CMO:.cmo=.mli) $(CORE_CMO:.cmo=.mli) \
 	src/driver/call_provers.mli \
 	src/driver/driver.mli \
-	manager/db.mli
+	src/manager/state.mli
 
 .PHONY: apidoc
 

src/manager/orm_schema.ml

+#load "printer_utils.cmo"
+#load "sql_orm_header.cmo"
+#load "sql_orm.cmo"
+
+open Sql_orm
+
+open Schema
+
+let boolean = integer
+
+let all_tables = make 
+  [
+    (* table of challenges *)
+    ("challenge",
+     [ integer "log"; (* ref to log it belongs to *)
+       text "input"; (* input of the problem *)
+       text ~flags:[`Optional] "answer";
+       (* no answer means "timeout" *)
+       real "time"; (* time to answer *)
+       boolean "correct"; 
+     ],
+     [], default_opts);
+
+    (* log entries *)
+    ("log_entry",
+     [ integer "attempt"; (* ref to attempt it belongs to *)
+       boolean "successful";
+       date "starting_date";
+       date "end_date";
+       foreign_many "challenge" "challenges";
+     ],
+     [], default_opts);
+
+    (* table of attempts *)
+    ("attempts",
+     [ integer "solution"; (* ref to solution it belongs to *)
+       foreign_many "log_entry" "log_entries";
+     ],
+     [], default_opts);
+       
+    (* table of submitted solutions, successful or not *)
+    ("solution",
+     [ text "user";
+       integer "problem_id";
+       boolean "solved";
+       foreign_many "attempts" "attempts"; (* list of attempts *)
+     ],
+     [], default_opts);
+
+    (* table of problems *)
+    ("problems",
+     [ integer ~flags:[`Unique; `Index] "number";
+       text "short_descr";
+       text "description";
+       integer "solved_by" ;
+     ],
+     [],
+     default_opts);
+    
+    
+    (* table of user profiles *)
+    ("user" ,
+     [ text ~flags:[`Unique ; `Index] "username";
+       text "password";       
+       text "email";
+       boolean "allow_contact"; (* if allows to make email public *)
+       text ~flags:[`Optional; `Index] "nationality";
+       text ~flags:[`Optional; `Index] "preferred_language";
+       integer "score";
+       foreign_many "solution" "solutions"; (* list of submitted solutions *)
+     ],
+     [], default_opts) ;
+    
+
+
+  ]       
+
+let () = generate ~debug:false all_tables "src/manager/db"
+

src/manager/state.mli

+
+
+(** {1 Proof manager database} *)
+
+
+(** {2 proof attempts and transformations} *)
+
+(** status of an external proof attempt *)
+type proof_attempt_status =
+  | Running (** external proof attempt is in progress *)
+  | Success (** external proof attempt succeeded *)
+  | Timeout (** external proof attempt was interrupted *)
+  | Unknown (** external prover answered ``don't know'' or equivalent *)
+  | HighFailure (** external prover call failed *)
+
+(** a proof attempt by some external provers *)
+type external_proof =
+  { prover : Driver.driver; (** prover driver *)
+    timelimit : int; (** CPU limit given in seconds *)
+    status : proof_attempt_status; (** the current state *)
+    result_time : float ; (** CPU time for that run *)
+    trace : string; 
+      (** any kind of trace returned by the prover.
+          when redoing the same attempt, the former trace is sent again *)
+    obsolete : bool;
+      (** when true, goal as changed after that proof attempt *)
+  } 
+
+type transf = Task.task Register.tlist_reg
+
+(** an proof attempt is either an external proof or a transformation 
+    into subtasks *)
+type attempt =
+  | External of external_proof
+  | Transf of transf
+
+(** {2 proof goals in a proof project} *)
+
+
+type loc
+
+type explain
+
+type identifier
+
+type goal_origin =
+  | Goal of Decl.prsymbol
+  | VCfun of loc * explain * identifier
+  | Subgoal of goal
+
+and goal =
+    {
+      task : Task.task;
+      task_checksum: string;
+      origin : goal_origin;
+      mutable attempts : attempt list;
+      mutable proved : bool;
+      (** invariant: g.proved == true iff
+             exists attempts a in g.attempts, a.obsolete == false and
+             (a = External e and e.result == Valid or
+              a = Transf(gl) and forall g in gl, g.proved)
+      *)
+      mutable observers: (bool -> unit) list;
+      (** observers that wants to be notified by any changes of the proved status *)
+    }
+
+
+(** {2 database for a proof project} *)
+
+type loc_record_in_db =
+  { file : string;
+    line : int;
+    cbegin : int;
+    cend : int;
+  }
+
+type goal_record_in_db =
+  { 
+    task_checksum : string; 
+    parent : transf_in_db option;
+    name : string; (* qualified proposition name *)
+    origin : loc_record_in_db option;
+    external_proofs : external_proof_in_db list;
+    transformations : transf_in_db list;
+    proved : bool;
+  }
+
+and external_proof_in_db =
+  {
+    prover : string; (** prover identifier *)
+    timelimit : int; (** CPU limit given in seconds *)
+    memlimit : int; (** VM limit given in megabytes *)
+    status : int; (** enum{proof_attempt_status}; the current state *)
+    result_time : float ; (** CPU time for that run in seconds *)
+    trace : string option; 
+      (** any kind of trace returned by an automatic prover,
+          or any kind of proof script for an interactive prover *)
+    obsolete : bool;
+  }
+
+and transf_in_db =
+  {
+    name : string; (** transformation name *)
+    obsolete : bool;
+  }
+
+val read_db_from_file : unit -> goal list
+(** returns the set of root goals *)
+
+(** {2 attempts to solve goals} *)
+
+exception AlreadyAttempted
+
+val try_prover : 
+  timelimit:int -> ?memlimit:int -> goal -> Driver.driver -> unit 
+  (** attempts to prove goal with the given prover. This function adds
+      a new corresponding attempt for that goal, sets its current
+      status to Running, launches the prover in a separate process and
+      returns immediately.
+
+      Upon termination of the external process, the prover's answer is
+      retrieved and database is updated. The [proved] field of the
+      database is updated, and also these of any goal affected, according
+      to invariant above. Goal observers are notified of any change
+      of goal statuses.
+
+      @param timelimit CPU time limit given for that attempt, must be positive
+
+      @raise AlreadyAttempted if there already exists a non-obsolete
+      external proof attempt with the same driver and time limit, or
+      with a different time limit and a result different from Timeout
+
+
+  *)
+
+val add_transformation: goal -> transf -> unit
+  (** adds a transformation on the goal. This function adds a new
+      corresponding attempt for that goal, computes the subgoals and
+      and them in the database. In the case where no subgoal is
+      genereated, the [proved] field is updated, and those of parent
+      goals.
+
+      if this transformation has already been attempted but is markes
+      as obsolete, it is retried, and the new lists of goals is
+      carefully matched with the older subgoals, so that if some
+      subgoals are identical to older ones, then the proof is kept.
+      Notice that no old proof attempts should be lost in this
+      process, e.g if the old trans formation produced 3 subgoals
+      A,B,C, C was proved interactively, and the new transformations
+      produces only 2 goals, the interactive proof of C is keep in an
+      extra dummy goal "true"
+      
+      @raise AlreadyAttempted if this transformation has already been attempted
+      and is not obsolete
+
+  *)
+
+
+
+(** TODO: removal of attempts *)
+
+(* {2 goal updates} *)
+
+val add_or_replace_goal: goal -> unit 
+  (** updates the database with the new goal.  If a goal with the same
+      origin already exists, it is checked whether the task to
+      prove is different or not. If it is the same, proof attempts are
+      preserved. If not the same, former proof attempts are marked as
+      obsolete.
+
+
+      IMPORTANT: this kills every running prover tasks
+
+  *)
+
+(** TODO: full update, removing goals that are not pertinent anymore *)
+
+
+  
+
+
+

src/orm/convert.ml

+open Printf
+
+let _ =
+   let fin = open_in Sys.argv.(1) in
+   let fout = open_out Sys.argv.(2) in
+   fprintf fout "(* autogenerated from convert.ml and sql_access.ml *)\n";
+   fprintf fout "open Printer_utils\n";
+   fprintf fout "let print_header e =\n";
+   (try while true do
+      let l = input_line fin in
+      fprintf fout "  e.p \"%s\";\n" (String.escaped l);
+    done with End_of_file -> ());
+   fprintf fout "  ()";
+   close_out fout;
+   close_in fin

src/orm/printer_utils.ml

+(*
+ * Copyright (c) 2009 Anil Madhavapeddy <anil@recoil.org>
+ *
+ * Permission to use, copy, modify, and distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *)
+
+open Printf
+
+    type env = {
+        fn: int -> string -> unit;
+        p: string -> unit;         (* printer function *)
+        i: int;                    (* indent level *)
+        nl: unit -> unit;          (* new line *)
+        dbg: bool;
+    }
+
+    let indent e = { e with i = succ e.i; p = e.fn (succ e.i) }
+
+    let indent_fn e fn =
+        let e = indent e in
+        fn e
+
+
+    let list_iter_indent e fn l =
+        List.iter (indent_fn e fn) l
+
+    let hashtbl_iter_indent e fn h =
+        Hashtbl.iter (indent_fn e fn) h
+
+    let may fn = function
+        |None -> ()
+        |Some x -> fn x
+
+    let must fn = function
+        |None -> failwith "must"
+        |Some x -> fn x
+
+    let init_printer ?(msg=None) ?(debug=false) fout =
+        let ind i s = String.make (i * 2) ' ' ^ s in
+        let out i s = output_string fout ((ind i s) ^ "\n") in
+        may (out 0) msg;
+        {
+            fn = out;
+            i = 0;
+            p = (out 0);
+            nl = (fun (x:unit) -> out 0 "");
+            dbg = debug;
+        }
+        
+    let print_module e n fn =
+        e.p (sprintf "module %s = struct" (String.capitalize n));
+        indent_fn e fn;
+        e.p "end";
+        e.nl ()
+
+    let print_module_sig e n fn =
+        e.p (sprintf "module %s : sig" (String.capitalize n));
+        indent_fn e fn;
+        e.p "end"
+    
+    let print_record e nm fn =
+        e.p (sprintf "type %s = {" nm);
+        indent_fn e fn;
+        e.p "}";
+        e.nl ()
+
+    let print_object e nm fn =
+        e.p (sprintf "type %s = <" nm);
+        indent_fn e fn;
+        e.p ">";
+        e.nl ()
+
+    let print_comment e fmt =
+        let xfn s = e.p ("(* " ^ s ^ " *)") in
+        kprintf xfn fmt
+
+    let print_ocamldoc e ?(raises="") ?(args="") body =
+        e.p (sprintf "(** %s%s" (match args with "" -> "" |x -> sprintf "[%s] " x)  body);
+        (match raises with "" -> () |r -> e.p (" @raise " ^ r));
+        e.p "  *)"
+    
+    let pfn e fmt =
+        let xfn s = e.p s in
+        kprintf xfn fmt
+
+    let dbg e fmt =
+        let xfn s = if e.dbg then pfn e "print_endline (%s);" s in
+        kprintf xfn fmt
+
+    let (--*) = print_comment
+    let (-->) e fn = indent_fn e fn
+    let (+=) = pfn 
+    let (-=) = dbg
+    let ($) f x = f x
+ 
+

src/orm/sql_access.ml

+(*
+ * Copyright (c) 2009 Anil Madhavapeddy <anil@recoil.org>
+ *
+ * Permission to use, copy, modify, and distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *)
+
+open Sqlite3
+open Printf
+
+type transaction_mode = [
+    |`Deferred
+    |`Immediate
+    |`Exclusive
+]
+
+type state = {
+    db : db;
+    mutable in_transaction: int;
+    busyfn: db -> unit;
+    mode: transaction_mode;
+}
+
+let default_busyfn (db:Sqlite3.db) =
+    print_endline "WARNING: busy";
+    Thread.delay (Random.float 1.)
+
+let raise_sql_error x =
+    raise (Sqlite3.Error (Rc.to_string x))
+
+let try_finally fn finalfn =
+    try
+      let r = fn () in
+      finalfn ();
+      r
+    with e -> begin
+      print_endline (sprintf "WARNING: exception: %s" (Printexc.to_string e));
+      finalfn ();
+      raise e
+    end
+
+(* retry until a non-BUSY error code is returned *)
+let rec db_busy_retry db fn =
+    match fn () with
+    |Rc.BUSY -> 
+       db.busyfn db.db;
+       db_busy_retry db fn;
+    |x -> x
+
+(* make sure an OK is returned from the database *)
+let db_must_ok db fn =
+    match db_busy_retry db fn with
+    |Rc.OK -> ()
+    |x -> raise_sql_error x
+
+(* make sure a DONE is returned from the database *)
+let db_must_done db fn = 
+   match db_busy_retry db fn with
+   |Rc.DONE -> ()
+   |x -> raise_sql_error x
+
+(* request a transaction *)
+let transaction db fn =
+    let m = match db.mode with
+    |`Deferred -> "DEFERRED" |`Immediate -> "IMMEDIATE" |`Exclusive -> "EXCLUSIVE" in
+    try_finally (fun () ->
+        if db.in_transaction = 0 then (
+           db_must_ok db (fun () -> exec db.db (sprintf "BEGIN %s TRANSACTION" m));
+        );
+        db.in_transaction <- db.in_transaction + 1;
+        fn ();
+    ) (fun () ->
+        if db.in_transaction = 1 then (
+           db_must_ok db (fun () -> exec db.db "END TRANSACTION");
+        );
+        db.in_transaction <- db.in_transaction - 1
+    )
+
+(* iterate over a result set *)
+let step_fold db stmt iterfn =
+    let stepfn () = Sqlite3.step stmt in
+    let rec fn a = match db_busy_retry db stepfn with
+    |Sqlite3.Rc.ROW -> fn (iterfn stmt :: a)
+    |Sqlite3.Rc.DONE -> a
+    |x -> raise_sql_error x
+    in
+    fn []

src/orm/sql_orm_header.ml

+(* autogenerated from convert.ml and sql_access.ml *)
+open Printer_utils
+let print_header e =
+  e.p "(*";
+  e.p " * Copyright (c) 2009 Anil Madhavapeddy <anil@recoil.org>";
+  e.p " *";
+  e.p " * Permission to use, copy, modify, and distribute this software for any";
+  e.p " * purpose with or without fee is hereby granted, provided that the above";
+  e.p " * copyright notice and this permission notice appear in all copies.";
+  e.p " *";
+  e.p " * THE SOFTWARE IS PROVIDED \"AS IS\" AND THE AUTHOR DISCLAIMS ALL WARRANTIES";
+  e.p " * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF";
+  e.p " * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR";
+  e.p " * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES";
+  e.p " * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN";
+  e.p " * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF";
+  e.p " * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.";
+  e.p " *)";
+  e.p "";
+  e.p "open Sqlite3";
+  e.p "open Printf";
+  e.p "";
+  e.p "type transaction_mode = [";
+  e.p "    |`Deferred";
+  e.p "    |`Immediate";
+  e.p "    |`Exclusive";
+  e.p "]";
+  e.p "";
+  e.p "type state = {";
+  e.p "    db : db;";
+  e.p "    mutable in_transaction: int;";
+  e.p "    busyfn: db -> unit;";
+  e.p "    mode: transaction_mode;";
+  e.p "}";
+  e.p "";
+  e.p "let default_busyfn (db:Sqlite3.db) =";
+  e.p "    print_endline \"WARNING: busy\";";
+  e.p "    Thread.delay (Random.float 1.)";
+  e.p "";
+  e.p "let raise_sql_error x =";
+  e.p "    raise (Sqlite3.Error (Rc.to_string x))";
+  e.p "";
+  e.p "let try_finally fn finalfn =";
+  e.p "    try";
+  e.p "      let r = fn () in";
+  e.p "      finalfn ();";
+  e.p "      r";
+  e.p "    with e -> begin";
+  e.p "      print_endline (sprintf \"WARNING: exception: %s\" (Printexc.to_string e));";
+  e.p "      finalfn ();";
+  e.p "      raise e";
+  e.p "    end";
+  e.p "";
+  e.p "(* retry until a non-BUSY error code is returned *)";
+  e.p "let rec db_busy_retry db fn =";
+  e.p "    match fn () with";
+  e.p "    |Rc.BUSY -> ";
+  e.p "       db.busyfn db.db;";
+  e.p "       db_busy_retry db fn;";
+  e.p "    |x -> x";
+  e.p "";
+  e.p "(* make sure an OK is returned from the database *)";
+  e.p "let db_must_ok db fn =";
+  e.p "    match db_busy_retry db fn with";
+  e.p "    |Rc.OK -> ()";
+  e.p "    |x -> raise_sql_error x";
+  e.p "";
+  e.p "(* make sure a DONE is returned from the database *)";
+  e.p "let db_must_done db fn = ";
+  e.p "   match db_busy_retry db fn with";
+  e.p "   |Rc.DONE -> ()";
+  e.p "   |x -> raise_sql_error x";
+  e.p "";
+  e.p "(* request a transaction *)";
+  e.p "let transaction db fn =";
+  e.p "    let m = match db.mode with";
+  e.p "    |`Deferred -> \"DEFERRED\" |`Immediate -> \"IMMEDIATE\" |`Exclusive -> \"EXCLUSIVE\" in";
+  e.p "    try_finally (fun () ->";
+  e.p "        if db.in_transaction = 0 then (";
+  e.p "           db_must_ok db (fun () -> exec db.db (sprintf \"BEGIN %s TRANSACTION\" m));";
+  e.p "        );";
+  e.p "        db.in_transaction <- db.in_transaction + 1;";
+  e.p "        fn ();";
+  e.p "    ) (fun () ->";
+  e.p "        if db.in_transaction = 1 then (";
+  e.p "           db_must_ok db (fun () -> exec db.db \"END TRANSACTION\");";
+  e.p "        );";
+  e.p "        db.in_transaction <- db.in_transaction - 1";
+  e.p "    )";
+  e.p "";
+  e.p "(* iterate over a result set *)";
+  e.p "let step_fold db stmt iterfn =";
+  e.p "    let stepfn () = Sqlite3.step stmt in";
+  e.p "    let rec fn a = match db_busy_retry db stepfn with";
+  e.p "    |Sqlite3.Rc.ROW -> fn (iterfn stmt :: a)";
+  e.p "    |Sqlite3.Rc.DONE -> a";
+  e.p "    |x -> raise_sql_error x";
+  e.p "    in";
+  e.p "    fn []";
+  ()
\ No newline at end of file