matitaB/matita/matitaFilesystem.ml

   1 (* Copyright (C) 2004-2011, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 exception SvnError of string;;
  27
  28 let mutex = Mutex.create ();;
  29
  30 let to_be_committed = ref [];;
  31
  32 let exec_process cmd =
  33   let (stdout, stdin, stderr) as chs = Unix.open_process_full cmd [||] in
  34   let outlines = ref [] in
  35   let errlines = ref [] in
  36   (try
  37      while true do
  38        outlines := input_line stdout :: !outlines;
  39      done;
  40      assert false
  41    with End_of_file ->
  42    (try
  43      while true do
  44        errlines := input_line stderr :: !errlines;
  45      done;
  46      assert false
  47     with End_of_file ->
  48      match (Unix.close_process_full chs) with
  49      | Unix.WEXITED errno -> errno, !outlines, !errlines
  50      | _ -> assert false))
  51
  52 let string_of_output outlines errlines =
  53   let output = "std out =\n" ^ String.concat "\n" (List.rev outlines) in
  54   let errors = "std err =\n" ^ String.concat "\n" (List.rev errlines) in
  55   output ^ "\n\n" ^ errors
  56
  57 type svn_flag =
  58 | Add
  59 | Conflict
  60 | Modified
  61 | NotAdded
  62 | Delete
  63 | Update
  64 | Merge
  65
  66 type matita_flag =
  67 | MUnversioned
  68 | MSynchronized
  69 | MAdd
  70 | MModified
  71 | MConflict
  72
  73 let string_of_matita_flag = function
  74 | MUnversioned -> "unversioned"
  75 | MSynchronized -> "synchronized"
  76 | MAdd -> "new"
  77 | MModified -> "modified"
  78 | MConflict -> "conflict!"
  79
  80 exception SvnAnomaly of string
  81
  82 let stat_classify line =
  83   let rec aux n acc =
  84     match (line.[n], n) with
  85     | _, n when n = 7 -> String.sub line 8 ((String.length line) - 8), acc
  86     | ' ', _ -> aux (n+1) acc
  87     | 'A',0 -> aux (n+1) (Add::acc)
  88     | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
  89 (*  | 'D',0 -> aux (n+1) (Delete::acc) *)
  90 (*  | 'I',0 -> aux (n+1) (Ignore::acc) *)
  91     | 'M',_ when n = 0 || n = 1 -> aux (n+1) (Modified::acc)
  92 (*  | 'R',0 -> aux (n+1) (Replaced::acc) *)
  93 (*  | 'X',0 -> aux (n+1) (UnversionedDir::acc) *)
  94     | '?',0 -> aux (n+1) (NotAdded::acc)
  95 (*  | '!',0 -> aux (n+1) (Missing::acc) *)
  96 (*  | '~',0 -> aux (n+1) (Obstructed::acc) *)
  97 (*  | 'L',2 -> aux (n+1) (Lock::acc) *)
  98 (*  | '+',3 -> aux (n+1) (History::acc) *)
  99 (*  | 'S',4 -> aux (n+1) (SwitchedUrl::acc) *)
 100 (*  | 'X',4 -> aux (n+1) (External::acc) *)
 101 (*  | 'K',5 -> aux (n+1) (LockToken::acc) *)
 102 (*  | 'C',6 -> aux (n+1) (TreeConflict::acc) *)
 103     | _ -> raise (SvnAnomaly line)
 104   in aux 0 []
 105
 106 let stat_user user =
 107   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 108   let repo = Helm_registry.get "matita.weblib" in
 109
 110   let errno, outlines, errlines = exec_process
 111     ("svn stat " ^ rt_dir ^ "/users/" ^ user ^ "/")
 112   in
 113   let files, anomalies =
 114     List.fold_left (fun (facc,eacc) line ->
 115       try
 116         (stat_classify line::facc), eacc
 117       with
 118       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 119   in
 120   if errno = 0 then files, anomalies
 121   else raise (SvnError ("Anomalies: " ^ (String.concat "\n" anomalies) ^ "\n\n" ^ (string_of_output outlines errlines)))
 122 ;;
 123
 124 (* update and checkout *)
 125 let up_classify line uid =
 126   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid ^ "/" in
 127   let rec aux n acc =
 128     match (line.[n], n) with
 129     | _, n when n = 4 ->
 130        let fn = String.sub line 5 ((String.length line) - 5) in
 131        let prefix_len = String.length basedir in
 132        let fn_len = String.length fn in
 133        if String.sub fn 0 prefix_len = basedir
 134           then String.sub fn prefix_len (fn_len - prefix_len), acc
 135           else fn, acc
 136     | ' ', _ -> aux (n+1) acc
 137     | 'A',_ when n = 0 || n = 1 -> aux (n+1) (Add::acc)
 138     | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
 139     | 'D',_ when n = 0 || n = 1 -> aux (n+1) (Delete::acc)
 140     | 'U',_ when n = 0 || n = 1 -> aux (n+1) (Update::acc)
 141     | 'G',_ when n = 0 || n = 1 -> aux (n+1) (Merge::acc)
 142 (*  | 'E',_ when n = 0 || n = 1 -> aux (n+1) (Exist::acc) *)
 143     | _ -> raise (SvnAnomaly line)
 144   in aux 0 []
 145
 146 let matita_flag_of_update fs =
 147   if List.mem Conflict fs then Some MConflict
 148   else if List.mem Delete fs then None
 149   else if List.mem Merge fs then Some MModified
 150   else Some MSynchronized
 151
 152 (* this should be executed only for a freshly created user so no CS is needed *)
 153 let checkout user =
 154   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 155   let repo = Helm_registry.get "matita.weblib" in
 156
 157   let errno, outlines, errlines = exec_process
 158     ("svn co " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/")
 159   in
 160   let files, anomalies =
 161     List.fold_left (fun (facc,eacc) line ->
 162       try
 163         (up_classify line user::facc), eacc
 164       with
 165       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 166   in
 167   if errno = 0 then List.map (fun (f,_) -> f,MSynchronized) files
 168   else raise (SvnError (string_of_output outlines errlines))
 169
 170 (* normalize qualified file name *)
 171 let normalize_qfn p =
 172   (* trim leading "./" *)
 173   let p =
 174     try
 175       if String.sub p 0 2 <> "./" then p
 176       else String.sub p 2 (String.length p - 2)
 177     with
 178     | Invalid_argument _ -> p
 179   in
 180   (* trim trailing "/" *)
 181   try
 182     if String.sub p (String.length p - 1) 1 <> "/" then p
 183     else String.sub p 0 (String.length p - 1)
 184   with
 185   | Invalid_argument _ -> p
 186
 187 let html_of_library uid ft =
 188   let i = ref 0 in
 189   let newid () = incr i; ("node" ^ string_of_int !i) in
 190
 191   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in
 192
 193
 194   let branch lpath children =
 195     let id = newid () in
 196     let name = Filename.basename lpath in
 197     let name = if name <> "." then name else "cic:/matita" in
 198     let flag =
 199       try List.assoc lpath ft
 200       with Not_found -> MSynchronized in
 201     let szflag = string_of_matita_flag flag in
 202     "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "','" ^ lpath ^ "')\">\n" ^
 203     "<img src=\"treeview/closed.gif\" id=\"I" ^ id ^ "\"/>\n" ^
 204     name ^ " " ^ szflag ^ "<br/></span>\n" ^
 205     "<span class=\"branch\" id=\"" ^ id ^ "\">\n" ^
 206     children ^ "\n</span>"
 207   in
 208   let leaf lpath =
 209     let flag =
 210       try List.assoc lpath ft
 211       with Not_found -> MSynchronized in
 212     let szflag = string_of_matita_flag flag in
 213     "<img src=\"treeview/doc.gif\"/>\n" ^
 214     "<a href=\"javascript:void(0)\" onClick=\"selectFile('" ^ lpath ^ "')\" onDblClick=\"dialogBox.callback('" ^ lpath ^ "')\">" ^
 215      (Filename.basename lpath) ^ " " ^ szflag ^ "</a><br/>"
 216   in
 217
 218   let rec aux path =
 219     let lpath filename = path ^ "/" ^ filename in
 220     let gpath filename = basedir ^ "/" ^ path ^ "/" ^ filename in
 221
 222     (* hide hidden dirs ... including svn stuff *)
 223     let dirlist =
 224       List.filter (fun x -> String.sub x 0 1 <> ".")
 225         (Array.to_list (Sys.readdir (basedir ^ "/" ^ path))) in
 226     let subdirs = List.filter (fun x -> Sys.is_directory (gpath x)) dirlist in
 227
 228     (* only .ma scripts, hidden files excluded *)
 229     let scripts =
 230       List.filter (fun x ->
 231         try
 232           let i = String.rindex x '.' in
 233           let len = String.length x - i in
 234           not (Sys.is_directory (gpath x)) &&
 235           (String.sub x 0 1 <> ".") && (String.sub x i len = ".ma")
 236         with Not_found | Invalid_argument _ -> false) dirlist in
 237     let subdirtags =
 238       String.concat "\n" (List.map (fun x -> aux (normalize_qfn (lpath x ^ "/"))) subdirs) in
 239     let scripttags =
 240       String.concat "\n"
 241        (List.map (fun x -> leaf (normalize_qfn (lpath x))) scripts)
 242     in
 243     branch path (subdirtags ^ "\n" ^ scripttags)
 244   in
 245
 246   let res = aux "." in
 247   prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE";
 248   res
 249 ;;
 250
 251 let reset_lib () =
 252   let to_be_removed = (Helm_registry.get "matita.rt_base_dir") ^ "/users/*" in
 253   ignore (Sys.command ("rm -rf " ^ to_be_removed))
 254 ;;
 255
 256 (* adds a user to the commit queue; concurrent instances possible, so we
 257  * enclose the update in a CS
 258  *)
 259 let add_user uid =
 260   Mutex.lock mutex;
 261   to_be_committed := uid::List.filter (fun x -> x <> uid) !to_be_committed;
 262   Mutex.unlock mutex;
 263 ;;
 264
 265 let update_user user =
 266   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 267   let repo = Helm_registry.get "matita.weblib" in
 268
 269   let errno, outlines, errlines = exec_process
 270     ("svn up " ^ rt_dir ^ "/users/" ^ user ^ "/ --non-interactive")
 271   in
 272   let files, anomalies =
 273     List.fold_left (fun (facc,eacc) line ->
 274       try
 275         (let fname,flags = up_classify line user in
 276          (fname,matita_flag_of_update flags)::facc), eacc
 277       with
 278       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 279   in
 280   if errno = 0 then files, anomalies
 281   else raise (SvnError (string_of_output outlines errlines))
 282 ;;
 283
 284 (* this function and the next one should only be called by the server itself (or
 285  * the admin) at a scheduled time, so no concurrent instances and no CS needed
 286  * also, svn should already be safe as far as concurrency is concerned *)
 287 let commit user =
 288   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 289   let repo = Helm_registry.get "matita.weblib" in
 290
 291   let errno, outlines, errlines = exec_process
 292     ("svn ci --message \"commit by user " ^ user ^ "\" " ^ rt_dir ^ "/users/" ^ user ^ "/")
 293   in
 294   if errno = 0 then ()
 295   else raise (SvnError (string_of_output outlines errlines))
 296 ;;
 297
 298 let do_global_commit () =
 299   prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed);
 300   List.fold_left
 301     (fun acc u ->
 302        try
 303          commit u;
 304          acc
 305        with
 306        | SvnError outstr ->
 307            prerr_endline outstr;
 308            u::acc)
 309   [] (List.rev !to_be_committed)
 310 ;;