From: Stefano Zacchiroli Date: Wed, 2 Nov 2005 10:36:01 +0000 (+0000) Subject: matita distribution stuff X-Git-Tag: V_0_7_2_3~161 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=688b371f4bf16e749f16143f8c225d2cb2f225d5;p=helm.git matita distribution stuff --- diff --git a/helm/matita/dist/Makefile b/helm/matita/dist/Makefile new file mode 100644 index 000000000..669137bf2 --- /dev/null +++ b/helm/matita/dist/Makefile @@ -0,0 +1,17 @@ +MYSQL_FLAGS = --extended_insert --lock-tables=off --no-create-info +DB = -u helm -h mowgli.cs.unibo.it matita +TABLE_CREATOR = ../../ocaml/metadata/table_creator/table_creator +TABLES := $(shell $(TABLE_CREATOR) list all) +all: static_link +clean: static_link_clean +.PHONY: static_link +static_link: + $(MAKE) -C static_link/ +static_link_clean: + $(MAKE) -C static_link/ clean +dist: matita_stdlib.sql.gz +.PHONY: matita_stdlib.sql +matita_stdlib.sql: + mysqldump $(MYSQL_FLAGS) $(DB) $(TABLES) > $@ +%.gz: % + gzip -c $< > $@ diff --git a/helm/matita/dist/static_link/.cvsignore b/helm/matita/dist/static_link/.cvsignore new file mode 100644 index 000000000..a922053a0 --- /dev/null +++ b/helm/matita/dist/static_link/.cvsignore @@ -0,0 +1,3 @@ +static_link +static_link.cmi +static_link.cmo diff --git a/helm/matita/dist/static_link/Makefile b/helm/matita/dist/static_link/Makefile new file mode 100644 index 000000000..5a02bb3b7 --- /dev/null +++ b/helm/matita/dist/static_link/Makefile @@ -0,0 +1,5 @@ +all: static_link +static_link: static_link.ml + ocamlfind ocamlc -package unix,str -linkpkg -o $@ $< +clean: + rm -f static_link.cm* static_link diff --git a/helm/matita/dist/static_link/static_link.ml b/helm/matita/dist/static_link/static_link.ml new file mode 100644 index 000000000..f910cd3ef --- /dev/null +++ b/helm/matita/dist/static_link/static_link.ml @@ -0,0 +1,162 @@ + +open Printf + +exception Found of string list + +let ocamlobjinfo = "ocamlobjinfo" +let noautolink = "-noautolink" +let dummy_opt_cmd = "dummy_ocamlopt" +let opt_cmd = "ocamlopt" +let libdirs = [ "/lib"; "/usr/lib" ] +let exceptions = [ "threads.cma", [ "-lthreads", "-lthreadsnat" ] ] + +let blanks_RE = Str.regexp "[ \t\r\n]+" +let cmxa_RE = Str.regexp "\\.cmxa$" +let extra_cfiles_RE = Str.regexp "^.*Extra +C +object +files:\\(.*\\)$" +let extra_copts_RE = Str.regexp "^.*Extra +C +options:\\(.*\\)$" +let lib_RE = Str.regexp "^lib" +let l_RE = Str.regexp "^-l" +let opt_line_RE = Str.regexp (sprintf "^\\+ +%s +\\(.*\\)$" dummy_opt_cmd) +let trailing_cmxa_RE = Str.regexp ".*\\.cmxa$" + +let message s = prerr_endline ("STATIC_LINK: " ^ s) +let warning s = message ("WARNING: " ^ s) + +let handle_exceptions ~cma cflag = + try + let cma_exns = List.assoc (Filename.basename cma) exceptions in + let cflag' = List.assoc cflag cma_exns in + message (sprintf "using %s exception %s -> %s" cma cflag cflag'); + cflag' + with Not_found -> cflag + +let parse_cmdline () = + let mine, rest = ref [], ref [] in + let is_mine = ref true in + Array.iter + (function + | "--" -> is_mine := false + | s when !is_mine -> + if Str.string_match lib_RE s 0 then + warning (sprintf + ("libraries to be statically linked must be specified " + ^^ "without heading \"lib\", \"%s\" argument may be wrong") s); + mine := s :: !mine + | s -> rest := s :: !rest) + Sys.argv; + if !rest = [] then begin + prerr_endline "Usage: static_link [ CLIB .. ] -- COMMAND [ ARG .. ]"; + prerr_endline ("Example: static_link pcre expat --" + ^ " ocamlfind opt -package pcre,expat -linkpkg -o foo foo.ml"); + exit 0 + end; + List.tl (List.rev !mine), List.rev !rest + +let extract_opt_flags cmd = + let ic = Unix.open_process_in cmd in + (try + while true do + let l = input_line ic in + if Str.string_match opt_line_RE l 0 then begin + message ("got ocamlopt line: " ^ l); + raise (Found (Str.split blanks_RE (Str.matched_group 1 l))); + end + done; + [] (* dummy value *) + with + | End_of_file -> failwith "compiler command not found" + | Found flags -> + close_in ic; + flags) + +let cma_of_cmxa = Str.replace_first cmxa_RE ".cma" + +let find_clib libname = + let rec aux = + function + | [] -> raise Not_found + | libdir :: tl -> + let fname = sprintf "%s/lib%s.a" libdir libname in + if Sys.file_exists fname then fname else aux tl + in + aux libdirs + +let a_of_cflag cflag = (* "-lfoo" -> "/usr/lib/libfoo.a" *) + let libname = Str.replace_first l_RE "" cflag in + find_clib libname + +let cflags_of_cma fname = + let ic = Unix.open_process_in (sprintf "%s %s" ocamlobjinfo fname) in + let extra_copts = ref "" in + let extra_cfiles = ref "" in + (try + while true do + match input_line ic with + | s when Str.string_match extra_copts_RE s 0 -> + extra_copts := Str.matched_group 1 s + | s when Str.string_match extra_cfiles_RE s 0 -> + extra_cfiles := Str.matched_group 1 s + | _ -> () + done + with End_of_file -> ()); + close_in ic; + let extra_cfiles = List.rev (Str.split blanks_RE !extra_cfiles) in + let extra_copts = Str.split blanks_RE !extra_copts in + extra_copts @ extra_cfiles + +let staticize static_libs flags = + let static_flags = List.map ((^) "-l") static_libs in + let aux ~add_cclib ~cma cflag = + let cflag = + if List.mem cflag static_flags + then + (try + let a = a_of_cflag cflag in + message (sprintf "using static %s instead of shared %s" a cflag); + a + with Not_found -> warning ("can't find lib for " ^ cflag); cflag) + else (handle_exceptions ~cma cflag) + in + if add_cclib then [ "-cclib"; cflag ] else [ cflag ] + in + List.fold_right + (fun flag acc -> + let cma = cma_of_cmxa flag in + if Str.string_match trailing_cmxa_RE flag 0 then begin + message ("processing native archive: " ^ flag); + let cflags = cflags_of_cma cma in + let cflags' = + List.fold_right + (fun cflag acc -> (aux ~add_cclib:true ~cma cflag) @ acc) + cflags [] + in + flag :: (cflags' @ acc) + end else + (aux ~add_cclib:false ~cma flag) @ acc) + flags [] + +let quote_if_needed s = + try + ignore (Str.search_forward blanks_RE s 0); + "\"" ^ s ^ "\"" + with Not_found -> s + +let main () = + let static_libs, args = parse_cmdline () in + printf "C libraries to be linked-in: %s\n" (String.concat " " static_libs); + flush stdout; + let verbose_cmd = + sprintf "OCAMLFIND_COMMANDS='ocamlopt=%s' %s -verbose 2>&1" dummy_opt_cmd + (String.concat " " (List.map quote_if_needed args)) + in + let orig_opt_flags = extract_opt_flags verbose_cmd in + message ("original ocamlopt flags: " ^ String.concat " " orig_opt_flags); + let opt_flags = staticize static_libs orig_opt_flags in + message ("new ocamlopt flags: " ^ String.concat " " opt_flags); + let flags = noautolink :: opt_flags in + let cmd = String.concat " " (opt_cmd :: flags) in + message ("executing command: " ^ cmd); + exit (Sys.command cmd) + +let _ = main () +