From: Enrico Tassi Date: Thu, 3 Jan 2008 10:13:04 +0000 (+0000) Subject: implementation of the make algorithm, still unfinished. X-Git-Tag: make_still_working~5693 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc61d11ba810d23ff947c14e3a39d6e3879d673e;p=helm.git implementation of the make algorithm, still unfinished. to be integrated with matitac to drop our beloved developments. --- diff --git a/helm/software/make/main.ml b/helm/software/make/main.ml new file mode 100644 index 000000000..df20a35f2 --- /dev/null +++ b/helm/software/make/main.ml @@ -0,0 +1,34 @@ + +module F = struct + type source_object = string + type target_object = string + let string_of_source_object s = s + let string_of_target_object s = s + let target_of s = s ^ ".o" + let build t = + print_string ("build "^t^"\n"); flush stdout; + ignore(Unix.system ("touch "^target_of t)) + ;; + let mtime_of_source_object s = + try Some (Unix.stat s).Unix.st_mtime + with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> + prerr_endline ("Source file not found: "^s);assert false + ;; + let mtime_of_target_object t = + try Some (Unix.stat t).Unix.st_mtime + with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = t -> None + ;; +end + +module M = Make.Make(F) + +let deps = [ + "a.c", [ "b.c"; "d.c" ]; + "b.c", [ "c.c"; "d.c" ]; + "c.c", []; + "d.c", ["e.c"]; + "e.c", []; + ] +;; + +M.make deps;; diff --git a/helm/software/make/make.ml b/helm/software/make/make.ml new file mode 100644 index 000000000..c243d7935 --- /dev/null +++ b/helm/software/make/make.ml @@ -0,0 +1,103 @@ + +module type Format = sig + + type source_object + type target_object + + val target_of : source_object -> target_object + val string_of_source_object : source_object -> string + val string_of_target_object : target_object -> string + + val build : source_object -> unit + + val mtime_of_source_object : source_object -> float option + val mtime_of_target_object : target_object -> float option +end + +module Make = functor (F:Format) -> struct + + let prerr_endline _ = ();; + + let younger_s_t a b = + match F.mtime_of_source_object a, F.mtime_of_target_object b with + | Some a, Some b -> a < b + | _ -> false (* XXX check if correct *) + ;; + let younger_t_t a b = + match F.mtime_of_target_object a, F.mtime_of_target_object b with + | Some a, Some b -> a < b + | _ -> false (* XXX check if correct *) + ;; + + let is_built t = younger_s_t t (F.target_of t);; + + let rec needs_build deps compiled (t,dependencies) = + prerr_endline ("Checking if "^F.string_of_source_object t^" needs to be built"); + if List.mem t compiled then + (prerr_endline "already compiled"; + false) + else + if not (is_built t) then + (prerr_endline (F.string_of_source_object t^ + " is not built, thus needs to be built"); + true) + else + try + let unsat = + List.find + (needs_build deps compiled) + (List.map (fun x -> x, List.assoc x deps) dependencies) + in + prerr_endline + (F.string_of_source_object t^" depends on "^F.string_of_source_object (fst unsat)^ + " that needs to be built, thus needs to be built"); + true + with Not_found -> + try + let unsat = + List.find (younger_t_t (F.target_of t)) (List.map F.target_of dependencies) + in + prerr_endline + (F.string_of_source_object t^" depends on "^F.string_of_target_object + unsat^" and "^F.string_of_source_object t^".o is younger than "^ + F.string_of_target_object unsat^", thus needs to be built"); + true + with Not_found -> false + ;; + + let is_buildable compiled deps (t,dependencies) = + prerr_endline ("Checking if "^F.string_of_source_object t^" is buildable"); + let b = needs_build deps compiled (t,dependencies) in + if not b then + (prerr_endline (F.string_of_source_object t^ + " does not need to be built, thus it not buildable"); + false) + else + try + let unsat = + List.find (needs_build deps compiled) + (List.map (fun x -> x, List.assoc x deps) dependencies) + in + prerr_endline + (F.string_of_source_object t^" depends on "^ + F.string_of_source_object (fst unsat)^ + " that needs build, thus is not buildable"); + false + with Not_found -> + prerr_endline + ("None of "^F.string_of_source_object t^ + " dependencies needs to be built, thus it is buildable"); + true + ;; + + let rec make compiled deps = + let todo = List.filter (is_buildable compiled deps) deps in + if todo <> [] then + (List.iter F.build (List.map fst todo); + make (compiled@List.map fst todo) deps) + ;; + + let make deps = make [] deps + +end + diff --git a/helm/software/make/make.mli b/helm/software/make/make.mli new file mode 100644 index 000000000..8830a8319 --- /dev/null +++ b/helm/software/make/make.mli @@ -0,0 +1,18 @@ + +module type Format = + sig + type source_object + type target_object + val target_of : source_object -> target_object + val string_of_source_object : source_object -> string + val string_of_target_object : target_object -> string + val build : source_object -> unit + val mtime_of_source_object : source_object -> float option + val mtime_of_target_object : target_object -> float option + end + +module Make : + functor (F : Format) -> + sig + val make : (F.source_object * F.source_object list) list -> unit + end diff --git a/helm/software/make/test/a.c b/helm/software/make/test/a.c new file mode 100644 index 000000000..e69de29bb diff --git a/helm/software/make/test/b.c b/helm/software/make/test/b.c new file mode 100644 index 000000000..e69de29bb diff --git a/helm/software/make/test/c.c b/helm/software/make/test/c.c new file mode 100644 index 000000000..e69de29bb diff --git a/helm/software/make/test/d.c b/helm/software/make/test/d.c new file mode 100644 index 000000000..e69de29bb diff --git a/helm/software/make/test/e.c b/helm/software/make/test/e.c new file mode 100644 index 000000000..e69de29bb