diff options
| author | letouzey | 2013-04-15 16:05:25 +0000 |
|---|---|---|
| committer | letouzey | 2013-04-15 16:05:25 +0000 |
| commit | 4bd2e928e3b8d463bb793ad814ff42abdabf9611 (patch) | |
| tree | 37d79b53c7713599b5fe9d83786c7b9b8ddaf9b3 | |
| parent | 589c0c07eb3f9554f6d0949c07f475be53b1bb2b (diff) | |
Checker : a md5-based way to ensure checker/values.ml is always in sync
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16404 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 8 | ||||
| -rw-r--r-- | checker/values.ml | 11 |
2 files changed, 15 insertions, 4 deletions
diff --git a/Makefile.build b/Makefile.build index 0601abef26..6c24357026 100644 --- a/Makefile.build +++ b/Makefile.build @@ -368,12 +368,16 @@ install-ide-info: # tests ########################################################################### -.PHONY: validate check test-suite $(ALLSTDLIB).v +.PHONY: validate check test-suite $(ALLSTDLIB).v md5chk +md5chk: + $(SHOW)'MD5SUM cic.mli' + $(HIDE)if grep -q `md5sum checker/cic.mli` checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml"; false; fi VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -validate:: $(CHICKEN) $(ALLVO) +validate: $(CHICKEN) md5chk | $(ALLVO) $(SHOW)'COQCHK <theories & plugins>' $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) diff --git a/checker/values.ml b/checker/values.ml index 227f18ca25..5b33439916 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -8,7 +8,14 @@ (** Abstract representations of values in a vo *) -(** NB: UPDATE THIS FILE EACH TIME cic.mli IS MODIFIED ! *) +(** NB: UPDATE THIS FILE EACH TIME cic.mli IS MODIFIED ! + +To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli +with a copy we maintain here: + +MD5 9a9abd32a97761c8de8902f314cb0649 checker/cic.mli + +*) (** We reify here the types of values present in a vo (see cic.mli), in order to validate its structure. Maybe this reification @@ -274,7 +281,7 @@ let v_libobj = Tuple ("libobj", [|v_id;v_obj|]) let v_libobjs = List v_libobj let v_libraryobjs = Tuple ("library_objects",[|v_mp;v_libobjs;v_libobjs|]) -(** Main structures of a vo *) +(** Toplevel structures in a vo (see Cic.mli) *) let v_lib = Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|]) |