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 ->
  50         let output = "std out =\n" ^ String.concat "\n" (List.rev !outlines) in
  51         let errors = "std err =\n" ^ String.concat "\n" (List.rev !errlines) in
  52         errno, output ^ "\n\n" ^ errors
  53      | _ -> assert false))
  54
  55 (* this should be executed only for a freshly created user
  56  * so no CS is needed *)
  57 let checkout user =
  58   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
  59   let repo = Helm_registry.get "matita.weblib" in
  60
  61   let errno, outstr = exec_process
  62     ("svn co " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/")
  63   in
  64   if errno = 0 then ()
  65   else raise (SvnError outstr)
  66
  67 let html_of_library uid =
  68   let i = ref 0 in
  69   let newid () = incr i; ("node" ^ string_of_int !i) in
  70
  71   let basedir = (Helm_registry.get "matita.rt_base_dir") ^ "/users/" ^ uid in
  72
  73   let branch lpath children =
  74     let id = newid () in
  75     let name = Filename.basename lpath in
  76     let name = if name <> "." then name else "cic:/matita" in
  77     "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "','" ^ lpath ^ "/')\">\n" ^
  78     "<img src=\"treeview/closed.gif\" id=\"I" ^ id ^ "\"/>\n" ^
  79     name ^ "<br/></span>\n" ^
  80     "<span class=\"branch\" id=\"" ^ id ^ "\">\n" ^
  81     children ^ "\n</span>"
  82   in
  83   let leaf lpath =
  84     "<img src=\"treeview/doc.gif\"/>\n" ^
  85     "<a href=\"javascript:selectFile('" ^ lpath ^ "')\">" ^
  86      (Filename.basename lpath) ^ "</a><br/>"
  87   in
  88
  89   let rec aux path =
  90     let lpath filename = path ^ "/" ^ filename in
  91     let gpath filename = basedir ^ "/" ^ path ^ "/" ^ filename in
  92     let dirlist =
  93       List.filter (fun x -> String.sub x 0 1 <> ".")
  94         (Array.to_list (Sys.readdir (basedir ^ "/" ^ path))) in
  95     let subdirs = List.filter (fun x -> Sys.is_directory (gpath x)) dirlist in
  96     let scripts =
  97       List.filter (fun x ->
  98         try
  99           let i = String.rindex x '.' in
 100           let len = String.length x - i in
 101           not (Sys.is_directory (gpath x)) &&
 102           (String.sub x 0 1 <> ".") && (String.sub x i len = ".ma")
 103         with Not_found | Invalid_argument _ -> false) dirlist in
 104     let subdirtags =
 105       String.concat "\n" (List.map (fun x -> aux (lpath x)) subdirs) in
 106     let scripttags =
 107       String.concat "\n"
 108        (List.map (fun x -> leaf (lpath x)) scripts)
 109     in
 110     branch path (subdirtags ^ "\n" ^ scripttags)
 111   in
 112
 113   let res = aux "." in
 114   prerr_endline "BEGIN TREE";prerr_endline res;prerr_endline "END TREE";
 115   res
 116 ;;
 117
 118 let reset_lib () =
 119   let to_be_removed = (Helm_registry.get "matita.rt_base_dir") ^ "/users/*" in
 120   ignore (Sys.command ("rm -rf " ^ to_be_removed))
 121 ;;
 122
 123 (* adds a user to the commit queue; concurrent instances possible, so we
 124  * enclose the update in a CS
 125  *)
 126 let add_user uid =
 127   Mutex.lock mutex;
 128   to_be_committed := uid::List.filter (fun x -> x <> uid) !to_be_committed;
 129   Mutex.unlock mutex;
 130 ;;
 131
 132 (* this function and the next one should only be called by the server itself (or
 133  * the admin) at a scheduled time, so no concurrent instances and no CS needed
 134  * also, svn should already be safe as far as concurrency is concerned *)
 135 let commit user =
 136   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
 137   let repo = Helm_registry.get "matita.weblib" in
 138
 139   let errno, outstr = exec_process
 140     ("svn ci --message \"commit by user " ^ user ^ "\" " ^ rt_dir ^ "/users/" ^ user ^ "/")
 141   in
 142   if errno = 0 then ()
 143   else raise (SvnError outstr)
 144
 145 let do_global_commit () =
 146   prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed);
 147   List.fold_left
 148     (fun acc u ->
 149        try
 150          commit u;
 151          acc
 152        with
 153        | SvnError outstr ->
 154            prerr_endline outstr;
 155            u::acc)
 156   [] (List.rev !to_be_committed)
 157 ;;