matita/make.ml

   1
   2 module type Format = sig
   3
   4         type source_object
   5         type target_object
   6
   7         val target_of : source_object -> target_object
   8         val string_of_source_object : source_object -> string
   9         val string_of_target_object : target_object -> string
  10
  11         val build : source_object -> bool
  12
  13         val mtime_of_source_object : source_object -> float option
  14         val mtime_of_target_object : target_object -> float option
  15 end
  16
  17 module Make = functor (F:Format) -> struct
  18
  19   let prerr_endline _ = ();;
  20
  21   let younger_s_t a b =
  22     match F.mtime_of_source_object a, F.mtime_of_target_object b with
  23     | Some a, Some b -> a < b
  24     | _ -> false (* XXX check if correct *)
  25   ;;
  26   let younger_t_t a b =
  27     match F.mtime_of_target_object a, F.mtime_of_target_object b with
  28     | Some a, Some b -> a < b
  29     | _ -> false (* XXX check if correct *)
  30   ;;
  31
  32   let is_built t = younger_s_t t (F.target_of t);;
  33
  34   let rec needs_build deps compiled (t,dependencies) =
  35     prerr_endline ("Checking if "^F.string_of_source_object t^" needs to be built");
  36     if List.mem t compiled then
  37       (prerr_endline "already compiled";
  38       false)
  39     else
  40     if not (is_built t) then
  41       (prerr_endline (F.string_of_source_object t^
  42        " is not built, thus needs to be built");
  43       true)
  44     else
  45     try
  46       let unsat =
  47         List.find
  48           (needs_build deps compiled)
  49           (List.map (fun x -> x, List.assoc x deps) dependencies)
  50       in
  51         prerr_endline
  52          (F.string_of_source_object t^" depends on "^F.string_of_source_object (fst unsat)^
  53          " that needs to be built, thus needs to be built");
  54         true
  55     with Not_found ->
  56       try
  57         let unsat =
  58           List.find (younger_t_t (F.target_of t)) (List.map F.target_of dependencies)
  59         in
  60           prerr_endline
  61            (F.string_of_source_object t^" depends on "^F.string_of_target_object
  62            unsat^" and "^F.string_of_source_object t^".o is younger than "^
  63            F.string_of_target_object unsat^", thus needs to be built");
  64           true
  65       with Not_found -> false
  66   ;;
  67
  68   let is_buildable compiled deps (t,dependencies) =
  69     prerr_endline ("Checking if "^F.string_of_source_object t^" is buildable");
  70     let b = needs_build deps compiled (t,dependencies) in
  71     if not b then
  72       (prerr_endline (F.string_of_source_object t^
  73        " does not need to be built, thus it not buildable");
  74       false)
  75     else
  76     try
  77       let unsat =
  78         List.find (needs_build deps compiled)
  79           (List.map (fun x -> x, List.assoc x deps) dependencies)
  80       in
  81         prerr_endline
  82           (F.string_of_source_object t^" depends on "^
  83           F.string_of_source_object (fst unsat)^
  84           " that needs build, thus is not buildable");
  85         false
  86     with Not_found ->
  87       prerr_endline
  88         ("None of "^F.string_of_source_object t^
  89         " dependencies needs to be built, thus it is buildable");
  90       true
  91   ;;
  92
  93   let rec make compiled failed deps =
  94     let todo = List.filter (is_buildable compiled deps) deps in
  95     let todo = List.filter (fun (f,_) -> not (List.mem f failed)) todo in
  96     if todo <> [] then
  97       let compiled, failed =
  98         List.fold_left
  99           (fun (c,f) (file,_) ->
 100             if F.build file then (file::c,f)
 101             else (c,file::f))
 102           (compiled,failed) todo
 103       in
 104        make compiled failed deps
 105   ;;
 106
 107   let rec purge_unwanted_roots wanted deps =
 108     let roots, rest =
 109        List.partition
 110          (fun (t,d) ->
 111            not (List.exists (fun (_,d1) -> List.mem t d1) deps))
 112          deps
 113     in
 114     let newroots = List.filter (fun (t,_) -> List.mem t wanted) roots in
 115     if newroots = roots then
 116       deps
 117     else
 118       purge_unwanted_roots wanted (newroots @ rest)
 119   ;;
 120
 121   let make deps targets =
 122     if targets = [] then
 123       make [] [] deps
 124     else
 125       make [] [] (purge_unwanted_roots targets deps)
 126   ;;
 127
 128 end
 129
 130 let load_deps_file f =
 131   let deps = ref [] in
 132   let ic = open_in f in
 133   try
 134     while true do
 135       begin
 136         let l = input_line ic in
 137         match Str.split (Str.regexp " ") l with
 138         | [] -> HLog.error "malformed deps file"; exit 1
 139         | he::tl -> deps := (he,tl) :: !deps
 140       end
 141     done; !deps
 142     with End_of_file -> !deps
 143 ;;