Add Whyconfig and the target local_config which create a configuration for the build directory

.gitignore

 *.o
 *.svn
 .*.swp
+.why.conf
 
 # /
 /config.status

Makefile.in

@@ -311,6 +311,60 @@ clean::
 install::
 	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/why3ml
 
+
+########
+# Config
+########
+
+CONFIG_FILES = whyconfig
+
+CONFIGMODULES = $(addprefix src/config/, $(CONFIG_FILES))
+
+CONFIGML  = $(addsuffix .ml,  $(CONFIGMODULES))
+CONFIGMLI = $(addsuffix .mli, $(CONFIGMODULES))
+CONFIGCMO = $(addsuffix .cmo, $(CONFIGMODULES))
+CONFIGCMX = $(addsuffix .cmx, $(CONFIGMODULES))
+
+$(CONFIGCMO) $(CONFIGCMX): INCLUDES += -I src/programs
+
+# build targets
+
+byte: bin/whyconfig.byte
+opt:  bin/whyconfig.opt
+
+bin/whyconfig.opt: src/why.cmxa $(CONFIGCMX)
+	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
+	$(STRIP) $@
+
+bin/whyconfig.byte: src/why.cma $(CONFIGCMO)
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
+
+# depend and clean targets
+
+include .depend.config
+
+.depend.config: $(CONFIGGENERATED)
+	$(OCAMLDEP) -slash -I src -I src/config $(CONFIGML) $(CONFIGMLI) > $@
+
+depend: .depend.config
+
+clean::
+	rm -f src/config/*.cm[iox] src/config/*.o
+	rm -f src/config/*.annot src/config/*~
+	rm -f src/config/*.output src/config/*.automaton
+	rm -f bin/whyconfig.byte bin/whyconfig.opt
+	rm -f .why.conf
+	rm -f .depend.config
+
+local_config: bin/whyconfig.@OCAMLBEST@
+	WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/whyconfig.@OCAMLBEST@ --autodetect-provers --conf_file .why.conf
+
+install::
+	cp -f bin/whyconfig.@OCAMLBEST@ $(BINDIR)/why3config
+
+
 ###############
 # IDE
 ###############

src/config/whyconfig.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Format
+open Why
+open Util
+open Whyconf
+
+let usage_msg =
+  sprintf "Usage: [WHY3LIB=... WHY3DATA=... %s [options]@.\t\
+$WHY3LIB and $WHYDATA are used only when a configuration file is created"
+    (Filename.basename Sys.argv.(0))
+
+(* let libdir = ref None *)
+(* let datadir = ref None *)
+let conf_file = ref None
+let auto = ref false
+
+let set_oref r = (fun s -> r := Some s)
+
+let option_list = Arg.align [
+  (* "--libdir", Arg.String (set_oref libdir), *)
+  (* "<dir> set the lib directory ($WHY3LIB)"; *)
+  (* "--datadir", Arg.String (set_oref datadir), *)
+  (* "<dir> set the data directory ($WHY3DATA)"; *)
+  "--conf_file", Arg.String (set_oref conf_file),
+  "<file> use this configuration file, create it if it doesn't exist
+($WHY_CONFIG), otherwise use the default one";
+  "--autodetect-provers", Arg.Set auto,
+  " autodetect the provers in the $PATH"]
+
+let anon_file _ = Arg.usage option_list usage_msg; exit 1
+
+let () =
+  Arg.parse option_list anon_file usage_msg;
+  let config =
+    try read_config !conf_file
+    with Not_found ->
+      let conf_file = match !conf_file with
+        | None -> Sys.getenv "WHY_CONFIG"
+        | Some f -> f in
+      default_config conf_file in
+  let main = get_main config in
+  (* let main = option_apply main (fun d -> {main with libdir = d})
+     !libdir in *)
+  (* let main = option_apply main (fun d -> {main with datadir = d})
+     !datadir in *)
+  let config = set_main config main in
+  let config =
+    if !auto
+    then Autodetection.run_auto_detection config
+    else config in
+  save_config config

src/driver/whyconf.ml

@@ -149,6 +149,9 @@ let get_config (filename,rc) =
     provers   = provers;
   }
 
+let default_config conf_file = get_config (conf_file,Rc.empty)
+
+
 let read_config conf_file =
   let filenamerc = try read_config_rc conf_file
     with Exit ->
@@ -173,6 +176,8 @@ let set_provers config provers =
     provers = provers;
   }
 
+let set_conf_file config conf_file = {config with conf_file = conf_file}
+
 let get_section config name = assert (name <> "main");
   get_section config.config name
 

src/driver/whyconf.mli

@@ -50,8 +50,8 @@ type config
     "./why.conf"; "./.why.conf"; "$HOME/.why.conf";
     "$USERPROFILE/.why.conf"; the built-in default_config *)
 val read_config : string option -> config
-
 val save_config : config -> unit
+val default_config : string -> config
 
 val get_main    : config  -> main
 val get_provers : config  -> config_prover Mstr.t
@@ -59,6 +59,8 @@ val get_provers : config  -> config_prover Mstr.t
 val set_main    : config -> main                 -> config
 val set_provers : config -> config_prover Mstr.t -> config
 
+val set_conf_file : config -> string -> config
+
 val get_section : config -> string -> Rc.section option
 val get_family  : config -> string -> Rc.family