diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-10 18:29:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:45 +0200 |
| commit | 973b6c69f0861c113f7bd5b94604d2497520a334 (patch) | |
| tree | 9c56073db17f918ff826900252377c56d2c7592e | |
| parent | c2249c3b4c3387a3c8510e68fc447274d7299695 (diff) | |
Adding a target check-beautify for testing reparsability of
beautification of the standard library.
Currently not intrusive but needs two extra phases of compilation.
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | Makefile.build | 34 |
2 files changed, 35 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index b50bca3cf..2e5c74c3d 100644 --- a/.gitignore +++ b/.gitignore @@ -38,6 +38,8 @@ *.v.html *.stamp *.native +*.beautified +*.backup revision TAGS .DS_Store diff --git a/Makefile.build b/Makefile.build index 6a25eda75..fb6bfa87f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -498,6 +498,25 @@ test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) all $(MAKE) $(MAKE_TSOPTS) report +BEAUTIFIED=$(THEORIESVO) +TOBEAUTIFY=$(BEAUTIFIED:.vo=.v.beautified) + +check-beautify: $(TOBEAUTIFY) + @echo Upgrading with beautified files + $(HIDE)for i in $(TOBEAUTIFY);\ + do j=`dirname $$i`/`basename $$i .v.beautified`.v;\ + mv -f $$j $$j.backup;\ + if [ $$i -nt $$j ]; then mv -f $$i $$j; fi;\ + rm -f "$$j"o;\ + done + @echo Recompiling beautified files + $(HIDE)$(MAKE) $(BEAUTIFIED) + @echo Restoring initial files + $(HIDE)for i in $(TOBEAUTIFY);\ + do j=`dirname $$i`/`basename $$i .v.beautified`.v;\ + mv -f $$j.backup $$j;\ + done; + ################################################################## # partial targets: 1) core ML parts ################################################################## @@ -1110,11 +1129,24 @@ theories/Init/%.v.beautified: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/ $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQC) $< -beautify -noinit -R theories Coq -%.v.beautified: %.v | %.v.d +%.v.beautified: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d $(SHOW)'COQC -beautify $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $< -beautify +theories/Init/%.v.backup: theories/Init/%.v.beautified $(VO_TOOLS_DEP) | theories/Init/%.v.d + $(SHOW)'COQC -noinit $<' + mv -f theories/Init/$*.v theories/Init/$*.v.backup + mv -f theories/Init/$*.v.beautified theories/Init/$*.v + rm -f theories/Init/$*.vo + $(BOOTCOQC) theories/Init/$* -noinit -R theories Coq + +%.v.backup: %.v.beautified theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d + $(SHOW)'COQC $<.v.beautified' + $(HIDE)mv -f $*.v $*.v.backup + $(HIDE)mv -f $*.v.beautified $*.v + $(HIDE)$(BOOTCOQC) $* + ########################################################################### # this sets up developper supporting stuff ########################################################################### |