helm/software/matita/matitamake.ml

   1 (* Copyright (C) 2005, 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 (* $Id$ *)
  27
  28 module MK = MatitamakeLib ;;
  29
  30 let main () =
  31   MatitaInit.fill_registry ();
  32   MatitaInit.parse_cmdline ();
  33   MatitaInit.load_configuration_file ();
  34   MK.initialize ();
  35   let usage = ref (fun () -> ()) in
  36   let dev_of_name name =
  37     match MK.development_for_name name with
  38     | None ->
  39         prerr_endline ("Unable to find a development called " ^ name);
  40         exit 1
  41     | Some d -> d
  42   in
  43   let dev_for_dir dir =
  44     match MK.development_for_dir dir with
  45     | None ->
  46         prerr_endline ("Unable to find a development holding directory: "^ dir);
  47         exit 1
  48     | Some d -> d
  49   in
  50   let init_dev args =
  51     let name, path =
  52       match args with
  53       | [ name; path ] when path.[0] = '/' -> name, path
  54       | [ name; path ] -> name, Unix.getcwd () ^ "/" ^ path
  55       | [ name ] -> name, Unix.getcwd ()
  56       | _ -> !usage (); (* should not be reached *) assert false
  57     in
  58     match MK.initialize_development name path with
  59     | None -> exit 2
  60     | Some _ -> exit 0
  61   in
  62   let list_dev args =
  63     if List.length args <> 0 then !usage ();
  64     match MK.list_known_developments () with
  65     | [] -> print_string "No developments found.\n"; exit 0
  66     | l ->
  67         List.iter
  68           (fun (name, root) ->
  69             print_string (Printf.sprintf "%-10s\trooted in %s\n" name root))
  70           l;
  71         exit 0
  72   in
  73   let destroy_dev args =
  74     if List.length args <> 1 then !usage ();
  75     let name = (List.hd args) in
  76     let dev = dev_of_name name in
  77     MK.destroy_development dev;
  78     exit 0
  79   in
  80   let clean_dev args =
  81     let dev =
  82       match args with
  83       | [] -> dev_for_dir (Unix.getcwd ())
  84       | [name] -> dev_of_name name
  85       | _ -> !usage (); exit 1
  86     in
  87     match MK.clean_development dev with
  88     | true -> exit 0
  89     | false -> exit 1
  90   in
  91   let build_dev args =
  92     if List.length args <> 1 then !usage ();
  93     let name = (List.hd args) in
  94     let dev = dev_of_name name in
  95     match MK.build_development dev with
  96     | true -> exit 0
  97     | false -> exit 1
  98   in
  99   let publish_dev args =
 100     if List.length args <> 1 then !usage ();
 101     let name = (List.hd args) in
 102     let dev = dev_of_name name in
 103     match MK.publish_development dev with
 104     | true -> exit 0
 105     | false -> exit 1
 106   in
 107   let target args =
 108     if List.length args < 1 then !usage ();
 109     let dev = dev_for_dir (Unix.getcwd ()) in
 110     List.iter
 111       (fun t ->
 112         ignore(MK.build_development ~target:t dev))
 113       args
 114   in
 115   let params = [
 116     "init", init_dev;
 117     "clean", clean_dev;
 118     "list", list_dev;
 119     "destroy", destroy_dev;
 120     "build", build_dev;
 121     "publish", publish_dev;
 122   ]
 123   in
 124   usage := MatitaInit.die_usage;
 125   let parse args =
 126     match args with
 127     | [] -> target [ "all" ]
 128     | s :: tl ->
 129         let f, args =
 130           try
 131             (List.assoc s params), tl
 132           with Not_found ->
 133             if s.[0] = '-' then (!usage ();assert false) else target, args
 134         in
 135         f args
 136   in
 137   parse (Helm_registry.get_list Helm_registry.string "matita.args")