diff options
147 files changed, 2220 insertions, 2263 deletions
diff --git a/.gitignore b/.gitignore index bc1a05684..0193c9dfa 100644 --- a/.gitignore +++ b/.gitignore @@ -44,7 +44,6 @@ TAGS .pc bin/ _build -plugins/*/*_mod.ml myocamlbuild_config.ml config/Makefile config/coq_config.ml @@ -114,7 +113,7 @@ tools/ocamllibdep.ml tools/coqdoc/cpretty.ml ide/xml_lexer.ml -# .ml4 files +# .ml4 / .mlp files g_*.ml @@ -36,8 +36,12 @@ Changes from V8.5pl1 to V8.5pl2 Bugfixes -- #4677: fix alpha-conversion in notations needing eta-expansion +- #4677: fix alpha-conversion in notations needing eta-expansion. - Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode. +- #4644: a regression in unification. +- #4777: printing inefficiency with implicit arguments +- #4752: CoqIDE crash on files not ended by ".v". +- #4398: type_scope used consistently in "match goal". Changes from V8.5 to V8.5pl1 ============================ @@ -66,7 +66,7 @@ endef ## Files in the source tree LEXFILES := $(call find, '*.mll') -export MLLIBFILES := $(call find, '*.mllib') +export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack') export ML4FILES := $(call find, '*.ml4') export CFILES := $(call find, '*.c') @@ -80,9 +80,7 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENML4FILES:= $(ML4FILES:.ml4=.ml) -GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(GENPLUGINSMOD) \ - tools/tolink.ml kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) @@ -153,7 +151,7 @@ noconfig: # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles -Makefile Makefile.build Makefile.common config/Makefile : ; +Makefile $(wildcard Makefile.*) config/Makefile : ; ########################################################################### # Cleaning @@ -173,7 +171,7 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(FAKEIDE) + rm -f $(COQTOPBYTE) $(CHICKENBYTE) find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete rm -f */*.pp[iox] plugins/*/*.pp[iox] rm -rf $(SOURCEDOCDIR) @@ -206,8 +204,8 @@ archclean: clean-ide optclean voclean rm -f $(ALLSTDLIB).* optclean: - rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT) - rm -f $(TOOLS) $(CSDPCERT) + rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN) + rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f clean-ide: @@ -236,6 +234,7 @@ distclean: clean cleanconfig cacheclean voclean: find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -delete + find theories plugins test-suite -name .coq-native -empty -delete devdocclean: find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f diff --git a/Makefile.build b/Makefile.build index fc92507e6..4eafe1d61 100644 --- a/Makefile.build +++ b/Makefile.build @@ -10,30 +10,40 @@ # some variables. ########################################################################### -# Starting rule +# Default starting rule ########################################################################### -# build the different subsystems: coq, coqide -world: revision coq coqide documentation +# build the different subsystems: -.PHONY: world +world: coq coqide documentation revision + +coq: coqlib coqbinaries tools printers + +.PHONY: world coq ########################################################################### # Includes ########################################################################### -include Makefile.common -include Makefile.doc - +# This list of ml files used to be in the main Makefile, we moved it here +# to avoid exhausting the variable env in Win32 MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml) -DEPENDENCIES := \ - $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES)) -# This include below will lauch the build of all concerned .d. +include Makefile.common +include Makefile.doc ## provides the 'documentation' rule +include Makefile.checker +include Makefile.ide ## provides the 'coqide' rule +include Makefile.install +include Makefile.dev ## provides the 'printers' and 'revision' rules + +# This include below will lauch the build of all .d. # The - at front is for disabling warnings about currently missing ones. # For creating the missing .d, make will recursively build things like # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). +DEPENDENCIES := \ + $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES)) + -include $(DEPENDENCIES) # All dependency includes must be declared secondary, otherwise make will @@ -43,7 +53,6 @@ DEPENDENCIES := \ .SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml) - ########################################################################### # Compilation options ########################################################################### @@ -56,7 +65,6 @@ NO_RECALC_DEPS= READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= COQ_XML= # is "-xml" when building XML library -VM= # is "-no-vm" to not use the vm" TIMED= # non-empty will activate a default time command # when compiling .v (see $(STDTIME) below) @@ -75,7 +83,7 @@ TIMECMD= # if you prefer a specific time command instead of $(STDTIME) STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) -COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) +COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands @@ -104,12 +112,32 @@ LINKMETADATA= CODESIGN=true endif +# Best OCaml compiler, used in a generic way + +ifeq ($(BEST),opt) +OPT:=opt +BESTOBJ:=.cmx +BESTLIB:=.cmxa +BESTDYN:=.cmxs +else +OPT:= +BESTOBJ:=.cmo +BESTLIB:=.cma +BESTDYN:=.cma +endif + +define bestobj +$(patsubst %.cma,%$(BESTLIB),$(patsubst %.cmo,%$(BESTOBJ),$(1))) +endef + define bestocaml $(if $(OPT),\ $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@,\ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^) endef +# Camlp4 / Camlp5 settings + CAMLP4DEPS:=tools/compat5.cmo grammar/grammar.cma ifeq ($(CAMLP4),camlp5) CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) @@ -172,13 +200,11 @@ endif TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV}) ########################################################################### -# Compilation option for .c files +# Compilation of .c files ########################################################################### CINCLUDES= -I $(CAMLHLIB) -# libcoqrun.a, dllcoqrun.so - # NB: We used to do a ranlib after ocamlmklib, but it seems that # ocamlmklib is already doing it @@ -186,7 +212,6 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u))) -#coq_jumptbl.h is required only if you have GCC 2.0 or later kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ -e '/^}/q' $< $(TOTARGET) @@ -195,6 +220,17 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' $< | \ awk -f kernel/make-opcodes $(TOTARGET) +%.o: %.c + $(SHOW)'OCAMLC $<' + $(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<) + +%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) + $(SHOW)'CCDEP $<' + $(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@ + +%.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES) + $(SHOW)'CCDEP $<' + $(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET) ########################################################################### # grammar/grammar.cma @@ -207,8 +243,7 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h ## Explicit dependencies for grammar stuff GRAMBASEDEPS := grammar/gramCompat.cmo grammar/q_util.cmi -GRAMCMO := \ - grammar/gramCompat.cmo grammar/q_util.cmo \ +GRAMCMO := grammar/gramCompat.cmo grammar/q_util.cmo \ grammar/argextend.cmo grammar/tacextend.cmo grammar/vernacextend.cmo grammar/q_util.cmi : grammar/gramCompat.cmo @@ -227,10 +262,9 @@ GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \ grammar/grammar.cma : $(GRAMCMO) $(SHOW)'Testing $@' - @touch test.mlp - $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl test.mlp -o test.ml - $(HIDE)$(GRAMC) test.ml -o test-grammar - @rm -f test-grammar test.* + @touch grammar/test.mlp + $(HIDE)$(GRAMC) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test + @rm -f grammar/test.* grammar/test $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ @@ -266,25 +300,16 @@ grammar/%.cmi: grammar/%.mli # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -.PHONY: coqbinaries coq coqlib coqlight states +.PHONY: coqbinaries -coqbinaries: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE} +coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \ + $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE) -coq: coqlib tools coqbinaries - -coqlib: theories plugins - -coqlight: theories-light tools coqbinaries - -states: theories/Init/Prelude.vo - -miniopt: $(COQTOPEXE) pluginsopt -minibyte: $(COQTOPBYTE) pluginsbyte ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ + $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@ $(STRIP) $@ $(CODESIGN) $@ else @@ -294,28 +319,13 @@ endif $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@ - -LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) ) -CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB) + $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ -ifeq ($(BEST),opt) -$(CHICKEN): checker/check.cmxa checker/main.ml - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(SYSCMXA) $^ - $(STRIP) $@ - $(CODESIGN) $@ -else -$(CHICKEN): $(CHICKENBYTE) - cp $< $@ -endif +# coqmktop -$(CHICKENBYTE): checker/check.cma checker/main.ml - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -thread -o $@ $(SYSCMA) $^ +COQMKTOPCMO:=lib/clib.cma lib/errors.cmo tools/tolink.cmo tools/coqmktop.cmo -# coqmktop -$(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ))) +$(COQMKTOP): $(call bestobj, $(COQMKTOPCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) @@ -326,351 +336,19 @@ tools/tolink.ml: Makefile.build Makefile.common $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ # coqc -$(COQC): $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ))) - $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) - -# Target for libraries .cma and .cmxa - -# The dependency over the .mllib is somewhat artificial, since -# ocamlc -a won't use this file, hence the $(filter-out ...) below. -# But this ensures that the .cm(x)a is rebuilt when needed, -# (especially when removing a module in the .mllib). -# We used to have a "order-only" dependency over .mllib.d here, -# but the -include mechanism should already ensure that we have -# up-to-date dependencies. -%.cma: %.mllib - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) - -%.cmxa: %.mllib - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) +COQCCMO:=lib/clib.cma lib/errors.cmo toplevel/usage.cmo tools/coqc.cmo -# For the checker, different flags may be used - -checker/check.cma: checker/check.mllib | md5chk - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) - -checker/check.cmxa: checker/check.mllib | md5chk - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) - -########################################################################### -# Csdp to micromega special targets -########################################################################### - -plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ)) \ - $(addsuffix $(BESTLIB), lib/clib) +$(COQC): $(call bestobj, $(COQCCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,nums unix clib) - -########################################################################### -# CoqIde special targets -########################################################################### - -.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files - -# target to build CoqIde -coqide: coqide-files coqide-binaries theories/Init/Prelude.vo - -COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) - -.SUFFIXES:.vo - -IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map - -coqide-binaries: coqide-$(HASCOQIDE) ide-toploop -coqide-no: -coqide-byte: $(COQIDEBYTE) $(COQIDE) -coqide-opt: $(COQIDEBYTE) $(COQIDE) -coqide-files: $(IDEFILES) -ifeq ($(BEST),opt) -ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs) -else -ide-toploop: $(IDETOPLOOPCMA) -endif - -ifeq ($(HASCOQIDE),opt) -$(COQIDE): $(LINKIDEOPT) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \ - lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^ - $(STRIP) $@ -else -$(COQIDE): $(COQIDEBYTE) - cp $< $@ -endif - -$(COQIDEBYTE): $(LINKIDE) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \ - lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^ - -# install targets - -.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles - -ifeq ($(HASCOQIDE),no) -install-coqide: install-ide-toploop -else -install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles -endif - -install-ide-bin: - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) - -install-ide-toploop: - $(MKDIR) $(FULLCOQLIB)/toploop - $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ -ifeq ($(BEST),opt) - $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ -endif - -install-ide-devfiles: - $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ - $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) -ifeq ($(BEST),opt) - $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) -endif - -install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time - $(MKDIR) $(FULLDATADIR) - $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR) - $(MKDIR) $(FULLCONFIGDIR) - if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi - -install-ide-info: - $(MKDIR) $(FULLDOCDIR) - $(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde - -########################################################################### -# CoqIde MacOS special targets -########################################################################### - -.PHONY: $(COQIDEAPP)/Contents - -$(COQIDEAPP)/Contents: - rm -rdf $@ - $(MKDIR) $@ - sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist - $(MKDIR) "$@/MacOS" - -$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ - unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \ - threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^ - $(STRIP) $@ - -$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents - $(MKDIR) $@/coq/ - $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/ - $(MKDIR) $@/gtksourceview-2.0/{language-specs,styles} - $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/ - $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/ - cp -R "$(GTKSHARE)/"locale $@ - cp -R "$(GTKSHARE)/"icons $@ - cp -R "$(GTKSHARE)/"themes $@ - -$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents - $(MKDIR) $@ - $(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@ - -$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents - $(MKDIR) $@ - $(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@ - - -$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib - $(MKDIR) $@/xdg/coq - $(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys - $(MKDIR) $@/gtk-2.0 - { "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ - sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ - > $@/gtk-2.0/gdk-pixbuf.loaders - { "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\ - sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ - sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ - > $@/gtk-2.0/gtk-immodules.loaders - $(MKDIR) $@/pango - echo "[Pango]" > $@/pango/pangorc - -$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) - $(MKDIR) $@ - $(INSTALLLIB) $(GTKLIBS)/charset.alias $@/ - $(MKDIR) $@/pango/1.8.0/modules - $(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/ - { "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\ - sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \ - > $@/pango/1.8.0/modules.cache - - for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ - do cp $$i $@/; \ - ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \ - done - for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \ - do \ - for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ - do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ - ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \ - done - EXTRAWORK=1; \ - while [ $${EXTRAWORK} -eq 1 ]; \ - do EXTRAWORK=0; \ - for i in $@/*.dylib; \ - do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ - do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ - done; \ - done - ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@ - -$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share - $(INSTALLLIB) ide/MacOS/*.icns $@ - -$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources - $(CODESIGN) $@ - -########################################################################### -# tests -########################################################################### - -.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) - $(SHOW)'COQCHK <theories & plugins>' - $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) - -$(ALLSTDLIB).v: - $(SHOW)'MAKE $(notdir $@)' - $(HIDE)echo "Require $(ALLMODS)." > $@ - -MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE) - -check: validate test-suite - -test-suite: world $(ALLSTDLIB).v - $(MAKE) $(MAKE_TSOPTS) clean - $(MAKE) $(MAKE_TSOPTS) all - $(MAKE) $(MAKE_TSOPTS) report - -################################################################## -# partial targets: 1) core ML parts -################################################################## - -.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine highparsing stm toplevel ltac - -lib: lib/clib.cma lib/lib.cma -kernel: kernel/kernel.cma -byterun: $(BYTERUN) -library: library/library.cma -engine: engine/engine.cma -proofs: proofs/proofs.cma -tactics: tactics/tactics.cma -interp: interp/interp.cma -parsing: parsing/parsing.cma -pretyping: pretyping/pretyping.cma -highparsing: parsing/highparsing.cma -stm: stm/stm.cma -toplevel: toplevel/toplevel.cma -ltac: ltac/ltac.cma - -########################################################################### -# 2) theories and plugins files -########################################################################### - -.PHONY: init theories theories-light -.PHONY: logic arith bool narith zarith qarith lists strings sets -.PHONY: fsets relations wellfounded reals setoids sorting numbers noreal -.PHONY: msets mmaps compat - -init: $(INITVO) - -theories: $(THEORIESVO) -theories-light: $(THEORIESLIGHTVO) - -logic: $(LOGICVO) -arith: $(ARITHVO) -bool: $(BOOLVO) -narith: $(NARITHVO) -zarith: $(ZARITHVO) -qarith: $(QARITHVO) -lists: $(LISTSVO) -strings: $(STRINGSVO) -sets: $(SETSVO) -fsets: $(FSETSVO) -relations: $(RELATIONSVO) -wellfounded: $(WELLFOUNDEDVO) -reals: $(REALSVO) -setoids: $(SETOIDSVO) -sorting: $(SORTINGVO) -numbers: $(NUMBERSVO) -unicode: $(UNICODEVO) -classes: $(CLASSESVO) -program: $(PROGRAMVO) -structures: $(STRUCTURESVO) -vectors: $(VECTORSVO) -msets: $(MSETSVO) -compat: $(COMPATVO) - -noreal: unicode logic arith bool zarith qarith lists sets fsets \ - relations wellfounded setoids sorting - -########################################################################### -# 3) plugins -########################################################################### - -.PHONY: plugins omega micromega setoid_ring nsatz extraction -.PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte - -plugins: $(PLUGINSVO) -omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) -micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) -setoid_ring: $(RINGVO) $(RINGCMA) -nsatz: $(NSATZVO) $(NSATZCMA) -extraction: $(EXTRACTIONCMA) -fourier: $(FOURIERVO) $(FOURIERCMA) -funind: $(FUNINDCMA) $(FUNINDVO) -cc: $(CCVO) $(CCCMA) -rtauto: $(RTAUTOVO) $(RTAUTOCMA) -btauto: $(BTAUTOVO) $(BTAUTOCMA) - -pluginsopt: $(PLUGINSOPT) -pluginsbyte: $(PLUGINS) - -########################################################################### -# rules to make theories and plugins -########################################################################### - -theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) - $(SHOW)'COQC $(COQ_XML) -noinit $<' - $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq - -theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml - $(OCAML) $< $(TOTARGET) + $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) ########################################################################### -# tools +# other tools ########################################################################### -.PHONY: printers tools - -printers: $(DEBUGPRINTERS) - -tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP) +.PHONY: +tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) # coqdep_boot : a basic version of coqdep, with almost no dependencies. @@ -696,355 +374,149 @@ $(OCAMLLIBDEP): tools/ocamllibdep.ml # The full coqdep (unused by this build, but distributed by make install) -$(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ))) +COQDEPCMO:=lib/clib.cma lib/errors.cmo lib/minisys.cmo lib/system.cmo \ + tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo + +$(COQDEP): $(call bestobj, $(COQDEPCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) -$(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina) +$(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -$(COQMAKEFILE): $(patsubst %.cma,%$(BESTLIB),$(COQMAKEFILECMO:.cmo=$(BESTOBJ))) +COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo + +$(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix threads) -$(COQTEX): tools/coq_tex$(BESTOBJ) +$(COQTEX): $(call bestobj, tools/coq_tex.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str) -$(COQWC): tools/coqwc$(BESTOBJ) +$(COQWC): $(call bestobj, tools/coqwc.cmo) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -$(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ))) +COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ + cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) + +$(COQDOC): $(call bestobj, $(COQDOCCMO)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix) -$(COQWORKMGR): $(addsuffix $(BESTOBJ), stm/coqworkmgrApi tools/coqworkmgr) \ - $(addsuffix $(BESTLIB), lib/clib) +$(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,, $(SYSMOD) clib) + $(HIDE)$(call bestocaml,, $(SYSMOD)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -$(FAKEIDE): lib/clib$(BESTLIB) lib/errors$(BESTOBJ) \ - lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) \ - ide/serialize$(BESTOBJ) ide/xml_lexer$(BESTOBJ) \ - ide/xml_parser$(BESTOBJ) ide/xml_printer$(BESTOBJ) \ - ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | \ - $(IDETOPLOOPCMA:.cma=$(BESTDYN)) +FAKEIDECMO:= lib/clib.cma lib/errors.cmo lib/spawn.cmo ide/document.cmo \ + ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \ + ide/xmlprotocol.cmo tools/fake_ide.cmo + +$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,-I ide,str unix threads) # votour: a small vo explorer (based on the checker) -bin/votour: lib/cObj$(BESTOBJ) checker/analyze$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml +bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo) checker/votour.ml $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I checker,) -# Special rule for the compatibility-with-camlp5 extension for camlp4 - -ifeq ($(CAMLP4),camlp4) -tools/compat5.cmo: tools/compat5.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< -tools/compat5b.cmo: tools/compat5b.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< -else -tools/compat5.cmo: tools/compat5.ml - $(OCAMLC) -c $< -endif - ########################################################################### -# Documentation : cf Makefile.doc +# Csdp to micromega special targets ########################################################################### -documentation: doc-$(WITHDOC) -doc-all: doc -doc-no: +CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \ + mutils.cmo micromega.cmo \ + sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) -.PHONY: documentation doc-all doc-no +$(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,nums unix) ########################################################################### -# Installation +# tests ########################################################################### -ifeq ($(LOCAL),true) -install: - @echo "Nothing to install in a local build!" -else -install: install-coq install-coqide install-doc-$(WITHDOC) -endif - -install-doc-all: install-doc -install-doc-no: - -.PHONY: install install-doc-all install-doc-no - -#These variables are intended to be set by the caller to make -#COQINSTALLPREFIX= -#OLDROOT= - - # Can be changed for a local installation (to make packages). - # You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). +.PHONY: validate check test-suite $(ALLSTDLIB).v -ifdef COQINSTALLPREFIX -FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -else -FULLBINDIR=$(BINDIR) -FULLCOQLIB=$(COQLIBINSTALL) -FULLCONFIGDIR=$(CONFIGDIR) -FULLDATADIR=$(DATADIR) -FULLMANDIR=$(MANDIR) -FULLEMACSLIB=$(EMACSLIB) -FULLCOQDOCDIR=$(COQDOCDIR) -FULLDOCDIR=$(DOCDIR) -endif - -.PHONY: install-coq install-coqlight install-binaries install-byte install-opt -.PHONY: install-tools install-library install-library-light install-devfiles -.PHONY: install-coq-info install-coq-manpages install-emacs install-latex +VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -install-coq: install-binaries install-library install-coq-info install-devfiles -install-coqlight: install-binaries install-library-light +validate: $(CHICKEN) | $(ALLVO) + $(SHOW)'COQCHK <theories & plugins>' + $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) -install-binaries: install-tools - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) - $(MKDIR) $(FULLCOQLIB)/toploop - $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ -ifeq ($(BEST),opt) - $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ -endif +$(ALLSTDLIB).v: + $(SHOW)'MAKE $(notdir $@)' + $(HIDE)echo "Require $(ALLMODS)." > $@ +MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE) -install-tools: - $(MKDIR) $(FULLBINDIR) - # recopie des fichiers de style pour coqide - $(MKDIR) $(FULLCOQLIB)/tools/coqdoc - touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715) - $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc - $(INSTALLBIN) $(TOOLS) $(FULLBINDIR) +check: validate test-suite -# The list of .cmi to install, including the ones obtained -# from .mli without .ml, and the ones obtained from .ml without .mli +test-suite: world $(ALLSTDLIB).v + $(MAKE) $(MAKE_TSOPTS) clean + $(MAKE) $(MAKE_TSOPTS) all + $(MAKE) $(MAKE_TSOPTS) report -INSTALLCMI = $(sort \ - $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ - $(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) +########################################################################### +### Special rules (Camlp5 / Camlp4) +########################################################################### -install-devfiles: - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) - $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA) - $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) -ifeq ($(BEST),opt) - $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) -endif +# Special rule for the compatibility-with-camlp5 extension for camlp4 -install-library: - $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) - $(MKDIR) $(FULLCOQLIB)/user-contrib -ifndef CUSTOM - $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) -endif -ifeq ($(BEST),opt) - $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) -endif -# csdpcert is not meant to be directly called by the user; we install -# it with libraries - -$(MKDIR) $(FULLCOQLIB)/plugins/micromega - $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega - rm -f $(FULLCOQLIB)/revision - -$(INSTALLLIB) revision $(FULLCOQLIB) - -install-library-light: - $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) - rm -f $(FULLCOQLIB)/revision - -$(INSTALLLIB) revision $(FULLCOQLIB) -ifndef CUSTOM - $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) -endif -ifeq ($(BEST),opt) - $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT) +ifeq ($(CAMLP4),camlp4) +tools/compat5.cmo: tools/compat5.mlp + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< +tools/compat5b.cmo: tools/compat5b.mlp + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< +else +tools/compat5.cmo: tools/compat5.ml + $(OCAMLC) -c $< endif -install-coq-info: install-coq-manpages install-emacs install-latex - -install-coq-manpages: - $(MKDIR) $(FULLMANDIR)/man1 - $(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1 - -install-emacs: - $(MKDIR) $(FULLEMACSLIB) - $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB) - -# command to update TeX' kpathsea database -#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null - -install-latex: - $(MKDIR) $(FULLCOQDOCDIR) - $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) -# -$(UPDATETEX) - ########################################################################### -# Documentation of the source code (using ocamldoc) +# Default rules for compiling ML code ########################################################################### -.PHONY: source-doc mli-doc ml-doc - -source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf - -$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) - $(SHOW)'OCAMLDOC -latex -o $@' - $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ - $(DOCMLIS) -noheader -t "Coq mlis documentation" \ - -intro $(OCAMLDOCDIR)/docintro -o $@.tmp - $(SHOW)'OCAMLDOC utf8 fix' - $(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp - $(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@ - rm $@.tmp - -mli-doc: $(DOCMLIS:.mli=.cmi) - $(SHOW)'OCAMLDOC -html' - $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ - $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ - -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ - -css-style style.css - -ml-dot: $(MLFILES) - $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \ - $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot - -%_dep.png: %.dot - $(DOT) -Tpng $< -o $@ - -%_types.dot: %.mli - $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< - -OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ - $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib)))) - -%.dot: | %.mllib.d - $(OCAMLDOC_MLLIBD) - -ml-doc: - $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) - -parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d - $(OCAMLDOC_MLLIBD) - -grammar/grammar.dot : | grammar/grammar.mllib.d - $(OCAMLDOC_MLLIBD) - -tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d - $(OCAMLDOC_MLLIBD) - -%.dot: %.mli - $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< +# Target for libraries .cma and .cmxa -$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex - $(SHOW)'PDFLATEX $*.tex' - $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) - $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) +# The dependency over the .mllib is somewhat artificial, since +# ocamlc -a won't use this file, hence the $(filter-out ...) below. +# But this ensures that the .cm(x)a is rebuilt when needed, +# (especially when removing a module in the .mllib). +# We used to have a "order-only" dependency over .mllib.d here, +# but the -include mechanism should already ensure that we have +# up-to-date dependencies. -########################################################################### -### Special rules -########################################################################### +%.cma: %.mllib + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) -dev/printers.cma: dev/printers.mllib - $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer - @rm -f test-printer - $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@ +%.cmxa: %.mllib + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) -ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ - -# pretty printing of the revision number when compiling a checked out -# source tree -.PHONY: revision - -revision: - $(SHOW)'CHECK revision' - $(HIDE)rm -f revision.new -ifeq ($(CHECKEDOUT),svn) - $(HIDE)set -e; \ - if test -x "`which svn`"; then \ - export LC_ALL=C;\ - svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \ - svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \ - fi -endif -ifeq ($(CHECKEDOUT),gnuarch) - $(HIDE)set -e; \ - if test -x "`which tla`"; then \ - LANG=C; export LANG; \ - tla tree-version > revision.new ; \ - tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \ - fi -endif -ifeq ($(CHECKEDOUT),git) - $(HIDE)set -e; \ - if test -x "`which git`"; then \ - LANG=C; export LANG; \ - GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ - GIT_HOST=$$(hostname); \ - GIT_PATH=$$(pwd); \ - (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ - (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ - fi -endif - $(HIDE)set -e; \ - if test -e revision.new; then \ - if test -e revision; then \ - if test "`cat revision`" = "`cat revision.new`" ; then \ - rm -f revision.new; \ - else \ - mv -f revision.new revision; \ - fi; \ - else \ - mv -f revision.new revision; \ - fi \ - fi +# For plugin packs : -########################################################################### -# Default rules -########################################################################### +%.cmo: %.mlpack + $(SHOW)'OCAMLC -pack -o $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) -## Three flavor of flags: checker/* ide/* and normal files +%.cmx: %.mlpack + $(SHOW)'OCAMLOPT -pack -o $@' + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) COND_BYTEFLAGS= \ - $(if $(filter checker/%,$<), $(CHKLIBS) -thread, \ - $(if $(filter ide/%,$<), $(COQIDEFLAGS), \ - $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(BYTEFLAGS) + $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS) COND_OPTFLAGS= \ - $(if $(filter checker/%,$<), $(CHKLIBS) -thread, \ - $(if $(filter ide/%,$<), $(COQIDEFLAGS), \ - $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(OPTFLAGS) - -%.o: %.c - $(SHOW)'OCAMLC $<' - $(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<) - -%.o: %.rc - $(SHOW)'WINDRES $<' - $(HIDE)i686-w64-mingw32-windres -i $< -o $@ + $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(OPTFLAGS) %.cmi: %.mli $(SHOW)'OCAMLC $<' @@ -1075,18 +547,22 @@ $(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the $(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo +# NB: the *_FORPACK variables are generated in *.mlpack.d by ocamllibdep +# The only exceptions are the sources of the csdpcert binary. +# To avoid warnings, we set them manually here: +plugins/micromega/sos_lib_FORPACK:= +plugins/micromega/sos_FORPACK:= +plugins/micromega/sos_print_FORPACK:= +plugins/micromega/csdpcert_FORPACK:= + +plugins/%.cmx: plugins/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< + %.cmx: %.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $< -%.cmxs: %.cmxa - $(SHOW)'OCAMLOPT -shared -o $@' -ifeq ($(HASNATDYNLINK),os5fixme) - $(HIDE)dev/ocamlopt_shared_os5fix.sh "$(OCAMLOPT)" $@ -else - $(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $< -endif - %.cmxs: %.cmx $(SHOW)'OCAMLOPT -shared -o $@' $(HIDE)$(OCAMLOPT) -shared -o $@ $< @@ -1095,97 +571,84 @@ endif $(SHOW)'OCAMLLEX $<' $(HIDE)$(OCAMLLEX) -o $@ "$*.mll" -plugins/%_mod.ml: plugins/%.mllib - $(SHOW)'ECHO... > $@' - $(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@ - $(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@ - %.ml: %.ml4 | $(CAMLP4DEPS) $(SHOW)'CAMLP4O $<' $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) \ $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@ -%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) - $(SHOW)'COQC $<' - $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQC) $< -ifdef VALIDATE - $(SHOW)'COQCHK $(call vo_to_mod,$@)' - $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) -endif ########################################################################### -# Dependencies +# Dependencies of ML code ########################################################################### -# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to -# the option -ml-synonym - -OCAMLDEP_NG = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 - -checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) - -checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) - $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) +# Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) +OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack %.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) %.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" $(TOTARGET) -checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) - $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(LOCALCHKLIBS) "$<" $(TOTARGET) - -dev/%.mllib.d: $(D_DEPEND_BEFORE_SRC) dev/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) +%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) $(SHOW)'OCAMLLIBDEP $<' - $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) -I dev "$<" $(TOTARGET) + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) -%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) +%.mlpack.d: $(D_DEPEND_BEFORE_SRC) %.mlpack $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) $(SHOW)'OCAMLLIBDEP $<' $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) +########################################################################### +# Compilation of .v files +########################################################################### -%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) - $(SHOW)'CCDEP $<' - $(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@ +# NB: for make world, no need to mention explicitly the .cmxs of the plugins, +# since they are all mentioned in at least one Declare ML Module in some .v -%.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES) - $(SHOW)'CCDEP $<' - $(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET) +coqlib: theories plugins -########################################################################### -# this sets up developper supporting stuff -########################################################################### +theories: $(THEORIESVO) +plugins: $(PLUGINSVO) + +.PHONY: coqlib theories plugins + +# One of the .v files is macro-generated + +theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml + $(OCAML) $< $(TOTARGET) -.PHONY: devel otags -devel: $(DEBUGPRINTERS) +# The .vo files in Init are built with the -noinit option -# NOTA : otags only accepts camlp4 as preprocessor, so the following rule -# won't build tags of .ml4 when compiling with camlp5 -otags: - otags $(MLIFILES) $(filter-out configure.ml, $(MLSTATICFILES)) \ - $(if $(filter camlp5,$(CAMLP4)), , \ - -pa op -pa g -pa m -pa rq $(addprefix -pa , $(CAMLP4DEPS)) \ - $(addprefix -impl , $(ML4FILES))) +theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) + $(SHOW)'COQC $(COQ_XML) -noinit $<' + $(HIDE)rm -f theories/Init/$*.glob + $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq +# The general rule for building .vo files : + +%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) + $(SHOW)'COQC $<' + $(HIDE)rm -f $*.glob + $(HIDE)$(BOOTCOQC) $< +ifdef VALIDATE + $(SHOW)'COQCHK $(call vo_to_mod,$@)' + $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) +endif + +# Dependencies of .v files + +%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) ########################################################################### # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles -Makefile Makefile.build Makefile.common config/Makefile : ; - +Makefile $(wildcard Makefile.*) config/Makefile : ; # For emacs: # Local Variables: diff --git a/Makefile.checker b/Makefile.checker new file mode 100644 index 000000000..3ea0baced --- /dev/null +++ b/Makefile.checker @@ -0,0 +1,86 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +## Makefile rules for building Coqchk + +## NB: For the moment, the build system of Coqchk is part of +## the one of Coq. In particular, this Makefile.checker is included in +## Makefile.build. Please ensure that the rules define here are +## indeed specific to files of the form checker/* + +# The binaries + +CHICKENBYTE:=bin/coqchk.byte$(EXE) +CHICKEN:=bin/coqchk$(EXE) + +# The sources + +CHKLIBS:= -I config -I lib -I checker + +## NB: currently, both $(OPTFLAGS) and $(BYTEFLAGS) contain -thread + +# The rules + +ifeq ($(BEST),opt) +$(CHICKEN): checker/check.cmxa checker/main.ml + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(SYSCMXA) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ + $(STRIP) $@ + $(CODESIGN) $@ +else +$(CHICKEN): $(CHICKENBYTE) + cp $< $@ +endif + +$(CHICKENBYTE): checker/check.cma checker/main.ml + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(SYSCMA) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ + +checker/check.cma: checker/check.mllib | md5chk + $(SHOW)'OCAMLC -a -o $@' + $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^) + +checker/check.cmxa: checker/check.mllib | md5chk + $(SHOW)'OCAMLOPT -a -o $@' + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) + +checker/%.ml.d: checker/%.ml + $(SHOW)'OCAMLDEP $<' + $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET) + +checker/%.mli.d: checker/%.mli + $(SHOW)'OCAMLDEP $<' + $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) "$<" $(TOTARGET) + +checker/%.mllib.d: checker/%.mllib | $(OCAMLLIBDEP) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(CHKLIBS) "$<" $(TOTARGET) + +checker/%.cmi: checker/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -c $< + +checker/%.cmo: checker/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -c $< + +checker/%.cmx: checker/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $< + +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 + +.PHONY: md5chk + +# For emacs: +# Local Variables: +# mode: makefile +# End: diff --git a/Makefile.common b/Makefile.common index 86a7ea847..4742bb51e 100644 --- a/Makefile.common +++ b/Makefile.common @@ -14,19 +14,32 @@ COQMKTOP:=bin/coqmktop$(EXE) -COQC:=bin/coqc$(EXE) - COQTOPBYTE:=bin/coqtop.byte$(EXE) COQTOPEXE:=bin/coqtop$(EXE) -CHICKENBYTE:=bin/coqchk.byte$(EXE) -CHICKEN:=bin/coqchk$(EXE) +COQDEP:=bin/coqdep$(EXE) +COQMAKEFILE:=bin/coq_makefile$(EXE) +GALLINA:=bin/gallina$(EXE) +COQTEX:=bin/coq-tex$(EXE) +COQWC:=bin/coqwc$(EXE) +COQDOC:=bin/coqdoc$(EXE) +COQC:=bin/coqc$(EXE) +COQWORKMGR:=bin/coqworkmgr$(EXE) -ifeq ($(CAMLP4),camlp4) -CAMLP4MOD:=camlp4lib -else -CAMLP4MOD:=gramlib -endif +TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ + $(COQWORKMGR) + +COQDEPBOOT:=bin/coqdep_boot$(EXE) +OCAMLLIBDEP:=bin/ocamllibdep$(EXE) +FAKEIDE:=bin/fake_ide$(EXE) + +PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT) + +CSDPCERT:=plugins/micromega/csdpcert$(EXE) + +########################################################################### +# Object and Source files +########################################################################### ifeq ($(HASNATDYNLINK)-$(BEST),true-opt) DEPNATDYN:= @@ -39,27 +52,6 @@ INSTALLLIB:=install -m 644 INSTALLSH:=./install.sh MKDIR:=install -d -COQIDEBYTE:=bin/coqide.byte$(EXE) -COQIDE:=bin/coqide$(EXE) -COQIDEAPP:=bin/CoqIDE_$(VERSION).app -COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide - -ifeq ($(BEST),opt) -OPT:=opt -else -OPT:= -endif - -BESTOBJ:=$(if $(OPT),.cmx,.cmo) -BESTLIB:=$(if $(OPT),.cmxa,.cma) -BESTDYN:=$(if $(OPT),.cmxs,.cma) - -COQBINARIES:= $(COQMKTOP) \ - $(COQTOPBYTE) $(COQTOPEXE) \ - $(CHICKENBYTE) $(CHICKEN) - -CSDPCERT:=plugins/micromega/csdpcert$(EXE) - CORESRCDIRS:=\ config lib kernel kernel/byterun library \ proofs tactics pretyping interp stm \ @@ -76,82 +68,6 @@ SRCDIRS:=\ tools tools/coqdoc \ $(addprefix plugins/, $(PLUGINS)) -IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils - -CHKSRCDIRS:= config lib checker - -########################################################################### -# Tools -########################################################################### - -COQDEP:=bin/coqdep$(EXE) -COQDEPBOOT:=bin/coqdep_boot$(EXE) -OCAMLLIBDEP:=bin/ocamllibdep$(EXE) -COQMAKEFILE:=bin/coq_makefile$(EXE) -GALLINA:=bin/gallina$(EXE) -COQTEX:=bin/coq-tex$(EXE) -COQWC:=bin/coqwc$(EXE) -COQDOC:=bin/coqdoc$(EXE) -FAKEIDE:=bin/fake_ide$(EXE) -COQWORKMGR:=bin/coqworkmgr$(EXE) - -TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ - $(COQWORKMGR) - -PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT) - -########################################################################### -# Documentation -########################################################################### - -LATEX:=latex -BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 -MAKEINDEX:=makeindex -PDFLATEX:=pdflatex -DVIPS:=dvips -FIG2DEV:=fig2dev -CONVERT:=convert -HEVEA:=hevea -HACHA:=hacha -HEVEAOPTS:=-fix -exec xxdate.exe -HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea -HTMLSTYLE:=simple -export TEXINPUTS:=$(HEVEALIB): -COQTEXOPTS:=-boot -n 72 -sl -small - -DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex - -REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ - RefMan-gal.v.tex RefMan-ext.v.tex \ - RefMan-mod.v.tex RefMan-tac.v.tex \ - RefMan-cic.v.tex RefMan-lib.v.tex \ - RefMan-tacex.v.tex RefMan-syn.v.tex \ - RefMan-oth.v.tex RefMan-ltac.v.tex \ - RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \ - Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ - Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ - Setoid.v.tex Classes.v.tex Universes.v.tex \ - Misc.v.tex) - -REFMANTEXFILES:=$(addprefix doc/refman/, \ - headers.sty Reference-Manual.tex \ - RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ - RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \ - AsyncProofs.tex ) \ - $(REFMANCOQTEXFILES) \ - -REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps - -REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib - -REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) - - - -########################################################################### -# Object and Source files -########################################################################### - COQRUN := coqrun LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT) @@ -173,28 +89,36 @@ TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma -OMEGACMA:=plugins/omega/omega_plugin.cma -ROMEGACMA:=plugins/romega/romega_plugin.cma -MICROMEGACMA:=plugins/micromega/micromega_plugin.cma -QUOTECMA:=plugins/quote/quote_plugin.cma -RINGCMA:=plugins/setoid_ring/newring_plugin.cma -NSATZCMA:=plugins/nsatz/nsatz_plugin.cma -FOURIERCMA:=plugins/fourier/fourier_plugin.cma -EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma -FUNINDCMA:=plugins/funind/recdef_plugin.cma -FOCMA:=plugins/firstorder/ground_plugin.cma -CCCMA:=plugins/cc/cc_plugin.cma -BTAUTOCMA:=plugins/btauto/btauto_plugin.cma -RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma -NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma +# modules known by the toplevel of Coq + +OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib)) + +########################################################################### +# plugins object files +########################################################################### + +OMEGACMA:=plugins/omega/omega_plugin.cmo +ROMEGACMA:=plugins/romega/romega_plugin.cmo +MICROMEGACMA:=plugins/micromega/micromega_plugin.cmo +QUOTECMA:=plugins/quote/quote_plugin.cmo +RINGCMA:=plugins/setoid_ring/newring_plugin.cmo +NSATZCMA:=plugins/nsatz/nsatz_plugin.cmo +FOURIERCMA:=plugins/fourier/fourier_plugin.cmo +EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cmo +FUNINDCMA:=plugins/funind/recdef_plugin.cmo +FOCMA:=plugins/firstorder/ground_plugin.cmo +CCCMA:=plugins/cc/cc_plugin.cmo +BTAUTOCMA:=plugins/btauto/btauto_plugin.cmo +RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cmo +NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cmo OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ - z_syntax_plugin.cma \ - numbers_syntax_plugin.cma \ - r_syntax_plugin.cma \ - ascii_syntax_plugin.cma \ - string_syntax_plugin.cma ) -DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma -DERIVECMA:=plugins/derive/derive_plugin.cma + z_syntax_plugin.cmo \ + numbers_syntax_plugin.cmo \ + r_syntax_plugin.cmo \ + ascii_syntax_plugin.cmo \ + string_syntax_plugin.cmo ) +DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cmo +DERIVECMA:=plugins/derive/derive_plugin.cmo PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) \ @@ -207,17 +131,17 @@ ifneq ($(HASNATDYNLINK),false) STATICPLUGINS:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ $(FUNINDCMA) $(NATSYNTAXCMA) - INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) + INITPLUGINSOPT:=$(INITPLUGINS:.cmo=.cmxs) PLUGINS:=$(PLUGINSCMA) - PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) + PLUGINSOPT:=$(PLUGINSCMA:.cmo=.cmxs) else ifeq ($(BEST),byte) STATICPLUGINS:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) \ $(FUNINDCMA) $(NATSYNTAXCMA) - INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) + INITPLUGINSOPT:=$(INITPLUGINS:.cmo=.cmxs) PLUGINS:=$(PLUGINSCMA) - PLUGINSOPT:=$(PLUGINSCMA:.cma=.cmxs) + PLUGINSOPT:=$(PLUGINSCMA:.cmo=.cmxs) else STATICPLUGINS:=$(PLUGINSCMA) INITPLUGINS:= @@ -228,43 +152,7 @@ endif endif LINKCMO:=$(CORECMA) $(STATICPLUGINS) -LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) - -IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo -IDECMA:=ide/ide.cma -IDETOPLOOPCMA=ide/coqidetop.cma - -LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml - -# modules known by the toplevel of Coq - -OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib)) - -IDEMOD:=$(shell cat ide/ide.mllib) - -# coqmktop, coqc - -COQENVCMO:=lib/clib.cma lib/errors.cmo - -COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo - -COQCCMO:=$(COQENVCMO) toplevel/usage.cmo tools/coqc.cmo - -## Misc - -CSDPCERTCMO:=$(addprefix plugins/micromega/, \ - mutils.cmo micromega.cmo \ - sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) - -DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma - -COQDEPCMO:=$(COQENVCMO) lib/minisys.cmo lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo - -COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ - cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) - -COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo +LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) ########################################################################### # vo files @@ -272,127 +160,41 @@ COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo ## we now retrieve the names of .vo file to compile in */vo.itarget files -cat_vo_itarget = $(addprefix $(1)/,$(shell cat $(1)/vo.itarget)) - -## Theories - -INITVO:=$(call cat_vo_itarget, theories/Init) -LOGICVO:=$(call cat_vo_itarget, theories/Logic) -STRUCTURESVO:=$(call cat_vo_itarget, theories/Structures) -ARITHVO:=$(call cat_vo_itarget, theories/Arith) -SORTINGVO:=$(call cat_vo_itarget, theories/Sorting) -BOOLVO:=$(call cat_vo_itarget, theories/Bool) -PARITHVO:=$(call cat_vo_itarget, theories/PArith) -NARITHVO:=$(call cat_vo_itarget, theories/NArith) -ZARITHVO:=$(call cat_vo_itarget, theories/ZArith) -QARITHVO:=$(call cat_vo_itarget, theories/QArith) -LISTSVO:=$(call cat_vo_itarget, theories/Lists) -VECTORSVO:=$(call cat_vo_itarget, theories/Vectors) -STRINGSVO:=$(call cat_vo_itarget, theories/Strings) -SETSVO:=$(call cat_vo_itarget, theories/Sets) -FSETSVO:=$(call cat_vo_itarget, theories/FSets) -MSETSVO:=$(call cat_vo_itarget, theories/MSets) -RELATIONSVO:=$(call cat_vo_itarget, theories/Relations) -WELLFOUNDEDVO:=$(call cat_vo_itarget, theories/Wellfounded) -REALSVO:=$(call cat_vo_itarget, theories/Reals) -NUMBERSVO:=$(call cat_vo_itarget, theories/Numbers) -SETOIDSVO:=$(call cat_vo_itarget, theories/Setoids) -UNICODEVO:=$(call cat_vo_itarget, theories/Unicode) -CLASSESVO:=$(call cat_vo_itarget, theories/Classes) -PROGRAMVO:=$(call cat_vo_itarget, theories/Program) -COMPATVO:=$(call cat_vo_itarget, theories/Compat) - -THEORIESVO:=\ - $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \ - $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) \ - $(RELATIONSVO) $(WELLFOUNDEDVO) $(SETOIDSVO) \ - $(LISTSVO) $(STRINGSVO) \ - $(PARITHVO) $(NARITHVO) $(ZARITHVO) \ - $(SETSVO) $(FSETSVO) $(MSETSVO) \ - $(REALSVO) $(SORTINGVO) $(QARITHVO) \ - $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) \ - $(COMPATVO) - -THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO) - -## Plugins - -OMEGAVO:=$(call cat_vo_itarget, plugins/omega) -ROMEGAVO:=$(call cat_vo_itarget, plugins/romega) -MICROMEGAVO:=$(call cat_vo_itarget, plugins/micromega) -QUOTEVO:=$(call cat_vo_itarget, plugins/quote) -RINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) -NSATZVO:=$(call cat_vo_itarget, plugins/nsatz) -FOURIERVO:=$(call cat_vo_itarget, plugins/fourier) -FUNINDVO:=$(call cat_vo_itarget, plugins/funind) -BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto) -RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto) -EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction) -CCVO:= -DERIVEVO:=$(call cat_vo_itarget, plugins/derive) - -PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \ - $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \ - $(NSATZVO) $(EXTRACTIONVO) $(DERIVEVO) +THEORIESVO:= $(foreach f, $(wildcard theories/*/vo.itarget), \ + $(addprefix $(dir $(f)),$(shell cat $(f)))) + +PLUGINSVO:= $(foreach f, $(wildcard plugins/*/vo.itarget), \ + $(addprefix $(dir $(f)),$(shell cat $(f)))) ALLVO:= $(THEORIESVO) $(PLUGINSVO) VFILES:= $(ALLVO:.vo=.v) + +## More specific targets + +THEORIESLIGHTVO:= \ + $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO)) + ALLSTDLIB := test-suite/misc/universes/all_stdlib # convert a (stdlib) filename into a module name: # remove .vo, replace theories and plugins by Coq, and replace slashes by dots vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=)))) +ALLMODS:=$(call vo_to_mod,$(ALLVO)) + + # Converting a stdlib filename into native compiler filenames # Used for install targets vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*))))) vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) -ALLMODS:=$(call vo_to_mod,$(ALLVO)) - LIBFILES:=$(THEORIESVO) $(PLUGINSVO) $(call vo_to_cm,$(THEORIESVO)) \ $(call vo_to_cm,$(PLUGINSVO)) $(call vo_to_obj,$(THEORIESVO)) \ $(call vo_to_obj,$(PLUGINSVO)) \ $(PLUGINSVO:.vo=.v) $(THEORIESVO:.vo=.v) \ $(PLUGINSVO:.vo=.glob) $(THEORIESVO:.vo=.glob) -LIBFILESLIGHT:=$(THEORIESLIGHTVO) - -########################################################################### -# Miscellaneous -########################################################################### - -MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ - man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ - man/coqwc.1 man/coqdoc.1 man/coqide.1 \ - man/coq_makefile.1 man/coqmktop.1 man/coqchk.1 - -########################################################################### -# Source documentation -########################################################################### - -OCAMLDOCDIR=dev/ocamldoc - -DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ - ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ - ./parsing/*.mli ./proofs/*.mli \ - ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli) - -# Defining options to generate dependencies graphs -DOT=dot -ODOCDOTOPTS=-dot -dot-reduce - -########################################################################### -# GTK for Coqide MacOS bundle -########################################################################### - -GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share -GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin -GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) - - # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.dev b/Makefile.dev new file mode 100644 index 000000000..f35b861c1 --- /dev/null +++ b/Makefile.dev @@ -0,0 +1,223 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +# Extra targets for developpers : +# debug printers, revision, partial targets ... + +######################### +# Debug printers in dev/ +######################### + +.PHONY: devel printers + +DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma + +devel: printers +printers: $(DEBUGPRINTERS) + +dev/printers.cma: dev/printers.mllib + $(SHOW)'Testing $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer + @rm -f test-printer + $(SHOW)'OCAMLC -a $@' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@ + +dev/%.mllib.d: dev/%.mllib | $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) -I dev "$<" $(TOTARGET) + +############ +# revision +############ + +# display the revision number when compiling a checked out source tree + +revision: + $(SHOW)'CHECK revision' + $(HIDE)rm -f revision.new +ifeq ($(CHECKEDOUT),svn) + $(HIDE)set -e; \ + if test -x "`which svn`"; then \ + export LC_ALL=C;\ + svn info . | sed -ne '/URL/s/.*\/\([^\/]\{1,\}\)/\1/p' > revision.new; \ + svn info . | sed -ne '/Revision/s/Revision: \([0-9]\{1,\}\)/\1/p'>> revision.new; \ + fi +endif +ifeq ($(CHECKEDOUT),gnuarch) + $(HIDE)set -e; \ + if test -x "`which tla`"; then \ + LANG=C; export LANG; \ + tla tree-version > revision.new ; \ + tla tree-revision | sed -ne 's|.*--||p' >> revision.new ; \ + fi +endif +ifeq ($(CHECKEDOUT),git) + $(HIDE)set -e; \ + if test -x "`which git`"; then \ + LANG=C; export LANG; \ + GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ + GIT_HOST=$$(hostname); \ + GIT_PATH=$$(pwd); \ + (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ + (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ + fi +endif + $(HIDE)set -e; \ + if test -e revision.new; then \ + if test -e revision; then \ + if test "`cat revision`" = "`cat revision.new`" ; then \ + rm -f revision.new; \ + else \ + mv -f revision.new revision; \ + fi; \ + else \ + mv -f revision.new revision; \ + fi \ + fi + +.PHONY: revision + +################### +# Partial builds +################### + +# The following partial targets are normally not necessary +# for a complete build of coq, see instead 'make world' for that. +# But these partial targets could be quite handy for quick builds +# of specific components of Coq. + +############################### +### 1) general-purpose targets +############################### + +coqlight: theories-light tools coqbinaries + +states: theories/Init/Prelude.vo + +miniopt: $(COQTOPEXE) pluginsopt +minibyte: $(COQTOPBYTE) pluginsbyte + +pluginsopt: $(PLUGINSOPT) +pluginsbyte: $(PLUGINS) + +.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte + +########################## +### 2) core ML components +########################## + +lib: lib/clib.cma lib/lib.cma +kernel: kernel/kernel.cma +byterun: $(BYTERUN) +library: library/library.cma +engine: engine/engine.cma +proofs: proofs/proofs.cma +tactics: tactics/tactics.cma +interp: interp/interp.cma +parsing: parsing/parsing.cma +pretyping: pretyping/pretyping.cma +highparsing: parsing/highparsing.cma +stm: stm/stm.cma +toplevel: toplevel/toplevel.cma +ltac: ltac/ltac.cma + +.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping +.PHONY: engine highparsing stm toplevel ltac + +###################### +### 3) theories files +###################### + +init: $(filter theories/Init/%, $(THEORIESVO)) +logic: $(filter theories/Logic/%, %(THEORIESVO)) +arith: $(filter theories/Arith/%, $(THEORIESVO)) +bool: $(filter theories/Bool/%, $(THEORIESVO)) +parith: $(filter theories/PArith/%, $(THEORIESVO)) +narith: $(filter theories/NArith/%, $(THEORIESVO)) +zarith: $(filter theories/ZArith/%, $(THEORIESVO)) +qarith: $(filter theories/QArith/%, $(THEORIESVO)) +lists: $(filter theories/Lists/%, $(THEORIESVO)) +strings: $(filter theories/Strings/%, $(THEORIESVO)) +sets: $(filter theories/Sets/%, $(THEORIESVO)) +fsets: $(filter theories/FSets/%, $(THEORIESVO)) +relations: $(filter theories/Relations/%, $(THEORIESVO)) +wellfounded: $(filter theories/Wellfounded/%, $(THEORIESVO)) +reals: $(filter theories/Reals/%, $(THEORIESVO)) +setoids: $(filter theories/Setoids/%, $(THEORIESVO)) +sorting: $(filter theories/Sorting/%, $(THEORIESVO)) +numbers: $(filter theories/Numbers/%, $(THEORIESVO)) +unicode: $(filter theories/Unicode/%, $(THEORIESVO)) +classes: $(filter theories/Classes/%, $(THEORIESVO)) +program: $(filter theories/Program/%, $(THEORIESVO)) +structures: $(filter theories/Structures/%, $(THEORIESVO)) +vectors: $(filter theories/Vectors/%, $(THEORIESVO)) +msets: $(filter theories/MSets/%, $(THEORIESVO)) +compat: $(filter theories/Compat/%, $(THEORIESVO)) + +theories-light: $(THEORIESLIGHTVO) + +noreal: unicode logic arith bool zarith qarith lists sets fsets \ + relations wellfounded setoids sorting + +.PHONY: init theories-light noreal +.PHONY: logic arith bool narith zarith qarith lists strings sets +.PHONY: fsets relations wellfounded reals setoids sorting numbers +.PHONY: msets mmaps compat + +################ +### 4) plugins +################ + +OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) +ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO)) +MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) +QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO)) +RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) +NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) +FOURIERVO:=$(filter plugins/fourier/%, $(PLUGINSVO)) +FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) +BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) +RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) +EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) +CCVO:= +DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) + +omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) +micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) +setoid_ring: $(RINGVO) $(RINGCMA) +nsatz: $(NSATZVO) $(NSATZCMA) +extraction: $(EXTRACTIONCMA) +fourier: $(FOURIERVO) $(FOURIERCMA) +funind: $(FUNINDCMA) $(FUNINDVO) +cc: $(CCVO) $(CCCMA) +rtauto: $(RTAUTOVO) $(RTAUTOCMA) +btauto: $(BTAUTOVO) $(BTAUTOCMA) + +.PHONY: omega micromega setoid_ring nsatz extraction +.PHONY: fourier funind cc rtauto btauto + +################################# +### Misc other development rules +################################# + +# NOTA : otags only accepts camlp4 as preprocessor, so the following rule +# won't build tags of .ml4 when compiling with camlp5 + +otags: + otags $(MLIFILES) $(filter-out configure.ml, $(MLSTATICFILES)) \ + $(if $(filter camlp5,$(CAMLP4)), , \ + -pa op -pa g -pa m -pa rq $(addprefix -pa , $(CAMLP4DEPS)) \ + $(addprefix -impl , $(ML4FILES))) + +.PHONY: otags + + +# For emacs: +# Local Variables: +# mode: makefile +# End: diff --git a/Makefile.doc b/Makefile.doc index b7251ce57..6c345025a 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -1,3 +1,11 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + # Makefile for the Coq documentation # To compile documentation, you need the following tools: @@ -5,6 +13,61 @@ # Pdf: pdflatex # Html: hevea (http://hevea.inria.fr) >= 1.05 +# The main entry point : + +documentation: doc-$(WITHDOC) ## see $(WITHDOC) in config/Makefile +doc-all: doc +doc-no: + +.PHONY: documentation doc-all doc-no + +###################################################################### +### Variables +###################################################################### + +LATEX:=latex +BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 +MAKEINDEX:=makeindex +PDFLATEX:=pdflatex +DVIPS:=dvips +FIG2DEV:=fig2dev +CONVERT:=convert +HEVEA:=hevea +HACHA:=hacha +HEVEAOPTS:=-fix -exec xxdate.exe +HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea +HTMLSTYLE:=simple +export TEXINPUTS:=$(HEVEALIB): +COQTEXOPTS:=-boot -n 72 -sl -small + +DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex + +REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ + RefMan-gal.v.tex RefMan-ext.v.tex \ + RefMan-mod.v.tex RefMan-tac.v.tex \ + RefMan-cic.v.tex RefMan-lib.v.tex \ + RefMan-tacex.v.tex RefMan-syn.v.tex \ + RefMan-oth.v.tex RefMan-ltac.v.tex \ + RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \ + Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ + Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ + Setoid.v.tex Classes.v.tex Universes.v.tex \ + Misc.v.tex) + +REFMANTEXFILES:=$(addprefix doc/refman/, \ + headers.sty Reference-Manual.tex \ + RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ + RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \ + AsyncProofs.tex ) \ + $(REFMANCOQTEXFILES) \ + +REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps + +REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib + +REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) + + ###################################################################### ### General rules ###################################################################### @@ -339,6 +402,80 @@ install-doc-index-urls: $(MKDIR) $(FULLDATADIR) $(INSTALLLIB) $(INDEXURLS) $(FULLDATADIR) + +########################################################################### +# Documentation of the source code (using ocamldoc) +########################################################################### + +OCAMLDOCDIR=dev/ocamldoc + +DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ + ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ + ./parsing/*.mli ./proofs/*.mli \ + ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli) + +# Defining options to generate dependencies graphs +DOT=dot +ODOCDOTOPTS=-dot -dot-reduce + +.PHONY: source-doc mli-doc ml-doc + +source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf + +$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) + $(SHOW)'OCAMLDOC -latex -o $@' + $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ + $(DOCMLIS) -noheader -t "Coq mlis documentation" \ + -intro $(OCAMLDOCDIR)/docintro -o $@.tmp + $(SHOW)'OCAMLDOC utf8 fix' + $(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp + $(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@ + rm $@.tmp + +mli-doc: $(DOCMLIS:.mli=.cmi) + $(SHOW)'OCAMLDOC -html' + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ + -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ + -css-style style.css + +ml-dot: $(MLFILES) + $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot + +%_dep.png: %.dot + $(DOT) -Tpng $< -o $@ + +%_types.dot: %.mli + $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< + +OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ + $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib)))) + +%.dot: | %.mllib.d + $(OCAMLDOC_MLLIBD) + +ml-doc: + $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) + +parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d + $(OCAMLDOC_MLLIBD) + +grammar/grammar.dot : | grammar/grammar.mllib.d + $(OCAMLDOC_MLLIBD) + +tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d + $(OCAMLDOC_MLLIBD) + +%.dot: %.mli + $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< + +$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex + $(SHOW)'PDFLATEX $*.tex' + $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) + $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) + + # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.ide b/Makefile.ide new file mode 100644 index 000000000..8d6b5de36 --- /dev/null +++ b/Makefile.ide @@ -0,0 +1,254 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +## Makefile rules for building the CoqIDE interface + +## NB: For the moment, the build system of CoqIDE is part of +## the one of Coq. In particular, this Makefile.ide is included in +## Makefile.build. Please ensure that the rules define here are +## indeed specific to files of the form ide/* + +## Coqide-related variables set by ./configure in config/Makefile + +#COQIDEINCLUDES : something like -I +lablgtk2 +#HASCOQIDE : opt / byte / no +#IDEFLAGS : some extra cma, for instance +#IDEOPTCDEPS : on windows, ide/ide_win32_stubs.o ide/coq_icon.o +#IDECDEPS +#IDECDEPSFLAGS +#IDEINT : X11 / QUARTZ / WIN32 + +## CoqIDE Executable + +COQIDEBYTE:=bin/coqide.byte$(EXE) +COQIDE:=bin/coqide$(EXE) +COQIDEAPP:=bin/CoqIDE_$(VERSION).app +COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide + +## CoqIDE source directory and files + +# Note : for just building bin/coqide, we could only consider +# config, lib, ide and ide/utils. But the coqidetop plugin (the +# one that will be loaded by coqtop -ideslave) refers to some +# core modules of coq, for instance printing/*. + +IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils + +COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) + +IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo +IDECMA:=ide/ide.cma +IDETOPLOOPCMA=ide/coqidetop.cma + +LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml + +IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map + +## GTK for Coqide MacOS bundle + +GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share +GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin +GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) + + +########################################################################### +# CoqIde special targets +########################################################################### + +.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files + +# target to build CoqIde +coqide: coqide-files coqide-binaries theories/Init/Prelude.vo + +coqide-binaries: coqide-$(HASCOQIDE) ide-toploop +coqide-no: +coqide-byte: $(COQIDEBYTE) $(COQIDE) +coqide-opt: $(COQIDEBYTE) $(COQIDE) +coqide-files: $(IDEFILES) +ifeq ($(BEST),opt) +ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs) +else +ide-toploop: $(IDETOPLOOPCMA) +endif + +ifeq ($(HASCOQIDE),opt) +$(COQIDE): $(LINKIDEOPT) + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \ + lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^ + $(STRIP) $@ +else +$(COQIDE): $(COQIDEBYTE) + cp $< $@ +endif + +$(COQIDEBYTE): $(LINKIDE) + $(SHOW)'OCAMLC -o $@' + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \ + lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^ + +ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here + $(SHOW)'CAMLP4O $<' + $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ + + +ide/%.cmi: ide/%.mli + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + +ide/%.cmo: ide/%.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -c $< + +ide/%.cmx: ide/%.ml + $(SHOW)'OCAMLOPT $<' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $< + + +#################### +## Install targets +#################### + +.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles + +ifeq ($(HASCOQIDE),no) +install-coqide: install-ide-toploop +else +install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles +endif + +install-ide-bin: + $(MKDIR) $(FULLBINDIR) + $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) + +install-ide-toploop: + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif + +install-ide-devfiles: + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ + $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) +ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) +endif + +install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time + $(MKDIR) $(FULLDATADIR) + $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR) + $(MKDIR) $(FULLCONFIGDIR) + if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi + +install-ide-info: + $(MKDIR) $(FULLDOCDIR) + $(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde + +########################################################################### +# CoqIde MacOS special targets +########################################################################### + +.PHONY: $(COQIDEAPP)/Contents + +$(COQIDEAPP)/Contents: + rm -rdf $@ + $(MKDIR) $@ + sed -e "s/VERSION/$(VERSION4MACOS)/g" ide/MacOS/Info.plist.template > $@/Info.plist + $(MKDIR) "$@/MacOS" + +$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ + unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \ + threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^ + $(STRIP) $@ + +$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents + $(MKDIR) $@/coq/ + $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/ + $(MKDIR) $@/gtksourceview-2.0/{language-specs,styles} + $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/ + $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/ + cp -R "$(GTKSHARE)/"locale $@ + cp -R "$(GTKSHARE)/"icons $@ + cp -R "$(GTKSHARE)/"themes $@ + +$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents + $(MKDIR) $@ + $(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@ + +$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents + $(MKDIR) $@ + $(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@ + + +$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib + $(MKDIR) $@/xdg/coq + $(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys + $(MKDIR) $@/gtk-2.0 + { "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ + sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ + > $@/gtk-2.0/gdk-pixbuf.loaders + { "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\ + sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ + sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ + > $@/gtk-2.0/gtk-immodules.loaders + $(MKDIR) $@/pango + echo "[Pango]" > $@/pango/pangorc + +$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) + $(MKDIR) $@ + $(INSTALLLIB) $(GTKLIBS)/charset.alias $@/ + $(MKDIR) $@/pango/1.8.0/modules + $(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/ + { "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\ + sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \ + > $@/pango/1.8.0/modules.cache + + for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do cp $$i $@/; \ + ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \ + done + for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \ + do \ + for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ + ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \ + done + EXTRAWORK=1; \ + while [ $${EXTRAWORK} -eq 1 ]; \ + do EXTRAWORK=0; \ + for i in $@/*.dylib; \ + do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ + done; \ + done + ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@ + +$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share + $(INSTALLLIB) ide/MacOS/*.icns $@ + +$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources + $(CODESIGN) $@ + +########################################################################### +# CoqIde for Windows special targets +########################################################################### + +%.o: %.rc + $(SHOW)'WINDRES $<' + $(HIDE)i686-w64-mingw32-windres -i $< -o $@ + + +# For emacs: +# Local Variables: +# mode: makefile +# End: diff --git a/Makefile.install b/Makefile.install new file mode 100644 index 000000000..ed29bc1e7 --- /dev/null +++ b/Makefile.install @@ -0,0 +1,136 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +# This makefile regroups installation rules +# It is included by Makefile.build + +ifeq ($(LOCAL),true) +install: + @echo "Nothing to install in a local build!" +else +install: install-coq install-coqide install-doc-$(WITHDOC) +endif + +install-doc-all: install-doc +install-doc-no: + +.PHONY: install install-doc-all install-doc-no + +#These variables are intended to be set by the caller to make +#COQINSTALLPREFIX= +#OLDROOT= + + # Can be changed for a local installation (to make packages). + # You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). + +ifdef COQINSTALLPREFIX +FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +else +FULLBINDIR=$(BINDIR) +FULLCOQLIB=$(COQLIBINSTALL) +FULLCONFIGDIR=$(CONFIGDIR) +FULLDATADIR=$(DATADIR) +FULLMANDIR=$(MANDIR) +FULLEMACSLIB=$(EMACSLIB) +FULLCOQDOCDIR=$(COQDOCDIR) +FULLDOCDIR=$(DOCDIR) +endif + +.PHONY: install-coq install-binaries install-byte install-opt +.PHONY: install-tools install-library install-devfiles +.PHONY: install-coq-info install-coq-manpages install-emacs install-latex + +install-coq: install-binaries install-library install-coq-info install-devfiles + +install-binaries: install-tools + $(MKDIR) $(FULLBINDIR) + $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif + + +install-tools: + $(MKDIR) $(FULLBINDIR) + # recopie des fichiers de style pour coqide + $(MKDIR) $(FULLCOQLIB)/tools/coqdoc + touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715) + $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc + $(INSTALLBIN) $(TOOLS) $(FULLBINDIR) + +# The list of .cmi to install, including the ones obtained +# from .mli without .ml, and the ones obtained from .ml without .mli + +INSTALLCMI = $(sort \ + $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ + $(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) + +install-devfiles: + $(MKDIR) $(FULLBINDIR) + $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA) + $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) +ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) +endif + +install-library: + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) + $(MKDIR) $(FULLCOQLIB)/user-contrib +ifndef CUSTOM + $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) +endif +ifeq ($(BEST),opt) + $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) +endif +# csdpcert is not meant to be directly called by the user; we install +# it with libraries + -$(MKDIR) $(FULLCOQLIB)/plugins/micromega + $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega + rm -f $(FULLCOQLIB)/revision + -$(INSTALLLIB) revision $(FULLCOQLIB) + +install-coq-info: install-coq-manpages install-emacs install-latex + +MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ + man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ + man/coqwc.1 man/coqdoc.1 man/coqide.1 \ + man/coq_makefile.1 man/coqmktop.1 man/coqchk.1 + +install-coq-manpages: + $(MKDIR) $(FULLMANDIR)/man1 + $(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1 + +install-emacs: + $(MKDIR) $(FULLEMACSLIB) + $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB) + +# command to update TeX' kpathsea database +#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null + +install-latex: + $(MKDIR) $(FULLCOQDOCDIR) + $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) +# -$(UPDATETEX) + +# For emacs: +# Local Variables: +# mode: makefile +# End: diff --git a/_tags b/_tags deleted file mode 100644 index 9f77416a0..000000000 --- a/_tags +++ /dev/null @@ -1,75 +0,0 @@ - -## tags for binaries - -<tools/coqmktop.{native,byte}> : use_str, use_unix -<tools/coqc.{native,byte}> : use_str, use_unix -<tools/coqdep_boot.{native,byte}> : use_unix -<tools/coqdep.{native,byte}> : use_str, use_unix -<tools/coq_tex.{native,byte}> : use_str -<tools/coq_makefile.{native,byte}> : use_str, use_unix -<tools/coqdoc/main.{native,byte}> : use_str -<ide/coqide_main.{native,byte}> : use_str, use_unix, ide -<checker/main.{native,byte}> : use_str, use_unix, thread -<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix -<tools/mkwinapp.{native,byte}> : use_unix -<tools/fake_ide.{native,byte}> : use_unix, use_str - -## tags for ide - -<ide/**/*.{ml,mli}>: ide - -## tags for grammar.cm* - -<grammar/grammar.{cma,cmxa}> : use_unix - -## tags for camlp4 files - -"parsing/g_constr.ml4": use_compat5 -"parsing/g_ltac.ml4": use_compat5 -"parsing/g_prim.ml4": use_compat5 -"parsing/g_proofs.ml4": use_compat5 -"parsing/g_tactic.ml4": use_compat5 -"parsing/g_vernac.ml4": use_compat5 -"parsing/g_xml.ml4": use_compat5 -"parsing/pcoq.ml4": use_compat5 -"parsing/g_obligations.ml4": use_grammar - -"grammar/argextend.ml4": use_compat5b -"grammar/tacextend.ml4": use_compat5b -"grammar/vernacextend.ml4": use_compat5b - -<tactics/*.ml4>: use_grammar - -<plugins/**/*.ml4>: use_grammar -"plugins/decl_mode/g_decl_mode.ml4": use_compat5 -"plugins/funind/g_indfun.ml4": use_compat5 - -## sub-directory inclusion - -# Note: "checker" is deliberately not included -# Note: same for "config" (we create a special coq_config.ml) - -"parsing": include -"ide": include -"ide/utils": include -"interp": include -"intf": include -"grammar": include -"kernel": include -"kernel/byterun": include -"lib": include -"library": include -"parsing": include -"plugins": include -"engine": include -"pretyping": include -"printing": include -"proofs": include -"stm": include -"tactics": include -"theories": include -"tools": include -"tools/coqdoc": include -"toplevel": include - -<plugins/**>: include diff --git a/build b/build deleted file mode 100755 index debf29cf4..000000000 --- a/build +++ /dev/null @@ -1,32 +0,0 @@ -#!/bin/sh - -FLAGS="-j 2" -OCAMLBUILD=ocamlbuild -MYCFG=myocamlbuild_config.ml - -export CAML_LD_LIBRARY_PATH=`pwd`/_build/kernel/byterun - -check_config() { - if [ ! -f $MYCFG ]; then echo "please run ./configure first"; exit 1; fi -} - -ocb() { $OCAMLBUILD $FLAGS $*; } - -rule() { - check_config - case $1 in - clean) ocb -clean && rm -rf bin/*;; - all) ocb coq.otarget;; - win32) ocb coq-win32.otarget;; - *) ocb $1;; - esac; -} - -if [ $# -eq 0 ]; then - rule all -else - while [ $# -gt 0 ]; do - rule $1; - shift - done -fi diff --git a/checker/check.ml b/checker/check.ml index 93eb2a0d2..da3cd0316 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -303,7 +303,7 @@ let intern_from_file (dir, f) = try let ch = System.with_magic_number_check raw_intern_library f in let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in - let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in + let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in let (discharging:'a option), _, _ = System.marshal_in_segment f ch in let (tasks:'a option), _, _ = System.marshal_in_segment f ch in diff --git a/checker/checker.ml b/checker/checker.ml index 61b13c60b..9d76fb09e 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -179,10 +179,7 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -I dir -as coqdir map physical dir to logical coqdir\ -\n -I dir map directory dir to the empty logical path\ -\n -include dir (idem)\ -\n -R dir coqdir recursively map physical dir to logical coqdir\ +" -R dir coqdir map physical dir to logical coqdir\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ diff --git a/configure.ml b/configure.ml index ade43810b..f2f239075 100644 --- a/configure.ml +++ b/configure.ml @@ -513,43 +513,32 @@ exception NoCamlp5 let check_camlp5 testcma = match !Prefs.camlp5dir with | Some dir -> - if Sys.file_exists (dir/testcma) then dir + if Sys.file_exists (dir/testcma) then + let camlp5o = + try which_camlpX "camlp5o" + with Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" in + dir, camlp5o else let msg = sprintf "Cannot find camlp5 libraries in '%s' (%s not found)." dir testcma in die msg | None -> - let dir,_ = tryrun "camlp5" ["-where"] in - let dir2 = - if Sys.file_exists (camllib/"camlp5"/testcma) then - camllib/"camlp5" - else if Sys.file_exists (camllib/"site-lib"/"camlp5"/testcma) then - camllib/"site-lib"/"camlp5" - else "" - in - (* if the two values are different then camlp5 has been relocated - * and will not be able to find its own files, so we prefer the - * path where the files actually do exist *) - if dir2 = "" then - if dir = "" then - let () = printf "No Camlp5 installation found." in - let () = printf "Looking for Camlp4 instead...\n" in - raise NoCamlp5 - else dir - else dir2 - -let check_camlp5_version () = - try - let camlp5o = which_camlpX "camlp5o" in - let version_line, _ = run ~err:StdOut camlp5o ["-v"] in - let version = List.nth (string_split ' ' version_line) 2 in - match string_split '.' version with - | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) -> - printf "You have Camlp5 %s. Good!\n" version; camlp5o, version - | _ -> failwith "bad version" - with - | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" + try + let camlp5o = which_camlpX "camlp5o" in + let dir,_ = tryrun camlp5o ["-where"] in + dir, camlp5o + with Not_found -> + let () = printf "No Camlp5 installation found." in + let () = printf "Looking for Camlp4 instead...\n" in + raise NoCamlp5 + +let check_camlp5_version camlp5o = + let version_line, _ = run ~err:StdOut camlp5o ["-v"] in + let version = List.nth (string_split ' ' version_line) 2 in + match string_split '.' version with + | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) -> + printf "You have Camlp5 %s. Good!\n" version; version | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n" let check_caml_version_for_camlp4 () = @@ -563,8 +552,8 @@ let config_camlpX () = try if not !Prefs.usecamlp5 then raise NoCamlp5; let camlp5mod = "gramlib" in - let camlp5libdir = check_camlp5 (camlp5mod^".cma") in - let camlp5o, camlp5_version = check_camlp5_version () in + let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in + let camlp5_version = check_camlp5_version camlp5o in "camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version with NoCamlp5 -> (* We now try to use Camlp4, either by explicit choice or @@ -1003,7 +992,7 @@ let write_dbg_wrapper f = let _ = write_dbg_wrapper "dev/ocamldebug-coq" -(** * Build the config/coq_config.ml file (+ link to myocamlbuild_config.ml) *) +(** * Build the config/coq_config.ml file *) let write_configml f = safe_remove f; @@ -1070,14 +1059,7 @@ let write_configml f = close_out o; Unix.chmod f 0o444 -let write_configml_my f f' = - write_configml f; - if os_type_win32 then - write_configml f' - else - (safe_remove f'; Unix.symlink f f') - -let _ = write_configml_my "config/coq_config.ml" "myocamlbuild_config.ml" +let _ = write_configml "config/coq_config.ml" (** * Build the config/Makefile file *) diff --git a/coq-win32.itarget b/coq-win32.itarget deleted file mode 100644 index 9e2c7a2b6..000000000 --- a/coq-win32.itarget +++ /dev/null @@ -1,2 +0,0 @@ -binariesopt -plugins/pluginsdyn.otarget diff --git a/coq.itarget b/coq.itarget deleted file mode 100644 index dd8b25905..000000000 --- a/coq.itarget +++ /dev/null @@ -1,8 +0,0 @@ -# NB: for the moment we start with bytecode compilation -# for early error detection in .ml -binariesbyte -plugins/pluginsbyte.otarget -binariesopt -plugins/pluginsopt.otarget -theories/theories.otarget -plugins/pluginsvo.otarget diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 4a0130bef..4135ddd2d 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -148,6 +148,38 @@ define_evar_* mostly used internally in the unification engine. - The Refine module was move out of Proofview. + Proofview.Refine.* ---> Refine.* + +- A statically monotonous evarmap type was introduced in Sigma. Not all the API + has been converted, so that the user may want to use compatibility functions + Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when + needed. Code can be straightforwardly adapted in the following way: + + let (sigma, x1) = ... in + ... + let (sigma, xn) = ... in + (sigma, ans) + + should be turned into: + + open Sigma.Notations + + let Sigma (x1, sigma, p1) = ... in + ... + let Sigma (xn, sigma, pn) = ... in + Sigma (ans, sigma, p1 +> ... +> pn) + +- The Proofview.Goal.*enter family of functions now takes a polymorphic + continuation given as a record as an argument. + + Proofview.Goal.enter begin fun gl -> ... end + + should be turned into + + open Proofview.Notations + + Proofview.Goal.enter { enter = begin fun gl -> ... end } + ========================================= = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = ========================================= diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt new file mode 100644 index 000000000..efedbc506 --- /dev/null +++ b/dev/doc/ocamlbuild.txt @@ -0,0 +1,30 @@ +Ocamlbuild & Coq +---------------- + +A quick note in case someone else gets interested someday in compiling +Coq via ocamlbuild : such an experimental build system has existed +in the past (more or less maintained from 2009 to 2013), in addition +to the official build system via gnu make. But this build via +ocamlbuild has been severly broken since early 2014 (and don't work +in 8.5, for instance). This experiment has attracted very limited +interest from other developers over the years, and has been quite +cumbersome to maintain, so it is now officially discontinued. +If you want to have a look at the files of this build system +(especially myocamlbuild.ml), you can fetch : + - my last effort at repairing this build system (up to coqtop.native) : + https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair + - coq official v8.5 branch (recent but broken) + - coq v8.4 branch(less up-to-date, but works). + +For the record, the three main drawbacks of this experiments were: + - recurrent issues with circularities reported by ocamlbuild + (even though make was happy) during the evolution of Coq sources + - no proper support of parallel build + - quite slow re-traversal of already built things +See the two corresponding bug reports on Mantis, or +https://github.com/ocaml/ocamlbuild/issues/52 + +As an interesting feature, I successfully used this to cross-compile +Coq 8.4 from linux to win32 via mingw. + +Pierre Letouzey, june 2016 diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt new file mode 100644 index 000000000..9d2ebf0d4 --- /dev/null +++ b/dev/doc/profiling.txt @@ -0,0 +1,76 @@ +# How to profile Coq? + +I (Pierre-Marie Pédrot) mainly use two OCaml branches to profile Coq, whether I +want to profile time or memory consumption. AFAIK, this only works for Linux. + +## Time + +In Coq source folder: + +opam switch 4.02.1+fp +./configure -local -debug +make +perf record -g bin/coqtop -compile file.v +perf report -g fractal,callee --no-children + +To profile only part of a file, first load it using + +bin/coqtop -l file.v + +and plug into the process + +perf record -g -p PID + +## Memory + +You first need a few commits atop trunk for this to work. + +git remote add ppedrot https://github.com/ppedrot/coq.git +git fetch ppedrot +git checkout ppedrot/allocation-profiling +git rebase master + +Then: + +opam switch 4.00.1+alloc-profiling +./configure -local -debug +make + +Note that linking the coqtop binary takes quite an amount of time with this +branch, so do not worry too much. There are more recent branches of +alloc-profiling on mshinwell's repo which can be found at: + +https://github.com/mshinwell/opam-repo-dev + +### For memory dump: + +CAMLRUNPARAM=T,mj bin/coqtop -compile file.v + +In another terminal: + +pkill -SIGUSR1 $COQTOPPID +... +pkill -SIGUSR1 $COQTOPPID +dev/decode-major-heap.sh heap.$COQTOPPID.$N bin/coqtop + +where $COQTOPPID is coqtop pid and $N the index of the call to pkill. + +First column is the memory taken by the objects (in words), second one is the +number of objects and third is the place where the objects where allocated. + +### For complete memory graph: + +CAMLRUNPARAM=T,gr bin/coqtop -compile file.v + +In another terminal: + +pkill -SIGUSR1 $COQTOPPID +... +pkill -SIGUSR1 $COQTOPPID +ocaml dev/decodegraph.ml edge.$COQTOPPID.$N bin/coqtop > memory.dot +dot -Tpdf -o memory.pdf memory.dot + +where $COQTOPPID is coqtop pid and $N the index of the call to pkill. + +The pdf produced by the last command gives a compact graphical representation of +the various objects allocated. diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi index e1052b1e1..80da84517 100755 --- a/dev/nsis/coq.nsi +++ b/dev/nsis/coq.nsi @@ -83,6 +83,7 @@ FunctionEnd Section "Coq" Sec1 SetOutPath "$INSTDIR\" + File ${COQ_SRC_PATH}\LICENSE SetOutPath "$INSTDIR\bin" File ${COQ_SRC_PATH}\bin\*.exe diff --git a/dev/printers.mllib b/dev/printers.mllib index 74b42842c..e39b78072 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -189,7 +189,6 @@ Logic Refiner Clenv Evar_refiner -Proof_errors Refine Proof Proof_global diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index a3372c296..275e1c2d5 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -4,7 +4,7 @@ \label{CS-full} \index{Canonical Structures!presentation} -This chapter explains the basics of Canonical Structure and how thy can be used +\noindent This chapter explains the basics of Canonical Structure and how they can be used to overload notations and build a hierarchy of algebraic structures. The examples are taken from~\cite{CSwcu}. We invite the interested reader to refer to this paper for all the details that are omitted here for brevity. diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index a08cd1475..36518e6fa 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -201,7 +201,8 @@ universes and explicitly instantiate polymorphic definitions. In the monorphic case, this command declares a new global universe named {\ident}. It supports the polymorphic flag only in sections, meaning the universe quantification will be discharged on each section definition -independently. +independently. One cannot mix polymorphic and monomorphic declarations +in the same section. \subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}. \comindex{Constraint} @@ -212,6 +213,7 @@ The order relation can be one of $<$, $\le$ or $=$. If consistent, the constraint is then enforced in the global environment. Like \texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix in sections only to declare constraints discharged at section closing time. +One cannot declare a global constraint on polymorphic universes. \begin{ErrMsgs} \item \errindex{Undeclared universe {\ident}}. diff --git a/engine/evarutil.mli b/engine/evarutil.mli index ffff2c5dd..111d0f3e8 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -11,7 +11,7 @@ open Term open Evd open Environ -(** {5 This modules provides useful functions for unification modulo evars } *) +(** This module provides useful higher-level functions for evar manipulation. *) (** {6 Metas} *) diff --git a/engine/evd.mli b/engine/evd.mli index 3ae6e586c..df491c27b 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -12,7 +12,10 @@ open Names open Term open Environ -(** {5 Existential variables and unification states} +(** This file defines the pervasive unification state used everywhere in Coq + tactic engine. It is very low-level and most of the functions exported here + are irrelevant to the standard API user. Consider using {!Evarutil}, + {!Sigma} or {!Proofview} instead. A unification state (of type [evar_map]) is primarily a finite mapping from existential variables to records containing the type of the evar @@ -23,6 +26,8 @@ open Environ It also contains conversion constraints, debugging information and information about meta variables. *) +(** {5 Existential variables and unification states} *) + (** {6 Evars} *) type evar = existential_key @@ -343,7 +348,6 @@ val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map - (** {5 Meta machinery} These functions are almost deprecated. They were used before the diff --git a/engine/ftactic.mli b/engine/ftactic.mli index 19041f169..5db373199 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -8,7 +8,9 @@ open Proofview.Notations -(** Potentially focussing tactics *) +(** This module defines potentially focussing tactics. They are used by Ltac to + emulate the historical behaviour of always-focussed tactics while still + allowing to remain global when the goal is not needed. *) type +'a focus diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 42e1e3784..b70671a2d 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Interpretation functions for generic arguments. *) +(** Interpretation functions for generic arguments and interpreted Ltac + values. *) open Names open Genarg diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index c5160443b..dd122cca0 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** This file defines the low-level monadic operations used by the +(** This file implements the low-level monadic operations used by the tactic monad. The monad is divided into two layers: a non-logical layer which consists in operations which will not (or cannot) be backtracked in case of failure (input/output or persistent state) diff --git a/engine/namegen.mli b/engine/namegen.mli index a2923fee9..e5c156b4e 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This file features facilities to generate fresh names. *) + open Names open Term open Environ diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 0aff0a720..637414cce 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -7,7 +7,8 @@ (************************************************************************) (** This file defines the datatypes used as internal states by the - tactic monad, and specialises the [Logic_monad] to these type. *) + tactic monad, and specialises the [Logic_monad] to these types. It should + not be used directly. Consider using {!Proofview} instead. *) (** {6 Traces} *) diff --git a/engine/sigma.mli b/engine/sigma.mli index 643bea403..aaf603efd 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -12,7 +12,9 @@ open Constr (** Monotonous state enforced by typing. This module allows to constrain uses of evarmaps in a monotonous fashion, - and in particular statically suppress evar leaks and the like. + and in particular statically suppress evar leaks and the like. To this + ends, it defines a type of indexed evarmaps whose phantom typing ensures + monotonous use. *) (** {5 Stages} *) @@ -32,7 +34,7 @@ val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le (** {5 Monotonous evarmaps} *) type 'r t -(** Stage-indexed evarmaps. *) +(** Stage-indexed evarmaps. This is just a plain evarmap with a phantom type. *) type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma (** Return values at a later stage *) diff --git a/engine/termops.mli b/engine/termops.mli index c2a4f3323..76a31037b 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This file defines various utilities for term manipulation that are not + needed in the kernel. *) + open Pp open Names open Term diff --git a/engine/uState.mli b/engine/uState.mli index c5c454020..0cdc6277a 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -6,7 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Universe unification states *) +(** This file defines universe unification states which are part of evarmaps. + Most of the API below is reexported in {!Evd}. Consider using higher-level + primitives when needed. *) open Names diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib deleted file mode 100644 index 6c3ce7f03..000000000 --- a/grammar/grammar.mllib +++ /dev/null @@ -1,5 +0,0 @@ -GramCompat -Q_util -Argextend -Tacextend -Vernacextend diff --git a/ide/coq.ml b/ide/coq.ml index 82fd48c9e..61f002576 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -357,7 +357,9 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = let print_exception = function | Xml_parser.Error e -> Xml_parser.error e - | Serialize.Marshal_error -> "Protocol violation" + | Serialize.Marshal_error(expected,actual) -> + "Protocol violation. Expected: " ^ expected ^ " Actual: " + ^ Xml_printer.to_string actual | e -> Printexc.to_string e let input_watch handle respawner feedback_processor = diff --git a/ide/coqide.ml b/ide/coqide.ml index 758a5a4c9..d1a799a77 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -677,12 +677,18 @@ let searchabout sn = let searchabout () = on_current_term searchabout +let doquery query sn = + sn.messages#clear; + Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore + let otherquery command sn = - let word = get_current_word sn in - if word <> "" then - let query = command ^ " " ^ word ^ "." in - sn.messages#clear; - Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore + Option.iter (fun query -> doquery (query ^ ".") sn) + begin try + let i = CString.string_index_from command 0 "..." in + let word = get_current_word sn in + if word = "" then None + else Some (CString.sub command 0 i ^ " " ^ word) + with Not_found -> Some command end let otherquery command = cb_on_current_term (otherquery command) @@ -859,12 +865,12 @@ let toggle_items menu_name l = in List.iter f l +let no_under = Util.String.map (fun x -> if x = '_' then '-' else x) + (** Create alphabetical menu items with elements in sub-items. [l] is a list of lists, one per initial letter *) let alpha_items menu_name item_name l = - let no_under = Util.String.map (fun x -> if x = '_' then '-' else x) - in let mk_item text = let text' = let last = String.length text - 1 in @@ -911,6 +917,16 @@ let template_item (text, offset, len, key) = in item name ~label ~callback:(cb_on_current_term callback) ~accel:(modifier^key) +(** Create menu items for pairs (query, shortcut key). *) +let user_queries_items menu_name item_name l = + let mk_item (query, key) = + let callback = Query.query query in + let accel = if not (CString.is_empty key) then + Some (modifier_for_queries#get^key) else None in + item (item_name^" "^(no_under query)) ~label:query ?accel ~callback menu_name + in + List.iter mk_item l + let emit_to_focus window sgn = let focussed_widget = GtkWindow.Window.get_focus window#as_window in let obj = Gobject.unsafe_cast focussed_widget in @@ -1100,16 +1116,22 @@ let build_ui () = ]; alpha_items templates_menu "Template" Coq_commands.commands; - let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in + let qitem s sc ?(dots = true) = + let query = if dots then s ^ "..." else s in + item s ~label:("_"^s) + ~accel:(modifier_for_queries#get^sc) + ~callback:(Query.query query) + in menu queries_menu [ item "Queries" ~label:"_Queries"; - qitem "Search" (Some "<Ctrl><Shift>K"); - qitem "Check" (Some "<Ctrl><Shift>C"); - qitem "Print" (Some "<Ctrl><Shift>P"); - qitem "About" (Some "<Ctrl><Shift>A"); - qitem "Locate" (Some "<Ctrl><Shift>L"); - qitem "Print Assumptions" (Some "<Ctrl><Shift>N"); + qitem "Search" "K" ~dots:false; + qitem "Check" "C"; + qitem "Print" "P"; + qitem "About" "A"; + qitem "Locate" "L"; + qitem "Print Assumptions" "N"; ]; + user_queries_items queries_menu "User-Query" user_queries#get; menu tools_menu [ item "Tools" ~label:"_Tools"; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index edfe28b26..2ae18593a 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -18,6 +18,15 @@ let list_items menu li = let () = List.iter (fun b -> Buffer.add_buffer res_buf (tactic_item b)) li in res_buf +let list_queries menu li = + let res_buf = Buffer.create 500 in + let query_item (q, _) = + let s = "<menuitem action='"^menu^" "^(no_under q)^"' />\n" in + Buffer.add_string res_buf s + in + let () = List.iter query_item li in + res_buf + let init () = let theui = Printf.sprintf "<ui> <menubar name='CoqIde MenuBar'> @@ -119,6 +128,8 @@ let init () = <menuitem action='About' /> <menuitem action='Locate' /> <menuitem action='Print Assumptions' /> + <separator /> + %s </menu> <menu name='Tools' action='Tools'> <menuitem action='Comment' /> @@ -162,5 +173,6 @@ let init () = (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "") (Buffer.contents (list_items "Tactic" Coq_commands.tactics)) (Buffer.contents (list_items "Template" Coq_commands.commands)) + (Buffer.contents (list_queries "User-Query" Preferences.user_queries#get)) in ignore (ui_m#add_ui_from_string theui); diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 0e09d8409..79affb36f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -281,11 +281,33 @@ let export_coq_object t = { Interface.coq_object_object = t.Search.coq_object_object } +let pattern_of_string ?env s = + let env = + match env with + | None -> Global.env () + | Some e -> e + in + let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in + let (_, pat) = Constrintern.intern_constr_pattern env constr in + pat + +let dirpath_of_string_list s = + let path = String.concat "." s in + let m = Pcoq.parse_string Pcoq.Constr.global path in + let (_, qid) = Libnames.qualid_of_reference m in + let id = + try Nametab.full_name_module qid + with Not_found -> + Errors.errorlabstrm "Search.interface_search" + (str "Module " ++ str path ++ str " not found.") + in + id + let import_search_constraint = function - | Interface.Name_Pattern s -> Search.Name_Pattern s - | Interface.Type_Pattern s -> Search.Type_Pattern s - | Interface.SubType_Pattern s -> Search.SubType_Pattern s - | Interface.In_Module ms -> Search.In_Module ms + | Interface.Name_Pattern s -> Search.Name_Pattern (Str.regexp s) + | Interface.Type_Pattern s -> Search.Type_Pattern (pattern_of_string s) + | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s) + | Interface.In_Module ms -> Search.In_Module (dirpath_of_string_list ms) | Interface.Include_Blacklist -> Search.Include_Blacklist let search flags = @@ -361,8 +383,6 @@ let init = match file with | None -> Stm.get_current_state () | Some file -> - if not (Filename.check_suffix file ".v") then - error "A file with suffix .v is expected."; let dir = Filename.dirname file in let open Loadpath in let open CUnix in let initial_id, _ = @@ -499,7 +519,7 @@ let loop () = | Xml_parser.Error (err, loc) -> pr_debug ("Syntax error in query: " ^ Xml_parser.error_msg err); exit 1 - | Serialize.Marshal_error -> + | Serialize.Marshal_error _ -> pr_debug "Incorrect query."; exit 1 | any -> diff --git a/ide/preferences.ml b/ide/preferences.ml index c4dc55972..3a33bbb1d 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -144,6 +144,18 @@ object method into s = Some s end +let string_pair_list (sep : char) : (string * string) list repr = +object + val sep' = String.make 1 sep + method from = CList.map (fun (s1, s2) -> CString.concat sep' [s1; s2]) + method into l = + try + Some (CList.map (fun s -> + let split = CString.split sep s in + CList.nth split 0, CList.nth split 1) l) + with Failure _ -> None +end + let bool : bool repr = object method from s = [string_of_bool s] @@ -303,10 +315,14 @@ let modifier_for_tactics = let modifier_for_display = new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string) +let modifier_for_queries = + new preference ~name:["modifier_for_queries"] ~init:"<Control><Shift>" ~repr:Repr.(string) + let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/" let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/" let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/" let _ = attach_modifiers modifier_for_display "<Actions>/View/" +let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/" let modifiers_valid = new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string) @@ -507,6 +523,9 @@ let highlight_current_line = let nanoPG = new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool) +let user_queries = + new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$') + class tag_button (box : Gtk.box Gtk.obj) = object (self) @@ -837,6 +856,9 @@ let configure ?(apply=(fun () -> ())) () = let modifier_for_display = pmodifiers "Modifiers for View Menu" modifier_for_display in + let modifier_for_queries = + pmodifiers "Modifiers for Queries Menu" modifier_for_queries + in let modifiers_valid = pmodifiers ~all:true "Allowed modifiers" modifiers_valid in @@ -908,6 +930,36 @@ let configure ?(apply=(fun () -> ())) () = let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch; vertical_tabs;opposite_tabs] in + let add_user_query () = + let input_string l v = + match GToolbox.input_string ~title:l v with + | None -> "" + | Some s -> s + in + let q = input_string "User query" "Your query" in + let k = input_string "Shortcut key" "Shortcut (a single letter)" in + let q = CString.map (fun c -> if c = '$' then ' ' else c) q in + (* Anything that is not a simple letter will be ignored. *) + let k = + if Int.equal (CString.length k) 1 && Util.is_letter k.[0] then k + else "" in + let k = CString.uppercase k in + [q, k] + in + + let user_queries = + list + ~f:user_queries#set + (* Disallow same query, key or empty query. *) + ~eq:(fun (q1, k1) (q2, k2) -> k1 = k2 || q1 = "" || q2 = "" || q1 = q2) + ~add:add_user_query + ~titles:["User query"; "Shortcut key"] + "User queries" + (fun (q, s) -> [q; s]) + user_queries#get + + in + (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! (shame on Benjamin) *) let cmds = @@ -937,9 +989,10 @@ let configure ?(apply=(fun () -> ())) () = [automatic_tactics]); Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; - modifier_for_templates; modifier_for_display; modifier_for_navigation]); + modifier_for_templates; modifier_for_display; modifier_for_navigation; + modifier_for_queries; user_queries]); Section("Misc", Some `ADD, - misc)] + misc)] in (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font); diff --git a/ide/preferences.mli b/ide/preferences.mli index 1733091a5..426b0a328 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -65,6 +65,7 @@ val modifier_for_navigation : string preference val modifier_for_templates : string preference val modifier_for_tactics : string preference val modifier_for_display : string preference +val modifier_for_queries : string preference val modifiers_valid : string preference val cmd_browse : string preference val cmd_editor : string preference @@ -95,6 +96,7 @@ val spaces_instead_of_tabs : bool preference val tab_length : int preference val highlight_current_line : bool preference val nanoPG : bool preference +val user_queries : (string * string) list preference val save_pref : unit -> unit val load_pref : unit -> unit diff --git a/ide/serialize.ml b/ide/serialize.ml index 685ec6049..7b568501e 100644 --- a/ide/serialize.ml +++ b/ide/serialize.ml @@ -8,7 +8,7 @@ open Xml_datatype -exception Marshal_error +exception Marshal_error of string * xml (** Utility functions *) @@ -19,30 +19,31 @@ let rec get_attr attr = function let massoc x l = try get_attr x l - with Not_found -> raise Marshal_error + with Not_found -> raise (Marshal_error("attribute " ^ x,PCData "not there")) let constructor t c args = Element (t, ["val", c], args) let do_match t mf = function | Element (s, attrs, args) when CString.equal s t -> let c = massoc "val" attrs in mf c args - | _ -> raise Marshal_error + | x -> raise (Marshal_error (t,x)) let singleton = function | [x] -> x - | _ -> raise Marshal_error + | l -> raise (Marshal_error + ("singleton",PCData ("list of length " ^ string_of_int (List.length l)))) let raw_string = function | [] -> "" | [PCData s] -> s - | _ -> raise Marshal_error + | x::_ -> raise (Marshal_error("raw string",x)) (** Base types *) let of_unit () = Element ("unit", [], []) let to_unit : xml -> unit = function | Element ("unit", [], []) -> () - | _ -> raise Marshal_error + | x -> raise (Marshal_error ("unit",x)) let of_bool (b : bool) : xml = if b then constructor "bool" "true" [] @@ -50,13 +51,13 @@ let of_bool (b : bool) : xml = let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with | "true" -> true | "false" -> false - | _ -> raise Marshal_error) + | x -> raise (Marshal_error("bool",PCData x))) let of_list (f : 'a -> xml) (l : 'a list) = Element ("list", [], List.map f l) let to_list (f : xml -> 'a) : xml -> 'a list = function | Element ("list", [], l) -> List.map f l - | _ -> raise Marshal_error + | x -> raise (Marshal_error("list",x)) let of_option (f : 'a -> xml) : 'a option -> xml = function | None -> Element ("option", ["val", "none"], []) @@ -64,24 +65,24 @@ let of_option (f : 'a -> xml) : 'a option -> xml = function let to_option (f : xml -> 'a) : xml -> 'a option = function | Element ("option", ["val", "none"], []) -> None | Element ("option", ["val", "some"], [x]) -> Some (f x) - | _ -> raise Marshal_error + | x -> raise (Marshal_error("option",x)) let of_string (s : string) : xml = Element ("string", [], [PCData s]) let to_string : xml -> string = function | Element ("string", [], l) -> raw_string l - | _ -> raise Marshal_error + | x -> raise (Marshal_error("string",x)) let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)]) let to_int : xml -> int = function | Element ("int", [], [PCData s]) -> - (try int_of_string s with Failure _ -> raise Marshal_error) - | _ -> raise Marshal_error + (try int_of_string s with Failure _ -> raise(Marshal_error("int",PCData s))) + | x -> raise (Marshal_error("int",x)) let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml = Element ("pair", [], [f (fst x); g (snd x)]) let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function | Element ("pair", [], [x; y]) -> (f x, g y) - | _ -> raise Marshal_error + | x -> raise (Marshal_error("pair",x)) let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function | CSig.Inl x -> Element ("union", ["val","in_l"], [f x]) @@ -89,7 +90,7 @@ let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = funct let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x) | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x) - | _ -> raise Marshal_error + | x -> raise (Marshal_error("union",x)) (** More elaborate types *) @@ -99,7 +100,7 @@ let to_edit_id = function let id = int_of_string i in assert (id <= 0 ); id - | _ -> raise Marshal_error + | x -> raise (Marshal_error("edit_id",x)) let of_loc loc = let start, stop = Loc.unloc loc in @@ -107,14 +108,14 @@ let of_loc loc = let to_loc xml = match xml with | Element ("loc", l,[]) -> + let start = massoc "start" l in + let stop = massoc "stop" l in (try - let start = massoc "start" l in - let stop = massoc "stop" l in Loc.make_loc (int_of_string start, int_of_string stop) - with Not_found | Invalid_argument _ -> raise Marshal_error) - | _ -> raise Marshal_error + with Not_found | Invalid_argument _ -> raise (Marshal_error("loc",PCData(start^":"^stop)))) + | x -> raise (Marshal_error("loc",x)) let of_xml x = Element ("xml", [], [x]) let to_xml xml = match xml with | Element ("xml", [], [x]) -> x -| _ -> raise Marshal_error +| x -> raise (Marshal_error("xml",x)) diff --git a/ide/serialize.mli b/ide/serialize.mli index d7c14e7e7..bf9e184eb 100644 --- a/ide/serialize.mli +++ b/ide/serialize.mli @@ -8,7 +8,7 @@ open Xml_datatype -exception Marshal_error +exception Marshal_error of string * xml val massoc: string -> (string * string) list -> string val constructor: string -> string -> xml list -> xml diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 45279a7c3..a55d19aa1 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -39,7 +39,7 @@ let to_search_cst = do_match "search_cst" (fun s args -> match s with | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) | "in_module" -> In_Module (to_list to_string (singleton args)) | "include_blacklist" -> Include_Blacklist - | _ -> raise Marshal_error) + | x -> raise (Marshal_error("search",PCData x))) let of_coq_object f ans = let prefix = of_list of_string ans.coq_object_prefix in @@ -56,7 +56,7 @@ let to_coq_object f = function coq_object_qualid = qualid; coq_object_object = obj; } -| _ -> raise Marshal_error +| x -> raise (Marshal_error("coq_object",x)) let of_option_value = function | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i] @@ -68,7 +68,7 @@ let to_option_value = do_match "option_value" (fun s args -> match s with | "boolvalue" -> BoolValue (to_bool (singleton args)) | "stringvalue" -> StringValue (to_string (singleton args)) | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args)) - | _ -> raise Marshal_error) + | x -> raise (Marshal_error("*value",PCData x))) let of_option_state s = Element ("option_state", [], [ @@ -82,7 +82,7 @@ let to_option_state = function opt_depr = to_bool depr; opt_name = to_string name; opt_value = to_option_value value } - | _ -> raise Marshal_error + | x -> raise (Marshal_error("option_state",x)) let to_stateid = function | Element ("state_id",["val",i],[]) -> @@ -95,7 +95,7 @@ let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)], let of_richpp x = Element ("richpp", [], [Richpp.repr x]) let to_richpp xml = match xml with | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x - | _ -> raise Serialize.Marshal_error + | x -> raise Serialize.(Marshal_error("richpp",x)) let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) @@ -116,14 +116,14 @@ let to_value f = function let loc_s = int_of_string (Serialize.massoc "loc_s" attrs) in let loc_e = int_of_string (Serialize.massoc "loc_e" attrs) in Some (loc_s, loc_e) - with Marshal_error | Failure _ -> None + with Marshal_error _ | Failure _ -> None in - let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise Marshal_error in + let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in let id = to_stateid id in let msg = to_richpp msg in Fail (id, loc, msg) - else raise Marshal_error -| _ -> raise Marshal_error + else raise (Marshal_error("good or fail",PCData ans)) +| x -> raise (Marshal_error("value",x)) let of_status s = let of_so = of_option of_string in @@ -139,12 +139,12 @@ let to_status = function status_proofname = to_option to_string name; status_allproofs = to_list to_string prfs; status_proofnum = to_int pnum; } - | _ -> raise Marshal_error + | x -> raise (Marshal_error("status",x)) let of_evar s = Element ("evar", [], [PCData s.evar_info]) let to_evar = function | Element ("evar", [], data) -> { evar_info = raw_string data; } - | _ -> raise Marshal_error + | x -> raise (Marshal_error("evar",x)) let of_goal g = let hyp = of_list of_richpp g.goal_hyp in @@ -157,7 +157,7 @@ let to_goal = function let ccl = to_richpp ccl in let id = to_string id in { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } - | _ -> raise Marshal_error + | x -> raise (Marshal_error("goal",x)) let of_goals g = let of_glist = of_list of_goal in @@ -175,7 +175,7 @@ let to_goals = function let given_up = to_list to_goal given_up in { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; given_up_goals = given_up } - | _ -> raise Marshal_error + | x -> raise (Marshal_error("goals",x)) let of_coq_info info = let version = of_string info.coqtop_version in @@ -189,7 +189,7 @@ let to_coq_info = function protocol_version = to_string protocol; release_date = to_string release; compile_date = to_string compile; } - | _ -> raise Marshal_error + | x -> raise (Marshal_error("coq_info",x)) end include Xml_marshalling @@ -695,7 +695,7 @@ let to_call : xml -> unknown_call = | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a)) | "PrintAst" -> Unknown (PrintAst (mkCallArg print_ast_sty_t a)) | "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a)) - | _ -> raise Marshal_error) + | x -> raise (Marshal_error("call",PCData x))) (** Debug printing *) @@ -782,12 +782,16 @@ let to_message_level = | "notice" -> Notice | "warning" -> Warning | "error" -> Error - | _ -> raise Serialize.Marshal_error) + | x -> raise Serialize.(Marshal_error("error level",PCData x))) let of_message lvl msg = let lvl = of_message_level lvl in let content = of_richpp msg in Xml_datatype.Element ("message", [], [lvl; content]) +let to_message xml = match xml with + | Xml_datatype.Element ("message", [], [lvl; content]) -> + Message(to_message_level lvl, to_richpp content) + | x -> raise (Marshal_error("message",x)) let is_message = function | Xml_datatype.Element ("message", [], [lvl; content]) -> @@ -811,15 +815,13 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with let n, s = to_pair to_string to_string ns in WorkerStatus(n,s) | "goals", [loc;s] -> Goals (to_loc loc, to_string s) - (* | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) *) + | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) | "filedependency", [from; dep] -> FileDependency (to_option to_string from, to_string dep) | "fileloaded", [dirpath; filename] -> FileLoaded (to_string dirpath, to_string filename) - | "message", [lvl; content] -> - Message (to_message_level lvl, to_richpp content) - - | _ -> raise Marshal_error) + | "message", [x] -> to_message x + | x,l -> raise (Marshal_error("feedback_content",PCData (x ^ " with attributes " ^ string_of_int (List.length l))))) let of_feedback_content = function | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] @@ -849,8 +851,8 @@ let of_feedback_content = function [of_pair of_string of_string (n,s)] | Goals (loc,s) -> constructor "feedback_content" "goals" [of_loc loc;of_string s] - (* | Custom (loc, name, x) -> *) - (* constructor "feedback_content" "custom" [of_loc loc; of_string name; x] *) + | Custom (loc, name, x) -> + constructor "feedback_content" "custom" [of_loc loc; of_string name; x] | FileDependency (from, depends_on) -> constructor "feedback_content" "filedependency" [ of_option of_string from; @@ -880,7 +882,7 @@ let to_feedback xml = match xml with id = State(to_stateid id); route = int_of_string route; contents = to_feedback_content content } - | _ -> raise Marshal_error + | x -> raise (Marshal_error("feedback",x)) let is_feedback = function | Element ("feedback", _, _) -> true diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e5ccb76b4..57091ca89 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -481,15 +481,15 @@ let explicitize loc inctx impl (cf,f) args = (!print_implicits && !print_implicits_explicit_args) || (is_needed_for_correct_partial_application tail imp) || (!print_implicits_defensive && - is_significant_implicit a && - not (is_inferable_implicit inctx n imp)) + not (is_inferable_implicit inctx n imp) && + is_significant_implicit (Lazy.force a)) in if visible then - (a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail + (Lazy.force a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail else tail - | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl) - | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*) + | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl) + | args, [] -> List.map (fun a -> (Lazy.force a,None)) args (*In case of polymorphism*) | [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp -> (* The non-explicit application cannot be parsed back with the same type *) raise Expl @@ -516,7 +516,7 @@ let explicitize loc inctx impl (cf,f) args = with Expl -> let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in let ip = if !print_projections then ip else None in - CAppExpl (loc, (ip, f', us), args) + CAppExpl (loc, (ip, f', us), List.map Lazy.force args) let is_start_implicit = function | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp @@ -538,19 +538,21 @@ let extern_app loc inctx impl (cf,f) us args = (!print_implicits && not !print_implicits_explicit_args)) && List.exists is_status_implicit impl) then + let args = List.map Lazy.force args in CAppExpl (loc, (is_projection (List.length args) cf,f,us), args) else explicitize loc inctx impl (cf,CRef (f,us)) args -let rec extern_args extern scopes env args subscopes = - match args with - | [] -> [] - | a::args -> - let argscopes, subscopes = match subscopes with - | [] -> (None,scopes), [] - | scopt::subscopes -> (scopt,scopes), subscopes in - extern argscopes env a :: extern_args extern scopes env args subscopes +let rec fill_arg_scopes args subscopes scopes = match args, subscopes with +| [], _ -> [] +| a :: args, scopt :: subscopes -> + (a, (scopt, scopes)) :: fill_arg_scopes args subscopes scopes +| a :: args, [] -> + (a, (None, scopes)) :: fill_arg_scopes args [] scopes +let extern_args extern env args = + let map (arg, argscopes) = lazy (extern argscopes env arg) in + List.map map args let match_coercion_app = function | GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args) @@ -647,8 +649,7 @@ let rec extern inctx scopes vars r = (match f with | GRef (rloc,ref,us) -> let subscopes = find_arguments_scope ref in - let args = - extern_args (extern true) (snd scopes) vars args subscopes in + let args = fill_arg_scopes args subscopes (snd scopes) in begin try if !Flags.raw_print then raise Exit; @@ -683,12 +684,14 @@ let rec extern inctx scopes vars r = match args with | [] -> raise No_match (* we give up since the constructor is not complete *) - | head :: tail -> ip q locs' tail - ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) + | (arg, scopes) :: tail -> + let head = extern true scopes vars arg in + ip q locs' tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) in CRecord (loc, List.rev (ip projs locals args [])) with | Not_found | No_match | Exit -> + let args = extern_args (extern true) vars args in extern_app loc inctx (select_stronger_impargs (implicits_of_global ref)) (Some ref,extern_reference rloc vars ref) (extern_universes us) args @@ -696,7 +699,7 @@ let rec extern inctx scopes vars r = | _ -> explicitize loc inctx [] (None,sub_extern false scopes vars f) - (List.map (sub_extern true scopes vars) args)) + (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) | GLetIn (loc,na,t,c) -> CLetIn (loc,(loc,na),sub_extern false scopes vars t, @@ -916,7 +919,8 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function if List.is_empty l then a else CApp (loc,(None,a),l) in if List.is_empty args then e else - let args = extern_args (extern true) scopes vars args argsscopes in + let args = fill_arg_scopes args argsscopes scopes in + let args = extern_args (extern true) vars args in explicitize loc false argsimpls (None,e) args with No_match -> extern_notation allscopes vars t rules diff --git a/kernel/closure.ml b/kernel/closure.ml index 65123108f..960bdb649 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -363,6 +363,7 @@ let set_norm v = v.norm <- Norm let is_val v = match v.norm with Norm -> true | _ -> false let mk_atom c = {norm=Norm;term=FAtom c} +let mk_red f = {norm=Red;term=f} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) diff --git a/kernel/closure.mli b/kernel/closure.mli index 07176cb7d..8e172290f 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -164,6 +164,9 @@ val inject : constr -> fconstr (** mk_atom: prevents a term from being evaluated *) val mk_atom : constr -> fconstr +(** mk_red: makes a reducible term (used in newring) *) +val mk_red : fterm -> fconstr + val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : diff --git a/kernel/constr.mli b/kernel/constr.mli index f76b5ae4f..42d298e3b 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This file defines the most important datatype of Coq, namely kernel terms, + as well as a handful of generic manipulation functions. *) + open Names (** {6 Value under universe substitution } *) diff --git a/kernel/names.mli b/kernel/names.mli index 56f0f8c60..feaedc775 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -6,6 +6,20 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This file defines a lot of different notions of names used pervasively in + the kernel as well as in other places. The essential datatypes exported by + this API are: + + - Id.t is the type of identifiers, that is morally a subset of strings which + only contains Unicode characters of the Letter kind (and a few more). + - Name.t is an ad-hoc variant of Id.t option allowing to handle optionally + named objects. + - DirPath.t represents generic paths as sequences of identifiers. + - Label.t is an equivalent of Id.t made distinct for semantical purposes. + - ModPath.t are module paths. + - KerName.t are absolute names of objects in Coq. +*) + open Util (** {6 Identifiers } *) diff --git a/lib/genarg.mli b/lib/genarg.mli index b8bb6af04..d7ad9b93b 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Generic arguments used by the extension mechanisms of several Coq ASTs. *) + (** The route of a generic argument, from parsing to evaluation. In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. @@ -34,36 +36,10 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. effective use {% \end{%}verbatim{% }%} -To distinguish between the uninterpreted (raw), globalized and +To distinguish between the uninterpreted, globalized and interpreted worlds, we annotate the type [generic_argument] by a -phantom argument which is either [constr_expr], [glob_constr] or -[constr]. +phantom argument. -Transformation for each type : -{% \begin{%}verbatim{% }%} -tag raw open type cooked closed type - -BoolArgType bool bool -IntArgType int int -IntOrVarArgType int or_var int -StringArgType string (parsed w/ "") string -PreIdentArgType string (parsed w/o "") (vernac only) -IdentArgType true identifier identifier -IdentArgType false identifier (pattern_ident) identifier -IntroPatternArgType intro_pattern_expr intro_pattern_expr -VarArgType identifier located identifier -RefArgType reference global_reference -QuantHypArgType quantified_hypothesis quantified_hypothesis -ConstrArgType constr_expr constr -ConstrMayEvalArgType constr_expr may_eval constr -OpenConstrArgType open_constr_expr open_constr -ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings -BindingsArgType constr_expr bindings constr bindings -List0ArgType of argument_type -List1ArgType of argument_type -OptArgType of argument_type -ExtraArgType of string '_a '_b -{% \end{%}verbatim{% }%} *) (** {5 Generic types} *) @@ -77,14 +53,14 @@ sig val name : string -> any option end +(** Generic types. The first parameter is the OCaml lowest level, the second one + is the globalized level, and third one the internalized level. *) type (_, _, _) genarg_type = | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type | ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type | OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type | PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type -(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized - one, and ['top] the internalized one. *) type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type (** Alias for concision when the three types agree. *) @@ -99,21 +75,18 @@ val create_arg : string -> ('raw, 'glob, 'top) genarg_type (** {5 Specialized types} *) (** All of [rlevel], [glevel] and [tlevel] must be non convertible - to ensure the injectivity of the type inference from type - ['co generic_argument] to [('a,'co) abstract_argument_type]; - this guarantees that, for 'co fixed, the type of - out_gen is monomorphic over 'a, hence type-safe -*) + to ensure the injectivity of the GADT type inference. *) type rlevel = [ `rlevel ] type glevel = [ `glevel ] type tlevel = [ `tlevel ] +(** Generic types at a fixed level. The first parameter embeds the OCaml type + and the second one the level. *) type (_, _) abstract_argument_type = | Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type | Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type | Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type -(** Type at level ['co] represented by an OCaml value of type ['a]. *) type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type (** Specialized type at raw level. *) @@ -207,9 +180,11 @@ sig end -(** {5 Basic generic type constructors} *) +(** {5 Compatibility layer} + +The functions below are aliases for generic_type constructors. -(** {6 Parameterized types} *) +*) val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type diff --git a/library/declare.ml b/library/declare.ml index b0df32b8d..84284fd18 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -440,8 +440,9 @@ let cache_universes (p, l) = let glob = Universes.global_universe_names () in let glob', ctx = List.fold_left (fun ((idl,lid),ctx) (id, lev) -> - ((Idmap.add id lev idl, Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) + ((Idmap.add id (p, lev) idl, + Univ.LMap.add lev id lid), + Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in Global.push_context_set p ctx; @@ -457,6 +458,12 @@ let input_universes : universe_decl -> Libobject.obj = classify_function = (fun a -> Keep a) } let do_universe poly l = + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err_loc (Loc.ghost, "Constraint", + str"Cannot declare polymorphic universes outside sections") + in let l = List.map (fun (l, id) -> let lev = Universes.new_univ_level (Global.current_dirpath ()) in @@ -485,14 +492,30 @@ let input_constraints : constraint_decl -> Libobject.obj = let do_constraint poly l = let u_of_id = let names, _ = Universes.global_universe_names () in - fun (loc, id) -> - try Idmap.find id names - with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + fun (loc, id) -> + try Idmap.find id names + with Not_found -> + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + in + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err_loc (Loc.ghost, "Constraint", + str"Cannot declare polymorphic constraints outside sections") + in + let check_poly loc p loc' p' = + if poly then () + else if p || p' then + let loc = if p then loc else loc' in + user_err_loc (loc, "Constraint", + str "Cannot declare a global constraint on " ++ + str "a polymorphic universe, use " + ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let lu = u_of_id l and ru = u_of_id r in - Univ.Constraint.add (lu, d, ru) acc) + let p, lu = u_of_id l and p', ru = u_of_id r in + check_poly (fst l) p (fst r) p'; + Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in Lib.add_anonymous_leaf (input_constraints (poly, constraints)) diff --git a/library/library.ml b/library/library.ml index 192700be7..4d0082850 100644 --- a/library/library.ml +++ b/library/library.ml @@ -35,7 +35,7 @@ module Delayed : sig type 'a delayed -val in_delayed : string -> in_channel -> 'a delayed +val in_delayed : string -> in_channel -> 'a delayed * Digest.t val fetch_delayed : 'a delayed -> 'a end = @@ -50,7 +50,7 @@ type 'a delayed = { let in_delayed f ch = let pos = pos_in ch in let _, digest = System.skip_in_segment f ch in - { del_file = f; del_digest = digest; del_off = pos; } + ({ del_file = f; del_digest = digest; del_off = pos; }, digest) (** Fetching a table of opaque terms at position [pos] in file [f], expecting to find first a copy of [digest]. *) @@ -427,23 +427,23 @@ let mk_summary m = { let intern_from_file f = let ch = raw_intern_library f in let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in - let (lmd : seg_lib delayed) = in_delayed f ch in + let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in let _ = System.skip_in_segment f ch in let _ = System.skip_in_segment f ch in - let (del_opaque : seg_proofs delayed) = in_delayed f ch in + let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in close_in ch; register_library_filename lsd.md_name f; add_opaque_table lsd.md_name (ToFetch del_opaque); let open Safe_typing in match univs with - | None -> mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty + | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty | Some (utab,uall,true) -> add_univ_table lsd.md_name (Fetched utab); - mk_library lsd lmd (Dvivo (digest_lsd,digest_u)) uall + mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall | Some (utab,_,false) -> add_univ_table lsd.md_name (Fetched utab); - mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty + mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty module DPMap = Map.Make(DirPath) diff --git a/library/universes.ml b/library/universes.ml index c4eb2afcb..75cbd5604 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -13,10 +13,11 @@ open Term open Environ open Univ open Globnames +open Decl_kinds (** Global universe names *) type universe_names = - Univ.universe_level Idmap.t * Id.t Univ.LMap.t + (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t let global_universes = Summary.ref ~name:"Global universe names" diff --git a/library/universes.mli b/library/universes.mli index 53cf5f384..a5740ec49 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -19,7 +19,7 @@ val is_set_minimization : unit -> bool (** Global universe name <-> level mapping *) type universe_names = - Univ.universe_level Idmap.t * Id.t Univ.LMap.t + (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t val global_universe_names : unit -> universe_names val set_global_universe_names : universe_names -> unit diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index d39f83552..7cda7d137 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -424,7 +424,7 @@ let intern_hyp_location ist ((occs,id),hl) = (* Reads a pattern *) let intern_pattern ist ?(as_type=false) ltacvars = function | Subterm (b,ido,pc) -> - let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in + let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in ido, metas, Subterm (b,ido,pc) | Term pc -> let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in @@ -446,7 +446,7 @@ let opt_cons accu = function | Some id -> Id.Set.add id accu (* Reads the hypotheses of a "match goal" rule *) -let rec intern_match_goal_hyps ist lfun = function +let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function | (Hyp ((_,na) as locna,mp))::tl -> let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in @@ -455,7 +455,7 @@ let rec intern_match_goal_hyps ist lfun = function | (Def ((_,na) as locna,mv,mp))::tl -> let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in - let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in + let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in let lfun' = name_cons (opt_cons (opt_cons lfun ido) ido') na in lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps | [] -> lfun, [], [] @@ -564,7 +564,7 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u) | TacMatchGoal (lz,lr,lmr) -> - ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr)) + ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist ~as_type:true lmr)) | TacMatch (lz,c,lmr) -> ist.ltacvars, TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr) @@ -666,18 +666,18 @@ and intern_tacarg strict onlytac ist = function TacGeneric arg (* Reads the rules of a Match Context or a Match *) -and intern_match_rule onlytac ist = function +and intern_match_rule onlytac ist ?(as_type=false) = function | (All tc)::tl -> - All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl) + All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist ~as_type tl) | (Pat (rl,mp,tc))::tl -> let {ltacvars=lfun; genv=env} = ist in - let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in - let ido,metas2,pat = intern_pattern ist lfun mp in + let lfun',metas1,hyps = intern_match_goal_hyps ist ~as_type lfun rl in + let ido,metas2,pat = intern_pattern ist ~as_type lfun mp in let fold accu x = Id.Set.add x accu in let ltacvars = List.fold_left fold (opt_cons lfun' ido) metas1 in let ltacvars = List.fold_left fold ltacvars metas2 in let ist' = { ist with ltacvars } in - Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl) + Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist ~as_type tl) | [] -> [] and intern_genarg ist (GenArg (Rawwit wit, x)) = diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml index d661f9677..e657eb9bc 100644 --- a/ltac/tactic_debug.ml +++ b/ltac/tactic_debug.ml @@ -330,10 +330,9 @@ let db_breakpoint debug s = let is_defined_ltac trace = let rec aux = function - | (_, Tacexpr.LtacNameCall f) :: tail -> - not (Tacenv.is_ltac_for_ml_tactic f) - | (_, Tacexpr.LtacAtomCall _) :: tail -> - false + | (_, Tacexpr.LtacNameCall f) :: _ -> not (Tacenv.is_ltac_for_ml_tactic f) + | (_, Tacexpr.LtacNotationCall f) :: _ -> true + | (_, Tacexpr.LtacAtomCall _) :: _ -> false | _ :: tail -> aux tail | [] -> false in aux (List.rev trace) @@ -341,7 +340,7 @@ let is_defined_ltac trace = let explain_ltac_call_trace last trace loc = let calls = last :: List.rev_map snd trace in let pr_call ck = match ck with - | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn) + | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn) | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst) | Tacexpr.LtacMLCall t -> quote (Pptactic.pr_glob_tactic (Global.env()) t) @@ -363,6 +362,7 @@ let explain_ltac_call_trace last trace loc = in match calls with | [] -> mt () + | [a] -> hov 0 (str "Ltac call to " ++ pr_call a ++ str " failed.") | _ -> let kind_of_last_call = match List.last calls with | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed." @@ -373,10 +373,13 @@ let explain_ltac_call_trace last trace loc = let skip_extensions trace = let rec aux = function - | (_,Tacexpr.LtacNameCall f as tac) :: _ - when Tacenv.is_ltac_for_ml_tactic f -> [tac] - | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac) - :: _ -> [tac] + | (_,Tacexpr.LtacNameCall f as tac) :: _ + when Tacenv.is_ltac_for_ml_tactic f -> [tac] + | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ -> + (* Case of an ML defined tactic with entry of the form <<"foo" args>> *) + (* see tacextend.mlp *) + [tac] + | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac] | t :: tail -> t :: aux tail | [] -> [] in List.rev (aux (List.rev trace)) diff --git a/myocamlbuild.ml b/myocamlbuild.ml deleted file mode 100644 index b81b280ff..000000000 --- a/myocamlbuild.ml +++ /dev/null @@ -1,482 +0,0 @@ -(** * Plugin for building Coq via Ocamlbuild *) - -open Ocamlbuild_plugin -open Ocamlbuild_pack -open Printf -open Scanf - -(** WARNING !! this is preliminary stuff. It should allows you to - build coq and its libraries if everything goes right. - Support for all the build rules and configuration options - is progressively added. Tested only on linux + ocaml 3.11 + - local + natdynlink for now. - - Usage: - ./configure -local -opt - ./build (which launches ocamlbuild coq.otarget) - - Then you can (hopefully) launch bin/coqtop, bin/coqide and so on. - Apart from the links in bin, every created files are in _build. - A "./build clean" should give you back a clean source tree - -*) - -(** F.A.Q about ocamlbuild: - -* P / Px ? - - Same, except that the second can be use to signal the main target - of a rule, in order to get a nicer log (otherwise the full command - is used as target name) - -*) - - - -(** Generic file reader, which produces a list of strings, one per line *) - -let read_file f = - let ic = open_in f and l = ref [] in - (try while true do l := (input_line ic)::!l done with End_of_file -> ()); - close_in ic; List.rev !l - - -(** Configuration *) - -(** First, we access coq_config.ml indirectly : we symlink it to - myocamlbuild_config.ml, which is linked with this myocamlbuild.ml *) - -module Coq_config = struct include Myocamlbuild_config end - -let _ = begin - Options.ocamlc := A Coq_config.ocamlc; - Options.ocamlopt := A Coq_config.ocamlopt; - Options.ocamlmklib := A Coq_config.ocamlmklib; - Options.ocamldep := A Coq_config.ocamldep; - Options.ocamldoc := A Coq_config.ocamldoc; - Options.ocamlyacc := A Coq_config.ocamlyacc; - Options.ocamllex := A Coq_config.ocamllex; -end - -let w32 = Coq_config.arch_is_win32 - -let w32pref = "i586-mingw32msvc" -let w32ocamlc = w32pref^"-ocamlc" -let w32ocamlopt = w32pref^"-ocamlopt" -let w32ocamlmklib = w32pref^"-ocamlmklib" -let w32res = w32pref^"-windres" -let w32lib = "/usr/"^w32pref^"/lib/" -let w32bin = "/usr/"^w32pref^"/bin/" -let w32ico = "ide/coq_icon.o" - -let _ = if w32 then begin - Options.ocamlopt := A w32ocamlopt; - Options.ocamlmklib := A w32ocamlmklib; -end - -let use_camlp5 = (Coq_config.camlp4 = "camlp5") - -let camlp4args = - if use_camlp5 then [A "pa_extend.cmo";A "q_MLast.cmo";A "pa_macro.cmo"] - else [] - -let ocaml = A Coq_config.ocaml -let camlp4o = S ((A Coq_config.camlp4o) :: camlp4args) -let camlp4incl = S[A"-I"; A Coq_config.camlp4lib] -let camlp4compat = Sh Coq_config.camlp4compat -let opt = (Coq_config.best = "opt") -let ide = Coq_config.has_coqide -let hasdynlink = Coq_config.has_natdynlink -let os5fix = (Coq_config.natdynlinkflag = "os5fixme") -let dep_dynlink = if hasdynlink then N else Sh"-natdynlink no" -let lablgtkincl = Sh Coq_config.coqideincl -let local = Coq_config.local -let cflags = S[A"-ccopt";A Coq_config.cflags] - -(** Do we want to inspect .ml generated from .ml4 ? *) -let readable_genml = false -let readable_flag = if readable_genml then A"pr_o.cmo" else N - -let _build = Options.build_dir - - -(** Abbreviations about files *) - -let core_libs = - ["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library"; - "engine/engine"; "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; - "parsing/parsing"; "printing/printing"; "tactics/tactics"; - "stm/stm"; "toplevel/toplevel"; "parsing/highparsing"; - "ltac/ltac"] -let core_cma = List.map (fun s -> s^".cma") core_libs -let core_cmxa = List.map (fun s -> s^".cmxa") core_libs -let core_mllib = List.map (fun s -> s^".mllib") core_libs - -let tolink = "tools/tolink.ml" - -let c_headers_base = - ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; - "coq_gc.h"; "coq_interp.h"; "coq_values.h"; - "coq_jumptbl.h"] -let c_headers = List.map ((^) "kernel/byterun/") c_headers_base - -let coqinstrs = "kernel/byterun/coq_instruct.h" -let coqjumps = "kernel/byterun/coq_jumptbl.h" -let copcodes = "kernel/copcodes.ml" - -let libcoqrun = "kernel/byterun/libcoqrun.a" - -let init_vo = "theories/Init/Prelude.vo" - -let nmake = "theories/Numbers/Natural/BigN/NMake_gen.v" -let nmakegen = "theories/Numbers/Natural/BigN/NMake_gen.ml" - -let adapt_name (pref,oldsuf,newsuf) f = - pref ^ (Filename.chop_suffix f oldsuf) ^ newsuf - -let get_names (oldsuf,newsuf) s = - let pref = Filename.dirname s ^ "/" in - List.map (adapt_name (pref,oldsuf,newsuf)) (string_list_of_file s) - -let get_vo_itargets f = - let vo_itargets = get_names (".otarget",".itarget") f in - List.flatten (List.map (get_names (".vo",".v")) vo_itargets) - -let theoriesv = get_vo_itargets "theories/theories.itarget" - -let pluginsv = get_vo_itargets "plugins/pluginsvo.itarget" - -let pluginsmllib = get_names (".cma",".mllib") "plugins/pluginsbyte.itarget" - -(** for correct execution of coqdep_boot, source files should have - been imported in _build (and NMake_gen.v should have been created). *) - -let coqdepdeps = theoriesv @ pluginsv @ pluginsmllib - -let coqtop = "toplevel/coqtop" -let coqide = "ide/coqide" -let coqdepboot = "tools/coqdep_boot" -let coqmktop = "tools/coqmktop" - -(** The list of binaries to build: - (name of link in bin/, name in _build, install both or only best) *) - -type links = Both | Best | BestInPlace | Ide - -let all_binaries = - (if w32 then [ "mkwinapp", "tools/mkwinapp", Best ] else []) @ - [ "coqtop", coqtop, Both; - "coqide", "ide/coqide_main", Ide; - "coqmktop", coqmktop, Both; - "coqc", "tools/coqc", Both; - "coqchk", "checker/main", Both; - "coqdep_boot", coqdepboot, Best; - "coqdep", "tools/coqdep", Best; - "coqdoc", "tools/coqdoc/main", Best; - "coqwc", "tools/coqwc", Best; - "coq_makefile", "tools/coq_makefile", Best; - "coq-tex", "tools/coq_tex", Best; - "gallina", "tools/gallina", Best; - "csdpcert", "plugins/micromega/csdpcert", BestInPlace; - "fake_ide", "tools/fake_ide", Best; - ] - - -let best_oext = if opt then ".native" else ".byte" -let best_ext = if opt then ".opt" else ".byte" -let best_iext = if ide = "opt" then ".opt" else ".byte" - -let coqtopbest = coqtop^best_oext -(* For inner needs, we rather use the bytecode versions of coqdep - and coqmktop: slightly slower but compile quickly, and ok with - w32 cross-compilation *) -let coqdep_boot = coqdepboot^".byte" -let coqmktop_boot = coqmktop^".byte" - -let binariesopt_deps = - let addext b = b ^ ".native" in - let rec deps = function - | [] -> [] - | (_,b,Ide)::l -> if ide="opt" then addext b :: deps l else deps l - | (_,b,_)::l -> if opt then addext b :: deps l else deps l - in deps all_binaries - -let binariesbyte_deps = - let addext b = b ^ ".byte" in - let rec deps = function - | [] -> [] - | (_,b,Ide)::l -> if ide<>"no" then addext b :: deps l else deps l - | (_,b,Both)::l -> addext b :: deps l - | (_,b,_)::l -> if not opt then addext b :: deps l else deps l - in deps all_binaries - -let ln_sf toward f = - Command.execute ~quiet:true (Cmd (S [A"ln";A"-sf";P toward;P f])) - -let rec make_bin_links = function - | [] -> () - | (b,ob,kind)::l -> - make_bin_links l; - let obd = "../"^ !_build^"/"^ob and bd = "bin/"^b in - match kind with - | Ide when ide <> "no" -> - ln_sf (obd^".byte") (bd^".byte"); - if ide = "opt" then ln_sf (obd^".native") (bd^".opt"); - ln_sf (b^best_iext) bd - | Ide (* when ide = "no" *) -> () - | Both -> - ln_sf (obd^".byte") (bd^".byte"); - if opt then ln_sf (obd^".native") (bd^".opt"); - ln_sf (b^best_ext) bd - | Best -> ln_sf (obd^best_oext) bd - | BestInPlace -> ln_sf (b^best_oext) (!_build^"/"^ob) - -let incl f = Ocaml_utils.ocaml_include_flags f - -let cmd cl = (fun _ _ -> (Cmd (S cl))) - -let initial_actions () = begin - (** We "pre-create" a few subdirs in _build *) - Shell.mkdir_p (!_build^"/dev"); - Shell.mkdir_p (!_build^"/bin"); - Shell.mkdir_p (!_build^"/plugins/micromega"); - make_bin_links all_binaries; -end - -let extra_rules () = begin - -(** Virtual target for building all binaries *) - - rule "binariesopt" ~stamp:"binariesopt" ~deps:binariesopt_deps (fun _ _ -> Nop); - rule "binariesbyte" ~stamp:"binariesbyte" ~deps:binariesbyte_deps (fun _ _ -> Nop); - rule "binaries" ~stamp:"binaries" ~deps:["binariesbyte";"binariesopt"] (fun _ _ -> Nop); - -(** We create a special coq_config which mentions _build *) - - rule "coq_config.ml" ~prod:"coq_config.ml" ~dep:"config/coq_config.ml" - (fun _ _ -> - if w32 then cp "config/coq_config.ml" "coq_config.ml" else - let lines = read_file "config/coq_config.ml" in - let lines = List.map (fun s -> s^"\n") lines in - let line0 = "\n(* Adapted variables for ocamlbuild *)\n" in - (* TODO : line2 isn't completely accurate with respect to ./configure: - the case of -local -vmbyteflags foo isn't supported *) - let line1 = - "let vmbyteflags = [\"-dllib\";\"-lcoqrun\"]\n" - in - Echo (lines @ (if local then [line0;line1] else []), - "coq_config.ml")); - -(** Camlp4 extensions *) - - rule ".ml4.ml" ~dep:"%.ml4" ~prod:"%.ml" - (fun env _ -> - let ml4 = env "%.ml4" and ml = env "%.ml" in - Cmd (S[camlp4o;T(tags_of_pathname ml4 ++ "p4mod");readable_flag; - T(tags_of_pathname ml4 ++ "p4option"); camlp4compat; - A"-o"; Px ml; A"-impl"; P ml4])); - - flag_and_dep ["p4mod"; "use_grammar"] (P "grammar/grammar.cma"); - - flag_and_dep ["p4mod"; "use_compat5"] (P "tools/compat5.cmo"); - flag_and_dep ["p4mod"; "use_compat5b"] (P "tools/compat5b.cmo"); - - if w32 then begin - flag ["p4mod"] (A "-DWIN32"); - dep ["ocaml"; "link"; "ide"] ["ide/ide_win32_stubs.o"]; - end; - - if not use_camlp5 then begin - let mlp_cmo s = - let src=s^".mlp" and dst=s^".cmo" in - rule (src^".cmo") ~dep:src ~prod:dst ~insert:`top - (fun env _ -> - Cmd (S [!Options.ocamlc; A"-c"; A"-pp"; - Quote (S [camlp4o;A"-impl"]); camlp4incl; A"-impl"; P src])) - in - mlp_cmo "tools/compat5"; - mlp_cmo "tools/compat5b"; - end; - -(** All caml files are compiled with +camlp4/5 - and ide files need +lablgtk2 *) - - flag ["compile"; "ocaml"] (S [A"-thread";A"-rectypes"; camlp4incl]); - flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]); - flag ["ocaml"; "ide"; "compile"] lablgtkincl; - flag ["ocaml"; "ide"; "link"] lablgtkincl; - flag ["ocaml"; "ide"; "link"; "byte"] - (S [A"lablgtk.cma"; A"lablgtksourceview2.cma"]); - flag ["ocaml"; "ide"; "link"; "native"] - (S [A"lablgtk.cmxa"; A"lablgtksourceview2.cmxa"]); - -(** C code for the VM *) - - dep ["compile"; "c"] c_headers; - flag ["compile"; "c"] cflags; - dep ["ocaml"; "use_libcoqrun"; "compile"] [libcoqrun]; - dep ["ocaml"; "use_libcoqrun"; "link"; "native"] [libcoqrun]; - flag ["ocaml"; "use_libcoqrun"; "link"; "byte"] (Sh Coq_config.vmbyteflags); - - (* we need to use a different ocamlc. For now we copy the rule *) - if w32 then - rule ".c.o" ~deps:("%.c"::c_headers) ~prod:"%.o" ~insert:`top - (fun env _ -> - let c = env "%.c" in - let o = env "%.o" in - Seq [Cmd (S [P w32ocamlc;cflags;A"-c";Px c]); - mv (Filename.basename o) o]); - -(** VM: Generation of coq_jumbtbl.h and copcodes.ml from coq_instruct.h *) - - rule "coqinstrs" ~dep:coqinstrs ~prods:[coqjumps;copcodes] - (fun _ _ -> - let jmps = ref [] and ops = ref [] and i = ref 0 in - let add_instr instr comma = - if instr = "" then failwith "Empty" else begin - jmps:=sprintf "&&coq_lbl_%s%s \n" instr comma :: !jmps; - ops:=sprintf "let op%s = %d\n" instr !i :: !ops; - incr i - end - in - (** we recognize comma-separated uppercase instruction names *) - let parse_line s = - let b = Scanning.from_string s in - try while true do bscanf b " %[A-Z0-9_]%[,]" add_instr done - with _ -> () - in - List.iter parse_line (read_file coqinstrs); - Seq [Echo (List.rev !jmps, coqjumps); - Echo (List.rev !ops, copcodes)]); - -(** Generation of tolink.ml *) - - rule tolink ~deps:core_mllib ~prod:tolink - (fun _ _ -> - let cat s = String.concat " " (string_list_of_file s) in - let core_mods = String.concat " " (List.map cat core_mllib) in - let core_cmas = String.concat " " core_cma in - Echo (["let copts = \"-cclib -lcoqrun\"\n"; - "let core_libs = \""^core_cmas^"\"\n"; - "let core_objs = \""^core_mods^"\"\n"], - tolink)); - -(** For windows, building coff object file from a .rc (for the icon) *) - - if w32 then rule ".rc.o" ~deps:["%.rc";"ide/coq.ico"] ~prod:"%.o" - (fun env _ -> - let rc = env "%.rc" and o = env "%.o" in - Cmd (S [P w32res;A "--input-format";A "rc";A "--input";P rc; - A "--output-format";A "coff";A "--output"; Px o])); - -(** The windows version of Coqide is now a console-free win32 app, - which moreover contains the Coq icon. If necessary, the mkwinapp - tool can be used later to restore or suppress the console of Coqide. *) - - if w32 then dep ["link"; "ocaml"; "program"; "ide"] [w32ico]; - - if w32 then flag ["link"; "ocaml"; "program"; "ide"] - (S [A "-ccopt"; A "-link -Wl,-subsystem,windows"; P w32ico]); - -(** Coqtop *) - - let () = - let fo = coqtop^".native" and fb = coqtop^".byte" in - let depsall = (if w32 then [w32ico] else [])@[coqmktop_boot;libcoqrun] in - let depso = core_cmxa in - let depsb = core_cma in - let w32flag = - if not w32 then N else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]) - in - if opt then rule fo ~prod:fo ~deps:(depsall@depso) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;A"-thread";camlp4incl;A"-o";Px fo]); - rule fb ~prod:fb ~deps:(depsall@depsb) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;A"-thread";camlp4incl;A"-o";Px fb]); - in - -(** Coq files dependencies *) - - rule "coqdepready" ~stamp:"coqdepready" ~deps:coqdepdeps (fun _ _ -> Nop); - - rule ".v.d" ~prod:"%.v.depends" ~deps:["%.v";coqdep_boot;"coqdepready"] - (fun env _ -> - let v = env "%.v" and vd = env "%.v.depends" in - (** NB: this relies on all .v files being already in _build. *) - Cmd (S [P coqdep_boot;dep_dynlink;P v;Sh">";Px vd])); - -(** Coq files compilation *) - - let coq_build_dep f build = - (** NB: this relies on coqdep producing a single Makefile line - for one .v file, with some specific shape "f.vo ...: f.v deps.vo ..." *) - let src = f^".v" in - let depends = f^".v.depends" in - let rec get_deps keep = function - | [] -> [] - | d::deps when d = src -> get_deps keep deps - | d::deps when keep -> [d] :: get_deps keep deps - | d::deps -> get_deps (String.contains d ':') deps - in - let d = get_deps false (string_list_of_file depends) in - List.iter Outcome.ignore_good (build d) - - in - - let coq_v_rule d init = - let bootflag = if init then A"-noinit" else N in - let gendep = if init then coqtopbest else init_vo in - rule (d^".v.vo") - ~prods:[d^"%.vo";d^"%.glob"] ~deps:[gendep;d^"%.v";d^"%.v.depends"] - (fun env build -> - let f = env (d^"%") in - coq_build_dep f build; - Cmd (S [P coqtopbest;A"-boot";bootflag;A"-compile";Px f])) - in - coq_v_rule "theories/Init/" true; - coq_v_rule "" false; - -(** Generation of _plugin_mod.ml files *) - - rule "_mod.ml" ~prod:"%_plugin_mod.ml" ~dep:"%_plugin.mllib" - (fun env _ -> - let line s = "let _ = Mltop.add_known_module \""^s^"\"\n" in - let mods = - string_list_of_file (env "%_plugin.mllib") @ - [Filename.basename (env "%_plugin")] - in - Echo (List.map line mods, env "%_plugin_mod.ml")); - -(** Rule for native dynlinkable plugins *) - - rule ".cmxa.cmxs" ~prod:"%.cmxs" ~dep:"%.cmxa" - (fun env _ -> - let cmxs = Px (env "%.cmxs") and cmxa = P (env "%.cmxa") in - if os5fix then - Cmd (S [A"../dev/ocamlopt_shared_os5fix.sh"; !Options.ocamlopt; cmxs]) - else - Cmd (S [!Options.ocamlopt;A"-linkall";A"-shared";A"-o";cmxs;cmxa])); - -(** Generation of NMake.v from NMake_gen.ml *) - - rule "NMake" ~prod:nmake ~dep:nmakegen - (cmd [ocaml;P nmakegen;Sh ">";Px nmake]); - -end - -(** Registration of our rules (after the standard ones) *) - -let _ = dispatch begin function - | After_rules -> initial_actions (); extra_rules () - | _ -> () -end - -(** TODO / Remarques: - - * Apres un premier build, le second prend du temps, meme cached: - 1 min 25 pour les 2662 targets en cache. Etonnement, refaire - coqtop.byte ne prend que ~4s, au lieu des ~40s pour coqtop.opt. - A comprendre ... - - * Parallelisation: vraiment pas top - -*) diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mlpack index 319a9c302..2410f906a 100644 --- a/plugins/btauto/btauto_plugin.mllib +++ b/plugins/btauto/btauto_plugin.mlpack @@ -1,3 +1,2 @@ Refl_btauto G_btauto -Btauto_plugin_mod diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mlpack index 1bcfc5378..27e903fd3 100644 --- a/plugins/cc/cc_plugin.mllib +++ b/plugins/cc/cc_plugin.mlpack @@ -2,4 +2,3 @@ Ccalgo Ccproof Cctac G_congruence -Cc_plugin_mod diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mlpack index 39342dbd1..1b84a0790 100644 --- a/plugins/decl_mode/decl_mode_plugin.mllib +++ b/plugins/decl_mode/decl_mode_plugin.mlpack @@ -3,4 +3,3 @@ Decl_interp Decl_proof_instr Ppdecl_proof G_decl_mode -Decl_mode_plugin_mod diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 78a95143d..0feba6365 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "decl_mode_plugin" + open Compat open Pp open Decl_expr diff --git a/plugins/derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mlpack index 5ee0fc6da..5ee0fc6da 100644 --- a/plugins/derive/derive_plugin.mllib +++ b/plugins/derive/derive_plugin.mlpack diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index 39cad4d03..d4dc7e0ee 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -10,6 +10,8 @@ open Constrarg (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "derive_plugin" + let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mlpack index ad3212434..9184f6501 100644 --- a/plugins/extraction/extraction_plugin.mllib +++ b/plugins/extraction/extraction_plugin.mlpack @@ -9,4 +9,3 @@ Scheme Json Extract_env G_extraction -Extraction_plugin_mod diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 0a8cb0ccd..19fda4aea 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "extraction_plugin" + (* ML names *) open Genarg diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index a78532e33..cec3505a9 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -153,6 +153,8 @@ TACTIC EXTEND gintuition END open Proofview.Notations +open Cc_plugin +open Decl_mode_plugin let default_declarative_automation = Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *) diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mlpack index 447a1fb51..65fb2e9a1 100644 --- a/plugins/firstorder/ground_plugin.mllib +++ b/plugins/firstorder/ground_plugin.mlpack @@ -5,4 +5,3 @@ Rules Instances Ground G_ground -Ground_plugin_mod diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mlpack index 0383b1a80..b6262f8ae 100644 --- a/plugins/fourier/fourier_plugin.mllib +++ b/plugins/fourier/fourier_plugin.mlpack @@ -1,4 +1,3 @@ Fourier FourierR G_fourier -Fourier_plugin_mod diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 80866e8b8..95b4967fa 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1529,7 +1529,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in + let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mlpack index ec1f5436c..2b443f2a1 100644 --- a/plugins/funind/recdef_plugin.mllib +++ b/plugins/funind/recdef_plugin.mlpack @@ -8,4 +8,3 @@ Invfun Indfun Merge G_indfun -Recdef_plugin_mod diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mlpack index f53a9e379..ed253da3f 100644 --- a/plugins/micromega/micromega_plugin.mllib +++ b/plugins/micromega/micromega_plugin.mlpack @@ -7,4 +7,3 @@ Certificate Persistent_cache Coq_micromega G_micromega -Micromega_plugin_mod diff --git a/plugins/nsatz/nsatz_plugin.mllib b/plugins/nsatz/nsatz_plugin.mlpack index e991fb76f..b55adf43c 100644 --- a/plugins/nsatz/nsatz_plugin.mllib +++ b/plugins/nsatz/nsatz_plugin.mlpack @@ -3,4 +3,3 @@ Polynom Ideal Nsatz G_nsatz -Nsatz_plugin_mod diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mlpack index 2b387fdce..df7f1047f 100644 --- a/plugins/omega/omega_plugin.mllib +++ b/plugins/omega/omega_plugin.mlpack @@ -1,4 +1,3 @@ Omega Coq_omega G_omega -Omega_plugin_mod diff --git a/plugins/plugins.itarget b/plugins/plugins.itarget deleted file mode 100644 index 56aa42b06..000000000 --- a/plugins/plugins.itarget +++ /dev/null @@ -1,3 +0,0 @@ -pluginsopt.otarget -pluginsbyte.otarget -pluginsvo.otarget
\ No newline at end of file diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget deleted file mode 100644 index d8752f8b8..000000000 --- a/plugins/pluginsbyte.itarget +++ /dev/null @@ -1,21 +0,0 @@ -btauto/btauto_plugin.cma -setoid_ring/newring_plugin.cma -extraction/extraction_plugin.cma -decl_mode/decl_mode_plugin.cma -firstorder/ground_plugin.cma -rtauto/rtauto_plugin.cma -fourier/fourier_plugin.cma -romega/romega_plugin.cma -omega/omega_plugin.cma -micromega/micromega_plugin.cma -cc/cc_plugin.cma -nsatz/nsatz_plugin.cma -funind/recdef_plugin.cma -syntax/ascii_syntax_plugin.cma -syntax/nat_syntax_plugin.cma -syntax/numbers_syntax_plugin.cma -syntax/r_syntax_plugin.cma -syntax/string_syntax_plugin.cma -syntax/z_syntax_plugin.cma -quote/quote_plugin.cma -derive/derive_plugin.cma
\ No newline at end of file diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget deleted file mode 100644 index 220e5182d..000000000 --- a/plugins/pluginsdyn.itarget +++ /dev/null @@ -1,24 +0,0 @@ -btauto/btauto_plugin.cmxs -field/field_plugin.cmxs -setoid_ring/newring_plugin.cmxs -extraction/extraction_plugin.cmxs -decl_mode/decl_mode_plugin.cmxs -firstorder/ground_plugin.cmxs -rtauto/rtauto_plugin.cmxs -fourier/fourier_plugin.cmxs -romega/romega_plugin.cmxs -omega/omega_plugin.cmxs -micromega/micromega_plugin.cmxs -subtac/subtac_plugin.cmxs -ring/ring_plugin.cmxs -cc/cc_plugin.cmxs -nsatz/nsatz_plugin.cmxs -funind/recdef_plugin.cmxs -syntax/ascii_syntax_plugin.cmxs -syntax/nat_syntax_plugin.cmxs -syntax/numbers_syntax_plugin.cmxs -syntax/r_syntax_plugin.cmxs -syntax/string_syntax_plugin.cmxs -syntax/z_syntax_plugin.cmxs -quote/quote_plugin.cmxs -derive/derive_plugin.cmxs diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget deleted file mode 100644 index 04a1e711c..000000000 --- a/plugins/pluginsopt.itarget +++ /dev/null @@ -1,21 +0,0 @@ -btauto/btauto_plugin.cmxa -setoid_ring/newring_plugin.cmxa -extraction/extraction_plugin.cmxa -decl_mode/decl_mode_plugin.cmxa -firstorder/ground_plugin.cmxa -rtauto/rtauto_plugin.cmxa -fourier/fourier_plugin.cmxa -romega/romega_plugin.cmxa -omega/omega_plugin.cmxa -micromega/micromega_plugin.cmxa -cc/cc_plugin.cmxa -nsatz/nsatz_plugin.cmxa -funind/recdef_plugin.cmxa -syntax/ascii_syntax_plugin.cmxa -syntax/nat_syntax_plugin.cmxa -syntax/numbers_syntax_plugin.cmxa -syntax/r_syntax_plugin.cmxa -syntax/string_syntax_plugin.cmxa -syntax/z_syntax_plugin.cmxa -quote/quote_plugin.cmxa -derive/derive_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget deleted file mode 100644 index a59bf29c9..000000000 --- a/plugins/pluginsvo.itarget +++ /dev/null @@ -1,12 +0,0 @@ -btauto/vo.otarget -fourier/vo.otarget -funind/vo.otarget -nsatz/vo.otarget -micromega/vo.otarget -omega/vo.otarget -quote/vo.otarget -romega/vo.otarget -rtauto/vo.otarget -setoid_ring/vo.otarget -extraction/vo.otarget -derive/vo.otarget
\ No newline at end of file diff --git a/plugins/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib deleted file mode 100644 index d1b3ccbe1..000000000 --- a/plugins/quote/quote_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Quote -G_quote -Quote_plugin_mod diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack new file mode 100644 index 000000000..2e9be09d8 --- /dev/null +++ b/plugins/quote/quote_plugin.mlpack @@ -0,0 +1,2 @@ +Quote +G_quote diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 007a9ec67..a059512d8 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -9,7 +9,7 @@ open Pp open Util open Const_omega -module OmegaSolver = Omega.MakeOmegaSolver (Bigint) +module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver (* \section{Useful functions and flags} *) diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mlpack index 1625009d0..38d0e9411 100644 --- a/plugins/romega/romega_plugin.mllib +++ b/plugins/romega/romega_plugin.mlpack @@ -1,4 +1,3 @@ Const_omega Refl_omega G_romega -Romega_plugin_mod diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mlpack index 0e3460449..61c5e945b 100644 --- a/plugins/rtauto/rtauto_plugin.mllib +++ b/plugins/rtauto/rtauto_plugin.mlpack @@ -1,4 +1,3 @@ Proof_search Refl_tauto G_rtauto -Rtauto_plugin_mod diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 154ec6e1b..57ef92032 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -34,15 +34,6 @@ open Proofview.Notations (****************************************************************************) (* controlled reduction *) -(** ppedrot: something dubious here, we're obviously using evars the wrong - way. FIXME! *) - -let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) -let unmark_arg f c = - match destEvar c with - | (i,[|c|]) -> f (Evar.repr i) c - | _ -> assert false - type protect_flag = Eval|Prot|Rec let tag_arg tag_rec map subs i c = @@ -75,12 +66,10 @@ and mk_clos_app_but f_map subs f args n = let fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in match f_map (global_of_constr_nofail f') with - Some map -> - mk_clos_deep - (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) - subs - (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) - | None -> mk_clos_app_but f_map subs f args (n+1) + | Some map -> + let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in + mk_red (FApp (f (-1) f', Array.mapi f args')) + | None -> mk_atom (mkApp (f, args)) let interp_map l t = try Some(List.assoc_f eq_gr t l) with Not_found -> None @@ -106,6 +95,7 @@ let protect_tac_in map id = (****************************************************************************) let closed_term t l = + let open Quote_plugin in let l = List.map Universes.constr_of_global l in let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt()) diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib deleted file mode 100644 index 7d6c49588..000000000 --- a/plugins/setoid_ring/newring_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Newring -Newring_plugin_mod -G_newring diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack new file mode 100644 index 000000000..23663b409 --- /dev/null +++ b/plugins/setoid_ring/newring_plugin.mlpack @@ -0,0 +1,2 @@ +Newring +G_newring diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 67c9dd0a3..03b49e333 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "ascii_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + open Pp open Errors open Util diff --git a/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib deleted file mode 100644 index b00f92506..000000000 --- a/plugins/syntax/ascii_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Ascii_syntax -Ascii_syntax_plugin_mod diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack new file mode 100644 index 000000000..7b9213a0e --- /dev/null +++ b/plugins/syntax/ascii_syntax_plugin.mlpack @@ -0,0 +1 @@ +Ascii_syntax diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index fe9386039..3142c8cf0 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "nat_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + (* This file defines the printer for natural numbers in [nat] *) (*i*) diff --git a/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib deleted file mode 100644 index 69b0cb20f..000000000 --- a/plugins/syntax/nat_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Nat_syntax -Nat_syntax_plugin_mod diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack new file mode 100644 index 000000000..39bdd62f4 --- /dev/null +++ b/plugins/syntax/nat_syntax_plugin.mlpack @@ -0,0 +1 @@ +Nat_syntax diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index fe9f1319e..57cb2f897 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "numbers_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + (* digit-based syntax for int31, bigN bigZ and bigQ *) open Bigint @@ -180,7 +184,7 @@ let bigN_of_pos_bigint dloc n = let word = word_of_pos_bigint dloc h n in let args = if h < n_inlined then [word] - else [Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] + else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] in GApp (dloc, ref_constructor, args) diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib deleted file mode 100644 index ebc0bb202..000000000 --- a/plugins/syntax/numbers_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Numbers_syntax -Numbers_syntax_plugin_mod diff --git a/plugins/syntax/numbers_syntax_plugin.mlpack b/plugins/syntax/numbers_syntax_plugin.mlpack new file mode 100644 index 000000000..e48c00a0d --- /dev/null +++ b/plugins/syntax/numbers_syntax_plugin.mlpack @@ -0,0 +1 @@ +Numbers_syntax diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 05d73f9ec..3ae2d45f3 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -10,6 +10,10 @@ open Util open Names open Globnames +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "r_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + exception Non_closed_number (**********************************************************************) diff --git a/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib deleted file mode 100644 index 5c173a140..000000000 --- a/plugins/syntax/r_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -R_syntax -R_syntax_plugin_mod diff --git a/plugins/syntax/r_syntax_plugin.mlpack b/plugins/syntax/r_syntax_plugin.mlpack new file mode 100644 index 000000000..d4ee75ea4 --- /dev/null +++ b/plugins/syntax/r_syntax_plugin.mlpack @@ -0,0 +1 @@ +R_syntax diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 2e696f391..de0fa77ef 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -7,10 +7,14 @@ (***********************************************************************) open Globnames -open Ascii_syntax +open Ascii_syntax_plugin.Ascii_syntax open Glob_term open Coqlib +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "string_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + exception Non_closed_string (* make a string term from the string s *) diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib deleted file mode 100644 index b108c9e00..000000000 --- a/plugins/syntax/string_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -String_syntax -String_syntax_plugin_mod diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack new file mode 100644 index 000000000..45d6e0fa2 --- /dev/null +++ b/plugins/syntax/string_syntax_plugin.mlpack @@ -0,0 +1 @@ +String_syntax diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 53c1b5d7a..ce86c0a65 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -12,6 +12,10 @@ open Util open Names open Bigint +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "z_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + exception Non_closed_number (**********************************************************************) diff --git a/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib deleted file mode 100644 index 36d41acc2..000000000 --- a/plugins/syntax/z_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Z_syntax -Z_syntax_plugin_mod diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack new file mode 100644 index 000000000..411260c04 --- /dev/null +++ b/plugins/syntax/z_syntax_plugin.mlpack @@ -0,0 +1 @@ +Z_syntax diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 89cb723bc..e5fc5a188 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -103,8 +103,7 @@ let position_problem l2r = function | CUMUL -> Some l2r let occur_rigidly ev evd t = - let (l, app) = decompose_app_vect t in - let rec aux t = + let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true @@ -116,7 +115,7 @@ let occur_rigidly ev evd t = | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false | Case _ -> false - in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app + in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose the problem (t1 stack1) = (t2 stack2) into a problem @@ -368,8 +367,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = - let default_fail i = (* costly *) - UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in @@ -421,7 +418,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skM in let f1 i = match Stack.list_of_app_stack skF with - | None -> default_fail evd + | None -> quick_fail evd | Some lF -> let tM = Stack.zip apprM in miller_pfenning on_left @@ -468,10 +465,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = let switch f a b = if on_left then f a b else f b a in let eta evd = - match kind_of_term termR with - | Lambda _ -> eta env evd false skR termR skF termF - | Construct u -> eta_constructor ts env evd skR u skF termF - | _ -> UnifFailure (evd,NotSameHead) + match kind_of_term termR with + | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> + eta env evd false skR termR skF termF + | Construct u -> eta_constructor ts env evd skR u skF termF + | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with | None -> @@ -506,10 +504,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> + (* sk1[?ev1] =? sk2[?ev2] *) let f1 i = + (* Try first-order unification *) match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with - |None, Success i' -> - (* Evar can be defined in i' *) + | None, Success i' -> + (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) + (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) let ev1' = whd_evar i' (mkEvar ev1) in if isEvar ev1' then solve_simple_eqn (evar_conv_x ts) env i' @@ -517,7 +518,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) - |Some (r,[]), Success i' -> + | Some (r,[]), Success i' -> + (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) + (* we now unify r[?ev1] and ?ev2 *) let ev2' = whd_evar i' (mkEvar ev2) in if isEvar ev2' then solve_simple_eqn (evar_conv_x ts) env i' @@ -525,16 +528,46 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env evd pbty ((ev2', sk1), csts1) ((term2, sk2), csts2) - - |Some ([],r), Success i' -> + | Some ([],r), Success i' -> + (* Symmetrically *) + (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) + (* we now unify ?ev1 and r[?ev2] *) let ev1' = whd_evar i' (mkEvar ev1) in if isEvar ev1' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem true pbty,destEvar ev1',Stack.zip(term2,r)) else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) - |_, (UnifFailure _ as x) -> x - |Some _, _ -> UnifFailure (i,NotSameArgSize) + | None, (UnifFailure _ as x) -> + (* sk1 and sk2 have no common outer part *) + if Stack.not_purely_applicative sk2 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid true ev1 appr1 appr2 + else + if Stack.not_purely_applicative sk1 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid false ev2 appr2 appr1 + else + (* We could instead try Miller unification, then + postpone to see if other equations help, as in: + [Check fun a b : unit => (eqáµ£efl : _ a = _ a b)] *) + x + | Some _, Success _ -> + (* sk1 and sk2 have a common outer part *) + if Stack.not_purely_applicative sk2 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid true ev1 appr1 appr2 + else + if Stack.not_purely_applicative sk1 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid false ev2 appr2 appr1 + else + (* We could instead try Miller unification, then + postpone to see if other equations help, as in: + [Check fun a b c : unit => (eqáµ£efl : _ a b = _ c a b)] *) + UnifFailure (i,NotSameArgSize) + | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") + and f2 i = if Evar.equal sp1 sp2 then match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with @@ -712,10 +745,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f3; f4] (* Eta-expansion *) - | Rigid, _ when isLambda term1 -> + | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 -> eta env evd true sk1 term1 sk2 term2 - | _, Rigid when isLambda term2 -> + | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 -> eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin @@ -1071,7 +1104,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = abstract_free_holes evd subst, true with TypingFailed evd -> evd, false -let second_order_matching_with_args ts env evd ev l t = +let second_order_matching_with_args ts env evd pbty ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in @@ -1079,8 +1112,9 @@ let second_order_matching_with_args ts env evd ev l t = if b then Success evd else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) if b then Success evd else -*) - UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) + *) + let pb = (pbty,env,mkApp(mkEvar ev,l),t) in + UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in @@ -1096,7 +1130,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk1 evd term2 args1 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | (Rel _|Var _), Evar (evk2,args2) when app_empty && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a) (remove_instance_local_defs evd evk2 args2) -> @@ -1104,7 +1140,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk2 evd term1 args2 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd @@ -1119,20 +1157,20 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = ise_try evd [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2); (fun evd -> - second_order_matching_with_args ts env evd ev1 l1 t2)] + second_order_matching_with_args ts env evd pbty ev1 l1 t2)] | _,Evar ev2 when Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1); (fun evd -> - second_order_matching_with_args ts env evd ev2 l2 t1)] + second_order_matching_with_args ts env evd pbty ev2 l2 t1)] | Evar ev1,_ -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev1 l1 t2 + second_order_matching_with_args ts env evd pbty ev1 l1 t2 | _,Evar ev2 -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev2 l2 t1 + second_order_matching_with_args ts env evd pbty ev2 l2 t1 | _ -> (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index ae8b91c34..df1fc20f1 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -108,7 +108,6 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t = raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in let rec substrec k t = if nowhere_except_in && !pos > maxocc then t else - if not (Vars.closed0 t) then subst_below k t else try let subst = test.match_fun test.testing_state t in if Locusops.is_selected !pos occs then diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cf5b08c58..b0715af73 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -14,15 +14,16 @@ open Type_errors type unification_error = | OccurCheck of existential_key * constr - | NotClean of existential * env * constr + | NotClean of existential * env * constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * constr * constr + | ConversionFailed of env * constr * constr (* Non convertible closed terms *) | MetaOccurInBody of existential_key | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error + | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index f617df9ee..880f48e5f 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -24,6 +24,7 @@ type unification_error = | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error + | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index efc42aab7..378294c98 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -143,7 +143,7 @@ let interp_universe_level_name evd (loc,s) = with Not_found -> try let id = try Id.of_string s with _ -> raise Not_found in - evd, Idmap.find id names + evd, snd (Idmap.find id names) with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ~loc ~name:s univ_rigid evd diff --git a/pretyping/unification.ml b/pretyping/unification.ml index cdd543d25..21cf5548f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1058,8 +1058,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in try let res = - if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n - || subterm_restriction opt flags then None + if subterm_restriction opt flags || + occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n + then + None else let sigma, b = match flags.modulo_conv_on_closed_terms with | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 114410fed..5356cdee8 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -366,6 +366,23 @@ module Make in str "<" ++ name ++ str ">" ++ args + let pr_alias_key key = + try + let prods = (KNmap.find key !prnotation_tab).pptac_prods in + (* First printing strategy: only the head symbol *) + match prods with + | TacTerm s :: prods -> str s + | _ -> + (* Second printing strategy; if ever Tactic Notation is eventually *) + (* accepting notations not starting with an identifier *) + let rec pr = function + | [] -> [] + | TacTerm s :: prods -> s :: pr prods + | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in + str (String.concat " " (pr prods)) + with Not_found -> + KerName.print key + let pr_alias_gen pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 4ef2ea918..c08d6044d 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -45,9 +45,13 @@ module type Pp = sig val pr_extend : (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + val pr_alias_key : Names.KerName.t -> std_ppcmds + val pr_alias : (Val.t -> std_ppcmds) -> int -> Names.KerName.t -> Val.t list -> std_ppcmds + val pr_alias_key : Names.KerName.t -> std_ppcmds + val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds val pr_raw_tactic : raw_tactic_expr -> std_ppcmds diff --git a/printing/printing.mllib b/printing/printing.mllib index 52102e1d3..bc8f0750e 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -2,11 +2,8 @@ Genprint Pputils Ppannotation Ppconstr -Ppconstrsig Printer Pptactic -Pptacticsig Printmod Prettyp Ppvernac -Ppvernacsig diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 1ef0b087b..78dce0d64 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -491,7 +491,8 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e -> + | PretypeError (_,_,ActualTypeNotCoercible (_,_, + (NotClean _ | ConversionFailed _))) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 59b166ea0..e9236b1da 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This file defines clausenv, which is a deprecated way to handle open terms + in the proof engine. Most of the API here is legacy except for the + evar-based clauses. *) + open Names open Term open Environ diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 00e74a247..aa091aecd 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy components of the previous proof engine. *) + open Term open Clenv open Tacexpr diff --git a/proofs/goal.mli b/proofs/goal.mli index 8a3d6e815..6a79c1f45 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -6,7 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* This module implements the abstract interface to goals *) +(** This module implements the abstract interface to goals. Most of the code + here is useless and should be eventually removed. Consider using + {!Proofview.Goal} instead. *) type goal = Evar.t diff --git a/proofs/logic.mli b/proofs/logic.mli index 9aa4ac207..2764d28c0 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy proof engine. Do not use in newly written code. *) + open Names open Term open Evd diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index cfab8bd63..666730e1a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Global proof state. A quite redundant wrapper on {!Proof_global}. *) + open Loc open Names open Term diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index ef0d52b62..f7798a0ed 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy proof engine. Do not use in newly written code. *) + open Evd open Names open Term @@ -26,31 +28,6 @@ type prim_rule = type rule = prim_rule -(** The type [goal sigma] is the type of subgoal. It has the following form -{v it = \{ evar_concl = [the conclusion of the subgoal] - evar_hyps = [the hypotheses of the subgoal] - evar_body = Evar_Empty; - evar_info = \{ pgm : [The Realizer pgm if any] - lc : [Set of evar num occurring in subgoal] \}\} - sigma = \{ stamp = [an int chardacterizing the ed field, for quick compare] - ed : [A set of existential variables depending in the subgoal] - number of first evar, - it = \{ evar_concl = [the type of first evar] - evar_hyps = [the context of the evar] - evar_body = [the body of the Evar if any] - evar_info = \{ pgm : [Useless ??] - lc : [Set of evars occurring - in the type of evar] \} \}; - ... - number of last evar, - it = \{ evar_concl = [the type of evar] - evar_hyps = [the context of the evar] - evar_body = [the body of the Evar if any] - evar_info = \{ pgm : [Useless ??] - lc : [Set of evars occurring - in the type of evar] \} \} \} v} -*) - type goal = Goal.goal type tactic = goal sigma -> goal list sigma diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli index 1bf38b690..b2c65412f 100644 --- a/proofs/proof_using.mli +++ b/proofs/proof_using.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Utility code for section variables handling in Proof using... *) + val process_expr : Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list -> Names.Id.t list diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 9130a186b..804a54360 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,7 +2,6 @@ Miscprint Goal Evar_refiner Proof_using -Proof_errors Logic Refine Proof diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index b91911087..d4c2c4a6c 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Interpretation layer of redexprs such as hnf, cbv, etc. *) + open Names open Term open Pattern diff --git a/proofs/refine.mli b/proofs/refine.mli index 17c7e28ca..a9798b704 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -6,6 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** The primitive refine tactic used to fill the holes in partial proofs. This + is the recommanded way to write tactics when the proof term is easy to + write down. Note that this is not the user-level refine tactic defined + in Ltac which is actually based on the one below. *) + open Proofview (** {6 The refine tactic} *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index dd9153a02..6dcafb77a 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy proof engine. Do not use in newly written code. *) + open Evd open Proof_type diff --git a/tactics/auto.mli b/tactics/auto.mli index 8c4f35904..0fd95aead 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This files implements auto and related automation tactics *) + open Names open Term open Clenv @@ -13,8 +15,6 @@ open Pattern open Decl_kinds open Hints -(** Auto and related automation tactics *) - val priority : ('a * full_hint) list -> ('a * full_hint) list val default_search_depth : int ref diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index ac613b57c..070657179 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This files implements the autorewrite tactic. *) + open Term open Tacexpr open Equality diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index f1bcfa7dd..cac4b8844 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This files implements typeclasses eauto *) + open Names open Constr open Tacmach diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 75273e4b7..991922d90 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1661,7 +1661,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags - with UserError _ as exn -> + with exn when catchable_exception exn -> Proofview.tclZERO exn in let rec try_red_apply thm_ty (exn0, info) = @@ -2453,9 +2453,10 @@ let intro_patterns_bound_to n destopt = intro_patterns_core true [] [] [] destopt (Some (true,n)) 0 (fun _ l -> clear_wildcards l) -let intro_patterns_to destopt = +let intro_patterns_to destopt l = + (* Eta-expansion because of a side-effect *) intro_patterns_core (use_bracketing_last_or_and_intro_pattern ()) - [] [] [] destopt None 0 (fun _ l -> clear_wildcards l) + [] [] [] destopt None 0 (fun _ l -> clear_wildcards l) l let intro_pattern_to destopt pat = intro_patterns_to destopt [dloc,pat] diff --git a/tactics/tactics.mli b/tactics/tactics.mli index df41951c3..fa7b6791e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -21,7 +21,10 @@ open Unification open Misctypes open Locus -(** Main tactics. *) +(** Main tactics defined in ML. This file is huge and should probably be split + in more reasonable units at some point. Because of its size and age, the + implementation features various styles and stages of the proof engine. + This has to be uniformized someday. *) (** {6 General functions. } *) diff --git a/test-suite/bugs/closed/4644.v b/test-suite/bugs/closed/4644.v new file mode 100644 index 000000000..f09b27c2b --- /dev/null +++ b/test-suite/bugs/closed/4644.v @@ -0,0 +1,52 @@ +(* Testing a regression of unification in 8.5 in problems of the form + "match ?y with ... end = ?x args" *) + +Lemma foo : exists b, forall a, match a with tt => tt end = b a. +Proof. +eexists. intro. +refine (_ : _ = match _ with tt => _ end). +refine eq_refl. +Qed. + +(**********************************************************************) + +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Export Coq.Classes.Morphisms. +Require Import Coq.Lists.List. + +Global Set Implicit Arguments. + +Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs)) + ls + : P ls + := match ls with + | nil => N + | x::xs => C x xs + end. + +Axiom list_caset_Proper' + : forall {A P}, + Proper (eq + ==> pointwise_relation _ (pointwise_relation _ eq) + ==> eq + ==> eq) + (@list_caset A (fun _ => P)). +Goal forall (T T' : Set) (a3 : list T), exists y2, forall (a4 : T' -> bool), + match a3 with + | nil => 0 + | (_ :: _)%list => 1 + end = y2 a4. + clear; eexists; intros. + reflexivity. Undo. + Local Ltac t := + lazymatch goal with + | [ |- match ?v with nil => ?N | cons x xs => @?C x xs end = _ :> ?P ] + => let T := type of v in + let A := match (eval hnf in T) with list ?A => A end in + refine (@list_caset_Proper' A P _ _ _ _ _ _ _ _ _ + : @list_caset A (fun _ => P) N C v = match _ with nil => _ | cons x xs => _ end) + end. + (etransitivity; [ t | reflexivity ]) || fail 0 "too early". + Undo. + t. diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v new file mode 100644 index 000000000..ed4443786 --- /dev/null +++ b/test-suite/bugs/closed/4782.v @@ -0,0 +1,9 @@ +(* About typing of with bindings *) + +Record r : Type := mk_r { type : Type; cond : type -> Prop }. + +Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p. + +Goal p. +Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil. + diff --git a/test-suite/bugs/closed/4787.v b/test-suite/bugs/closed/4787.v new file mode 100644 index 000000000..b586cba50 --- /dev/null +++ b/test-suite/bugs/closed/4787.v @@ -0,0 +1,9 @@ +(* [Unset Bracketing Last Introduction Pattern] was not working *) + +Unset Bracketing Last Introduction Pattern. + +Goal forall T (x y : T * T), fst x = fst y /\ snd x = snd y -> x = y. +do 10 ((intros [] || intro); simpl); reflexivity. +Qed. + + diff --git a/test-suite/bugs/closed/4813.v b/test-suite/bugs/closed/4813.v new file mode 100644 index 000000000..5f8ea74c1 --- /dev/null +++ b/test-suite/bugs/closed/4813.v @@ -0,0 +1,9 @@ +(* On the strength of "apply with" (see also #4782) *) + +Record ProverT := { Facts : Type }. +Record ProverT_correct (P : ProverT) := { Valid : Facts P -> Prop ; + Valid_weaken : Valid = Valid }. +Definition reflexivityValid (_ : unit) := True. +Definition reflexivityProver_correct : ProverT_correct {| Facts := unit |}. +Proof. + eapply Build_ProverT_correct with (Valid := reflexivityValid). diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v new file mode 100644 index 000000000..86597c88f --- /dev/null +++ b/test-suite/bugs/closed/4816.v @@ -0,0 +1,17 @@ +Section foo. +Polymorphic Universes A B. +Fail Constraint A <= B. +End foo. +(* gives an anomaly Universe undefined *) + +Universes X Y. +Section Foo. + Polymorphic Universes Z W. + Polymorphic Constraint W < Z. + + Fail Definition bla := Type@{W}. + Polymorphic Definition bla := Type@{W}. + Section Bar. + Fail Constraint X <= Z. + End Bar. +End Foo. diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v new file mode 100644 index 000000000..7c65accfe --- /dev/null +++ b/test-suite/bugs/opened/4813.v @@ -0,0 +1,5 @@ +(* An example one would like to see succeeding *) + +Record T := BT { t : Set }. +Record U (x : T) := BU { u : t x -> Prop }. +Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 20e274e25..21a8cf9ed 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -3,3 +3,22 @@ Error: Ltac variable y depends on pattern variable name z which is not bound in Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize dependent z +The command has indeed failed with message: +In nested Ltac calls to "g1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "f1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "g2", "g1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "f2", "f1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +Ltac call to "h" failed. +Error: Ltac variable x is bound to I which cannot be coerced to +a declared or quantified hypothesis. +The command has indeed failed with message: +In nested Ltac calls to "h" and "injection", last call failed. +Error: No primitive equality found. diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 373b870b9..dfa60eeda 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -25,3 +25,21 @@ Ltac f x y z := generalize dependent z. Print Ltac f. + +(* Error messages *) + +Ltac g1 x := refine x. +Tactic Notation "g2" constr(x) := g1 x. +Tactic Notation "f1" constr(x) := refine x. +Ltac f2 x := f1 x. +Goal False. +Fail g1 I. +Fail f1 I. +Fail g2 I. +Fail f2 I. + +Ltac h x := injection x. +Goal True -> False. +Fail h I. +intro H. +Fail h H. diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index aa4411704..39bc59a65 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -7,6 +7,10 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.4 *) + +(** Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4. *) +Require Export Coq.Compat.Coq85. + (** See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates *) (** This is required in Coq 8.5 to use the [omega] tactic; in Coq 8.4, it's automatically available. But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't [Import] it. *) Require Coq.omega.Omega. diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index af2e04f88..3fc74943e 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -12,5 +12,5 @@ behave as "intros [H|H]" but leave instead hypotheses quantified in the goal, here producing subgoals A->C and B->C. *) -Unset Bracketing Last Introduction Pattern. - +Global Unset Bracketing Last Introduction Pattern. +Global Unset Regular Subst Tactic. diff --git a/theories/theories.itarget b/theories/theories.itarget deleted file mode 100644 index aacab2d97..000000000 --- a/theories/theories.itarget +++ /dev/null @@ -1,25 +0,0 @@ -Arith/vo.otarget -Bool/vo.otarget -Classes/vo.otarget -Compat/vo.otarget -FSets/vo.otarget -MSets/vo.otarget -Structures/vo.otarget -Init/vo.otarget -Lists/vo.otarget -Vectors/vo.otarget -Logic/vo.otarget -PArith/vo.otarget -NArith/vo.otarget -Numbers/vo.otarget -Program/vo.otarget -QArith/vo.otarget -Reals/vo.otarget -Relations/vo.otarget -Setoids/vo.otarget -Sets/vo.otarget -Sorting/vo.otarget -Strings/vo.otarget -Unicode/vo.otarget -Wellfounded/vo.otarget -ZArith/vo.otarget diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 91bb88753..45e843e60 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -27,8 +27,9 @@ let rec print_list sep = function | x :: l -> print x; print sep; print_list sep l | [] -> () -let list_iter_i f = - let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1 +let rec print_prefix_list sep = function + | x :: l -> print sep; print x; print_prefix_list sep l + | [] -> () let section s = let l = String.length s in @@ -104,8 +105,10 @@ let is_genrule r = (* generic rule (like bar%foo: ...) *) Str.string_match genrule r 0 let string_prefix a b = - let rec aux i = try if a.[i] = b.[i] then aux (i+1) else i with |Invalid_argument _ -> i in - String.sub a 0 (aux 0) + let rec aux i = + try if a.[i] = b.[i] then aux (i+1) else i with Invalid_argument _ -> i + in + String.sub a 0 (aux 0) let is_prefix dir1 dir2 = let l1 = String.length dir1 in @@ -120,7 +123,10 @@ let is_prefix dir1 dir2 = let physical_dir_of_logical_dir ldir = let le = String.length ldir - 1 in - let pdir = if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in + let pdir = + if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) + else String.copy ldir + in for i = 0 to le - 1 do if pdir.[i] = '.' then pdir.[i] <- '/'; done; @@ -135,62 +141,74 @@ let standard opt = print "\"\n\n" let classify_files_by_root var files (inc_ml,inc_i,inc_r) = - if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) - && not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_i) then - begin - let absdir_of_files = List.rev_map + if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r + || List.exists (fun (pdir,_,_) -> pdir = ".") inc_i + then () + else + let absdir_of_files =List.rev_map (fun x -> CUnix.canonical_path_name (Filename.dirname x)) - files in - (* files in scope of a -I option (assuming they are no overlapping) *) - let has_inc_i = List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml in - if has_inc_i then - begin - printf "%sINC=" var; - List.iter (fun (pdir,absdir) -> - if List.mem absdir absdir_of_files - then printf - "$(filter $(wildcard %s/*),$(%s)) " - pdir var - ) inc_ml; - printf "\n"; - end; - (* Files in the scope of a -R option (assuming they are disjoint) *) - list_iter_i (fun i (pdir,_,abspdir) -> - if List.exists (is_prefix abspdir) absdir_of_files then - printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" - var i pdir pdir var) - (inc_i@inc_r); - end + files + in + (* files in scope of a -I option (assuming they are no overlapping) *) + if List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml then + begin + printf "%sINC=" var; + List.iter (fun (pdir,absdir) -> + if List.mem absdir absdir_of_files + then printf "$(filter $(wildcard %s/*),$(%s)) " pdir var) + inc_ml; + printf "\n"; + end; + (* Files in the scope of a -R option (assuming they are disjoint) *) + List.iteri (fun i (pdir,_,abspdir) -> + if List.exists (is_prefix abspdir) absdir_of_files then + printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" + var i pdir pdir var) + (inc_i@inc_r) let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) = - let var_x_absdirs_l = List.rev_map - (fun (v,l) -> (v,List.rev_map (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l)) - var_x_files_l in - let var_filter f g = List.fold_left (fun acc (var,dirs) -> - if f dirs - then (g var)::acc else acc) [] var_x_absdirs_l in - (* All files caught by a -R . option (assuming it is the only one) *) + let var_x_absdirs_l = + List.rev_map + (fun (v,l) -> + (v,List.rev_map + (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l)) + var_x_files_l + in + let var_filter f g = + List.fold_left + (fun acc (var,dirs) -> if f dirs then (g var)::acc else acc) + [] var_x_absdirs_l + in + (* All files caught by a -R . option (assuming it is the only one) *) match inc_i@inc_r with - |[(".",t,_)] -> (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l]) + |[(".",t,_)] -> + (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l]) |l -> try let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in - let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n" in + let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n" + in (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l]) with Not_found -> - ( (* vars for -Q options *) - Some (var_filter (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml) (fun x -> x)), + let varq = var_filter + (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml) + (fun x -> x) + in (* (physical dir, physical dir of logical path,vars) for -R options (assuming physical dirs are disjoint) *) - if l = [] then - [".","$(INSTALLDEFAULTROOT)",[]] - else - Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) -> - let vars_r = var_filter (List.exists (is_prefix abspdir)) (fun x -> x^string_of_int i) in - let pdir' = physical_dir_of_logical_dir ldir in - (pdir,pdir',vars_r)::out) 1 [] l - ) + let other = + if l = [] then + [".","$(INSTALLDEFAULTROOT)",[]] + else + Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) -> + let vars_r = var_filter + (List.exists (is_prefix abspdir)) + (fun x -> x^string_of_int i) + in + let pdir' = physical_dir_of_logical_dir ldir in + (pdir,pdir',vars_r)::out) 1 [] l + in (Some varq, other) let install_include_by_root perms = let install_dir for_i (pdir,pdir',vars) = @@ -266,33 +284,38 @@ let where_put_doc = function install-doc will put anything in $INSTALLDEFAULTROOT\n" in "$(INSTALLDEFAULTROOT)" -let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) inc = function +let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function |Project_file.NoInstall -> () |is_install -> let not_empty = function |[] -> false |_::_ -> true in - let cmofiles = List.rev_append mlpackfiles (List.rev_append mlfiles ml4files) in - let cmifiles = List.rev_append mlifiles cmofiles in - let cmxsfiles = List.rev_append cmofiles mllibfiles in - let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in + let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in + let cmis = List.rev_append mlis cmos in + let cmxss = List.rev_append cmos mllibs in + let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in let where_what_oth = vars_to_put_by_root - [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)] + [("VOFILES",vfiles);("VFILES",vfiles); + ("GLOBFILES",vfiles);("NATIVEFILES",vfiles); + ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)] inc in let doc_dir = where_put_doc inc in - let () = if is_install = Project_file.UnspecInstall then - print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" in - if (not_empty cmxsfiles) then begin + if is_install = Project_file.UnspecInstall then begin + print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" + end; + if not_empty cmxss then begin print "install-natdynlink:\n"; install_include_by_root "0755" where_what_cmxs; print "\n"; end; - if (not_empty cmxsfiles) then begin + if not_empty cmxss then begin print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n"; printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; printf "\t install -m 0755 $? \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; print "\n"; end; print "install:"; - if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; + if not_empty cmxss then begin + print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; + end; print "\n"; install_include_by_root "0644" where_what_oth; List.iter @@ -307,7 +330,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in print "\tdone\n" in print "install-doc:\n"; if not_empty vfiles then install_one_kind "html" doc_dir; - if not_empty mlifiles then install_one_kind "mlihtml" doc_dir; + if not_empty mlis then install_one_kind "mlihtml" doc_dir; print "\n"; let uninstall_one_kind kind dir = printf "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL)/%s \\\\\\n' >> \"$@\"\n" dir; @@ -317,10 +340,10 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in in printf "uninstall_me.sh: %s\n" !makefile_name; print "\techo '#!/bin/sh' > $@\n"; - if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs; + if not_empty cmxss then uninstall_by_root where_what_cmxs; uninstall_by_root where_what_oth; if not_empty vfiles then uninstall_one_kind "html" doc_dir; - if not_empty mlifiles then uninstall_one_kind "mlihtml" doc_dir; + if not_empty mlis then uninstall_one_kind "mlihtml" doc_dir; print "\tchmod +x $@\n"; print "\n"; print "uninstall: uninstall_me.sh\n"; @@ -339,11 +362,14 @@ let make_makefile sds = let clean sds sps = print "clean::\n"; - if !some_mlfile || !some_mlifile || !some_ml4file || !some_mllibfile || !some_mlpackfile then begin - print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n"; - print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n"; - print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n"; - end; + if !some_mlfile || !some_mlifile || !some_ml4file + || !some_mllibfile || !some_mlpackfile + then + begin + print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n"; + print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n"; + print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n"; + end; if !some_vfile then begin print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n"; @@ -380,38 +406,67 @@ let header_includes () = () let implicit () = section "Implicit rules."; let mli_rules () = - print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n"; + print "\t$(SHOW)'CAMLC -c $<'\n"; + print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n"; - print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(SHOW)'CAMLDEP $<'\n"; + print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + in let ml4_rules () = - print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n"; + print "\t$(SHOW)'CAMLC -pp -c $<'\n"; + print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n"; - print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "\t$(SHOW)'CAMLOPT -pp -c $<'\n"; + print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; - print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(SHOW)'CAMLDEP -pp $<'\n"; + print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml_rules () = - print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n"; + print "\t$(SHOW)'CAMLC -c $<'\n"; + print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; - print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "\t$(SHOW)'CAMLOPT -c $<'\n"; + print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n"; - print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(SHOW)'CAMLDEP $<'\n"; + print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *) - print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx -\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; - print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" in + print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx\n"; + print "\t$(SHOW)'CAMLOPT -shared -o $@'\n"; + print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; + print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n"; + print "\t$(SHOW)'CAMLOPT -shared -o $@'\n"; + print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" + in let mllib_rules () = - print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; + print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n"; + print "\t$(SHOW)'CAMLC -a -o $@'\n"; + print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; + print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n"; + print "\t$(SHOW)'CAMLOPT -a -o $@'\n"; + print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n"; - print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(SHOW)'COQDEP $<'\n"; + print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + in let mlpack_rules () = - print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; - print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; + print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n"; + print "\t$(SHOW)'CAMLC -pack -o $@'\n"; + print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; + print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n"; + print "\t$(SHOW)'CAMLOPT -pack -o $@'\n"; + print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n"; - print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; -in + print "\t$(SHOW)'COQDEP $<'\n"; + print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" + in let v_rules () = - print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(VOFILES): %.vo: %.v\n"; + print "\t$(SHOW)COQC $*\n"; + print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n"; @@ -420,7 +475,8 @@ in print "$(VFILES:.v=.g.tex): %.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n"; print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@\n\n"; print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n"; - print "\t$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; + print "\t$(SHOW)'COQDEP $<'\n"; + print "\t$(HIDE)$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" in if !some_mlifile then mli_rules (); @@ -472,6 +528,7 @@ let variables is_install opt (args,defs) = print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n"; print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n"; print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n"; + print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n"; print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; print "ifeq ($(CAMLP4),camlp5) @@ -516,7 +573,11 @@ let parameters () = print "# TIMECMD set a command to log .v compilation time;\n"; print "# TIMED if non empty, use the default time command as TIMECMD;\n"; print "# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;\n"; - print "# DSTROOT to specify a prefix to install path.\n\n"; + print "# DSTROOT to specify a prefix to install path.\n"; + print "# VERBOSE to disable the short display of compilation rules.\n\n"; + print "VERBOSE?=\n"; + print "SHOW := $(if $(VERBOSE),@true \"\",@echo \"\")\n"; + print "HIDE := $(if $(VERBOSE),,@)\n\n"; print "# Here is a hack to make $(eval $(shell works:\n"; print "define donewline\n\n\nendef\n"; print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n"; @@ -527,28 +588,35 @@ let parameters () = print " $(filter-out Warning: Error:,\\\n"; print " $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n" -let include_dirs (inc_ml,inc_i,inc_r) = +let include_dirs (inc_ml,inc_q,inc_r) = let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in - let parse_includes l = List.map (fun (x,l,_) -> - let l' = if l = "" then "\"\"" else l in - "-Q \"" ^ x ^ "\" " ^ l' ^"") l in - let parse_rec_includes l = List.map (fun (p,l,_) -> - let l' = if l = "" then "\"\"" else l in - "-R \"" ^ p ^ "\" " ^ l' ^"") l in + let includes = + List.map (fun (p,l,_) -> + let l' = if l = "" then "\"\"" else l in + " \"" ^ p ^ "\" " ^ l' ^"") in let str_ml = parse_ml_includes inc_ml in - let str_i = parse_includes inc_i in - let str_r = parse_rec_includes inc_r in - section "Libraries definitions."; - if !some_ml4file || !some_mlfile || !some_mlifile then begin - print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n"; - end; - if !some_vfile || !some_mllibfile || !some_mlpackfile then begin - print "COQLIBS?="; print_list "\\\n " str_i; - List.iter (fun x -> print "\\\n "; print x) str_r; - List.iter (fun x -> print "\\\n "; print x) str_ml; print "\n"; - print "COQDOCLIBS?="; print_list "\\\n " str_i; - List.iter (fun x -> print "\\\n "; print x) str_r; print "\n\n"; - end + section "Libraries definitions."; + if !some_ml4file || !some_mlfile || !some_mlifile then begin + print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n"; + end; + if !some_vfile || !some_mllibfile || !some_mlpackfile then begin + print "COQLIBS?="; + print_prefix_list "\\\n -Q" (includes inc_q); + print_prefix_list "\\\n -R" (includes inc_r); + print_prefix_list "\\\n " str_ml; + print "\n"; + end; + if !some_vfile then begin + print "COQCHKLIBS?="; + print_prefix_list "\\\n -R" (includes inc_q); + print_prefix_list "\\\n -R" (includes inc_r); + print "\n"; + print "COQDOCLIBS?="; + print_prefix_list "\\\n -R" (includes inc_q); + print_prefix_list "\\\n -R" (includes inc_r); + print "\n"; + end; + print "\n" let double_colon = ["clean"; "cleanall"; "archclean"] @@ -579,10 +647,13 @@ let forpacks l = let () = if l <> [] then section "Ad-hoc implicit rules for mlpack." in List.iter (fun it -> let h = Filename.chop_extension it in + let pk = String.capitalize (Filename.basename h) in printf "$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml\n" h; - printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" (String.capitalize (Filename.basename h)); + printf "\t$(SHOW)'CAMLOPT -c -for-pack %s $<'\n" pk; + printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" pk; printf "$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml4\n" h; - printf "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" (String.capitalize (Filename.basename h)) + printf "\t$(SHOW)'CAMLOPT -c -pp -for-pack %s $<'\n" pk; + printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" pk ) l let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other_targets inc = @@ -721,7 +792,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "all-gal.pdf: $(VFILES)\n"; print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; print "validate: $(VOFILES)\n"; - print "\t$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))\n\n"; + print "\t$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))\n\n"; print "beautify: $(VFILES:=.beautified)\n"; print "\tfor file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done\n"; print "\t@echo \'Do not do \"make clean\" until you are sure that everything went well!\'\n"; @@ -774,22 +845,24 @@ let command_line args = print_list args; print "\n#\n\n" -let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l) = +let ensure_root_dir (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc = + let (ml_inc,i_inc,r_inc) = inc in let here = Sys.getcwd () in - let not_tops =List.for_all (fun s -> s <> Filename.basename s) in + let not_tops = List.for_all (fun s -> s <> Filename.basename s) in if List.exists (fun (_,_,x) -> x = here) i_inc || List.exists (fun (_,_,x) -> is_prefix x here) r_inc - || (not_tops v && not_tops mli && not_tops ml4 && not_tops ml - && not_tops mllib && not_tops mlpack) then - l + || (not_tops vfiles && not_tops mlis && not_tops ml4s && not_tops mls + && not_tops mllibs && not_tops mlpacks) + then + inc else ((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc) -let warn_install_at_root_directory - (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) = +let warn_install_at_root_directory (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc = + let (inc_ml,inc_i,inc_r) = inc in let inc_top = List.filter (fun (_,ldir,_) -> ldir = "") (inc_r@inc_i) in let inc_top_p = List.map (fun (p,_,_) -> p) inc_top in - let files = vfiles @ mlifiles @ ml4files @ mlfiles @ mllibfiles @ mlpackfiles in + let files = vfiles @ mlis @ ml4s @ mls @ mllibs @ mlpacks in if List.exists (fun f -> List.mem (Filename.dirname f) inc_top_p) files then Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R or -Q %sis recommended\n" @@ -827,7 +900,9 @@ let do_makefile args = |[] -> var := false |_::_ -> var := true in let (project_file,makefile,is_install,opt),l = - try Project_file.process_cmd_line Filename.current_dir_name (None,None,Project_file.UnspecInstall,true) [] args + try + Project_file.process_cmd_line Filename.current_dir_name + (None,None,Project_file.UnspecInstall,true) [] args with Project_file.Parsing_error -> usage () in let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs = Project_file.split_arguments l in @@ -851,7 +926,9 @@ let do_makefile args = List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; let inc = ensure_root_dir targets inc in - if is_install <> Project_file.NoInstall then warn_install_at_root_directory targets inc; + if is_install <> Project_file.NoInstall then begin + warn_install_at_root_directory targets inc; + end; check_overlapping_include inc; banner (); header_includes (); diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 670ff487c..57fcd5dd2 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -33,10 +33,6 @@ rule mllib_list = parse open Printf open Unix -(** [coqdep_boot] is a stripped-down version of [coqdep] used to treat - with mllib files. -*) - (* Makefile's escaping rules are awful: $ is escaped by doubling and other special characters are escaped by backslash prefixing while backslashes themselves must be escaped only if part of a sequence @@ -132,6 +128,7 @@ let add_ml_known, search_ml_known = mkknown () let add_mlpack_known, search_mlpack_known = mkknown () let mllibAccu = ref ([] : (string * dir) list) +let mlpackAccu = ref ([] : (string * dir) list) let add_caml_known phys_dir f = let basename,suff = get_extension f [".ml";".ml4";".mlpack"] in @@ -148,18 +145,15 @@ let traite_fichier_modules md ext = let chan = open_in (md ^ ext) in let list = mllib_list (Lexing.from_channel chan) in List.fold_left - (fun a_faire str -> match search_mlpack_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire^" "^file - | None -> + (fun acc str -> + match search_mlpack_known str with + | Some mldir -> (file_name str mldir) :: acc + | None -> match search_ml_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire^" "^file - | None -> a_faire) "" list + | Some mldir -> (file_name str mldir) :: acc + | None -> acc) [] (List.rev list) with - | Sys_error _ -> "" + | Sys_error _ -> [] | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) let addQueue q v = q := v :: !q @@ -167,22 +161,43 @@ let addQueue q v = q := v :: !q let treat_file old_name = let name = Filename.basename old_name in let dirname = Some (Filename.dirname old_name) in - match get_extension name [".mllib"] with + match get_extension name [".mllib";".mlpack"] with | (base,".mllib") -> addQueue mllibAccu (base,dirname) + | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) | _ -> () let mllib_dependencies () = List.iter (fun (name,dirname) -> let fullname = file_name name dirname in - let dep = traite_fichier_modules fullname ".mllib" in + let deps = traite_fichier_modules fullname ".mllib" in + let sdeps = String.concat " " deps in let efullname = escape fullname in - printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep; - printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname; + printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname sdeps; + printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" + efullname efullname; + printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" + efullname efullname efullname; flush Pervasives.stdout) (List.rev !mllibAccu) +let mlpack_dependencies () = + List.iter + (fun (name,dirname) -> + let fullname = file_name name dirname in + let modname = String.capitalize name in + let deps = traite_fichier_modules fullname ".mlpack" in + let sdeps = String.concat " " deps in + let efullname = escape fullname in + printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname sdeps; + List.iter (fun d -> printf "%s_FORPACK:= -for-pack %s\n" d modname) deps; + printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" + efullname efullname; + printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" + efullname efullname efullname; + flush Pervasives.stdout) + (List.rev !mlpackAccu) + let rec parse = function | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) @@ -192,10 +207,11 @@ let rec parse = function | f :: ll -> treat_file f; parse ll | [] -> () -let coqdep_boot () = +let main () = if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); - mllib_dependencies () + mllib_dependencies (); + mlpack_dependencies () -let _ = Printexc.catch coqdep_boot () +let _ = Printexc.catch main () } diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ad848ccfc..e17cd2086 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -69,12 +69,12 @@ let rec contract3' env a b c = function let (env',t1,t2) = contract2 env' t1 t2 in contract3 env a b c, ConversionFailed (env',t1,t2) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | MetaOccurInBody _ | InstanceNotSameType _ + | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities | UnifUnivInconsistency _ as x -> contract3 env a b c, x - | CannotSolveConstraint ((pb,env,t,u),x) -> - let env,t,u = contract2 env t u in + | CannotSolveConstraint ((pb,env',t,u),x) -> + let env',t,u = contract2 env' t u in let y,x = contract3' env a b c x in - y,CannotSolveConstraint ((pb,env,t,u),x) + y,CannotSolveConstraint ((pb,env',t,u),x) (** Ad-hoc reductions *) @@ -323,6 +323,8 @@ let explain_unification_error env sigma p1 p2 = function (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e + | ProblemBeyondCapabilities -> + [] in match aux p1 p2 e with | [] -> mt () diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 52117f13f..b22d53f54 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -827,7 +827,7 @@ let make_interpretation_type isrec isonlybinding = function | NtnInternTypeConstr | NtnInternTypeIdent -> if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr | NtnInternTypeBinder when isrec -> NtnTypeBinderList - | NtnInternTypeBinder -> error "Type not allowed in recursive notation." + | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders." let make_interpretation_vars recvars allvars = let eq_subscope (sc1, l1) (sc2, l2) = diff --git a/toplevel/search.ml b/toplevel/search.ml index 646e2e08a..e670b59b7 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -257,10 +257,10 @@ let search_about gopt items mods = format_display !ans type search_constraint = - | Name_Pattern of string - | Type_Pattern of string - | SubType_Pattern of string - | In_Module of string list + | Name_Pattern of Str.regexp + | Type_Pattern of Pattern.constr_pattern + | SubType_Pattern of Pattern.constr_pattern + | In_Module of Names.DirPath.t | Include_Blacklist type 'a coq_object = { @@ -269,40 +269,21 @@ type 'a coq_object = { coq_object_object : 'a; } -let interface_search flags = - let env = Global.env () in +let interface_search = let rec extract_flags name tpe subtpe mods blacklist = function | [] -> (name, tpe, subtpe, mods, blacklist) - | (Name_Pattern s, b) :: l -> - let regexp = - try Str.regexp s - with e when Errors.noncritical e -> - Errors.errorlabstrm "Search.interface_search" - (str "Invalid regexp: " ++ str s) - in + | (Name_Pattern regexp, b) :: l -> extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l - | (Type_Pattern s, b) :: l -> - let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern env constr in + | (Type_Pattern pat, b) :: l -> extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l - | (SubType_Pattern s, b) :: l -> - let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern env constr in + | (SubType_Pattern pat, b) :: l -> extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l - | (In_Module m, b) :: l -> - let path = String.concat "." m in - let m = Pcoq.parse_string Pcoq.Constr.global path in - let (_, qid) = Libnames.qualid_of_reference m in - let id = - try Nametab.full_name_module qid - with Not_found -> - Errors.errorlabstrm "Search.interface_search" - (str "Module " ++ str path ++ str " not found.") - in + | (In_Module id, b) :: l -> extract_flags name tpe subtpe ((id, b) :: mods) blacklist l | (Include_Blacklist, b) :: l -> extract_flags name tpe subtpe mods b l in + fun ?glnum flags -> let (name, tpe, subtpe, mods, blacklist) = extract_flags [] [] [] [] false flags in @@ -359,5 +340,5 @@ let interface_search flags = let iter ref env typ = if filter_function ref env typ then print_function ref env typ in - let () = generic_search None iter in (* TODO: chose a goal number? *) + let () = generic_search glnum iter in !ans diff --git a/toplevel/search.mli b/toplevel/search.mli index 78b0c45c0..9f209a17e 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -47,13 +47,13 @@ val search_about : int option -> (bool * glob_search_about_item) list type search_constraint = (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) - | Name_Pattern of string + | Name_Pattern of Str.regexp (** Whether the object type satisfies a pattern *) - | Type_Pattern of string + | Type_Pattern of Pattern.constr_pattern (** Whether some subtype of object type satisfies a pattern *) - | SubType_Pattern of string + | SubType_Pattern of Pattern.constr_pattern (** Whether the object pertains to a module *) - | In_Module of string list + | In_Module of Names.DirPath.t (** Bypass the Search blacklist *) | Include_Blacklist @@ -63,7 +63,7 @@ type 'a coq_object = { coq_object_object : 'a; } -val interface_search : (search_constraint * bool) list -> +val interface_search : ?glnum:int -> (search_constraint * bool) list -> string coq_object list (** {6 Generic search function} *) |