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 exec_process cmd =
  29   let (stdout, stdin, stderr) as chs = Unix.open_process_full cmd [||] in
  30   let outlines = ref [] in
  31   let errlines = ref [] in
  32   (try
  33      while true do
  34        outlines := input_line stdout :: !outlines;
  35      done;
  36      assert false
  37    with End_of_file ->
  38    (try
  39      while true do
  40        errlines := input_line stderr :: !errlines;
  41      done;
  42      assert false
  43     with End_of_file ->
  44      match (Unix.close_process_full chs) with
  45      | Unix.WEXITED errno -> errno, !outlines, !errlines
  46      | _ -> assert false))
  47
  48 let string_of_output outlines errlines =
  49   let output = "std out =\n" ^ String.concat "\n" (List.rev outlines) in
  50   let errors = "std err =\n" ^ String.concat "\n" (List.rev errlines) in
  51   output ^ "\n\n" ^ errors
  52
  53 type svn_flag =
  54 | Add
  55 | Conflict
  56 | Modified
  57 | NotAdded
  58 | Delete
  59 | Update
  60 | Merge
  61
  62 type matita_flag =
  63 | MUnversioned
  64 | MSynchronized
  65 | MAdd
  66 | MModified
  67 | MConflict
  68
  69 let string_of_matita_flag = function
  70 | MUnversioned -> "unversioned"
  71 | MSynchronized -> "synchronized"
  72 | MAdd -> "new"
  73 | MModified -> "modified"
  74 | MConflict -> "conflict!"
  75
  76 exception SvnAnomaly of string
  77
  78 let stat_classify line =
  79   let rec aux n acc =
  80     match (line.[n], n) with
  81     | _, n when n = 7 -> String.sub line 8 ((String.length line) - 8), acc
  82     | ' ', _ -> aux (n+1) acc
  83     | 'A',0 -> aux (n+1) (Add::acc)
  84     | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
  85 (*  | 'D',0 -> aux (n+1) (Delete::acc) *)
  86 (*  | 'I',0 -> aux (n+1) (Ignore::acc) *)
  87     | 'M',_ when n = 0 || n = 1 -> aux (n+1) (Modified::acc)
  88 (*  | 'R',0 -> aux (n+1) (Replaced::acc) *)
  89 (*  | 'X',0 -> aux (n+1) (UnversionedDir::acc) *)
  90     | '?',0 -> aux (n+1) (NotAdded::acc)
  91 (*  | '!',0 -> aux (n+1) (Missing::acc) *)
  92 (*  | '~',0 -> aux (n+1) (Obstructed::acc) *)
  93 (*  | 'L',2 -> aux (n+1) (Lock::acc) *)
  94 (*  | '+',3 -> aux (n+1) (History::acc) *)
  95 (*  | 'S',4 -> aux (n+1) (SwitchedUrl::acc) *)
  96 (*  | 'X',4 -> aux (n+1) (External::acc) *)
  97 (*  | 'K',5 -> aux (n+1) (LockToken::acc) *)
  98 (*  | 'C',6 -> aux (n+1) (TreeConflict::acc) *)
  99     | _ -> raise (SvnAnomaly line)
 100   in aux 0 []
 101
 102 let count p l =
 103   List.length (List.filter p l)
 104
 105 exception Unimplemented
 106
 107 let matita_flag_of_stat fs =
 108   if List.mem Conflict fs then MConflict
 109   else if List.mem Modified fs then MModified
 110   else if List.mem Add fs then MAdd
 111   else if List.mem Delete fs then raise Unimplemented
 112   else if List.mem NotAdded fs then MUnversioned
 113   else MSynchronized
 114
 115 let stat_user user =
 116   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 117   let _repo = Helm_registry.get "matita.weblib" in
 118
 119   let errno, outlines, errlines = exec_process
 120     ("svn stat " ^ rt_dir ^ "/users/" ^ user ^ "/")
 121   in
 122   let files, anomalies =
 123     List.fold_left (fun (facc,eacc) line ->
 124       try
 125         (stat_classify line::facc), eacc
 126       with
 127       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 128   in
 129   let files =
 130     List.map (fun (fname,flags) -> fname,Some (matita_flag_of_stat flags)) files
 131   in
 132
 133   if errno = 0 then files, anomalies
 134   else raise (SvnError ("Anomalies: " ^ (String.concat "\n" anomalies) ^ "\n\n" ^ (string_of_output outlines errlines)))
 135 ;;
 136
 137 (* update and checkout *)
 138 let up_classify line uid =
 139   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid ^ "/" in
 140   let rec aux n acc =
 141     match (line.[n], n) with
 142     | _, n when n = 4 ->
 143        let fn = String.sub line 5 ((String.length line) - 5) in
 144        let prefix_len = String.length basedir in
 145        let fn_len = String.length fn in
 146        if String.sub fn 0 prefix_len = basedir
 147           then String.sub fn prefix_len (fn_len - prefix_len), acc
 148           else fn, acc
 149     | ' ', _ -> aux (n+1) acc
 150     | 'A',_ when n = 0 || n = 1 -> aux (n+1) (Add::acc)
 151     | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
 152     | 'D',_ when n = 0 || n = 1 -> aux (n+1) (Delete::acc)
 153     | 'U',_ when n = 0 || n = 1 -> aux (n+1) (Update::acc)
 154     | 'G',_ when n = 0 || n = 1 -> aux (n+1) (Merge::acc)
 155 (*  | 'E',_ when n = 0 || n = 1 -> aux (n+1) (Exist::acc) *)
 156     | _ -> raise (SvnAnomaly line)
 157   in aux 0 []
 158
 159 let matita_flag_of_update fs =
 160   if List.mem Conflict fs then Some MConflict
 161   else if List.mem Delete fs then None
 162   else if List.mem Merge fs then Some MModified
 163   else Some MSynchronized
 164
 165 (* this should be executed only for a freshly created user so no CS is needed *)
 166 let checkout user =
 167   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 168   let repo = Helm_registry.get "matita.weblib" in
 169
 170   let errno, outlines, errlines = exec_process
 171     ("svn co --non-interactive " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/")
 172   in
 173   let files, anomalies =
 174     List.fold_left (fun (facc,eacc) line ->
 175       try
 176         (up_classify line user::facc), eacc
 177       with
 178       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 179   in
 180   if errno = 0 then List.map (fun (f,_) -> f,MSynchronized) files
 181   else raise (SvnError (string_of_output outlines errlines))
 182
 183 (* normalize qualified file name *)
 184 let normalize_qfn p =
 185   (* trim leading "./" *)
 186   let p =
 187     try
 188       if String.sub p 0 2 <> "./" then p
 189       else String.sub p 2 (String.length p - 2)
 190     with
 191     | Invalid_argument _ -> p
 192   in
 193   (* trim trailing "/" *)
 194   try
 195     if String.sub p (String.length p - 1) 1 <> "/" then p
 196     else String.sub p 0 (String.length p - 1)
 197   with
 198   | Invalid_argument _ -> p
 199
 200 let html_of_library uid ft =
 201   let i = ref 0 in
 202   let newid () = incr i; ("node" ^ string_of_int !i) in
 203
 204   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in
 205
 206
 207   let branch lpath children =
 208     let id = newid () in
 209     let name = Filename.basename lpath in
 210     let name = if name <> "." then name else "cic:/matita" in
 211     let flag =
 212       try List.assoc lpath ft
 213       with Not_found -> MSynchronized in
 214     let szflag = string_of_matita_flag flag in
 215     "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "','" ^ lpath ^ "')\">\n" ^
 216     "<img src=\"treeview/closed.gif\" id=\"I" ^ id ^ "\"/>\n" ^
 217     name ^ " " ^ szflag ^ "<br/></span>\n" ^
 218     "<span class=\"branch\" id=\"" ^ id ^ "\">\n" ^
 219     children ^ "\n</span>"
 220   in
 221   let leaf lpath =
 222     let flag =
 223       try List.assoc lpath ft
 224       with Not_found -> MSynchronized in
 225     let szflag = string_of_matita_flag flag in
 226     "<img src=\"treeview/doc.gif\"/>\n" ^
 227     "<a href=\"javascript:void(0)\" onClick=\"selectFile('" ^ lpath ^ "')\" onDblClick=\"dialogBox.callback('" ^ lpath ^ "')\">" ^
 228      (Filename.basename lpath) ^ " " ^ szflag ^ "</a><br/>"
 229   in
 230
 231   let rec aux path =
 232     let lpath filename = path ^ "/" ^ filename in
 233     let gpath filename = basedir ^ "/" ^ path ^ "/" ^ filename in
 234
 235     (* hide hidden dirs ... including svn stuff *)
 236     let dirlist =
 237       List.filter (fun x -> String.sub x 0 1 <> ".")
 238         (Array.to_list (Sys.readdir (basedir ^ "/" ^ path))) in
 239     let subdirs = List.filter (fun x -> Sys.is_directory (gpath x)) dirlist in
 240
 241     (* only .ma scripts, hidden files excluded *)
 242     let scripts =
 243       List.filter (fun x ->
 244         try
 245           let i = String.rindex x '.' in
 246           let len = String.length x - i in
 247           not (Sys.is_directory (gpath x)) &&
 248           (String.sub x 0 1 <> ".") && (String.sub x i len = ".ma")
 249         with Not_found | Invalid_argument _ -> false) dirlist in
 250     let subdirtags =
 251       String.concat "\n" (List.map (fun x -> aux (normalize_qfn (lpath x ^ "/"))) subdirs) in
 252     let scripttags =
 253       String.concat "\n"
 254        (List.map (fun x -> leaf (normalize_qfn (lpath x))) scripts)
 255     in
 256     branch path (subdirtags ^ "\n" ^ scripttags)
 257   in
 258
 259   let res = aux "." in
 260   prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE";
 261   res
 262 ;;
 263
 264 let reset_lib () =
 265   let to_be_removed = (Helm_registry.get "matita.rt_base_dir") ^ "/users/*" in
 266   ignore (Sys.command ("rm -rf " ^ to_be_removed))
 267 ;;
 268
 269 let update_user user =
 270   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 271   let _repo = Helm_registry.get "matita.weblib" in
 272
 273   let errno, outlines, errlines = exec_process
 274    ("svn up --non-interactive " ^ rt_dir ^ "/users/" ^ user ^ "/")
 275   in
 276   let files, anomalies =
 277     List.fold_left (fun (facc,eacc) line ->
 278       try
 279         (let fname,flags = up_classify line user in
 280          (fname, flags)::facc), eacc
 281       with
 282       | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
 283   in
 284   let added = count (fun (_,flags) -> List.mem Add flags) files in
 285   let conflict = count (fun (_,flags) -> List.mem Conflict flags) files in
 286   let del = count (fun (_,flags) -> List.mem Delete flags) files in
 287   let upd = count (fun (_,flags) -> List.mem Update flags) files in
 288   let merged = count (fun (_,flags) -> List.mem Merge flags) files in
 289
 290   let files =
 291     List.map (fun (fname,flags) -> fname,matita_flag_of_update flags) files
 292   in
 293
 294   if errno = 0 then files, anomalies, (added,conflict,del,upd,merged)
 295   else raise (SvnError (string_of_output outlines errlines))
 296 ;;
 297
 298 let add_files user files =
 299   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 300   let _repo = Helm_registry.get "matita.weblib" in
 301
 302   let files = String.concat " "
 303     (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in
 304
 305   let errno, outlines, errlines =
 306     if files <> "" then
 307       exec_process ("svn add --non-interactive " ^ files)
 308     else 0,[],[]
 309   in
 310   if errno = 0 then
 311     "BEGIN ADD - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END ADD - " ^ user ^ "\n\n"
 312   else raise (SvnError (string_of_output outlines errlines))
 313 ;;
 314
 315 (* this function should only be called by the server itself (or
 316  * the admin) at a scheduled time, so no concurrent instances and no CS needed
 317  * also, svn should already be safe as far as concurrency is concerned *)
 318 let commit user files =
 319   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 320   let _repo = Helm_registry.get "matita.weblib" in
 321
 322   let files = String.concat " "
 323     (List.map ((^) (rt_dir ^ "/users/" ^ user ^ "/")) files) in
 324
 325   let errno, outlines, errlines = exec_process
 326     ("svn ci --non-interactive --message \"commit by user " ^ user ^ "\" " ^ files)
 327   in
 328   if errno = 0 then
 329     "BEGIN COMMIT - " ^ user ^ ":\n" ^ (string_of_output outlines errlines) ^ "END COMMIT - " ^ user ^ "\n\n"
 330   else raise (SvnError (string_of_output outlines errlines))
 331 ;;
 332