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