added coqchk to the main Makefile and a make variable VALIDATE to check the vo files of the theories

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10962 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 81 insertions, 11 deletions

diff --git a/Makefile.build b/Makefile.build
index fb78e0cc2e..92d7160002 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -109,6 +109,9 @@ VO_TOOLS_DEP := $(BESTCOQTOP)
 ifdef COQ_XML
  VO_TOOLS_DEP += $(COQDOC)
 endif
+ifdef VALIDATE
+ VO_TOOLS_DEP += $(BESTCHICKEN)
+endif
 ifdef NO_RECOMPILE_LIB
  VO_TOOLS_ORDER_ONLY:=$(VO_TOOLS_DEP)
 else
@@ -175,6 +178,21 @@ $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
 $(COQTOP): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
 	cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
 
+LOCALCHKLIBS:=-I checker -I lib -I config -I kernel
+CHKLIBS:=$(LOCALCHKLIBS) -I +camlp4
+
+$(CHICKENOPT): checker/check.cmxa checker/main.ml
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(CHKLIBS) -o $@ unix.cmxa gramlib.cmxa checker/check.cmxa checker/main.ml
+	$(STRIP) $@
+
+$(CHICKENBYTE): checker/check.cma checker/main.ml
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(OCAMLC) $(CHKLIBS) -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
+
+$(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
+	cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
+
 # coqmktop 
 
 $(COQMKTOPBYTE): $(COQMKTOPCMO)
@@ -243,6 +261,14 @@ kernel/kernel.cmxa: $(KERNEL:.cmo=.cmx)
 	$(SHOW)'OCAMLOPT -a -o $@'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(KERNEL:.cmo=.cmx)
 
+checker/check.cma: $(MCHECKER)
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(CHKLIBS) -a -o $@ $(MCHECKER)
+
+checker/check.cmxa: $(MCHECKER:.cmo=.cmx)
+	$(SHOW)'OCAMLOPT -a -o $@'
+	$(HIDE)$(OCAMLOPT) $(CHKLIBS) -a -o $@ $(MCHECKER:.cmo=.cmx)
+
 library/library.cma: $(LIBRARY)
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBRARY)
@@ -771,6 +797,18 @@ endif
 # Default rules
 ###########################################################################
 
+checker/%.cmo: checker/%.ml | checker/%.ml.d
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) -c -I checker -I config -I lib -I kernel -I +camlp4 $<
+
+checker/%.cmx: checker/%.ml | checker/%.ml.d
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) -c -I checker -I config -I lib -I kernel -I +camlp4 $<
+
+checker/%.cmi: checker/%.mli | checker/%.mli.d
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) -c -I checker -I lib -I kernel $<
+
 %.o: %.c
 	$(SHOW)'CC        $<'
 	$(HIDE)$(CC) -o $@ $(CFLAGS) $(CINCLUDES)  -c $<
@@ -823,6 +861,11 @@ endif
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob 
 	$(HIDE)$(BOOTCOQTOP) -dump-glob $*.glob -compile $*
+ifdef VALIDATE
+	$(SHOW)'COQCHK    $(shell basename $*)'
+	$(HIDE)$(BESTCHICKEN) -silent -norec $(shell basename $*) \
+	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
+endif
 
 ###########################################################################
 # Dependencies
@@ -858,6 +901,14 @@ endif
 	$(SHOW)'OCAMLDEP  $<'
 	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@"
 
+checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC)
+	$(SHOW)'OCAMLDEP  $<'
+	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) $< > "$@"
+
+checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
+	$(SHOW)'OCAMLDEP  $<'
+	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) $< > "$@"
+
 ## Veerry nasty hack to keep ocamldep happy
 %.ml: | %.ml4
 	$(SHOW)'TOUCH     $@'
diff --git a/Makefile.common b/Makefile.common
index 354a147240..d821373097 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -24,15 +24,21 @@ COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPOPT:=bin/coqtop.opt$(EXE)
 BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE)
 COQTOP:=bin/coqtop$(EXE)
+CHICKENBYTE:=bin/coqchk.byte$(EXE)
+CHICKENOPT:=bin/coqchk.opt$(EXE)
+BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
+CHICKEN:=bin/coqchk$(EXE)
 
 COQIDEBYTE:=bin/coqide.byte$(EXE)
 COQIDEOPT:=bin/coqide.opt$(EXE)
 COQIDE:=bin/coqide$(EXE)
 
 ifeq ($(BEST),opt)
-COQBINARIES:= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(COQTOP)
+COQBINARIES:= $(COQMKTOP) $(COQC) \
+  $(COQTOPBYTE) $(COQTOPOPT) $(COQTOP) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN)
 else
-COQBINARIES:= $(COQMKTOP) $(COQC) $(COQTOPBYTE)              $(COQTOP)
+COQBINARIES:= $(COQMKTOP) $(COQC) \
+  $(COQTOPBYTE)              $(COQTOP) $(CHICKENBYTE)               $(CHICKEN)
 endif
 OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
 
@@ -393,6 +399,27 @@ COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
 	tools/coqdoc/index.cmo tools/coqdoc/output.cmo \
 	tools/coqdoc/pretty.cmo tools/coqdoc/main.cmo
 
+
+# checker
+
+MCHECKER:=\
+  config/coq_config.cmo \
+  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo \
+  lib/util.cmo lib/option.cmo lib/hashcons.cmo \
+  lib/system.cmo lib/flags.cmo \
+  lib/predicate.cmo lib/rtree.cmo \
+  kernel/names.cmo kernel/univ.cmo \
+  kernel/esubst.cmo checker/term.cmo \
+  checker/declarations.cmo checker/environ.cmo \
+  checker/closure.cmo checker/reduction.cmo \
+  checker/type_errors.cmo \
+  checker/modops.cmo \
+  checker/inductive.cmo checker/typeops.cmo \
+  checker/indtypes.cmo checker/subtyping.cmo checker/mod_checking.cmo \
+  checker/validate.cmo \
+  checker/safe_typing.cmo checker/check.cmo \
+  checker/check_stat.cmo checker/checker.cmo
+
 # minicoq
 
 MINICOQCMO:=$(CONFIG) $(LIBREP) $(KERNEL) \
diff --git a/checker/checker.ml b/checker/checker.ml
index 0ae94444da..1c7ace12f0 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -102,19 +102,11 @@ let set_default_rec_include d =
   check_coq_overwriting p; 
   push_rec_include (d, p)
 
-let safe_getenv_def var def =
-  try 
-    Sys.getenv var
-  with Not_found ->
-    warning ("Environment variable "^var^" not found: using '"^def^"' .");
-    flush_all();
-    def
-
 (* Initializes the LoadPath according to COQLIB and Coq_config *)
 let init_load_path () =
   let coqlib =
     (* variable COQLIB overrides the default library *)
-    safe_getenv_def "COQLIB"
+    getenv_else "COQLIB"
       (if Coq_config.local || !Flags.boot then Coq_config.coqtop
 	else Coq_config.coqlib) in
   let user_contrib = coqlib/"user-contrib" in