+$TITLE Documentation
++
+EOT
+cat html/depend.map >> html/index.html
+cat >>html/index.html </g;
+
+ # extra blank line
+ s//g;
+
+ # weird underscore
+ s/Â /_/g;
+
+ # putting back underscore
+ s/#\_#/\_/g;
+
+
+ # abundance of
+ s/\n
+
+
+
+
+
+$TITLE
+
+
+
+
+]-> a::b
+ and parse_name2 k = parser
+ []-> d::b
+ and parse_name_rem a b= parser
+ [<'Kwd "/";c=parse_name2 a >]-> c
+ | [<>]->[]
+
+and parse_ident = parser
+ [<'Ident a; b=parse_ident_rem a "" >]-> a ^ b
+ |[<'Int a; b=parse_ident_rem (string_of_int a) "" >]-> (string_of_int a) ^ b
+ and parse_ident2 k = parser
+ [<'Ident d; b=parse_ident_rem d k >]-> d ^ b
+ |[<'Int d; b=parse_ident_rem (string_of_int d) k >]-> (string_of_int d) ^ b
+ and parse_ident_rem a b= parser
+ [<'Kwd "-";c=parse_ident2 a >]-> "-" ^ c
+ | [<>]-> ""
+;;
+
+(*
+parse_name(lexer(Stream.of_string "u/sanglier/0/croap/pottier/Coq/Dist/contrib/Rocq/ALGEBRA/CATEGORY_THEORY/NT/YONEDA_LEMMA/NatFun.vo: "));;
+parse_ident(lexer(Stream.of_string "ARITH-OMEGA-ggg-2.vo:"));; PROBLEME
+*)
+
+(* reads the depend file *)
+let read_depend file=
+ let st =open_in file in
+ let lr =ref [] in
+ let rec other() =
+ (try
+ let d=parse_dep(lexer(Stream.of_string (input_line st))) in
+ lr:=d::(!lr);
+ other()
+ with _ ->[])
+ in (let _ = other() in ());
+ !lr;;
+
+(* graph of a directory (given by a path) *)
+let rec is_prefix p q = match p with
+ [] -> true
+ |a::p -> match q with [] -> false
+ |b::q -> if a=b then (is_prefix p q) else false
+;;
+
+let rec after_prefix p q = match p with
+ [] ->(match q with
+ [] -> "unknown"
+ |a::_ -> a)
+ |a::p -> match q with [] -> "unknown"
+ |b::q -> (after_prefix p q)
+;;
+
+let rec proj_graph p g = match g with
+ [] -> []
+ |(q,l)::g -> if (is_prefix p q)
+ then let rec proj_edges l = match l with
+ [] -> []
+ |r::l -> if (is_prefix p r)
+ then (after_prefix p r)::(proj_edges l)
+ else (proj_edges l)
+ in ((after_prefix p q),(proj_edges l))
+ ::(proj_graph p g)
+ else (proj_graph p g)
+
+;;
+
+let rec start_path p = match p with
+ [] ->[]
+ |a::p -> match p with
+ [] ->[]
+ |b::q -> a::(start_path p)
+;;
+
+
+(* the list of all the paths and subpaths in g *)
+let all_path g =
+ let ht =Hashtbl.create 50 in
+ let add_path p = Hashtbl.remove ht p;Hashtbl.add ht p true in
+ let rec add_subpath p = match p with
+ [] ->()
+ |_ -> add_path p; add_subpath (start_path p) in
+ let rec all_path g = match g with
+ [] -> ()
+ |(q,l)::g -> add_subpath (start_path q);
+ let rec all_pathl l = match l with
+ [] -> ()
+ |a::l -> add_subpath (start_path a);
+ all_pathl l
+ in all_pathl l;
+ all_path g
+ in all_path g;
+ let lp=ref [] in
+ Hashtbl.iter (fun x y -> lp:=x::!lp) ht;
+ !lp
+;;
+
+
+(*
+let g=read_depend "depend";;
+proj_graph ["theories"] g;;
+*)
+
+let rec endpath p = match p with
+ [] ->""
+ |a::p -> match p with
+ [] ->a
+ |_ -> endpath p
+;;
+
+let rec fpath p = match p with
+ [] ->""
+ |a::p -> a ^ "/" ^ (fpath p)
+;;
+
+let rec spath p = match p with
+ [] -> ""
+ |a::p -> match p with
+ [] ->a
+ |b::q -> a ^ "/" ^ (spath p)
+;;
+
+(* creates graphs for all paths *)
+
+
+let dependtodot file=
+ let g =(read_depend file) in
+ let lp1 = all_path g in
+ let lp = (if lp1=[] then [[]] else lp1) in
+ let rec ddv lp = match lp with
+ [] -> ()
+ |p::lp -> let name = (let f = (endpath p) in
+ if f="" then file else f) in
+ let filep = (let f = (spath p) in
+ if f="" then file else f) in
+ dot (remove_trans (proj_graph p g))
+ name filep;
+ ddv lp
+ in ddv lp
+
+;;
+let _ =
+ if (Array.length Sys.argv) == 2 then
+ dependtodot Sys.argv.(1)
+ else print_string "makedot depend";
+ print_newline()
+
diff --git a/etc/win-installer.nsi b/etc/win-installer.nsi
new file mode 100755
index 0000000..8562acc
--- /dev/null
+++ b/etc/win-installer.nsi
@@ -0,0 +1,115 @@
+SetCompressor lzma
+
+; The VERSION should be passed as an argument at compile time using :
+; nsis -DVERSION=1.5 win-installer.nsi
+
+!define MY_PRODUCT "Coq" ;Define your own software name here
+!define SRC ".\"
+!define SRC_SSR "C:\Coq\lib\user-contrib\Ssreflect\"
+!define SRC_MC "C:\Coq\lib\user-contrib\MathComp\"
+!define OUTFILE "ssr-mathcomp-installer-${VERSION}.exe"
+
+!include "MUI2.nsh"
+
+;--------------------------------
+;Configuration
+
+ Name "Ssreflect and the Mathematical Components library"
+
+ ;General
+ OutFile "${OUTFILE}"
+
+ ;Folder selection page
+ InstallDir "C:\Coq"
+
+ ;Remember install folder
+ InstallDirRegKey HKCU "Software\Coq" ""
+
+;--------------------------------
+;Modern UI Configuration
+
+ !insertmacro MUI_PAGE_WELCOME
+ !insertmacro MUI_PAGE_LICENSE "${SRC}\CeCILL-B"
+ !insertmacro MUI_PAGE_COMPONENTS
+ !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where Coq is installed."
+ !insertmacro MUI_PAGE_DIRECTORY
+ !insertmacro MUI_PAGE_INSTFILES
+ !insertmacro MUI_PAGE_FINISH
+
+ !insertmacro MUI_UNPAGE_WELCOME
+ !insertmacro MUI_UNPAGE_CONFIRM
+ !insertmacro MUI_UNPAGE_INSTFILES
+ !insertmacro MUI_UNPAGE_FINISH
+
+;--------------------------------
+;Languages
+
+ !insertmacro MUI_LANGUAGE "English"
+
+;--------------------------------
+;Language Strings
+
+ ;Description
+ LangString DESC_1 ${LANG_ENGLISH} "This package contains the Ssreflect proof language."
+ LangString DESC_2 ${LANG_ENGLISH} "This package contains the Mathematical Components lirbary."
+
+;--------------------------------
+;Installer Sections
+
+
+Section "Ssreflect" Sec1
+
+ SetOutPath "$INSTDIR\lib\user-contrib\Ssreflect\"
+
+ File /r ${SRC_SSR}\*.vo
+ File /r ${SRC_SSR}\*.v
+ File /r ${SRC_SSR}\*.glob
+ File /r ${SRC_SSR}\*.cmx
+ File /r ${SRC_SSR}\*.cmxs
+ File /r ${SRC_SSR}\*.cmi
+
+ CreateDirectory "$SMPROGRAMS\Coq"
+
+ WriteINIStr "$SMPROGRAMS\Coq\The Ssreflect Library.url" "InternetShortcut" "URL" "http://ssr.msr-inria.inria.fr/doc/ssreflect-${VERSION}/"
+
+ WriteINIStr "$SMPROGRAMS\Coq\The Ssreflect User Manaul.url" "InternetShortcut" "URL" "http://hal.inria.fr/inria-00258384/en"
+
+ SetOutPath "$INSTDIR"
+ writeUninstaller "Uninstall Ssreflect and MathComp.exe"
+
+SectionEnd
+
+Section "MathComp" Sec2
+
+ SetOutPath "$INSTDIR\lib\user-contrib\MathComp\"
+
+ File /r ${SRC_MC}\*.vo
+ File /r ${SRC_MC}\*.v
+ File /r ${SRC_MC}\*.glob
+ File /r ${SRC_MC}\*.cmx
+ File /r ${SRC_MC}\*.cmxs
+ File /r ${SRC_MC}\*.cmi
+
+ CreateDirectory "$SMPROGRAMS\Coq"
+
+ WriteINIStr "$SMPROGRAMS\Coq\The Mathematical Components Library.url" "InternetShortcut" "URL" "http://ssr.msr-inria.inria.fr/doc/mathcomp-${VERSION}/"
+
+SectionEnd
+
+!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
+ !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1)
+ !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
+!insertmacro MUI_FUNCTION_DESCRIPTION_END
+
+Section "Uninstall"
+
+ RMDir /r "$INSTDIR\lib\user-contrib\MathComp\"
+ RMDir /r "$INSTDIR\lib\user-contrib\Ssreflect\"
+
+ Delete "$SMPROGRAMS\Coq\The Mathematical Components Library.url"
+ Delete "$SMPROGRAMS\Coq\The Ssreflect Library.url"
+ Delete "$SMPROGRAMS\Coq\The Ssreflect User Manaul.url"
+
+ Delete "$INSTDIR\Uninstall Ssreflect and MathComp.exe"
+
+SectionEnd
--
cgit v1.2.3
+ s/\n
+
+
+
+
+EOT
+
+}
diff --git a/etc/utils/dependtodot.ml b/etc/utils/dependtodot.ml
new file mode 100644
index 0000000..1ea350f
--- /dev/null
+++ b/etc/utils/dependtodot.ml
@@ -0,0 +1,343 @@
+(* Loic Pottier, projet CROAP, INRIA Sophia Antipolis, April 1998. *)
+(* Laurent Théry , INRIA Sophia Antipolis, April 2007 *)
+
+(* Convert a dependencies file, in makefile form, into a graph in a file readable by dot.
+
+The function dependtodot takes as input the dependencies file, and create a file with the same name suffixed by ".dot", readable by dot.
+
+*)
+
+let nodecol="#dbc3b6";; (* #add8ff *)
+let edgecol="#676767";; (* #ff0000 *)
+
+(* parameters to draw edges and nodes *)
+let vnode x =
+ "l(\"" ^ x
+ ^ "\",n(\"\",[a(\"COLOR\",\""^ nodecol ^"\"),a(\"OBJECT\",\"" ^ x ^ "\")],"
+;;
+
+let wstring x = "\""^x^"\""
+;;
+
+let vnoder x = "r(\"" ^ x ^ "\")"
+;;
+
+let vedge =
+ "e(\"\",[a(\"_DIR\",\"inverse\"),a(\"EDGEPATTERN\",\"solid\"),a(\"EDGECOLOR\",\"" ^ edgecol ^ "\")],"
+;;
+
+let listdv l = match l with
+ [] -> "[]"
+ |x::l -> let rec listdvr l = match l with
+ [] -> ""
+ |y::l -> "," ^ y ^ (listdvr l)
+ in "[" ^ x ^ (listdvr l) ^ "]"
+;;
+
+let rec visit ht hte x s =
+ Hashtbl.add ht x x;
+ try let le=Hashtbl.find hte x in
+ let rec visit_edge ls le =
+ match le with
+ [] -> ls
+ |b::l ->
+ try let _ =Hashtbl.find ht b in
+ (visit_edge (ls@[vedge ^ (vnoder b) ^ ")"]) l)
+ with Not_found ->
+ (visit_edge (ls@[vedge ^ (visit ht hte b s) ^ ")"]) l)
+ in s ^ (vnode x) ^ (listdv (visit_edge [] le)) ^ "))"
+ with Not_found -> s ^ (vnode x) ^ "[]))"
+;;
+
+(* cloture transitive *)
+
+let rec merge_list a b = match a with
+ [] -> b
+ |x::a -> if (List.mem x b)
+ then (merge_list a b)
+ else x::(merge_list a b)
+;;
+
+let ht_graph g =
+ let ht =Hashtbl.create 50 in
+ let rec fill g = match g with
+ [] -> ()
+ |(a,lb)::g -> Hashtbl.add ht a lb; fill g
+ in fill g;
+ ht
+;;
+
+let trans_clos1 g =
+ let ht =ht_graph g in
+ List.map (fun (a,lb) ->
+ (a,(let l = ref lb in
+ let rec addlb lb = match lb with
+ [] -> ()
+ |b::lb -> (try l:=(merge_list (Hashtbl.find ht b) !l)
+ with Not_found -> ()); addlb lb
+ in addlb lb;
+ !l))) g
+;;
+
+let rec transitive_closure g =
+ let g1=trans_clos1 g in
+ if g1=g then g else (transitive_closure g1)
+;;
+
+(*
+let g=["A",["B"];
+ "B",["C"];
+ "C",["D"];
+ "D",["E"];
+ "E",["A"]];;
+transitive_closure g;;
+*)
+
+(* enlever les arcs de transitivite *)
+
+let remove_trans g =
+ let ht = ht_graph (transitive_closure g) in
+ List.map (fun (a,lb) ->
+ (a,(let l=ref [] in
+ (let rec sel l2 = match l2 with
+ [] -> ()
+ |b::l2 -> (let r=ref false in
+ (let rec testlb l3 = match l3 with
+ [] -> ()
+ |c::l3 -> if (not (b=a)) &&(not(b=c)) && (not (a=c)) &&
+ (try (List.mem b (Hashtbl.find ht c))
+ with Not_found -> false)
+ then r:=true
+ else ();
+ testlb l3
+ in testlb lb);
+ if (!r=false)
+ then l:=b::!l
+ else ());
+ sel l2
+ in sel lb);
+ !l))) g
+;;
+
+(*
+let g1=["Le", ["C";"Lt";"B"; "Plus"];
+ "Lt", ["A";"Plus"]];;
+
+let g=["A",["B";"C";"D";"E"];
+ "B",["C"];
+ "C",["D"];
+ "D",["E"]];;
+remove_trans g;;
+
+*)
+let dot g name file=
+ let chan_out = open_out (file^".dot") in
+ output_string chan_out "digraph ";
+ output_string chan_out name;
+ output_string chan_out " {\n";
+ output_string chan_out " bgcolor=transparent;\n";
+ output_string chan_out " splines=true;\n";
+ output_string chan_out " nodesep=1;\n";
+ output_string chan_out " node [fontsize=18, shape=rect, color=\"#dbc3b6\", style=filled];\n";
+ List.iter (fun (x,y) ->
+ output_string chan_out " ";
+ output_string chan_out (wstring x);
+ output_string chan_out " [URL=\"./";
+ output_string chan_out x;
+ output_string chan_out ".html\"]\n";
+ List.iter (fun y ->
+ output_string chan_out " ";
+ output_string chan_out (wstring x);
+ output_string chan_out " -> ";
+ output_string chan_out (wstring y);
+ output_string chan_out ";\n") y) g;
+ flush chan_out;
+ output_string chan_out "}";
+ close_out chan_out
+;;
+
+(*
+example: a complete 5-graph,
+
+let g=["A",["B";"C";"D";"E"];
+ "B",["A";"C";"D";"E"];
+ "C",["A";"B";"D";"E"];
+ "D",["A";"B";"C";"E"];
+ "E",["A";"B";"C";"D"]];;
+
+daVinci g "g2";;
+
+the file is then g2.daVinci
+
+*)
+(***********************************************************************)
+open Genlex;;
+
+(* change OP april 28 *)
+(*
+this parsing produce a pair where the first member is a paire (file,Directory)
+and the second is a list of pairs (file,Directory).
+from this we can compute the files graph dependency and also the directory graph dependency
+*)
+
+let lexer = make_lexer [":";".";"/";"-"];;
+
+let rec parse_dep = parser
+ [< a=parse_name; 'Kwd ".";'Ident b; _=parse_until_colon;
+ _=parse_name ;'Kwd "."; 'Ident d;n=parse_rem >] -> (a,n)
+and parse_rem = parser
+ [< a=parse_name;'Kwd ".";'Ident b;n=parse_rem >] -> a::n
+ | [<>]->[]
+and parse_until_colon = parser
+ [< 'Kwd ":" >] -> ()
+ | [< 'Kwd _; _=parse_until_colon >] -> ()
+ | [< 'Int _; _=parse_until_colon >] -> ()
+ | [< 'Ident _; _=parse_until_colon >] -> ()
+
+and parse_name = parser
+ [<'Kwd "/";a=parse_ident; b=parse_name_rem a "" >]-> a::b
+ |[
+
+
+
+
+
+
+EOT
+cat html/depend.map >> html/index.html
+cat >>html/index.html <
+Library index
+
+
++
+
+EOT
+cat html/depend.map >> html/index.html
+cat >>html/index.html <