diff options
26 files changed, 225 insertions, 131 deletions
@@ -118,7 +118,7 @@ else stage1 $(STAGE1_TARGETS): always $(call stage-template,1) -CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.dep.ps %.dot +CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot ifdef CM_STAGE1 $(CAML_OBJECT_PATTERNS): always $(call stage-template,1) @@ -189,7 +189,7 @@ archclean: clean-ide cleantheories rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT) rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE) - find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f + find . -name '*.cmx' -or -name '*.cmxs' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f rm -f $(TOOLS) $(CSDPCERT) clean-ide: diff --git a/Makefile.build b/Makefile.build index bba84709bd..61d4944835 100644 --- a/Makefile.build +++ b/Makefile.build @@ -67,6 +67,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ -I proofs -I tactics -I pretyping \ -I interp -I toplevel -I parsing -I ide/utils -I ide \ -I contrib/omega -I contrib/romega -I contrib/micromega \ + -I contrib/quote \ -I contrib/ring -I contrib/dp -I contrib/setoid_ring \ -I contrib/xml -I contrib/extraction \ -I contrib/interface -I contrib/fourier \ @@ -168,12 +169,14 @@ coqbinaries:: ${COQBINARIES} ${CSDPCERT} coq: coqlib tools coqbinaries -coqlib:: theories contrib +coqlib:: initplugins theories contrib -coqlight: theories-light tools coqbinaries +coqlight: initplugins theories-light tools coqbinaries states:: states/initial.coq +initplugins: $(INITPLUGINSOPT) $(INITPLUGINS) + $(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ @@ -193,12 +196,12 @@ CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(CHICKENOPT): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ unix.cmxa gramlib.cmxa checker/check.cmxa checker/main.ml + $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ unix.cmxa gramlib.cmxa $^ $(STRIP) $@ $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml + $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma $^ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE) @@ -207,13 +210,11 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) $(COQMKTOPBYTE): $(COQMKTOPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma \ - $(COQMKTOPCMO) $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^ $(OSDEPLIBS) $(COQMKTOPOPT): $(COQMKTOPCMX) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa \ - $(COQMKTOPCMX) $(OSDEPLIBS) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa $^ $(OSDEPLIBS) $(STRIP) $@ $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP) @@ -258,108 +259,109 @@ hightactics: $(HIGHTACTICS) # target for libraries lib/lib.cma: $(LIBREP) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBREP) - lib/lib.cmxa: $(LIBREP:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBREP:.cmo=.cmx) kernel/kernel.cma: $(KERNEL) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(KERNEL) - kernel/kernel.cmxa: $(KERNEL:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(KERNEL:.cmo=.cmx) - -checker/check.cma: $(MCHECKER) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $(MCHECKER) - -checker/check.cmxa: $(MCHECKER:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx) library/library.cma: $(LIBRARY) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBRARY) - library/library.cmxa: $(LIBRARY:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBRARY:.cmo=.cmx) pretyping/pretyping.cma: $(PRETYPING) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PRETYPING) - pretyping/pretyping.cmxa: $(PRETYPING:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PRETYPING:.cmo=.cmx) interp/interp.cma: $(INTERP) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(INTERP) - interp/interp.cmxa: $(INTERP:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(INTERP:.cmo=.cmx) parsing/parsing.cma: $(PARSING) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PARSING) - parsing/parsing.cmxa: $(PARSING:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PARSING:.cmo=.cmx) proofs/proofs.cma: $(PROOFS) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PROOFS) - proofs/proofs.cmxa: $(PROOFS:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PROOFS:.cmo=.cmx) tactics/tactics.cma: $(TACTICS) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TACTICS) - tactics/tactics.cmxa: $(TACTICS:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TACTICS:.cmo=.cmx) toplevel/toplevel.cma: $(TOPLEVEL) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TOPLEVEL) - toplevel/toplevel.cmxa: $(TOPLEVEL:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TOPLEVEL:.cmo=.cmx) parsing/highparsing.cma: $(HIGHPARSING) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHPARSING) - parsing/highparsing.cmxa: $(HIGHPARSING:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHPARSING:.cmo=.cmx) tactics/hightactics.cma: $(HIGHTACTICS) +tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx) + +contrib/contrib.cma: $(CONTRIBSTATIC) +contrib/contrib.cmxa: $(CONTRIBSTATIC:.cmo=.cmx) + +$(OMEGACMA): $(OMEGACMO) +$(OMEGACMA:.cma=.cmxa): $(OMEGACMO:.cmo=.cmx) + +$(ROMEGACMA): $(ROMEGACMO) +$(ROMEGACMA:.cma=.cmxa): $(ROMEGACMO:.cmo=.cmx) + +$(MICROMEGACMA): $(MICROMEGACMO) +$(MICROMEGACMA:.cma=.cmxa): $(MICROMEGACMO:.cmo=.cmx) + +$(QUOTACMA): $(QUOTECMO) +$(QUOTECMA:.cma=.cmxa): $(QUOTECMO:.cmo=.cmx) + +$(RINGCMA): $(RINGCMO) +$(RINGCMA:.cma=.cmxa): $(RINGCMO:.cmo=.cmx) + +$(NEWRINGCMA): $(NEWRINGCMO) +$(NEWRINGCMA:.cma=.cmxa): $(NEWRINGCMO:.cmo=.cmx) + +$(FIELDCMA): $(FIELDCMO) +$(FIELDCMA:.cma=.cmxa): $(FIELDCMO:.cmo=.cmx) + +$(XMLCMA): $(XMLCMO) +$(XMLCMA:.cma=.cmxa): $(XMLCMO:.cmo=.cmx) + +$(FOURIERCMA): $(FOURIERCMO) +$(FOURIERCMA:.cma=.cmxa): $(FOURIERCMO:.cmo=.cmx) + +$(EXTRACTIONCMA): $(EXTRACTIONCMO) +$(EXTRACTIONCMA:.cma=.cmxa): $(EXTRACTIONCMO:.cmo=.cmx) + +$(RTAUTOCMA): $(RTAUTOCMO) +$(RTAUTOCMA:.cma=.cmxa): $(RTAUTOCMO:.cmo=.cmx) + +$(JPROVERCMA): $(JPROVERCMO) +$(JPROVERCMA:.cma=.cmxa): $(JPROVERCMO:.cmo=.cmx) + +$(FOCMA): $(FOCMO) +$(FOCMA:.cma=.cmxa): $(FOCMO:.cmo=.cmx) + +$(CCCMA): $(CCCMO) +$(CCCMA:.cma=.cmxa): $(CCCMO:.cmo=.cmx) + +$(DPCMA): $(DPCMO) +$(DPCMA:.cma=.cmxa): $(DPCMO:.cmo=.cmx) + +$(FUNINDCMA): $(FUNINDCMO) +$(FUNINDCMA:.cma=.cmxa): $(FUNINDCMO:.cmo=.cmx) + +$(SUBTACCMA): $(SUBTACCMO) +$(SUBTACCMA:.cma=.cmxa): $(SUBTACCMO:.cmo=.cmx) + +%.cma: $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHTACTICS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^ -tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx) +%.cmxa: $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHTACTICS:.cmo=.cmx) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^ -contrib/contrib.cma: $(CONTRIB) +# For the checker, different flags may be used + +checker/check.cma: $(MCHECKER) $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(CONTRIB) + $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $^ -contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx) +checker/check.cmxa: $(MCHECKER:.cmo=.cmx) $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(CONTRIB:.cmo=.cmx) + $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $^ ########################################################################### # Csdp to micromega special targets @@ -368,12 +370,12 @@ contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx) ifeq ($(BEST),opt) contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $(CSDPCERTCMX) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $^ $(STRIP) $@ else contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $^ endif ########################################################################### @@ -421,11 +423,11 @@ ide/%.cmx: ide/%.ml | ide/%.ml.d ide/ide.cma: $(COQIDECMO) $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(COQIDECMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^ ide/ide.cmxa: $(COQIDECMO:.cmo=.cmx) $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(COQIDECMO:.cmo=.cmx) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^ # install targets @@ -551,7 +553,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \ # contribs (interface not included) ########################################################################### -contrib: $(CONTRIBVO) $(CONTRIBCMO) +contrib: $(CONTRIBVO) omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) ring: $(RINGVO) $(RINGCMO) @@ -575,7 +577,7 @@ states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/M $(SHOW)'BUILD $@' $(HIDE)$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq -theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) +theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC -nois $<' $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$* @@ -593,27 +595,27 @@ tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEP): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $^ $(OSDEPLIBS) $(GALLINA): $(GALLINACMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^ -$(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo +$(COQMAKEFILE): config/coq_config.cmo tools/coq_makefile.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^ $(COQTEX): tools/coq-tex.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^ $(COQWC): tools/coqwc.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^ $(COQDOC): $(COQDOCCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^ ########################################################################### # Installation @@ -730,7 +732,7 @@ dev/printers.cma: $(PRINTERSCMO) $(HIDE)$(OCAMLC) $(BYTEFLAGS) gramlib.cma $(PRINTERSCMO) -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(PRINTERSCMO) -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ parsing/grammar.cma: $(GRAMMARCMO) $(SHOW)'Testing $@' diff --git a/Makefile.common b/Makefile.common index 4ca7e2e45b..63740d086a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -234,33 +234,42 @@ HIGHTACTICS:=\ tactics/extratactics.cmo tactics/eauto.cmo tactics/class_tactics.cmo \ tactics/tauto.cmo tactics/eqdecide.cmo +OMEGACMA:=contrib/omega/omega_plugin.cma OMEGACMO:=\ contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ contrib/omega/g_omega.cmo +ROMEGACMA:=contrib/romega/romega_plugin.cma ROMEGACMO:=\ contrib/romega/const_omega.cmo \ contrib/romega/refl_omega.cmo contrib/romega/g_romega.cmo +MICROMEGACMA:=contrib/micromega/micromega_plugin.cma MICROMEGACMO:=\ contrib/micromega/mutils.cmo \ contrib/micromega/micromega.cmo contrib/micromega/mfourier.cmo \ contrib/micromega/certificate.cmo \ contrib/micromega/coq_micromega.cmo contrib/micromega/g_micromega.cmo +QUOTECMA:=contrib/quote/quote_plugin.cma +QUOTECMO:=\ + contrib/quote/quote.cmo contrib/quote/g_quote.cmo + +RINGCMA:=contrib/ring/ring_plugin.cma RINGCMO:=\ - contrib/ring/quote.cmo contrib/ring/g_quote.cmo \ contrib/ring/ring.cmo contrib/ring/g_ring.cmo -NEWRINGCMO:=\ - contrib/setoid_ring/newring.cmo +NEWRINGCMA:=contrib/setoid_ring/newring_plugin.cma +NEWRINGCMO:=contrib/setoid_ring/newring.cmo +DPCMA:=contrib/dp/dp_plugin.cma DPCMO:=contrib/dp/dp_why.cmo contrib/dp/dp_zenon.cmo \ contrib/dp/dp.cmo contrib/dp/dp_gappa.cmo contrib/dp/g_dp.cmo -FIELDCMO:=\ - contrib/field/field.cmo +FIELDCMO:=contrib/field/field.cmo +FIELDCMA:=contrib/field/field_plugin.cma +XMLCMA:=contrib/xml/xml_plugin.cma XMLCMO:=\ contrib/xml/unshare.cmo contrib/xml/xml.cmo contrib/xml/acic.cmo \ contrib/xml/doubleTypeInference.cmo \ @@ -270,10 +279,12 @@ XMLCMO:=\ contrib/xml/xmlentries.cmo contrib/xml/cic2Xml.cmo \ contrib/xml/dumptree.cmo +FOURIERCMA:=contrib/fourier/fourier_plugin.cma FOURIERCMO:=\ contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \ contrib/fourier/g_fourier.cmo +EXTRACTIONCMA:=contrib/extraction/extraction_plugin.cma EXTRACTIONCMO:=\ contrib/extraction/table.cmo\ contrib/extraction/mlutil.cmo\ @@ -286,12 +297,14 @@ EXTRACTIONCMO:=\ contrib/extraction/extract_env.cmo \ contrib/extraction/g_extraction.cmo +JPROVERCMA:=contrib/jprover/jprover_plugin.cma JPROVERCMO:=\ contrib/jprover/opname.cmo \ contrib/jprover/jterm.cmo contrib/jprover/jlogic.cmo \ contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \ contrib/jprover/jprover.cmo +FUNINDCMA:=contrib/funind/recdef_plugin.cma FUNINDCMO:=\ contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \ contrib/funind/recdef.cmo \ @@ -301,15 +314,18 @@ FUNINDCMO:=\ contrib/funind/invfun.cmo contrib/funind/indfun.cmo \ contrib/funind/merge.cmo contrib/funind/g_indfun.cmo +FOCMA:=contrib/firstorder/ground_plugin.cma FOCMO:=\ contrib/firstorder/formula.cmo contrib/firstorder/unify.cmo \ contrib/firstorder/sequent.cmo contrib/firstorder/rules.cmo \ contrib/firstorder/instances.cmo contrib/firstorder/ground.cmo \ contrib/firstorder/g_ground.cmo +CCCMA:=contrib/cc/cc_plugin.cma CCCMO:=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \ contrib/cc/g_congruence.cmo +SUBTACCMA:=contrib/subtac/subtac_plugin.cma SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \ contrib/subtac/g_eterm.cmo \ contrib/subtac/subtac_errors.cmo contrib/subtac/subtac_coercion.cmo \ @@ -319,14 +335,28 @@ SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \ contrib/subtac/subtac.cmo contrib/subtac/g_subtac.cmo \ contrib/subtac/equations.cmo +RTAUTOCMA:=contrib/rtauto/rtauto_plugin.cma RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ contrib/rtauto/g_rtauto.cmo -CONTRIB:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ - $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \ - $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ - $(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ - $(FUNINDCMO) +CONTRIBSTATIC:=\ + $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ + $(QUOTECMO) $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \ + $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ + $(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ + $(FUNINDCMO) + +ifeq ($(HASNATDYNLINK),true) + CONTRIBSTATIC:=$(SUBTACCMO) + INITPLUGINS:=$(EXTRACTIONCMA) $(JPROVERCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ + $(XMLCMA) $(FUNINDCMA) #$(SUBTACCMA) + INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) + ifeq ($(BEST),opt) + INITPLUGINSBEST:=$(INITPLUGINSOPT) + else + INITPLUGINSBEST:=$(INITPLUGINS) + endif +endif CMA:=$(CLIBS) $(CAMLP4OBJS) CMXA:=$(CMA:.cma=.cmxa) @@ -346,7 +376,7 @@ LINKCMX:=$(LINKCMOCMXA:.cmo=.cmx) # objects known by the toplevel of Coq OBJSCMO:=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \ $(PROOFS) $(PARSING) $(TACTICS) $(TOPLEVEL) $(HIGHPARSING) \ - $(HIGHTACTICS) $(CONTRIB) + $(HIGHTACTICS) $(CONTRIBSTATIC) COQIDECMO:=ide/utils/okey.cmo ide/utils/config_file.cmo \ ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \ @@ -753,7 +783,7 @@ THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO) ## Contribs OMEGAVO:=$(addprefix contrib/omega/, \ - PreOmega.vo OmegaLemmas.vo Omega.vo ) + PreOmega.vo OmegaLemmas.vo OmegaPlugin.vo Omega.vo ) ROMEGAVO:=$(addprefix contrib/romega/, \ ReflOmegaCore.vo ROmega.vo ) @@ -767,12 +797,15 @@ MICROMEGAVO:=$(addprefix contrib/micromega/, \ QMicromega.vo RMicromega.vo \ Tauto.vo ) +QUOTEVO:=$(addprefix contrib/quote/, \ + Quote.vo ) + RINGVO:=$(addprefix contrib/ring/, \ LegacyArithRing.vo Ring_normalize.vo \ LegacyRing_theory.vo LegacyRing.vo \ LegacyNArithRing.vo \ LegacyZArithRing.vo Ring_abstract.vo \ - Quote.vo Setoid_ring_normalize.vo \ + Setoid_ring_normalize.vo \ Setoid_ring.vo Setoid_ring_theory.vo ) FIELDVO:=$(addprefix contrib/field/, \ @@ -811,7 +844,7 @@ RTAUTOVO:=$(addprefix contrib/rtauto/, \ CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ $(XMLVO) $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) + $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO) VFILES:= $(ALLVO:.vo=.v) @@ -59,6 +59,8 @@ usage () { printf "\tSpecifies the architecture\n" echo "-opt" printf "\tSpecifies whether or not to generate optimized executables\n" + echo "-natdynlink (yes|no)" + printf "\tSpecifies whether or not to use dynamic loading of native code\n" echo "-fsets (all|basic)" echo "-reals (all|basic)" printf "\tSpecifies whether or not to compile full FSets/Reals library\n" @@ -104,6 +106,7 @@ coq_profile_flag= coq_annotate_flag= best_compiler=opt cflags="-fno-defer-pop -Wall -Wno-unused" +natdynlink=yes gcc_exec=gcc ar_exec=ar @@ -186,6 +189,11 @@ while : ; do -opt|--opt) bytecamlc=ocamlc.opt camlp4oexec=camlp4o # can't add .opt since dyn load'll be required nativecamlc=ocamlopt.opt;; + -natdynlink|--natdynlink) case "$2" in + yes) natdynlink=yes;; + *) natdynlink=no + esac + shift;; -fsets|--fsets) case "$2" in yes|all) fsets=all;; *) fsets=basic @@ -212,7 +220,7 @@ while : ; do esac shift;; -with-geoproof|--with-geoproof) - case $2 in + case "$2" in yes) with_geoproof=true;; no) with_geoproof=false;; esac @@ -442,7 +450,7 @@ if [ "$coq_debug_flag" = "-g" ]; then fi # Native dynlink -if test -f `"$CAMLC" -where`/dynlink.cmxa; then +if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then HASNATDYNLINK=true else HASNATDYNLINK=false diff --git a/contrib/field/LegacyField.v b/contrib/field/LegacyField.v index ee1ddd477b..efa53b4e9d 100644 --- a/contrib/field/LegacyField.v +++ b/contrib/field/LegacyField.v @@ -11,5 +11,6 @@ Require Export LegacyField_Compl. Require Export LegacyField_Theory. Require Export LegacyField_Tactic. +Declare ML Module "field_plugin". (* Command declarations are moved to the ML side *) diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v index ac1592beea..07b2973a4a 100644 --- a/contrib/fourier/Fourier.v +++ b/contrib/fourier/Fourier.v @@ -10,15 +10,11 @@ (* "Fourier's method to solve linear inequations/equations systems.".*) -Declare ML Module "quote". -Declare ML Module "ring". -Declare ML Module "fourier". -Declare ML Module "fourierR". -Declare ML Module "field". - -Require Export Fourier_util. +Require Export LegacyRing. Require Export LegacyField. Require Export DiscrR. +Require Export Fourier_util. +Declare ML Module "fourier_plugin". Ltac fourier := abstract (fourierz; field; discrR). diff --git a/contrib/micromega/Psatz.v b/contrib/micromega/Psatz.v index b2dd99100c..a3be562077 100644 --- a/contrib/micromega/Psatz.v +++ b/contrib/micromega/Psatz.v @@ -22,6 +22,7 @@ Require Import Raxioms. Require Export RingMicromega. Require Import VarMap. Require Tauto. +Declare ML Module "micromega_plugin". Ltac xpsatz dom d := let tac := lazymatch dom with diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v index c054f218aa..f02209459f 100644 --- a/contrib/micromega/QMicromega.v +++ b/contrib/micromega/QMicromega.v @@ -17,6 +17,7 @@ Require Import RingMicromega. Require Import Refl. Require Import QArith. Require Import Qfield. +Declare ML Module "micromega_plugin". Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq Qle Qlt. Proof. diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v index 7c6969c2f2..70786a0571 100644 --- a/contrib/micromega/RMicromega.v +++ b/contrib/micromega/RMicromega.v @@ -17,6 +17,7 @@ Require Import RingMicromega. Require Import Refl. Require Import Raxioms RIneq Rpow_def DiscrR. Require Setoid. +Declare ML Module "micromega_plugin". Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R). Proof. diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v index 0855925a3d..1da3228a98 100644 --- a/contrib/micromega/ZMicromega.v +++ b/contrib/micromega/ZMicromega.v @@ -19,6 +19,7 @@ Require Import Refl. Require Import ZArith. Require Import List. Require Import Bool. +Declare ML Module "micromega_plugin". Ltac flatten_bool := repeat match goal with diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v index 3b427162e8..30b9457183 100644 --- a/contrib/omega/Omega.v +++ b/contrib/omega/Omega.v @@ -19,6 +19,7 @@ Require Export ZArith_base. Require Export OmegaLemmas. Require Export PreOmega. +Declare ML Module "omega_plugin". Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l diff --git a/contrib/omega/OmegaPlugin.v b/contrib/omega/OmegaPlugin.v new file mode 100644 index 0000000000..21535f0d3b --- /dev/null +++ b/contrib/omega/OmegaPlugin.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +Declare ML Module "omega_plugin". diff --git a/contrib/ring/Quote.v b/contrib/quote/Quote.v index 9a11a70b9c..f21a678e1a 100644 --- a/contrib/ring/Quote.v +++ b/contrib/quote/Quote.v @@ -8,6 +8,8 @@ (* $Id$ *) +Declare ML Module "quote_plugin". + (*********************************************************************** The "abstract" type index is defined to represent variables. diff --git a/contrib/ring/g_quote.ml4 b/contrib/quote/g_quote.ml4 index 808cbbf274..808cbbf274 100644 --- a/contrib/ring/g_quote.ml4 +++ b/contrib/quote/g_quote.ml4 diff --git a/contrib/ring/quote.ml b/contrib/quote/quote.ml index 3b13283e13..9141dc2f52 100644 --- a/contrib/ring/quote.ml +++ b/contrib/quote/quote.ml @@ -119,7 +119,7 @@ open Tacexpr We do that lazily, because this code can be linked before the constants are loaded in the environment *) -let constant dir s = Coqlib.gen_constant "Quote" ("ring"::dir) s +let constant dir s = Coqlib.gen_constant "Quote" ("quote"::dir) s let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") @@ -388,7 +388,7 @@ let rec sort_subterm gl l = [gl: goal sigma]\\ *) let quote_terms ivs lc gl = - Coqlib.check_required_library ["Coq";"ring";"Quote"]; + Coqlib.check_required_library ["Coq";"quote";"Quote"]; let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in let varlist = ref ([] : constr list) in (* list of variables *) let counter = ref 1 in (* number of variables created + 1 *) diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v index ed1da9c56e..4ae85baf37 100644 --- a/contrib/ring/LegacyRing.v +++ b/contrib/ring/LegacyRing.v @@ -13,6 +13,7 @@ Require Export LegacyRing_theory. Require Export Quote. Require Export Ring_normalize. Require Export Ring_abstract. +Declare ML Module "ring_plugin". (* As an example, we provide an instantation for bool. *) (* Other instatiations are given in ArithRing and ZArithRing in the diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v index b5cd6b1d0c..93b9bc7cf5 100644 --- a/contrib/ring/Setoid_ring.v +++ b/contrib/ring/Setoid_ring.v @@ -10,4 +10,5 @@ Require Export Setoid_ring_theory. Require Export Quote. -Require Export Setoid_ring_normalize.
\ No newline at end of file +Require Export Setoid_ring_normalize. +Declare ML Module "ring_plugin". diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 92f74d1d94..bb6aaea7de 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -752,7 +752,7 @@ let constants_to_unfold = "Coq.ring.Ring_normalize.interp_vl"; "Coq.ring.Ring_abstract.interp_acs"; "Coq.ring.Ring_abstract.interp_sacs"; - "Coq.ring.Quote.varmap_find"; + "Coq.quote.Quote.varmap_find"; (* anciennement des Local devenus Definition *) "Coq.ring.Ring_normalize.ics_aux"; "Coq.ring.Ring_normalize.ivl_aux"; diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v index 4281cc5736..3ddb6bed12 100644 --- a/contrib/romega/ROmega.v +++ b/contrib/romega/ROmega.v @@ -10,3 +10,5 @@ Require Import ReflOmegaCore. Require Export Setoid. Require Export PreOmega. Require Export ZArith_base. +Require Import OmegaPlugin. +Declare ML Module "romega_plugin".
\ No newline at end of file diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v index 342c03dbac..4b95097e2f 100644 --- a/contrib/rtauto/Rtauto.v +++ b/contrib/rtauto/Rtauto.v @@ -14,6 +14,8 @@ Require Export Bintree. Require Import Bool. Unset Boxed Definitions. +Declare ML Module "rtauto_plugin". + Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t. Ltac clean:=try (simpl;congruence). diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v index 95b037e3b6..fd9dd8d0d3 100644 --- a/contrib/setoid_ring/Ring_base.v +++ b/contrib/setoid_ring/Ring_base.v @@ -10,7 +10,8 @@ ring tactic. Abstract rings need more theory, depending on ZArith_base. *) -Declare ML Module "newring". +Require Import Quote. +Declare ML Module "newring_plugin". Require Export Ring_theory. Require Export Ring_tac. Require Import InitialRing. diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index 46d106d37a..2ff3322380 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -4,7 +4,8 @@ Require Import BinPos. Require Import Ring_polynom. Require Import BinList. Require Import InitialRing. -Declare ML Module "newring". +Require Import Quote. +Declare ML Module "newring_plugin". (* adds a definition id' on the normal form of t and an hypothesis id diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index 8aadf8f5dd..e535a55683 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -177,7 +177,7 @@ assert (Z: Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)). split; intros H; simpl; unfold g; - destruct (eq_nat_dec 0 n); try reflexivity. + destruct (eq_nat_dec 0 n) as [t|f]; try reflexivity. elim f; auto with *. elimtype False; omega. destruct IHa as [IHa0 IHa1]. diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 529ca0ba54..3d93c8a908 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -246,11 +246,22 @@ let traite_fichier_Coq verbose f = try let mldir = Hashtbl.find mlKnown s in let filename = file_name ([String.uncapitalize s],mldir) in - if Coq_config.has_natdynlink then + if Coq_config.has_natdynlink then printf " %s.cmo %s.cmxs" filename filename else printf " %s.cmo" filename - with Not_found -> () + with Not_found -> + (** The .cmxs we want to load dynamically may come + from a .cmxa, that has no corresponding .ml file. + Idem with bytecode .cma. What dependency should + we produce then ? For the moment, we suppose the + .cmxs and .cma are at the same location. *) + let mldir = Some (Filename.dirname f) in + let filename = file_name ([String.uncapitalize s],mldir) in + if Coq_config.has_natdynlink then + printf " %s.cma %s.cmxs" filename filename + else + printf " %s.cma" filename end) sl | Load str -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b2589d42f0..fa8fca66f5 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -78,7 +78,21 @@ let set_include d p = let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p) let set_rec_include d p = let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p) - + +let load_initial_plugins () = + (** Order matters ! For instance ground_plugin needs cc_plugin *) + let initial_plugins = + [ "extraction_plugin"; + "jprover_plugin"; + "cc_plugin"; + "ground_plugin"; + "dp_plugin"; + "recdef_plugin"; + (*"subtac_plugin";*) + "xml_plugin"; + ] in + if Mltop.has_dynlink then Mltop.declare_ml_modules initial_plugins + let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list @@ -340,6 +354,7 @@ let init is_ide = if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); + load_initial_plugins (); load_vernac_obj (); require (); load_rcfile(); diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 57c1464286..611567af98 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -289,18 +289,20 @@ let cache_ml_module_object (_,{mnames=mnames}) = (fun name -> let mname = mod_of_name name in if not (module_is_known mname) then - let fname = file_of_name mname in - begin - try - if_verbose + if has_dynlink then + let fname = file_of_name mname in + try + if_verbose msg (str"[Loading ML file " ++ str fname ++ str" ..."); load_object mname fname; - if_verbose msgnl (str"done]") - with e -> - if_verbose msgnl (str"failed]"); + if_verbose msgnl (str"done]"); + add_loaded_module mname + with e -> + if_verbose msgnl (str"failed]"); raise e - end; - add_loaded_module mname) + else + if_verbose + msgnl (str"[Ignoring ML file " ++ str mname ++ str "]")) mnames let export_ml_module_object x = Some x |