diff options
| author | letouzey | 2012-08-23 12:52:51 +0000 |
|---|---|---|
| committer | letouzey | 2012-08-23 12:52:51 +0000 |
| commit | 12def92b4cecdbe2fc8242bc451f4ee0d86c0eb8 (patch) | |
| tree | 643aeaeee3c72ca4e3ae84440c9ac950fbdfdeb8 /Makefile.build | |
| parent | 492ad5ad0b4c55610c9896436d2165ac22b527a6 (diff) | |
No more states/initial.coq, instead coqtop now requires Prelude.vo
For starting a bare coqtop, the recommended option is now "-noinit"
that skips the load of Prelude.vo. Option "-nois" is kept for
compatibility, it is now an alias to "-noinit".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 18 |
1 files changed, 5 insertions, 13 deletions
diff --git a/Makefile.build b/Makefile.build index d11dcc7650..37bedcf3e7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -212,7 +212,7 @@ coqlib:: theories plugins coqlight: theories-light tools coqbinaries -states:: states/initial.coq +states: theories/Init/Prelude.vo ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) @@ -471,17 +471,13 @@ btauto: $(BTAUTOVO) $(BTAUTOCMA) pluginsopt: $(PLUGINSOPT) ########################################################################### -# rules to make theories, plugins and states +# rules to make theories and plugins ########################################################################### -states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/MakeInitial.v.d $(VO_TOOLS_ORDER_ONLY) - $(SHOW)'BUILD $@' - $(HIDE)$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq - theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) - $(SHOW)'COQC -nois $<' + $(SHOW)'COQC -noinit $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) theories/Init/$* -nois + $(HIDE)$(BOOTCOQC) theories/Init/$* -noinit theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml $(OCAML) $< $(TOTARGET) @@ -629,8 +625,6 @@ endif install-library: $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) - $(MKDIR) $(FULLCOQLIB)/states - $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLCOQLIB)/user-contrib $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) ifeq ($(BEST),opt) @@ -647,8 +641,6 @@ endif install-library-light: $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) - $(MKDIR) $(FULLCOQLIB)/states - $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states rm -f $(FULLCOQLIB)/revision -$(INSTALLLIB) revision $(FULLCOQLIB) ifeq ($(BEST),opt) @@ -905,7 +897,7 @@ plugins/%_mod.ml: plugins/%.mllib $(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \ else echo $< : Dependency $${DEPS} not ready yet; false; fi -%.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) +%.vo %.glob: %.v states $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $* |