diff options
46 files changed, 953 insertions, 380 deletions
diff --git a/Makefile.build b/Makefile.build index e078ed9d9..517ff3a62 100644 --- a/Makefile.build +++ b/Makefile.build @@ -211,8 +211,8 @@ scripts/tolink.ml: Makefile.build Makefile.common $(SHOW)"ECHO... >" $@ $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ - $(HIDE)echo "let core_objs = \""$(OBJSCMO)"\"" >> $@ - $(HIDE)echo "let ide = \""$(COQIDECMO)"\"" >> $@ + $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ + $(HIDE)echo "let ide = \""$(IDEMOD)"\"" >> $@ # coqc @@ -228,79 +228,23 @@ $(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP) $(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC) cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE) -# we provide targets for each subdirectory - -lib: $(LIBREP) -kernel: $(KERNEL) -byterun: $(BYTERUN) -library: $(LIBRARY) -proofs: $(PROOFS) -tactics: $(TACTICS) -interp: $(INTERP) -parsing: $(PARSING) -pretyping: $(PRETYPING) -highparsing: $(HIGHPARSING) -toplevel: $(TOPLEVEL) -hightactics: $(HIGHTACTICS) - # target for libraries -lib/lib.cma: $(LIBREP) -lib/lib.cmxa: $(LIBREP:.cmo=.cmx) - -kernel/kernel.cma: $(KERNEL) -kernel/kernel.cmxa: $(KERNEL:.cmo=.cmx) - -library/library.cma: $(LIBRARY) -library/library.cmxa: $(LIBRARY:.cmo=.cmx) - -pretyping/pretyping.cma: $(PRETYPING) -pretyping/pretyping.cmxa: $(PRETYPING:.cmo=.cmx) - -interp/interp.cma: $(INTERP) -interp/interp.cmxa: $(INTERP:.cmo=.cmx) - -parsing/parsing.cma: $(PARSING) -parsing/parsing.cmxa: $(PARSING:.cmo=.cmx) - -proofs/proofs.cma: $(PROOFS) -proofs/proofs.cmxa: $(PROOFS:.cmo=.cmx) - -tactics/tactics.cma: $(TACTICS) -tactics/tactics.cmxa: $(TACTICS:.cmo=.cmx) - -toplevel/toplevel.cma: $(TOPLEVEL) -toplevel/toplevel.cmxa: $(TOPLEVEL:.cmo=.cmx) - -parsing/highparsing.cma: $(HIGHPARSING) -parsing/highparsing.cmxa: $(HIGHPARSING:.cmo=.cmx) - -tactics/hightactics.cma: $(HIGHTACTICS) -tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx) - -plugins/%.cma: | plugins/%.mllib.d - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^ - -plugins/%.cmxa: | plugins/%.mllib.d - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^ - -%.cma: +%.cma: | %.mllib.d $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^ -%.cmxa: +%.cmxa: | %.mllib.d $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^ # For the checker, different flags may be used -checker/check.cma: $(MCHECKER) +checker/check.cma: | checker/check.mllib.d $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $^ -checker/check.cmxa: $(MCHECKER:.cmo=.cmx) +checker/check.cmxa: | checker/check.mllib.d $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $^ @@ -362,10 +306,6 @@ ide/%.cmx: ide/%.ml | ide/%.ml.d $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< -ide/ide.cma: $(COQIDECMO) - -ide/ide.cmxa: $(COQIDECMO:.cmo=.cmx) - # install targets FULLIDELIB=$(FULLCOQLIB)/ide @@ -475,8 +415,25 @@ check:: world validate env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log if grep -F 'Error!' test-suite/check.log ; then false; fi +################################################################## +# partial targets: 1) core ML parts +################################################################## + +lib: lib/lib.cma +kernel: kernel/kernel.cma +byterun: $(BYTERUN) +library: library/library.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 +toplevel: toplevel/toplevel.cma +hightactics: tactics/hightactics.cma + ########################################################################### -# theories and plugins files +# 2) theories and plugins files ########################################################################### init: $(INITVO) @@ -512,7 +469,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \ wellfounded setoids sorting ########################################################################### -# plugins (interface not included) +# 3) plugins (interface not included) ########################################################################### plugins: $(PLUGINSVO) @@ -683,7 +640,9 @@ install-library: $(MKDIR) $(FULLCOQLIB)/user-contrib $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA) - $(INSTALLSH) $(FULLCOQLIB) $(OBJSCMO:.cmo=.cmi) + # reconstitute the list of core .cmi + $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmi) \ + `cat $(CORECMA:.cma=.mllib.d) | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.cmi/p"` ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) @@ -737,20 +696,20 @@ source-doc: ### Special rules ########################################################################### -dev/printers.cma: $(PRINTERSCMO) +dev/printers.cma: | dev/printers.mllib.d $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) gramlib.cma $(PRINTERSCMO) -o test-printer + $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma gramlib.cma $^ -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $^ -linkall -a -o $@ -parsing/grammar.cma: $(GRAMMARCMO) +parsing/grammar.cma: | parsing/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $^ -impl" -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ # toplevel/mltop.ml4 (ifdef Byte) @@ -909,9 +868,12 @@ endif $(SHOW)'OCAMLYACC $<' $(HIDE)$(OCAMLYACC) $< -%_mod.ml: %.mllib - sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@ - echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@ +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 $*)\"" >> $@ + +.SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) %.ml4-preprocessed: %.ml4 | %.ml4.d $(SHOW)'CAMLP4O $<' @@ -970,12 +932,15 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' > "$@" +checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEPBOOT) -slash -boot -I checker -c "$<" > "$@" \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) + %.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -slash -boot -c "$<" > "$@" \ + $(HIDE)$(COQDEPBOOT) -slash -boot -I kernel -I tools/coqdoc -c "$<" > "$@" \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) - echo "$*".cma: "$*"_mod.cmo >> "$@" - echo "$*".cmxa "$*".cmxs: "$*"_mod.cmx >> "$@" ## Veerry nasty hack to keep ocamldep happy %.ml: | %.ml4 @@ -1005,42 +970,26 @@ devel: $(DEBUGPRINTERS) ########################################################################### -%.dot: %.mli - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< - %.types.dot: %.mli $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< %.dep.ps: %.dot $(DOT) $(DOTOPTS) -o $@ $< -kernel/kernel.dot: $(KERNEL) - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(KERNEL:.cmo=.ml)) - -interp/interp.dot: $(INTERP) - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(INTERP:.cmo=.ml)) +OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ + `cat $| | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.ml/p"` -pretyping/pretyping.dot: $(PRETYPING) - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(PRETYPING:.cmo=.ml)) +%.dot: | %.mllib.d + $(OCAMLDOC_MLLIBD) -library/library.dot: $(LIBRARY) - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(LIBRARY:.cmo=.ml)) +parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d + $(OCAMLDOC_MLLIBD) -parsing/parsing.dot: $(PARSING) $(HIGHPARSING) - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(PARSING:.cmo=.ml)) $(wildcard $(HIGHPARSING:.cmo=.ml)) +tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d + $(OCAMLDOC_MLLIBD) -tactics/tactics.dot: $(TACTICS) $(HIGHTACTICS) - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(TACTICS:.cmo=.ml)) $(wildcard $(HIGHTACTICS:.cmo=.ml)) - -proofs/proofs.dot: $(PROOFS) - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(PROOFS:.cmo=.ml)) - -toplevel/toplevel.dot: $(TOPLEVEL) - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(TOPLEVEL:.cmo=.ml)) - -COQCMO:=$(LIBREP) $(KERNEL) $(INTERP) $(PRETYPING) $(LIBRARY) $(PARSING) $(HIGHPARSING) $(TACTICS) $(HIGHTACTICS) $(PROOFS) $(TOPLEVEL) -coq.dot: $(COQCMO) - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(COQCMO:.cmo=.ml)) +%.dot: %.mli + $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< # For emacs: diff --git a/Makefile.common b/Makefile.common index b8462539d..461c1c78f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -144,107 +144,20 @@ CLIBS:=unix.cma CAMLP4OBJS:=gramlib.cma -CONFIG:=\ - config/coq_config.cmo - -LIBREP:=$(addprefix lib/, \ - pp_control.cmo pp.cmo compat.cmo flags.cmo \ - util.cmo bigint.cmo hashcons.cmo dyn.cmo \ - system.cmo envars.cmo bstack.cmo edit.cmo \ - gset.cmo gmap.cmo tlm.cmo gmapl.cmo \ - profile.cmo explore.cmo predicate.cmo rtree.cmo \ - heap.cmo option.cmo dnet.cmo ) -# Rem: Cygwin already uses variable LIB +CONFIG:=config/coq_config.cmo BYTERUN:=$(addprefix kernel/byterun/, \ coq_fix_code.o coq_memory.o coq_values.o coq_interp.o ) -KERNEL0:=$(addprefix kernel/, \ - names.cmo univ.cmo esubst.cmo term.cmo \ - mod_subst.cmo sign.cmo cbytecodes.cmo copcodes.cmo \ - cemitcodes.cmo declarations.cmo \ - retroknowledge.cmo pre_env.cmo cbytegen.cmo environ.cmo \ - conv_oracle.cmo closure.cmo reduction.cmo \ - type_errors.cmo entries.cmo modops.cmo inductive.cmo \ - typeops.cmo indtypes.cmo cooking.cmo \ - term_typing.cmo subtyping.cmo mod_typing.cmo safe_typing.cmo ) - -KERNEL1:=$(addprefix kernel/, vm.cmo csymtable.cmo vconv.cmo ) - -KERNEL:=$(KERNEL0) $(KERNEL1) - -LIBRARY:=$(addprefix library/, \ - nameops.cmo libnames.cmo libobject.cmo summary.cmo \ - nametab.cmo global.cmo lib.cmo declaremods.cmo \ - library.cmo states.cmo decl_kinds.cmo dischargedhypsmap.cmo \ - goptions.cmo decls.cmo heads.cmo ) - -PRETYPING:=$(addprefix pretyping/, \ - termops.cmo evd.cmo reductionops.cmo vnorm.cmo \ - inductiveops.cmo retyping.cmo cbv.cmo pretype_errors.cmo \ - typing.cmo evarutil.cmo term_dnet.cmo recordops.cmo \ - tacred.cmo evarconv.cmo typeclasses_errors.cmo \ - typeclasses.cmo classops.cmo coercion.cmo unification.cmo \ - clenv.cmo rawterm.cmo pattern.cmo detyping.cmo \ - indrec.cmo cases.cmo pretyping.cmo matching.cmo ) - -INTERP:=\ - parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo \ - interp/notation.cmo interp/dumpglob.cmo \ - interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \ - library/impargs.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \ - interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \ - toplevel/discharge.cmo library/declare.cmo - -PROOFS:=$(addprefix proofs/, \ - tacexpr.cmo proof_type.cmo redexpr.cmo proof_trees.cmo \ - logic.cmo refiner.cmo evar_refiner.cmo tacmach.cmo \ - pfedit.cmo tactic_debug.cmo clenvtac.cmo decl_mode.cmo ) - -PARSING:=$(addprefix parsing/, \ - extend.cmo pcoq.cmo egrammar.cmo g_xml.cmo \ - ppconstr.cmo printer.cmo pptactic.cmo ppdecl_proof.cmo \ - tactic_printer.cmo printmod.cmo prettyp.cmo ) - -HIGHPARSING:=$(addprefix parsing/, \ - g_constr.cmo g_vernac.cmo g_prim.cmo g_proofs.cmo \ - g_tactic.cmo g_ltac.cmo g_natsyntax.cmo g_zsyntax.cmo \ - g_rsyntax.cmo g_ascii_syntax.cmo g_string_syntax.cmo \ - g_decl_mode.cmo g_intsyntax.cmo ) - -TACTICS:=\ - tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ - tactics/nbtermdn.cmo tactics/tacticals.cmo \ - tactics/hipattern.cmo tactics/tactics.cmo \ - tactics/evar_tactics.cmo \ - tactics/hiddentac.cmo tactics/elim.cmo \ - tactics/dhyp.cmo tactics/auto.cmo \ - toplevel/ind_tables.cmo tactics/equality.cmo \ - tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \ - tactics/tacinterp.cmo tactics/autorewrite.cmo \ - tactics/decl_interp.cmo tactics/decl_proof_instr.cmo - -TOPLEVEL:=\ - toplevel/himsg.cmo toplevel/cerrors.cmo \ - toplevel/class.cmo toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ - toplevel/auto_ind_decl.cmo toplevel/libtypes.cmo toplevel/search.cmo \ - toplevel/autoinstance.cmo toplevel/command.cmo toplevel/record.cmo \ - parsing/ppvernac.cmo toplevel/classes.cmo \ - toplevel/vernacinterp.cmo toplevel/mltop.cmo \ - toplevel/vernacentries.cmo toplevel/whelp.cmo toplevel/vernac.cmo \ - toplevel/line_oriented_parser.cmo toplevel/protectedtoplevel.cmo \ - toplevel/toplevel.cmo toplevel/usage.cmo \ - toplevel/coqinit.cmo toplevel/coqtop.cmo - -HIGHTACTICS:=$(addprefix tactics/, \ - refine.cmo extraargs.cmo extratactics.cmo \ - eauto.cmo class_tactics.cmo tauto.cmo \ - eqdecide.cmo ) - -# NB: Dependencies of plugins are now in separate files -# plugins/*/*_plugin.mllib -# Format of these files are compatible with ocamlbuild, -# Even if we don't use it (yet ?) +# LINK ORDER: +# Beware that highparsing.cma should appear before hightactics.cma +# respecting this order is useful for developers that want to load or link +# the libraries directly + +CORECMA:=lib/lib.cma kernel/kernel.cma library/library.cma \ + pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ + parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ + parsing/highparsing.cma tactics/hightactics.cma OMEGACMA:=plugins/omega/omega_plugin.cma ROMEGACMA:=plugins/romega/romega_plugin.cma @@ -288,35 +201,17 @@ endif CMA:=$(CLIBS) $(CAMLP4OBJS) CMXA:=$(CMA:.cma=.cmxa) -# LINK ORDER: -# Beware that highparsing.cma should appear before hightactics.cma -# respecting this order is useful for developers that want to load or link -# the libraries directly +LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS) +LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) -LINKCMO:=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \ - pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ - parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ - parsing/highparsing.cma tactics/hightactics.cma $(STATICPLUGINS) -LINKCMX:=$(patsubst %.cma,%.cmxa,$(patsubst %.cmo,%.cmx,$(LINKCMO))) - -# objects known by the toplevel of Coq -OBJSCMO:=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \ - $(PROOFS) $(PARSING) $(TACTICS) $(TOPLEVEL) $(HIGHPARSING) \ - $(HIGHTACTICS) - -COQIDECMO:=\ - $(addprefix ide/utils/, \ - okey.cmo config_file.cmo configwin_keys.cmo \ - configwin_types.cmo configwin_messages.cmo configwin_ihm.cmo \ - configwin.cmo editable_cells.cmo ) \ - $(addprefix ide/, \ - config_parser.cmo typed_notebook.cmo config_lexer.cmo \ - utf8_convert.cmo preferences.cmo ideutils.cmo \ - gtk_parsing.cmo undo.cmo highlight.cmo \ - coq.cmo coq_commands.cmo coq_tactics.cmo \ - command_windows.cmo coqide.cmo ) - -COQIDECMX:=$(COQIDECMO:.cmo=.cmx) +# modules known by the toplevel of Coq + +OBJSMOD:=Coq_config \ + $(foreach lib,$(CORECMA),$(shell cat $(lib:.cma=.mllib))) + +IDEMOD:=$(shell cat ide/ide.mllib) + +# coqmktop, coqc COQENVCMO:=$(CONFIG) \ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \ @@ -371,53 +266,8 @@ COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo output.cmo pretty.cmo main.cmo ) COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx) -# checker - -MCHECKER:=\ - $(CONFIG) \ - lib/pp_control.cmo lib/pp.cmo lib/compat.cmo \ - lib/flags.cmo lib/util.cmo lib/option.cmo lib/hashcons.cmo \ - lib/system.cmo lib/envars.cmo \ - lib/predicate.cmo lib/rtree.cmo \ - kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo \ - checker/validate.cmo \ - checker/term.cmo \ - checker/declarations.cmo checker/environ.cmo \ - checker/closure.cmo checker/reduction.cmo \ - checker/type_errors.cmo \ - checker/modops.cmo \ - checker/inductive.cmo checker/typeops.cmo \ - checker/indtypes.cmo checker/subtyping.cmo checker/mod_checking.cmo \ - checker/safe_typing.cmo checker/check.cmo \ - checker/check_stat.cmo checker/checker.cmo - # grammar modules with camlp4 -GRAMMARNEEDEDCMO:=\ - $(addprefix lib/, \ - pp_control.cmo pp.cmo compat.cmo flags.cmo util.cmo \ - bigint.cmo dyn.cmo hashcons.cmo predicate.cmo rtree.cmo option.cmo ) \ - $(KERNEL0) \ - $(addprefix library/, \ - nameops.cmo libnames.cmo summary.cmo nametab.cmo libobject.cmo \ - lib.cmo goptions.cmo decl_kinds.cmo global.cmo ) \ - $(addprefix pretyping/, \ - termops.cmo evd.cmo reductionops.cmo inductiveops.cmo rawterm.cmo \ - detyping.cmo pattern.cmo ) \ - interp/topconstr.cmo interp/genarg.cmo interp/ppextend.cmo \ - proofs/tacexpr.cmo \ - parsing/lexer.cmo parsing/extend.cmo \ - toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_util.cmo \ - parsing/q_coqast.cmo - -CAMLP4EXTENSIONSCMO:=\ - parsing/argextend.cmo parsing/tacextend.cmo parsing/vernacextend.cmo - -GRAMMARSCMO:=$(addprefix parsing/, \ - g_prim.cmo g_tactic.cmo g_ltac.cmo g_constr.cmo ) - -GRAMMARCMO:=$(CONFIG) $(GRAMMARNEEDEDCMO) $(CAMLP4EXTENSIONSCMO) $(GRAMMARSCMO) - GRAMMARCMA:=parsing/grammar.cma GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \ @@ -427,37 +277,8 @@ GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \ parsing/lexer.ml4 parsing/q_coqast.ml4 STAGE1_ML4:=$(GRAMMARML4) parsing/q_constr.ml4 -STAGE1_CMO:=$(GRAMMARCMO) parsing/q_constr.cmo STAGE1:=parsing/grammar.cma parsing/q_constr.cmo -PRINTERSCMO:=\ - $(CONFIG) lib/lib.cma \ - $(KERNEL0) \ - $(addprefix library/, \ - summary.cmo global.cmo nameops.cmo libnames.cmo nametab.cmo \ - libobject.cmo lib.cmo goptions.cmo decls.cmo heads.cmo ) \ - $(addprefix pretyping/, \ - termops.cmo evd.cmo rawterm.cmo reductionops.cmo inductiveops.cmo \ - retyping.cmo cbv.cmo pretype_errors.cmo typing.cmo evarutil.cmo \ - term_dnet.cmo recordops.cmo evarconv.cmo tacred.cmo \ - classops.cmo typeclasses_errors.cmo typeclasses.cmo \ - detyping.cmo indrec.cmo coercion.cmo unification.cmo cases.cmo \ - pretyping.cmo clenv.cmo pattern.cmo ) \ - parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \ - interp/topconstr.cmo interp/notation.cmo interp/dumpglob.cmo interp/reserve.cmo \ - library/impargs.cmo interp/constrextern.cmo \ - interp/syntax_def.cmo interp/implicit_quantifiers.cmo \ - interp/constrintern.cmo proofs/proof_trees.cmo proofs/tacexpr.cmo \ - proofs/proof_type.cmo proofs/logic.cmo proofs/refiner.cmo \ - proofs/evar_refiner.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo \ - proofs/decl_mode.cmo \ - parsing/ppconstr.cmo parsing/extend.cmo parsing/pcoq.cmo \ - parsing/printer.cmo parsing/pptactic.cmo \ - parsing/ppdecl_proof.cmo \ - parsing/tactic_printer.cmo \ - parsing/egrammar.cmo toplevel/himsg.cmo toplevel/cerrors.cmo \ - toplevel/vernacexpr.cmo toplevel/vernacinterp.cmo \ - dev/top_printers.cmo ########################################################################### # vo files @@ -782,21 +603,6 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1 -######################################################### -# .mli files by directory (used for dependencies graphs # -######################################################### - -# We use wildcard to get rid of .cmo that do not have a .mli -KERNELMLI:=$(wildcard $(KERNEL:.cmo=.mli)) -INTERPMLI:=$(wildcard $(INTERP:.cmo=.mli)) -PRETYPINGMLI:=$(wildcard $(PRETYPING:.cmo=.mli)) -TOPLEVELMLI:=$(wildcard $(TOPLEVEL:.cmo=.mli)) -PROOFSMLI:=$(wildcard $(PROOFS:.cmo=.mli)) -LIBRARYMLI:=$(wildcard $(LIBRARY:.cmo=.mli)) -PARSINGMLI:=$(wildcard $(PARSING:.cmo=.mli) $(HIGHPARSING:.cmo=.mli)) -TACTICSMLI:=$(wildcard $(TACTICS:.cmo=.mli) $(HIGHTACTICS:.cmo=.mli)) -COQMLI:=$(KERNELMLI) $(INTERPMLI) $(PRETYPINGMLI) $(TOPLEVELMLI) $(PROOFSMLI) \ - $(LIBRARYMLI) $(PARSINGMLI) $(TACTICSMLI) ########################################################################### # Miscellaneous @@ -814,7 +620,7 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \ $(filter-out parsing/q_constr.cmo,$(STAGE1_CMO)) \ - $(STAGE1_CMO:.cmo=.cmi) $(STAGE1_CMO:.cmo=.cmx) $(GENFILES) \ + $(GENFILES) \ source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \ $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o diff --git a/Makefile.stage2 b/Makefile.stage2 index 9c1e461c4..8f3d4e8bf 100644 --- a/Makefile.stage2 +++ b/Makefile.stage2 @@ -11,8 +11,8 @@ include Makefile.doc -include $(MLLIBFILES:.mllib=.mllib.d) .SECONDARY: $(MLLIBFILES:.mllib=.mllib.d) --include $(MLLIBFILES:%.mllib=%_mod.ml.d) -.SECONDARY: $(MLLIBFILES:%.mllib=%_mod.ml.d) +-include $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml.d)) +.SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml.d)) -include $(ML4FILES:.ml4=.ml4.ml.d) .SECONDARY: $(ML4FILES:.ml4=.ml4.ml.d) -include $(VFILES:.v=.v.d) @@ -0,0 +1,59 @@ + +## tags for binaries + +<scripts/coqmktop.{native,byte}> : use_str, use_unix, use_gramlib + +## tags for camlp4 files + +<**/*.ml4>: is_ml4 + +"toplevel/mltop.ml4": is_mltop, use_macro + +"lib/compat.ml4": use_macro +"parsing/g_xml.ml4": use_extend +"parsing/q_constr.ml4": use_extend, use_MLast +"parsing/argextend.ml4": use_extend, use_MLast +"parsing/tacextend.ml4": use_extend, use_MLast +"parsing/g_prim.ml4": use_extend +"parsing/g_ltac.ml4": use_extend +"parsing/pcoq.ml4": use_extend, use_macro +"parsing/q_util.ml4": use_MLast +"parsing/vernacextend.ml4": use_extend, use_MLast +"parsing/g_constr.ml4": use_extend +"parsing/g_tactic.ml4": use_extend +"parsing/g_proofs.ml4": use_extend +"parsing/q_coqast.ml4": use_MLast, use_macro + +"toplevel/whelp.ml4": use_grammar +"parsing/g_vernac.ml4": use_grammar, use_extend +"parsing/g_decl_mode.ml4": use_grammar, use_extend, use_MLast +"tactics/extraargs.ml4": use_grammar +"tactics/extratactics.ml4": use_grammar +"tactics/class_tactics.ml4": use_grammar +"tactics/eauto.ml4": use_grammar +"tactics/tauto.ml4": use_grammar +"tactics/eqdecide.ml4": use_grammar +"tactics/hipattern.ml4": use_grammar, use_constr + + +## sub-directory inclusion + +"config": include +"parsing": include +"ide": include +"interp": include +"kernel": include +"kernel/byterun": include +"lib": include +"library": include +"parsing": include +"plugins": include +"pretyping": include +"proofs": include +"scripts": include +"states": include +"tactics": include +"theories": include +"tools": include +"toplevel": include + diff --git a/checker/check.mllib b/checker/check.mllib new file mode 100644 index 000000000..726beef1b --- /dev/null +++ b/checker/check.mllib @@ -0,0 +1,32 @@ +Coq_config +Pp_control +Pp +Compat +Flags +Util +Option +Hashcons +System +Envars +Predicate +Rtree +Names +Univ +Esubst +Validate +Term +Declarations +Environ +Closure +Reduction +Type_errors +Modops +Inductive +Typeops +Indtypes +Subtyping +Mod_checking +Safe_typing +Check +Check_stat +Checker
\ No newline at end of file diff --git a/coq.itarget b/coq.itarget new file mode 100644 index 000000000..4845e1cdc --- /dev/null +++ b/coq.itarget @@ -0,0 +1,5 @@ +bin/.foo +scripts/coqmktop.byte +scripts/coqmktop.native +bin/coqtop.opt +bin/coqtop.byte
\ No newline at end of file diff --git a/dev/printers.mllib b/dev/printers.mllib new file mode 100644 index 000000000..25ec05fba --- /dev/null +++ b/dev/printers.mllib @@ -0,0 +1,125 @@ +Coq_config + +Pp_control +Pp +Compat +Flags +Util +Bigint +Hashcons +Dyn +System +Envars +Bstack +Edit +Gset +Gmap +Tlm +Gmapl +Profile +Explore +Predicate +Rtree +Heap +Option +Dnet + +Names +Univ +Esubst +Term +Mod_subst +Sign +Cbytecodes +Copcodes +Cemitcodes +Declarations +Retroknowledge +Pre_env +Cbytegen +Environ +Conv_oracle +Closure +Reduction +Type_errors +Entries +Modops +Inductive +Typeops +Indtypes +Cooking +Term_typing +Subtyping +Mod_typing +Safe_typing + +Summary +Global +Nameops +Libnames +Nametab +Libobject +Lib +Goptions +Decls +Heads +Termops +Evd +Rawterm +Reductionops +Inductiveops +Retyping +Cbv +Pretype_errors +Typing +Evarutil +Term_dnet +Recordops +Evarconv +Tacred +Classops +Typeclasses_errors +Typeclasses +Detyping +Indrec +Coercion +Unification +Cases +Pretyping +Clenv +Pattern + +Lexer +Ppextend +Genarg +Topconstr +Notation +Dumpglob +Reserve +Impargs +Constrextern +Syntax_def +Implicit_quantifiers +Constrintern +Proof_trees +Tacexpr +Proof_type +Logic +Refiner +Evar_refiner +Pfedit +Tactic_debug +Decl_mode +Ppconstr +Extend +Pcoq +Printer +Pptactic +Ppdecl_proof +Tactic_printer +Egrammar +Himsg +Cerrors +Vernacexpr +Vernacinterp +Top_printers diff --git a/ide/ide.mllib b/ide/ide.mllib new file mode 100644 index 000000000..152331747 --- /dev/null +++ b/ide/ide.mllib @@ -0,0 +1,22 @@ +Okey +Config_file +Configwin_keys +Configwin_types +Configwin_messages +Configwin_ihm +Configwin +Editable_cells +Config_parser +Typed_notebook +Config_lexer +Utf8_convert +Preferences +Ideutils +Gtk_parsing +Undo +Highlight +Coq +Coq_commands +Coq_tactics +Command_windows +Coqide diff --git a/interp/interp.mllib b/interp/interp.mllib new file mode 100644 index 000000000..234487bc9 --- /dev/null +++ b/interp/interp.mllib @@ -0,0 +1,17 @@ +Lexer +Topconstr +Ppextend +Notation +Dumpglob +Genarg +Syntax_def +Reserve +Impargs +Implicit_quantifiers +Constrintern +Modintern +Constrextern +Coqlib +Discharge +Declare + diff --git a/kernel/byterun/libcoqrun.clib b/kernel/byterun/libcoqrun.clib new file mode 100644 index 000000000..c06e40867 --- /dev/null +++ b/kernel/byterun/libcoqrun.clib @@ -0,0 +1,4 @@ +coq_fix_code.o +coq_memory.o +coq_values.o +coq_interp.o diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib new file mode 100644 index 000000000..a628e5cfe --- /dev/null +++ b/kernel/kernel.mllib @@ -0,0 +1,32 @@ +Names +Univ +Esubst +Term +Mod_subst +Sign +Cbytecodes +Copcodes +Cemitcodes +Declarations +Retroknowledge +Pre_env +Cbytegen +Environ +Conv_oracle +Closure +Reduction +Type_errors +Entries +Modops +Inductive +Typeops +Indtypes +Cooking +Term_typing +Subtyping +Mod_typing +Safe_typing + +Vm +Csymtable +Vconv
\ No newline at end of file diff --git a/lib/lib.mllib b/lib/lib.mllib new file mode 100644 index 000000000..1f203ec8d --- /dev/null +++ b/lib/lib.mllib @@ -0,0 +1,23 @@ +Pp_control +Pp +Compat +Flags +Util +Bigint +Hashcons +Dyn +System +Envars +Bstack +Edit +Gset +Gmap +Tlm +Gmapl +Profile +Explore +Predicate +Rtree +Heap +Option +Dnet diff --git a/library/library.mllib b/library/library.mllib new file mode 100644 index 000000000..1fc63929f --- /dev/null +++ b/library/library.mllib @@ -0,0 +1,16 @@ +Nameops +Libnames +Libobject +Summary +Nametab +Global +Lib +Declaremods +Library +States +Decl_kinds +Dischargedhypsmap +Goptions +Decls +Heads + diff --git a/myocamlbuild.ml b/myocamlbuild.ml new file mode 100644 index 000000000..b518c50d0 --- /dev/null +++ b/myocamlbuild.ml @@ -0,0 +1,217 @@ +(** * Plugin for building Coq via Ocamlbuild *) + +open Ocamlbuild_plugin +open Ocamlbuild_pack +open Printf + +(** WARNING !! this is preliminary stuff, able only to build + coqtop.opt and coqtop.byte, and only in a precise environment + (ocaml 3.11 with natdynlink) + + Support for other rules and other configurations will be + added later... + + Usage: + + ocamlbuild coq.otarget + + Then you can (hopefully) launch coq (with no input state) via: + + _build/bin/coqtop.opt -nois -coqlib . + + or + + CAML_LD_LIBRARY_PATH=_build/kernel/byterun _build/bin/coqtop.byte -nois -coqlib . + + TODO: understand how to create the right symlinks towards _build ... + +*) + + + +(** Parse a config file such as config/Makefile: + valid lines are NAME=value, comments start by # *) + +let read_env f = + let ic = open_in f in + let vars = ref [] in + begin try while true do + let l = input_line ic in + if l <> "" && l.[0] <> '#' && l.[0] <> ' ' then + try + let i = String.index l '=' in + let var = String.sub l 0 i + and def = if i+1 >= String.length l then "" else + String.sub l (i+1) (String.length l - i - 1) + in + let def = if String.length def >= 2 && + def.[0]='\"' && def.[String.length def - 1] = '\"' + then String.sub def 1 (String.length def - 2) else def + in + vars:=(var,def)::!vars + with Not_found -> () + done with End_of_file -> () end; + close_in ic; + !vars + +let env_vars = + let f = "config/Makefile" in + try read_env f with _ -> (eprintf "Error while reading %s\n" f; exit 1) + +let get_env s = + try List.assoc s env_vars + with Not_found -> (eprintf "Unknown environment variable %s\n" s; exit 1) + + +(** Configuration *) + +let _ = Options.ocamlc := A(get_env "OCAMLC") + +let camlp4o = get_env "CAMLP4O" +let camlp4lib = get_env "MYCAMLP4LIB" +let camlp4compat = get_env "CAMLP4COMPAT" +let hasdynlink = (get_env "HASNATDYNLINK" = "true") +let flag_dynlink = if hasdynlink then "-DHasDynLink" else "" + +(** 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 core_libs = + ["lib/lib"; "kernel/kernel"; "library/library"; + "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; + "parsing/parsing"; "tactics/tactics"; "toplevel/toplevel"; + "parsing/highparsing"; "tactics/hightactics"] +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 _ = dispatch begin function + | After_rules -> (* Add our rules after the standard ones. *) + +(** Camlp4 extensions *) + + rule "ml4ml" ~dep:"%.ml4" ~prod:"%.ml" + (fun env _ -> + let ml4 = env "%.ml4" and ml = env "%.ml" in + Cmd (S[A camlp4o;T(tags_of_pathname ml4 ++ "p4mod");readable_flag; + T(tags_of_pathname ml4 ++ "p4option"); + Sh camlp4compat; A"-o"; P ml; A"-impl"; P ml4])); + + flag ["is_ml4"; "p4mod"; "use_macro"] (A"pa_macro.cmo"); + flag ["is_ml4"; "p4mod"; "use_extend"] (A"pa_extend.cmo"); + flag ["is_ml4"; "p4mod"; "use_MLast"] (A"q_MLast.cmo"); + + flag_and_dep ["is_ml4"; "p4mod"; "use_grammar"] (P"parsing/grammar.cma"); + flag_and_dep ["is_ml4"; "p4mod"; "use_constr"] (P"parsing/q_constr.cmo"); + +(** Special case of toplevel/mltop.ml4: + - mltop.ml will be the old mltop.optml and be used to obtain mltop.cmx + - we add a special mltop.ml4 --> mltop.cmo rule, before all the others +*) + flag ["is_mltop"; "p4option"] (A flag_dynlink); + +(*TODO: this is rather ugly for a simple file, we should try to + benefit more from predefined rules *) + let mltop = "toplevel/mltop" in + let ml4 = mltop^".ml4" and mlo = mltop^".cmo" and + ml = mltop^".ml" and mld = mltop^".ml.depends" + in + rule "mltop_byte" ~deps:[ml4;mld] ~prod:mlo ~insert:`top + (fun env build -> + Ocaml_compiler.prepare_compile build ml; + Cmd (S [!Options.ocamlc; A"-c";A"-rectypes"; A"-I"; A camlp4lib; + A"-pp"; + Quote (S [A camlp4o; T(tags_of_pathname ml4 ++ "p4mod"); + A"-DByte"; A"-DHasDynLink"; Sh camlp4compat; + A"-impl"]); + A"-rectypes"; A"-I"; A camlp4lib; + Ocaml_utils.ocaml_include_flags ml4; + A"-impl"; P ml4])); + +(** All caml files are compiled with -rectypes and +camlp5 *) + + flag ["compile"; "ocaml"] (S [A"-rectypes"; A"-I"; A camlp4lib]); + flag ["link"; "ocaml"] (S [A"-rectypes"; A"-I"; A camlp4lib]); + +(** Extra libraries *) + + ocaml_lib ~extern:true "gramlib"; + +(** C code for the VM *) + + let headers = List.map (fun s -> "kernel/byterun/"^s) + ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; "int64_emul.h"; + "coq_gc.h"; "coq_interp.h"; "coq_values.h"; "int64_native.h"; + "coq_jumptbl.h"] + in + dep ["compile"; "c"] headers; + flag ["compile"; "c"] (S[A"-ccopt";A"-fno-defer-pop -Wall -Wno-unused"]); + dep ["link"; "ocaml"; "use_libcoqrun"] ["kernel/byterun/libcoqrun.a"]; + +(** Generation of coq_jumbtbl.h for the VM *) + + let coqjump = "kernel/byterun/coq_jumptbl.h" + and coqinstr = "kernel/byterun/coq_instruct.h" in + let cmd = Printf.sprintf + "sed -n -e '/^ /s/ \\([A-Z]\\)/ \\&\\&coq_lbl_\\1/gp' -e '/^}/q' %s > %s" + coqinstr coqjump + in + rule "coqjump" ~deps:[coqinstr] ~prod:coqjump + (fun _ _ -> Cmd (Sh cmd)); + +(** Generation of opcodes for the VM *) + + let copcodes = "kernel/copcodes.ml" + and coqinstr = "kernel/byterun/coq_instruct.h" + and script = "kernel/make-opcodes" in + let cmd = Printf.sprintf + "sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' %s | awk -f %s > %s" + coqinstr script copcodes + in + rule "copcodes" ~deps:[coqinstr;script] ~prod:copcodes + (fun _ _ -> Cmd (Sh cmd)); + +(** Generation of tolink.ml *) + + let tolink = "scripts/tolink.ml" in + let core_cma_s = String.concat " " core_cma in + let core_mllib_s = String.concat " " core_mllib in + let cmd = + "(echo \'let copts = \"-cclib -lcoqrun\"\'; "^ + "echo \'let core_libs = \"config/coq_config.cmo "^core_cma_s^"\"\'; "^ + "echo \'let core_objs = \"Coq_config `cat "^core_mllib_s^"`\"\'; "^ + "echo \'let ide = \"`cat ide/ide.mllib`\"\' " ^ + ") > " ^ tolink + in + rule "tolink.ml" ~deps:core_mllib ~prod:tolink + (fun _ _ -> Cmd (Sh cmd)); + +(** Coqtop *) + + let coqtopopt = "bin/coqtop.opt" + and coqtopbyte = "bin/coqtop.byte" in + let deps = ["scripts/coqmktop.native";"kernel/byterun/libcoqrun.a"] in + let depsopt = [ "config/coq_config.cmx"] @ deps @ core_cmxa + and depsbyte = [ "config/coq_config.cmo"] @ deps @ core_cma + in begin + rule "coqtop.opt" ~deps:depsopt ~prod:coqtopopt + (fun _ _ -> + Cmd (S [P "scripts/coqmktop.native";A"-boot";A"-opt"; + Ocaml_utils.ocaml_include_flags coqtopopt; + A"-o";P coqtopopt])); + rule "coqtop.byte" ~deps:depsbyte ~prod:coqtopbyte + (fun _ _ -> + Cmd (S [P "scripts/coqmktop.native";A"-boot";A"-top"; + Ocaml_utils.ocaml_include_flags coqtopbyte; + A"-o";P coqtopbyte])); + end; + +(** bin : directory bin doesn't get made by default ??!! *) + + rule "bin dir" ~prod:"bin/.foo" (fun _ _ -> Cmd (Sh "mkdir -p bin && touch bin/.foo")); + + | _ -> () + +end diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib new file mode 100644 index 000000000..128ca9445 --- /dev/null +++ b/parsing/grammar.mllib @@ -0,0 +1,78 @@ +Coq_config + +Pp_control +Pp +Compat +Flags +Util +Bigint +Dyn +Hashcons +Predicate +Rtree +Option + +Names +Univ +Esubst +Term +Mod_subst +Sign +Cbytecodes +Copcodes +Cemitcodes +Declarations +Retroknowledge +Pre_env +Cbytegen +Environ +Conv_oracle +Closure +Reduction +Type_errors +Entries +Modops +Inductive +Typeops +Indtypes +Cooking +Term_typing +Subtyping +Mod_typing +Safe_typing + +Nameops +Libnames +Summary +Nametab +Libobject +Lib +Goptions +Decl_kinds +Global +Termops +Evd +Reductionops +Inductiveops +Rawterm +Detyping +Pattern +Topconstr +Genarg +Ppextend +Tacexpr +Lexer +Extend +Vernacexpr +Pcoq +Q_util +Q_coqast + +Argextend +Tacextend +Vernacextend + +G_prim +G_tactic +G_ltac +G_constr
\ No newline at end of file diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib new file mode 100644 index 000000000..03fb9c629 --- /dev/null +++ b/parsing/highparsing.mllib @@ -0,0 +1,13 @@ +G_constr +G_vernac +G_prim +G_proofs +G_tactic +G_ltac +G_natsyntax +G_zsyntax +G_rsyntax +G_ascii_syntax +G_string_syntax +G_decl_mode +G_intsyntax diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib new file mode 100644 index 000000000..c705e45cd --- /dev/null +++ b/parsing/parsing.mllib @@ -0,0 +1,11 @@ +Extend +Pcoq +Egrammar +G_xml +Ppconstr +Printer +Pptactic +Ppdecl_proof +Tactic_printer +Printmod +Prettyp diff --git a/plugins/_tags b/plugins/_tags new file mode 100644 index 000000000..a8291f6c8 --- /dev/null +++ b/plugins/_tags @@ -0,0 +1,44 @@ + +"romega/g_romega.ml4": use_grammar +"cc/g_congruence.ml4": use_grammar +"setoid_ring/newring.ml4": use_grammar +"dp/g_dp.ml4": use_grammar +"interface/centaur.ml4": use_grammar +"interface/debug_tac.ml4": use_grammar +"quote/g_quote.ml4": use_grammar +"subtac/equations.ml4": use_grammar +"subtac/g_eterm.ml4": use_grammar +"subtac/g_subtac.ml4": use_grammar +"rtauto/g_rtauto.ml4": use_grammar +"xml/xmlentries.ml4": use_grammar +"xml/dumptree.ml4": use_grammar +"firstorder/g_ground.ml4": use_grammar +"omega/g_omega.ml4": use_grammar +"micromega/g_micromega.ml4": use_grammar +"funind/g_indfun.ml4": use_grammar +"field/field.ml4": use_grammar +"extraction/g_extraction.ml4": use_grammar +"ring/g_ring.ml4": use_grammar +"fourier/g_fourier.ml4": use_grammar +"groebner/groebner.ml4": use_grammar + + +"cc": include +"extraction": include +"firstorder": include +"funind": include +"interface": include +"micromega": include +"quote": include +"romega": include +"setoid_ring": include +"xml": include +"dp": include +"field": include +"fourier": include +"groebner": include +"jprover": include +"omega": include +"ring": include +"rtauto": include +"subtac": include
\ No newline at end of file diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mllib index 27e903fd3..1bcfc5378 100644 --- a/plugins/cc/cc_plugin.mllib +++ b/plugins/cc/cc_plugin.mllib @@ -2,3 +2,4 @@ Ccalgo Ccproof Cctac G_congruence +Cc_plugin_mod diff --git a/plugins/dp/dp_plugin.mllib b/plugins/dp/dp_plugin.mllib index 361d6f832..adb9721a1 100644 --- a/plugins/dp/dp_plugin.mllib +++ b/plugins/dp/dp_plugin.mllib @@ -3,3 +3,4 @@ Dp_zenon Dp Dp_gappa G_dp +Dp_plugin_mod diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib index bb87b9e32..b7f458611 100644 --- a/plugins/extraction/extraction_plugin.mllib +++ b/plugins/extraction/extraction_plugin.mllib @@ -8,3 +8,4 @@ Haskell Scheme Extract_env G_extraction +Extraction_plugin_mod diff --git a/plugins/field/field_plugin.mllib b/plugins/field/field_plugin.mllib index 63492a64f..3c3e87af5 100644 --- a/plugins/field/field_plugin.mllib +++ b/plugins/field/field_plugin.mllib @@ -1 +1,2 @@ Field +Field_plugin_mod diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mllib index 863ccb50e..1647e0f3d 100644 --- a/plugins/firstorder/ground_plugin.mllib +++ b/plugins/firstorder/ground_plugin.mllib @@ -4,4 +4,5 @@ Sequent Rules Instances Ground -G_ground
\ No newline at end of file +G_ground +Ground_plugin_mod diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mllib index b6262f8ae..0383b1a80 100644 --- a/plugins/fourier/fourier_plugin.mllib +++ b/plugins/fourier/fourier_plugin.mllib @@ -1,3 +1,4 @@ Fourier FourierR G_fourier +Fourier_plugin_mod diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mllib index c30ee212f..31818c399 100644 --- a/plugins/funind/recdef_plugin.mllib +++ b/plugins/funind/recdef_plugin.mllib @@ -8,3 +8,4 @@ Invfun Indfun Merge G_indfun +Recdef_plugin_mod diff --git a/plugins/groebner/groebner_plugin.mllib b/plugins/groebner/groebner_plugin.mllib index 1da12fcf2..e227b5e09 100644 --- a/plugins/groebner/groebner_plugin.mllib +++ b/plugins/groebner/groebner_plugin.mllib @@ -2,3 +2,4 @@ Utile Polynom Ideal Groebner +Groebner_plugin_mod diff --git a/plugins/interface/coqinterface_plugin.mllib b/plugins/interface/coqinterface_plugin.mllib index e4b575b13..abb38cf79 100644 --- a/plugins/interface/coqinterface_plugin.mllib +++ b/plugins/interface/coqinterface_plugin.mllib @@ -12,3 +12,4 @@ Showproof Blast Depends Centaur +Coqinterface_plugin_mod diff --git a/plugins/interface/coqparser_plugin.mllib b/plugins/interface/coqparser_plugin.mllib index 65ec57715..e00b41c6d 100644 --- a/plugins/interface/coqparser_plugin.mllib +++ b/plugins/interface/coqparser_plugin.mllib @@ -1,4 +1,5 @@ Line_parser Vtp Xlate -Coqparser
\ No newline at end of file +Coqparser +Coqparser_plugin_mod diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mllib index 41753542f..518654a45 100644 --- a/plugins/micromega/micromega_plugin.mllib +++ b/plugins/micromega/micromega_plugin.mllib @@ -4,3 +4,4 @@ Mfourier Certificate Coq_micromega G_micromega +Micromega_plugin_mod diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mllib index 020901376..2b387fdce 100644 --- a/plugins/omega/omega_plugin.mllib +++ b/plugins/omega/omega_plugin.mllib @@ -1,3 +1,4 @@ Omega Coq_omega -G_omega
\ No newline at end of file +G_omega +Omega_plugin_mod diff --git a/plugins/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib index 21810acdf..d1b3ccbe1 100644 --- a/plugins/quote/quote_plugin.mllib +++ b/plugins/quote/quote_plugin.mllib @@ -1,2 +1,3 @@ Quote -G_quote
\ No newline at end of file +G_quote +Quote_plugin_mod diff --git a/plugins/ring/ring_plugin.mllib b/plugins/ring/ring_plugin.mllib index 183884ca6..3c5f995f7 100644 --- a/plugins/ring/ring_plugin.mllib +++ b/plugins/ring/ring_plugin.mllib @@ -1,2 +1,3 @@ Ring G_ring +Ring_plugin_mod diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mllib index 38d0e9411..1625009d0 100644 --- a/plugins/romega/romega_plugin.mllib +++ b/plugins/romega/romega_plugin.mllib @@ -1,3 +1,4 @@ Const_omega Refl_omega G_romega +Romega_plugin_mod diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mllib index 61c5e945b..0e3460449 100644 --- a/plugins/rtauto/rtauto_plugin.mllib +++ b/plugins/rtauto/rtauto_plugin.mllib @@ -1,3 +1,4 @@ Proof_search Refl_tauto G_rtauto +Rtauto_plugin_mod diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib index 54b7c8e67..a98392f1e 100644 --- a/plugins/setoid_ring/newring_plugin.mllib +++ b/plugins/setoid_ring/newring_plugin.mllib @@ -1 +1,2 @@ Newring +Newring_plugin_mod diff --git a/plugins/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib index 81b9ee2ba..394a4b30f 100644 --- a/plugins/subtac/subtac_plugin.mllib +++ b/plugins/subtac/subtac_plugin.mllib @@ -12,3 +12,4 @@ Subtac_classes Subtac G_subtac Equations +Subtac_plugin_mod diff --git a/plugins/xml/xml_plugin.mllib b/plugins/xml/xml_plugin.mllib index 3297ff068..90797e8dd 100644 --- a/plugins/xml/xml_plugin.mllib +++ b/plugins/xml/xml_plugin.mllib @@ -10,3 +10,4 @@ ProofTree2Xml Xmlentries Cic2Xml Dumptree +Xml_plugin_mod diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib new file mode 100644 index 000000000..ab0fac4a6 --- /dev/null +++ b/pretyping/pretyping.mllib @@ -0,0 +1,28 @@ +Termops +Evd +Reductionops +Vnorm +Inductiveops +Retyping +Cbv +Pretype_errors +Typing +Evarutil +Term_dnet +Recordops +Tacred +Evarconv +Typeclasses_errors +Typeclasses +Classops +Coercion +Unification +Clenv +Rawterm +Pattern +Detyping +Indrec +Cases +Pretyping +Matching + diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib new file mode 100644 index 000000000..05b86b1a0 --- /dev/null +++ b/proofs/proofs.mllib @@ -0,0 +1,12 @@ +Tacexpr +Proof_type +Redexpr +Proof_trees +Logic +Refiner +Evar_refiner +Tacmach +Pfedit +Tactic_debug +Clenvtac +Decl_mode diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 2c9c6d213..50059ae17 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -28,7 +28,7 @@ let split_list l = Str.split spaces l let copts = split_list Tolink.copts let core_objs = split_list Tolink.core_objs let core_libs = split_list Tolink.core_libs -let ide = split_list Tolink.ide +let ide = split_list Tolink.ide (* 3. Toplevel objects *) let camlp4topobjs = @@ -89,25 +89,21 @@ let files_to_link userfiles = if not !opt || Coq_config.has_natdynlink then dynobjs else [] in let toplevel_objs = if !top then topobjs else if !opt then notopobjs else [] in - let ide_objs = if !coqide then - "threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide - else [] + let ide_objs = + if !coqide then "Threads"::"Lablgtk"::"GtkThread"::ide else [] in - let ide_libs = if !coqide then - ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; - "ide/ide.cma" ] - else [] + let ide_libs = + if !coqide then + ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; "ide/ide.cma" ] + else [] in - let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs - and libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in - let objstolink,libstolink = - if !opt then - ((List.map native_suffix objs) @ userfiles, - (List.map native_suffix libs) @ userfiles) - else - (objs @ userfiles, libs @ userfiles ) + let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs in + let modules = List.map module_of_file (objs @ userfiles) + in + let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in + let libstolink = + (if !opt then List.map native_suffix libs else libs) @ userfiles in - let modules = List.map module_of_file objstolink in (modules, libstolink) (* Gives the list of all the directories under [dir]. diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib new file mode 100644 index 000000000..3445ec433 --- /dev/null +++ b/tactics/hightactics.mllib @@ -0,0 +1,7 @@ +Refine +Extraargs +Extratactics +Eauto +Class_tactics +Tauto +Eqdecide diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib new file mode 100644 index 000000000..220c8e782 --- /dev/null +++ b/tactics/tactics.mllib @@ -0,0 +1,21 @@ +Dn +Termdn +Btermdn +Nbtermdn +Tacticals +Hipattern +Tactics +Evar_tactics +Hiddentac +Elim +Dhyp +Auto +Ind_tables +Equality +Contradiction +Inv +Leminv +Tacinterp +Autorewrite +Decl_interp +Decl_proof_instr diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 59fe701aa..d259c3be5 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -22,19 +22,24 @@ let rec parse = function | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) + | "-I" :: r :: ll -> + (* To solve conflict (e.g. same filename in kernel and checker) + we allow to state an explicit order *) + add_dir add_known r []; + norecdir_list:=r::!norecdir_list; + parse ll | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep_boot () = if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); - add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "plugins" ["Coq"]; - List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; - List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; - List.iter (fun (f,_,d) -> add_ml_known f d) !mlAccu; - warning_mult ".mli" iter_mli_known; - warning_mult ".ml" iter_ml_known; + if !option_c then + add_rec_dir add_known "." [] + else begin + add_rec_dir add_known "theories" ["Coq"]; + add_rec_dir add_known "plugins" ["Coq"]; + end; if !option_c then mL_dependencies (); coq_dependencies () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 67a200921..7ac57a4f5 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -27,6 +27,8 @@ let option_noglob = ref false let option_slash = ref false let option_natdynlk = ref true +let norecdir_list = ref ([]:string list) + let suffixe = ref ".vo" type dir = string option @@ -98,7 +100,7 @@ let safe_hash_add clq q (k,v) = let mkknown () = let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in - let add x s = Hashtbl.add h x s + let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s and iter f = Hashtbl.iter f h and search x = try Some (Hashtbl.find h (String.uncapitalize x)) @@ -302,27 +304,32 @@ let mL_dependencies () = (fun (name,ext,dirname) -> let fullname = file_name name dirname in let (dep,dep_opt) = traite_fichier_ML fullname ext in - let intf = - if List.mem (name,dirname) !mliAccu then " "^fullname^".cmi" else "" + let intf = match search_mli_known name with + | None -> "" + | Some mldir -> " "^(file_name name mldir)^".cmi" in - printf "%s.cmo: %s%s%s%s\n" fullname fullname ext intf dep; - printf "%s.cmx: %s%s%s%s\n" fullname fullname ext intf dep_opt; - flush stdout) + if dep<>"" || intf<>"" then begin + printf "%s.cmo:%s%s\n" fullname dep intf; + printf "%s.cmx:%s%s\n" fullname dep_opt intf; + flush stdout; + end) (List.rev !mlAccu); List.iter (fun (name,dirname) -> let fullname = file_name name dirname in let (dep,_) = traite_fichier_ML fullname ".mli" in - printf "%s.cmi: %s.mli%s\n" fullname fullname dep; + if dep<>"" then printf "%s.cmi:%s\n" fullname dep; flush stdout) (List.rev !mliAccu); List.iter (fun (name,dirname) -> let fullname = file_name name dirname in let (dep,dep_opt) = traite_fichier_mllib fullname ".mllib" in - printf "%s.cma:%s\n" fullname dep; - printf "%s.cmxa %s.cmxs:%s\n" fullname fullname dep_opt; - flush stdout) + if dep<>"" then begin + printf "%s.cma:%s\n" fullname dep; + printf "%s.cmxa %s.cmxs:%s\n" fullname fullname dep_opt; + flush stdout + end) (List.rev !mllibAccu) let coq_dependencies () = @@ -382,9 +389,13 @@ let rec add_directory recur add_file phys_dir log_dir = let f = readdir dirh in (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *) if f.[0] <> '.' && f.[0] <> '_' then - let phys_f = phys_dir//f in + let phys_f = if phys_dir = "." then f else phys_dir//f in match try (stat phys_f).st_kind with _ -> S_BLK with - | S_DIR when recur -> add_directory recur add_file phys_f (log_dir@[f]) + | S_DIR when recur -> + if List.mem phys_f !norecdir_list then () + else + let log_dir' = if log_dir = [] then ["Coq"] else log_dir@[f] in + add_directory recur add_file phys_f log_dir' | S_REG -> add_file phys_dir log_dir f | _ -> () done diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 6d6a804da..3c7d09e1f 100755 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -34,15 +34,18 @@ let mllist = ref ([] : string list) let field_name s = String.sub s 1 (String.length s - 1) + } let space = [' ' '\t' '\n' '\r'] let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] -let identchar = +let identchar = ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] let coq_ident = ['a'-'z' '_' '0'-'9' 'A'-'Z']+ let coq_field = '.'['a'-'z' '_' '0'-'9' 'A'-'Z']+ +let caml_up_ident = uppercase identchar* +let caml_low_ident = lowercase identchar* let dot = '.' ( space+ | eof) rule coq_action = parse @@ -66,13 +69,14 @@ rule coq_action = parse { coq_action lexbuf } and caml_action = parse - | [' ' '\010' '\013' '\009' '\012'] + - { caml_action lexbuf } - | "open" [' ' '\010' '\013' '\009' '\012']* - { caml_opened_file lexbuf } - | lowercase identchar* + | space + { caml_action lexbuf } - | uppercase identchar* + | "open" space* (caml_up_ident as id) + { Use_module (String.uncapitalize id) } + | "module" space+ caml_up_ident + { caml_action lexbuf } + | caml_low_ident { caml_action lexbuf } + | caml_up_ident { ml_module_name := Lexing.lexeme lexbuf; qual_id lexbuf } | ['0'-'9']+ @@ -213,18 +217,11 @@ and modules = parse | _ { (Declare (List.rev !mllist)) } and qual_id = parse - | '.' [^ '.' '(' '['] { Use_module (String.uncapitalize !ml_module_name) } + | '.' [^ '.' '(' '['] { + Use_module (String.uncapitalize !ml_module_name) } | eof { raise Fin_fichier } | _ { caml_action lexbuf } -and caml_opened_file = parse - | uppercase identchar* - { let lex = (Lexing.lexeme lexbuf) in - let str = String.sub lex 0 (String.length lex) in - (Use_module (String.uncapitalize str)) } - | eof {raise Fin_fichier } - | _ { caml_action lexbuf } - and mllib_list = parse | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf) in s :: mllib_list lexbuf } diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib new file mode 100644 index 000000000..13b27d5ab --- /dev/null +++ b/toplevel/toplevel.mllib @@ -0,0 +1,24 @@ +Himsg +Cerrors +Class +Vernacexpr +Metasyntax +Auto_ind_decl +Libtypes +Search +Autoinstance +Command +Record +Ppvernac +Classes +Vernacinterp +Mltop +Vernacentries +Whelp +Vernac +Line_oriented_parser +Protectedtoplevel +Toplevel +Usage +Coqinit +Coqtop |