diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-09-08 00:15:04 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-09-08 00:15:04 +0200 |
| commit | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (patch) | |
| tree | c260a140410c796f113584a2f7e6b9b7f6e00aa5 | |
| parent | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (diff) | |
Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg
47 files changed, 701 insertions, 321 deletions
@@ -423,6 +423,7 @@ Tools - New stand-alone .vo files verifier "coqchk". - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir". - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R. +- The binary "parser" has been renamed to "coq-parser". Miscellaneous @@ -432,8 +433,13 @@ Miscellaneous Whelp search tool. - Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into "Test Printing Let for ref" and "Test Printing If for ref". -- An overhauled build system (new Makefiles); see dev/doc/build-system.txt -- Add -browser option to configure script +- An overhauled build system (new Makefiles); see dev/doc/build-system.txt. +- Add -browser option to configure script. +- Build a shared library for the C part of Coq, and use it by default. + Bytecode executables are now pure. The behaviour is configurable with + the -coqrunbyteflags configure option. +- Complexity tests can be skipped by setting the environment variable + COQTEST_SKIPCOMPLEXITY. Changes from V8.1gamma to V8.1 ============================== @@ -2,6 +2,7 @@ INSTALLATION PROCEDURES FOR THE COQ V8.2 SYSTEM ----------------------------------------------- + WHAT DO YOU NEED ? ================== @@ -160,6 +161,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). Disable the Objective Caml compiler warnings. This option has no effect on the result of the compilation. +-browser <command> + Use <command> to open an URL in a browser. %s must appear in <command>, + and will be replaced by the URL. + 5- Still in the root directory, do make world @@ -249,6 +254,7 @@ THE AVAILABLE COMMANDS. There is also a tutorial and a FAQ; see http://coq.inria.fr/doc1-eng.html + COMMON PROBLEMS. ================ @@ -263,6 +269,9 @@ COMMON PROBLEMS. not be present on certain systems. To fix that, try to replace mkdirhier with mkdir -p + * See also section on dynamically loaded libraries. + + COMPILING FOR DIFFERENT ARCHITECTURES. ====================================== @@ -308,3 +317,33 @@ MOVING BINARIES OR LIBRARY. the binaries directory) and -libdir (for the standard library directory) : coqtop -bindir <new directory> -libdir <new directory> + + See also next section. + + +DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES. +====================================================== + + Some bytecode executables of Coq use the OCaml runtime, which dynamically + loads a shared library (.so or .dll). When it is not installed properly, you + can get an error message of this kind: + + Fatal error: cannot load shared library dllcoqrun + Reason: dllcoqrun.so: cannot open shared object file: No such file or directory + + In this case, you need either: + - to set the CAML_LD_LIBRARY_PATH environment variable to point to the + directory where dllcoqrun.so is; this is suitable when you want to run + the command a limited number of times in a controlled environment (e.g. + during compilation of binary packages); + - install dllcoqrun.so in a location listed in the file ld.conf that is in + the directory of the standard library of OCaml; + - recompile your bytecode executables after reconfiguring the location of + of the shared library: + ./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath <path>" ... + where <path> is the directory where the dllcoqrun.so is installed; + - (not recommended) compile bytecode executables with a custom OCaml + runtime by using: + ./configure -coqrunbyteflags -custom ... + be aware that stripping executables generated this way, or performing + other executable-specific operations, will make them useless. @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 11309 2008-08-06 10:30:35Z herbelin $ +# $Id: Makefile 11387 2008-09-07 21:59:11Z glondu $ # Makefile for Coq @@ -24,7 +24,14 @@ # by Emacs' next-error. ########################################################################### -FIND_VCS_CLAUSE:='(' -name '{arch}' -or -name '.svn' -or -name '_darcs' -or -name '.git' -or -name "$${GIT_DIR}" ')' -prune -or +export FIND_VCS_CLAUSE:='(' \ + -name '{arch}' -or \ + -name '.svn' -or \ + -name '_darcs' -or \ + -name '.git' -or \ + -name 'debian' -or \ + -name "$${GIT_DIR}" \ +')' -prune -type f -or FIND_PRINTF_P:=-print | sed 's|^\./||' export YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P)) @@ -43,7 +50,7 @@ export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIN export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P)) #export VFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v' ')' $(FIND_PRINTF_P)) \ # $(GENVFILES) -export CFILES := $(shell find kernel/byterun -name '*.c') +export CFILES := $(shell find kernel/byterun $(FIND_VCS_CLAUSE) -name '*.c') export ML4FILESML:= $(ML4FILES:.ml4=.ml) @@ -148,12 +155,14 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(COQCBYTE) bin/coq-interface$(EXE) bin/parser$(EXE) + rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE) + rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE) find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f - find contrib -name '*.vo' -or -name '*.glob' | xargs rm -f + find contrib test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f rm -f */*.pp[iox] contrib/*/*.pp[iox] rm -rf $(SOURCEDOCDIR) rm -f toplevel/mltop.byteml toplevel/mltop.optml + rm -f test-suite/check.log rm -f glob.dump rm -f revision @@ -175,11 +184,11 @@ docclean: rm -f doc/coq.tex archclean: clean-ide cleantheories - rm -f $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP) - rm -f $(COQTOP) $(COQCOPT) $(COQMKTOPOPT) - rm -f bin/parser.opt$(EXE) bin/coq-interface.opt$(EXE) - find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' | xargs rm -f - rm -f $(TOOLS) + 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 + rm -f $(TOOLS) $(CSDPCERT) clean-ide: rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) @@ -194,7 +203,7 @@ ml4depclean: find . -name '*.ml4.d' | xargs rm -f depclean: - find . -name '*.d' | xargs rm -f + find . $(FIND_VCS_CLAUSE) -name '*.d' | xargs rm -f cleanconfig: rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli diff --git a/Makefile.build b/Makefile.build index a5bae4ea..b8d27b22 100644 --- a/Makefile.build +++ b/Makefile.build @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile.build 11309 2008-08-06 10:30:35Z herbelin $ +# $Id: Makefile.build 11383 2008-09-07 16:35:13Z glondu $ # Makefile for Coq @@ -137,10 +137,11 @@ endif CINCLUDES= -I $(CAMLHLIB) -# libcoqrun.a +# libcoqrun.a, dllcoqrun.so $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) - $(AR) rc $(LIBCOQRUN) $(BYTERUN) + cd $(dir $(LIBCOQRUN)) && \ + $(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u))) $(RANLIB) $(LIBCOQRUN) #coq_jumptbl.h is required only if you have GCC 2.0 or later @@ -180,7 +181,7 @@ $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ -$(COQTOP): $(ORDER_ONLY_SEP) $(BESTCOQTOP) +$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP) cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) LOCALCHKLIBS:=-I checker -I lib -I config -I kernel @@ -195,7 +196,7 @@ $(CHICKENOPT): checker/check.cmxa checker/main.ml $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -custom -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml + $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE) @@ -204,13 +205,14 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) $(COQMKTOPBYTE): $(COQMKTOPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma \ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma \ $(COQMKTOPCMO) $(OSDEPLIBS) $(COQMKTOPOPT): $(COQMKTOPCMX) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa \ $(COQMKTOPCMX) $(OSDEPLIBS) + $(STRIP) $@ $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP) cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE) @@ -226,11 +228,12 @@ scripts/tolink.ml: Makefile.build Makefile.common $(COQCBYTE): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS) $(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ unix.cmxa $(COQCCMX) $(OSDEPLIBS) + $(STRIP) $@ $(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC) cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE) @@ -361,13 +364,14 @@ contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx) ########################################################################### ifeq ($(BEST),opt) -bin/csdpcert$(EXE): $(CSDPCERTCMX) +contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $(CSDPCERTCMX) + $(STRIP) $@ else -bin/csdpcert$(EXE): $(CSDPCERTCMO) +contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) -custom $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO) endif ########################################################################### @@ -448,7 +452,7 @@ install-ide-info: $(INSTALLLIB) ide/FAQ $(FULLIDELIB) ########################################################################### -# Pcoq: special binaries for debugging (coq-interface, parser) +# Pcoq: special binaries for debugging (coq-interface, coq-parser) ########################################################################### # target to build Pcoq @@ -464,12 +468,12 @@ bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX) -bin/parser$(EXE):$(LIBCOQRUN) $(PARSERCMO) +bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) -custom -linkall $(BYTEFLAGS) -o $@ \ + $(HIDE)$(OCAMLC) $(COQRUNBYTEFLAGS) -linkall $(BYTEFLAGS) -o $@ \ dynlink.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO) -bin/parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX) +bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \ $(LIBCOQRUN) nums.cmxa $(CMXA) $(PARSERCMX) @@ -496,6 +500,10 @@ install-pcoq-manpages: # tests ########################################################################### +validate:: $(BESTCHICKEN) $(ALLVO) + $(SHOW)'COQCHK <theories & contrib>' + $(BESTCHICKEN) -boot -o -m $(ALLMODS) + check:: world cd test-suite; \ env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log @@ -583,27 +591,27 @@ tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEP): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS) $(GALLINA): $(GALLINACMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ $(GALLINACMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO) $(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo $(COQTEX): tools/coq-tex.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma tools/coq-tex.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo $(COQWC): tools/coqwc.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coqwc.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo $(COQDOC): $(COQDOCCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO) ########################################################################### # Installation @@ -617,7 +625,7 @@ $(COQDOC): $(COQDOCCMO) # You must NOT put a "/" at the end (Cygnus for win32 does not like "//"). FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLCOQLIB=$(COQLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) @@ -630,12 +638,12 @@ install-binaries:: install-$(BEST) install-tools install-byte:: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CSDPCERT) $(FULLBINDIR) + $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR) cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE) install-opt:: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CSDPCERT) $(FULLBINDIR) + $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR) cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE) install-tools:: @@ -655,8 +663,16 @@ install-library: $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLCOQLIB)/user-contrib - $(INSTALLLIB) $(LINKCMO) $(LINKCMX) $(GRAMMARCMA) $(FULLCOQLIB) - find . -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \; + $(INSTALLLIB) $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB) +ifeq ($(BEST),opt) + $(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB) +endif + find . $(FIND_VCS_CLAUSE) -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \; +# csdpcert is not meant to be directly called by the user; we install +# it with libraries + -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega + $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega + $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) install-library-light: $(MKDIR) $(FULLCOQLIB) @@ -699,7 +715,8 @@ install-latex: source-doc: if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi - $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) `find . -name "*.ml"` + $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) \ + `find . $(FIND_VCS_CLAUSE) -name "*.ml"` ########################################################################### @@ -716,7 +733,7 @@ dev/printers.cma: $(PRINTERSCMO) parsing/grammar.cma: $(GRAMMARCMO) $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar + $(HIDE)$(OCAMLC) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ @@ -823,8 +840,8 @@ checker/%.cmi: checker/%.mli | checker/%.mli.d $(HIDE)$(OCAMLC) -c $(CHKBYTEFLAGS) $< %.o: %.c - $(SHOW)'CC $<' - $(HIDE)$(CC) -o $@ $(CFLAGS) $(CINCLUDES) -c $< + $(SHOW)'OCAMLC $<' + $(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<) ifdef KEEP_ML4_PREPROCESSED .PRECIOUS: %.ml4-preprocessed @@ -875,8 +892,8 @@ endif $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQTOP) -dump-glob $*.glob -compile $* ifdef VALIDATE - $(SHOW)'COQCHK $(shell basename $*)' - $(HIDE)$(BESTCHICKEN) -silent -norec $(shell basename $*) \ + $(SHOW)'COQCHK $(call vo_to_mod,$@)' + $(HIDE)$(BESTCHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) endif diff --git a/Makefile.common b/Makefile.common index 0a5d4260..a752892d 100644 --- a/Makefile.common +++ b/Makefile.common @@ -23,7 +23,7 @@ COQC:=bin/coqc$(EXE) COQTOPBYTE:=bin/coqtop.byte$(EXE) COQTOPOPT:=bin/coqtop.opt$(EXE) BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE) -COQTOP:=bin/coqtop$(EXE) +COQTOPEXE:=bin/coqtop$(EXE) CHICKENBYTE:=bin/coqchk.byte$(EXE) CHICKENOPT:=bin/coqchk.opt$(EXE) BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE) @@ -39,14 +39,14 @@ COQIDE:=bin/coqide$(EXE) ifeq ($(BEST),opt) COQBINARIES:= $(COQMKTOP) $(COQC) \ - $(COQTOPBYTE) $(COQTOPOPT) $(COQTOP) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN) + $(COQTOPBYTE) $(COQTOPOPT) $(COQTOPEXE) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN) else COQBINARIES:= $(COQMKTOP) $(COQC) \ - $(COQTOPBYTE) $(COQTOP) $(CHICKENBYTE) $(CHICKEN) + $(COQTOPBYTE) $(COQTOPEXE) $(CHICKENBYTE) $(CHICKEN) endif OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE) -CSDPCERT:=bin/csdpcert$(EXE) +CSDPCERT:=contrib/micromega/csdpcert$(EXE) ########################################################################### # tools @@ -74,7 +74,7 @@ HEVEA:=hevea HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB): -COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOP) -v -sl -small +COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOPEXE) -v -sl -small DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex @@ -111,7 +111,9 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) # Object and Source files ########################################################################### -LIBCOQRUN:=kernel/byterun/libcoqrun.a +COQRUN := coqrun +LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a +DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN).so CLIBS:=unix.cma @@ -377,9 +379,9 @@ PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité... PARSERREQUIRESCMX:=$(LINKCMX) ifeq ($(BEST),opt) - COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE) bin/parser.opt$(EXE) + COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/coq-parser$(EXE) bin/coq-parser.opt$(EXE) else - COQINTERFACE:=bin/coq-interface$(EXE) bin/parser$(EXE) + COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE) endif PARSERCODE:=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \ @@ -811,6 +813,12 @@ CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO) VFILES:= $(ALLVO:.vo=.v) +# convert a (stdlib) filename into a module name: +# remove .vo, replace theories and contrib by Coq, and replace slashes by dots +vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst contrib/%,Coq.%,$(1:.vo=)))) + +ALLMODS:=$(call vo_to_mod,$(ALLVO)) + LIBFILES:=$(THEORIESVO) $(CONTRIBVO) LIBFILESLIGHT:=$(THEORIESLIGHTVO) @@ -821,10 +829,10 @@ INTERFACEVO:= 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/coqwc.1 man/coqdoc.1 man/coqide.1 \ man/coq_makefile.1 man/coqmktop.1 -PCOQMANPAGES:=man/coq-interface.1 man/parser.1 +PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1 RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \ parsing/pptactic.ml @@ -872,7 +880,7 @@ VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \ coqlight states pcoq-files check init theories theories-light contrib \ - $(DOC_TARGETS) $(VO_TARGETS) + $(DOC_TARGETS) $(VO_TARGETS) validate # For emacs: diff --git a/checker/check.ml b/checker/check.ml index e91516c7..40ac604e 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -23,8 +23,7 @@ type section_path = { dirpath : string list ; basename : string } let dir_of_path p = - make_dirpath - (id_of_string p.basename :: List.map id_of_string p.dirpath) + make_dirpath (List.map id_of_string p.dirpath) let path_of_dirpath dir = match repr_dirpath dir with [] -> failwith "path_of_dirpath" @@ -166,6 +165,9 @@ let remove_load_path dir = load_paths := list_filter2 (fun p d -> p <> dir) !load_paths let add_load_path (phys_path,coq_path) = + if !Flags.debug then + msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ + str phys_path); let phys_path = canonical_path_name phys_path in match list_filter2 (fun p d -> p = phys_path) !load_paths with | _,[dir] -> @@ -224,7 +226,7 @@ let locate_qualified_library qid = (* Search library in loadpath *) if qid.dirpath=[] then get_load_paths () else - (* we assume dir is an absolute dirpath *) + (* we assume qid is an absolute dirpath *) load_paths_of_dir_path (dir_of_path qid) in if loadpath = [] then raise LibUnmappedDir; diff --git a/checker/checker.ml b/checker/checker.ml index 7de25835..1ed094cf 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -191,6 +191,11 @@ let print_usage_channel co command = -where print Coq's standard library location and exit -v print Coq version and exit + -boot boot mode + -o print the list of assumptions + -m print the maximum heap size + + -impredicative-set set sort Set impredicative -h, --help print this list of options " @@ -323,10 +328,9 @@ let parse_args() = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - + | "-boot" :: rem -> boot := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem - - | ("-o" | "-output-context") :: rem -> + | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8c84fb0f..4c9b3d61 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -19,6 +19,21 @@ open Pp open Declarations open Environ +let rec debug_string_of_mp = function + | MPfile sl -> string_of_dirpath sl + | MPbound uid -> "bound("^string_of_mbid uid^")" + | MPself uid -> "self("^string_of_msid uid^")" + | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + +let rec string_of_mp = function + | MPfile sl -> string_of_dirpath sl + | MPbound uid -> string_of_mbid uid + | MPself uid -> string_of_msid uid + | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + +let string_of_mp mp = + if !Flags.debug then debug_string_of_mp mp else string_of_mp mp + let prkn kn = let (mp,_,l) = repr_kn kn in str(string_of_mp mp ^ "." ^ string_of_label l) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index ecf8d633..379273af 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -26,7 +26,7 @@ let refresh_arity ar = let check_constant_declaration env kn cb = Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn); - let env = add_constraints cb.const_constraints env in +(* let env = add_constraints cb.const_constraints env in*) let env' = check_named_ctxt env cb.const_hyps in (match cb.const_type with NonPolymorphicType ty -> @@ -47,58 +47,6 @@ let check_constant_declaration env kn cb = (* Checking modules *) -let rec add_struct_expr_constraints env = function - | SEBident _ -> env - - | SEBfunctor (_,mtb,meb) -> - add_struct_expr_constraints - (add_modtype_constraints env mtb) meb - - | SEBstruct (_,structure_body) -> - List.fold_left - (fun env (l,item) -> add_struct_elem_constraints env item) - env - structure_body - - | SEBapply (meb1,meb2,cst) -> -(* let g = Univ.merge_constraints cst Univ.initial_universes in -msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++ - Univ.pr_universes g++str"============="++fnl()); -*) - Environ.add_constraints cst - (add_struct_expr_constraints - (add_struct_expr_constraints env meb1) - meb2) - | SEBwith(meb,With_definition_body(_,cb))-> - Environ.add_constraints cb.const_constraints - (add_struct_expr_constraints env meb) - | SEBwith(meb,With_module_body(_,_,cst))-> - Environ.add_constraints cst - (add_struct_expr_constraints env meb) - -and add_struct_elem_constraints env = function - | SFBconst cb -> Environ.add_constraints cb.const_constraints env - | SFBmind mib -> Environ.add_constraints mib.mind_constraints env - | SFBmodule mb -> add_module_constraints env mb - | SFBalias (mp,Some cst) -> Environ.add_constraints cst env - | SFBalias (mp,None) -> env - | SFBmodtype mtb -> add_modtype_constraints env mtb - -and add_module_constraints env mb = - let env = match mb.mod_expr with - | None -> env - | Some meb -> add_struct_expr_constraints env meb - in - let env = match mb.mod_type with - | None -> env - | Some mtb -> - add_struct_expr_constraints env mtb - in - Environ.add_constraints mb.mod_constraints env - -and add_modtype_constraints env mtb = - add_struct_expr_constraints env mtb.typ_expr - exception Not_path let path_of_mexpr = function @@ -307,19 +255,18 @@ and check_module_type env mty = check_alias mty.typ_alias sub and check_module env mb = - let env' = add_module_constraints env mb in let sub = match mb.mod_expr, mb.mod_type with | None, None -> anomaly "Mod_typing.translate_module: empty type and expr in module entry" - | None, Some mtb -> check_modexpr env' mtb + | None, Some mtb -> check_modexpr env mtb | Some mexpr, _ -> - let sub1 = check_modexpr env' mexpr in + let sub1 = check_modexpr env mexpr in (match mb.mod_type with | None -> sub1 | Some mte -> - let sub2 = check_modexpr env' mte in + let sub2 = check_modexpr env mte in check_subtypes env {typ_expr = mexpr; typ_strength = None; @@ -342,21 +289,22 @@ and check_structure_field (s,env) mp lab = function let mp1 = MPdot(mp,lab) in let is_fun, sub = Modops.update_subst env msb mp1 in ((if is_fun then s else join s sub), - Modops.add_module (MPdot(mp,lab)) msb - (add_module_constraints env msb)) + Modops.add_module (MPdot(mp,lab)) msb env) | SFBalias(mp2,cst) -> + (* cf Safe_typing.add_alias *) (try + let mp' = MPdot(mp,lab) in let mp2' = scrape_alias mp2 env in - let msb = lookup_module mp2' env in - (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias), - Option.fold_right add_constraints cst - (register_alias (MPdot(mp,lab)) mp2 env)) + let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in + let sub = update_subst sub (map_mp mp' mp2') in + let sub = join_alias sub (map_mp mp' mp2') in + let sub = add_mp mp' mp2' sub in + (join s sub, register_alias mp' mp2 env) with Not_found -> failwith "unkown aliased module") | SFBmodtype mty -> let kn = MPdot(mp, lab) in check_module_type env mty; - (join s mty.typ_alias, - add_modtype kn mty (add_modtype_constraints env mty)) + (join s mty.typ_alias, add_modtype kn mty env) and check_modexpr env mse = match mse with | SEBident mp -> @@ -396,3 +344,57 @@ and check_modexpr env mse = match mse with List.fold_left (fun env (lab,mb) -> check_structure_field env mp lab mb) (empty_subst,env) msb in sub + +(* +let rec add_struct_expr_constraints env = function + | SEBident _ -> env + + | SEBfunctor (_,mtb,meb) -> + add_struct_expr_constraints + (add_modtype_constraints env mtb) meb + + | SEBstruct (_,structure_body) -> + List.fold_left + (fun env (l,item) -> add_struct_elem_constraints env item) + env + structure_body + + | SEBapply (meb1,meb2,cst) -> +(* let g = Univ.merge_constraints cst Univ.initial_universes in +msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++ + Univ.pr_universes g++str"============="++fnl()); +*) + Environ.add_constraints cst + (add_struct_expr_constraints + (add_struct_expr_constraints env meb1) + meb2) + | SEBwith(meb,With_definition_body(_,cb))-> + Environ.add_constraints cb.const_constraints + (add_struct_expr_constraints env meb) + | SEBwith(meb,With_module_body(_,_,cst))-> + Environ.add_constraints cst + (add_struct_expr_constraints env meb) + +and add_struct_elem_constraints env = function + | SFBconst cb -> Environ.add_constraints cb.const_constraints env + | SFBmind mib -> Environ.add_constraints mib.mind_constraints env + | SFBmodule mb -> add_module_constraints env mb + | SFBalias (mp,Some cst) -> Environ.add_constraints cst env + | SFBalias (mp,None) -> env + | SFBmodtype mtb -> add_modtype_constraints env mtb + +and add_module_constraints env mb = + let env = match mb.mod_expr with + | None -> env + | Some meb -> add_struct_expr_constraints env meb + in + let env = match mb.mod_type with + | None -> env + | Some mtb -> + add_struct_expr_constraints env mtb + in + Environ.add_constraints mb.mod_constraints env + +and add_modtype_constraints env mtb = + add_struct_expr_constraints env mtb.typ_expr +*) diff --git a/checker/reduction.ml b/checker/reduction.ml index 49f05daf..c398f0a4 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -195,6 +195,12 @@ let in_whnf (t,stk) = | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true | FLOCKED -> assert false +let oracle_order fl1 fl2 = + match fl1,fl2 with + ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false + | _, ConstKey _ -> true + | _ -> false + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) @@ -247,6 +253,14 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = with NotConvertible -> (* else the oracle tells which constant is to be expanded *) let (app1,app2) = + if oracle_order fl1 fl2 then + match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> + (match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> raise NotConvertible) + else match unfold_reference infos fl2 with | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) | None -> diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 4b156e7e..d5779923 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -31,7 +31,7 @@ let set_engagement c = let full_add_module dp mb digest = let env = !genv in let mp = MPfile dp in - let env = add_module_constraints env mb in + let env = add_constraints mb.mod_constraints env in let env = Modops.add_module mp mb env in genv := add_digest env dp digest @@ -121,7 +121,7 @@ let import file (dp,mb,depends,engmt as vo) digest = let env = !genv in check_imports msg_warning dp env depends; check_engagement env engmt; - check_module env mb; + check_module (add_constraints mb.mod_constraints env) mb; stamp_library file digest; (* We drop proofs once checked *) (* let mb = lighten_module mb in*) diff --git a/config/Makefile.template b/config/Makefile.template index fc8af173..e0e7bf0b 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -21,6 +21,10 @@ COQ_CONFIGURED=yes # Local use (no installation) LOCAL=LOCALINSTALLATION +# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun") +COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS +BUILDLDPATH= + # Paths for true installation # BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and # do_Makefile will reside @@ -28,7 +32,7 @@ LOCAL=LOCALINSTALLATION # MANDIR=path where to install manual pages # EMACSDIR=path where to put Coq's Emacs mode (coq.el) BINDIR="BINDIRDIRECTORY" -COQLIB="COQLIBDIRECTORY" +COQLIBINSTALL="COQLIBDIRECTORY" MANDIR="MANDIRDIRECTORY" DOCDIR="DOCDIRDIRECTORY" EMACSLIB="EMACSLIBDIRECTORY" @@ -58,6 +62,7 @@ COQIDEINCLUDES=LABLGTKINCLUDES # Objective-Caml compile command OCAML="OCAMLEXEC" OCAMLC="BYTECAMLC" +OCAMLMKLIB="OCAMLMKLIBEXEC" OCAMLOPT="NATIVECAMLC" OCAMLDEP="OCAMLDEPEXEC" OCAMLDOC="OCAMLDOCEXEC" diff --git a/config/coq_config.mli b/config/coq_config.mli index 3898a0f3..af943509 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coq_config.mli 11313 2008-08-07 11:15:03Z barras $ i*) +(*i $Id: coq_config.mli 11380 2008-09-07 12:27:27Z glondu $ i*) val local : bool (* local use (no installation) *) @@ -24,6 +24,8 @@ val camlp4lib : string (* where is the library of Camlp4 *) val best : string (* byte/opt *) val arch : string (* architecture *) val osdeplibs : string (* OS dependant link options for ocamlc *) +val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *) + (* val defined : string list (* options for lib/ocamlpp *) *) @@ -6,10 +6,13 @@ # ################################## -VERSION=8.2beta4 +VERSION=8.2 VOMAGIC=08193 STATEMAGIC=19764 -DATE="Aug. 2008" +DATE="Jun. 2008" + +# Create the bin/ directory if non-existent +test -d bin || mkdir bin # a local which command for sh which () { @@ -32,6 +35,8 @@ usage () { printf "\tSet installation directory to <dir>\n" echo "-local" printf "\tSet installation directory to the current source tree\n" + echo "-coqrunbyteflags" + printf "\tSet link flags for VM-dependent bytecode\n" echo "-src" printf "\tSpecifies the source directory\n" echo "-bindir" @@ -83,6 +88,7 @@ usage () { # Default OCaml binaries bytecamlc=ocamlc nativecamlc=ocamlopt +ocamlmklib=ocamlmklib ocamlexec=ocaml ocamldepexec=ocamldep ocamldocexec=ocamldoc @@ -104,6 +110,7 @@ ar_exec=ar ranlib_exec=ranlib local=false +coqrunbyteflags_spec=no src_spec=no prefix_spec=no bindir_spec=no @@ -137,6 +144,9 @@ while : ; do prefix="$2" shift;; -local|--local) local=true;; + -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes + coqrunbyteflags="$2" + shift;; -src|--src) src_spec=yes COQSRC="$2" shift;; @@ -754,6 +764,14 @@ case $coqdocdir_spec/$prefix_spec/$local in esac;; esac +BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!" +case $coqrunbyteflags_spec/$local in + yes/*) COQRUNBYTEFLAGS="$coqrunbyteflags";; + */true) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $COQTOP/kernel/byterun";; + *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $LIBDIR" + BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun";; +esac + # case $emacs_spec in # no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?" # read EMACS @@ -774,6 +792,7 @@ echo " Architecture : $ARCH" if test ! -z "$OS" ; then echo " Operating system : $OS" fi +echo " Coq VM bytecode link flags : $COQRUNBYTEFLAGS" echo " OS dependent libraries : $OSDEPLIBS" echo " Objective-Caml/Camlp4 version : $CAMLVERSION" echo " Objective-Caml/Camlp4 binaries in : $CAMLBIN" @@ -862,9 +881,10 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file (* DO NOT EDIT THIS FILE: automatically generated by ../configure *) let local = $local -let bindir = "$ESCBINDIR" -let coqlib = "$ESCLIBDIR" -let coqtop = "$ESCCOQTOP" +let coqrunbyteflags = "$COQRUNBYTEFLAGS" +let bindir = try Sys.getenv "COQBIN" with Not_found -> "$ESCBINDIR" +let coqlib = try Sys.getenv "COQLIB" with Not_found -> "$ESCLIBDIR" +let coqtop = try Sys.getenv "COQTOP" with Not_found -> "$ESCCOQTOP" let camldir = "$ESCCAMLDIR" let camllib = "$ESCCAMLLIB" let camlp4 = "$CAMLP4" @@ -909,10 +929,12 @@ chmod a-w "$mlconfig_file" rm -f "$COQSRC/config/Makefile" sed -e "s|LOCALINSTALLATION|$local|" \ + -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \ -e "s|COQSRCDIRECTORY|$COQSRC|" \ -e "s|COQVERSION|$VERSION|" \ -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \ -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \ + -e "s|BUILDLDPATH=|$BUILDLDPATH|" \ -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \ -e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \ -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \ @@ -937,6 +959,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|BESTCOMPILER|$best_compiler|" \ -e "s|EXECUTEEXTENSION|$EXE|" \ -e "s|BYTECAMLC|$bytecamlc|" \ + -e "s|OCAMLMKLIBEXEC|$ocamlmklib|" \ -e "s|NATIVECAMLC|$nativecamlc|" \ -e "s|OCAMLEXEC|$ocamlexec|" \ -e "s|OCAMLDEPEXEC|$ocamldepexec|" \ @@ -994,4 +1017,4 @@ echo echo "*Warning* To compile the system for a new architecture" echo " don't forget to do a 'make archclean' before './configure'." -# $Id: configure 11320 2008-08-07 19:40:59Z notin $ +# $Id: configure 11380 2008-09-07 12:27:27Z glondu $ diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml index 02ff61a1..5ae12394 100644 --- a/contrib/micromega/coq_micromega.ml +++ b/contrib/micromega/coq_micromega.ml @@ -1193,8 +1193,8 @@ let call_csdpcert provername poly = output_value ch_to (provername,poly : provername * micromega_polys); close_out ch_to; let cmdname = - Filename.concat Coq_config.bindir - ("csdpcert" ^ Coq_config.exec_extension) in + List.fold_left Filename.concat Coq_config.coqlib + ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in (try Sys.remove tmp_to with _ -> ()); if c <> 0 then Util.error ("Failed to call csdp certificate generator"); diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index b046f0b3..4d8f868f 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: subtac_coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Util open Names @@ -310,8 +310,6 @@ module Coercion = struct (* Typing operations dealing with coercions *) - let class_of1 env sigma t = class_of env sigma (nf_evar sigma t) - (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = let rec apply_rec acc typ = function @@ -339,19 +337,17 @@ module Coercion = struct (* raise Not_found if no coercion found *) let inh_pattern_coerce_to loc pat ind1 ind2 = - let i1 = inductive_class_of ind1 in - let i2 = inductive_class_of ind2 in - let p = lookup_pattern_path_between (i1,i2) in + let p = lookup_pattern_path_between (ind1,ind2) in apply_pattern_coercion loc pat p (* appliquer le chemin de coercions p à hj *) - let apply_coercion env p hj typ_cl = + let apply_coercion env sigma p hj typ_cl = try fst (List.fold_left (fun (ja,typ_cl) i -> let fv,isid = coercion_value i in - let argl = (class_args_of typ_cl)@[ja.uj_val] in + let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in let jres = apply_coercion_args env argl fv in (if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } @@ -370,9 +366,9 @@ module Coercion = struct (isevars',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in - let p = lookup_path_to_fun_from i1 in - (isevars,apply_coercion env p j t) + let t,p = + lookup_path_to_fun_from env (evars_of isevars) j.uj_type in + (isevars,apply_coercion env (evars_of isevars) p j t) with Not_found -> try let coercef, t = mu env isevars t in @@ -382,9 +378,8 @@ module Coercion = struct let inh_tosort_force loc env isevars j = try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in - let p = lookup_path_to_sort_from i1 in - let j1 = apply_coercion env p j t in + let t,p = lookup_path_to_sort_from env (evars_of isevars) j.uj_type in + let j1 = apply_coercion env (evars_of isevars) p j t in (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1)) with Not_found -> error_not_a_type_loc loc env (evars_of isevars) j @@ -417,12 +412,11 @@ module Coercion = struct else let v', t' = try - let t1,i1 = class_of1 env (evars_of evd) c1 in - let t2,i2 = class_of1 env (evars_of evd) t in - let p = lookup_path_between (i2,i1) in + let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in match v with Some v -> - let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in + let j = apply_coercion env (evars_of evd) p + {uj_val = v; uj_type = t} t2 in Some j.uj_val, j.uj_type | None -> None, t with Not_found -> raise NoCoercion diff --git a/dev/base_include b/dev/base_include index 398f60d2..0b7a0b67 100644 --- a/dev/base_include +++ b/dev/base_include @@ -29,6 +29,7 @@ #install_printer (* qualid *) ppqualid;; #install_printer (* kernel_name *) ppkn;; #install_printer (* constant *) ppcon;; +#install_printer (* cl_index *) ppclindex;; #install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; #install_printer (* values *) ppvalues;; @@ -13,6 +13,7 @@ install_printer Top_printers.ppkn install_printer Top_printers.ppcon install_printer Top_printers.ppsp install_printer Top_printers.ppqualid +install_printer Top_printers.ppclindex install_printer Top_printers.ppbigint install_printer Top_printers.pppattern diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index c9571f7c..9362aeeb 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -253,9 +253,8 @@ config/Makefile looks like it contains a lot of unused variables, clean that up (are any maybe used by nightly scripts on pauillac?). Also, the COQTOP variable from config/Makefile (and used in contribs) has a very poorly chosen name, because "coqtop" is the -name of a Coq executable! For example, in the Coq makefile it is -immediately clobbered by "bin/coqtop$(EXE)"! Rename it to COQROOT or -COQTREE or COQDIR or ... +name of a Coq executable! In the coq Makefiles, $(COQTOPEXE) is used +to refer to that executable. Promote the granular .glob handling to official way of doing things for Coq developments, that is implement it in coq_makefile and the diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 55b907ad..5d302660 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -13,11 +13,11 @@ #include <stdio.h> #include <stdlib.h> -#include <config.h> -#include <misc.h> -#include <mlvalues.h> -#include <fail.h> -#include <memory.h> +#include <caml/config.h> +#include <caml/misc.h> +#include <caml/mlvalues.h> +#include <caml/fail.h> +#include <caml/memory.h> #include "coq_instruct.h" #include "coq_fix_code.h" diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 00345318..c1a4e0ae 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -12,7 +12,7 @@ #ifndef _COQ_FIX_CODE_ #define _COQ_FIX_CODE_ -#include <mlvalues.h> +#include <caml/mlvalues.h> void * coq_stat_alloc (asize_t sz); #ifdef THREADED_CODE diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h index ccccbe78..c7b18b90 100644 --- a/kernel/byterun/coq_gc.h +++ b/kernel/byterun/coq_gc.h @@ -10,8 +10,8 @@ #ifndef _COQ_CAML_GC_ #define _COQ_CAML_GC_ -#include <mlvalues.h> -#include <alloc.h> +#include <caml/mlvalues.h> +#include <caml/alloc.h> typedef void (*scanning_action) (value, value *); diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 880e978a..98ef2791 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -21,7 +21,7 @@ #include "coq_values.h" /*spiwack : imports support functions for 64-bit integers */ -#include "config.h" +#include <caml/config.h> #ifdef ARCH_INT64_TYPE #include "int64_native.h" #else diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index edd05948..c0093a49 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -11,11 +11,11 @@ #ifndef _COQ_MEMORY_ #define _COQ_MEMORY_ -#include <config.h> -#include <fail.h> -#include <misc.h> -#include <memory.h> -#include <mlvalues.h> +#include <caml/config.h> +#include <caml/fail.h> +#include <caml/misc.h> +#include <caml/memory.h> +#include <caml/mlvalues.h> #define Coq_stack_size (4096 * sizeof(value)) diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 4c631fce..1bf493e2 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -11,8 +11,8 @@ #ifndef _COQ_VALUES_ #define _COQ_VALUES_ -#include <alloc.h> -#include <mlvalues.h> +#include <caml/alloc.h> +#include <caml/mlvalues.h> #define Default_tag 0 #define Accu_tag 0 diff --git a/lib/util.ml b/lib/util.ml index 75ee4246..a19cc65b 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: util.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: util.ml 11350 2008-09-02 15:37:49Z barras $ *) open Pp @@ -1361,7 +1361,7 @@ let heap_size () = let stat = Gc.stat () and control = Gc.get () in let max_words_total = stat.Gc.heap_words + control.Gc.minor_heap_size in - (max_words_total * Sys.word_size / 8) + (max_words_total * (Sys.word_size / 8)) let heap_size_kb () = (heap_size () + 1023) / 1024 diff --git a/man/coq-interface.1 b/man/coq-interface.1 index 2ab2bf95..ee013d95 100644 --- a/man/coq-interface.1 +++ b/man/coq-interface.1 @@ -1,7 +1,7 @@ .TH COQ 1 "April 25, 2001" .SH NAME -coq-interface \- +coq\-interface \- Customized Coq toplevel to make user interfaces .SH SYNOPSIS @@ -29,7 +29,7 @@ coq-interface (the same as coqtop). .BR coqc (1), .BR coqdep (1), .BR coqtop (1), -.BR parser (1). +.BR coq\-parser (1). .br .I The Coq Reference Manual. diff --git a/man/parser.1 b/man/coq-parser.1 index d89465d8..23dc8201 100644 --- a/man/parser.1 +++ b/man/coq-parser.1 @@ -1,11 +1,11 @@ .TH COQ 1 "April 25, 2001" .SH NAME -parser \- Coq parser +coq\-parser \- Coq parser .SH SYNOPSIS -.B parser +.B coq\-parser [ .B options ] @@ -19,7 +19,7 @@ program is not for the casual user. .SH SEE ALSO -.BR coq-interface (1), +.BR coq\-interface (1), .BR coqc (1), .BR coqtop (1), .BR coqdep (1). diff --git a/man/coq-tex.1 b/man/coq-tex.1 index 737de70a..7e0a2f81 100644 --- a/man/coq-tex.1 +++ b/man/coq-tex.1 @@ -15,19 +15,19 @@ coq-tex \- Process Coq phrases embedded in LaTeX files .BI \-image \ coq-image ] [ -.B -w +.B \-w ] [ -.B -v +.B \-v ] [ -.B -sl +.B \-sl ] [ -.B -hrule +.B \-hrule ] [ -.B -small +.B \-small ] .I input-file ... @@ -75,7 +75,7 @@ typewriter font. .TP .BI \-o \ output-file Specify the name of a file where the LaTeX output is to be stored. A -dash `-' causes the LaTeX output to be printed on standard output. +dash `\-' causes the LaTeX output to be printed on standard output. .TP .BI \-n \ line-width Set the line width. The default is 72 characters. The responses of the @@ -90,23 +90,23 @@ this is the command .IR coqtop without specifying any path which is used to evaluate the Coq phrases. .TP -.B -w +.B \-w Cause lines to be folded on a space character whenever possible, avoiding word cuts in the output. By default, folding occurs at the line width, regardless of word cuts. .TP -.B -v +.B \-v Verbose mode. Prints the Coq answers on the standard output. Useful to detect errors in Coq phrases. .TP -.B -sl +.B \-sl Slanted mode. The Coq answers are written in a slanted font. .TP -.B -hrule +.B \-hrule Horizontal lines mode. The Coq parts are written between two horizontal lines. .TP -.B -small +.B \-small Small font mode. The Coq parts are written in a smaller font. diff --git a/man/coqdep.1 b/man/coqdep.1 index 6ae89f8b..e2cbb40e 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -67,7 +67,7 @@ Prints a warning if a Coq command .IR Module \& is incorrect. (For instance, you wrote `Declare ML Module "A".', but the module A contains #open "B"). The correct command is printed -(see option -D). The warning is printed on standard error. +(see option \-D). The warning is printed on standard error. .TP .BI \-i Prints also the dependencies for .vi files (Coq specification modules). @@ -138,7 +138,7 @@ Z.v contains the commands `Require X' and `Declare ML Module "D"'. To get the dependencies of the Coq files: .IP .B -example% coqdep -I . *.v +example% coqdep \-I . *.v .RS .sp .5 .nf @@ -153,7 +153,7 @@ example% coqdep -I . *.v With a warning: .IP .B -example% coqdep -w -I . *.v +example% coqdep \-w \-I . *.v .RS .sp .5 .nf @@ -170,7 +170,7 @@ example% coqdep -w -I . *.v To get only the Caml dependencies: .IP .B -example% coqdep -c -I . *.ml +example% coqdep \-c \-I . *.ml .RS .sp .5 .nf @@ -190,4 +190,4 @@ example% coqdep -c -I . *.ml .SH BUGS Please report any bug to -.B coq-bugs@pauillac.inria.fr +.B coq\-bugs@pauillac.inria.fr diff --git a/man/coqdoc.1 b/man/coqdoc.1 index c443e8b0..45fcafd2 100644 --- a/man/coqdoc.1 +++ b/man/coqdoc.1 @@ -54,7 +54,7 @@ Redirect the output into the file Output files into directory .I dir instead of current directory (option --d does not change the filename specified with option -o, if any). +\-d does not change the filename specified with option \-o, if any). .TP .B \-s, \ \-\-short Do not insert titles for the files. The default behavior is to insert @@ -68,7 +68,7 @@ Suppress the header and trailer of the final document. Thus, you can insert the resulting document into a larger one. .TP .BI \-p \ string, \ \-\-preamble \ string -Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with -html). +Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with \-html). .TP .BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file Considers the file `file' respectively as a .v (or .g) file or a .tex file. @@ -114,7 +114,7 @@ it builds a table of contents into toc.html. .TP .B \-\-glob\-from \ file Make references using Coq globalizations from file file. (Such -globalizations are obtained with Coq option -dump-glob). +globalizations are obtained with Coq option \-dump\-glob). .TP .B \-\-no\-externals @@ -129,22 +129,22 @@ Set base URL for the Coq standard library (default is http://coq.inria.fr/librar Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css. .TP -.BI -R \ dir \ coqdir +.BI \-R \ dir \ coqdir Map physical directory dir to Coq logical directory coqdir (similarly -to Coq option -R). +to Coq option \-R). .B Note: -option -R only has effect on the files following it on the command +option \-R only has effect on the files following it on the command line, so you will probably need to put this option first. .SS Contents options .TP -.B -g, \ --gallina +.B \-g, \ \-\-gallina Do not print proofs. .TP -.B -l, \ --light -Light mode. Suppress proofs (as with -g) and the following commands: +.B \-l, \ \-\-light +Light mode. Suppress proofs (as with \-g) and the following commands: * [Recursive] Tactic Definition * Hint / Hints @@ -153,29 +153,29 @@ Light mode. Suppress proofs (as with -g) and the following commands: * Implicit Argument / Implicits * Section / Variable / Hypothesis / End -The behavior of options -g and -l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above). +The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above). .SS Language options Default behavior is to assume ASCII 7 bits input files. .TP -.B -latin1, \ --latin1 -Select ISO-8859-1 input files. It is equivalent to --inputenc latin1 ---charset iso-8859-1. +.B \-latin1, \ \-\-latin1 +Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1 +\-\-charset iso\-8859\-1. .TP -.B -utf8, \ --utf8 -Select UTF-8 (Unicode) input files. It is equivalent to --inputenc -utf8 --charset utf-8. LATEX UTF-8 support can be found at -http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/. +.B \-utf8, \ \-\-utf8 +Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc +utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at +http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/. .TP -.BI --inputenc \ string +.BI \-\-inputenc \ string Give a LATEX input encoding, as an option to LATEX package inputenc. .TP -.BI --charset \ string +.BI \-\-charset \ string Specify the HTML character set, to be inserted in the HTML header. diff --git a/man/coqide.1 b/man/coqide.1 new file mode 100644 index 00000000..20379ef4 --- /dev/null +++ b/man/coqide.1 @@ -0,0 +1,166 @@ +.TH COQIDE 1 "July 16, 2004" + +.SH NAME +coqide \- The Coq Proof Assistant graphical interface + + +.SH SYNOPSIS +.B coqide +[ +.B options +] + +.SH DESCRIPTION + +.B coqtop +is a gtk graphical interface for the Coq proof assistant. + +For command-line-oriented use of Coq, see +.BR coqide (1) +; for batch-oriented use of Coq, see +.BR coqc (1). + + +.SH OPTIONS + +.TP +.B \-h +Show the complete list of options accepted by +.BR coqide . +.TP +.BI \-I\ dir ,\ \-include\ dir +Add directory dir in the include path. +.TP +.BI \-R\ dir\ coqdir +Recursively map physical +.I dir +to logical +.IR coqdir . +.TP +.B \-src +Add source directories in the include path. +.TP +.BI \-is\ f ,\ \-inputstate\ f +Read state from +.IR f .coq. +.TP +.B \-nois +Start with an empty state. +.TP +.BI \-outputstate\ f +Write state in file +.IR f .coq. +.TP +.BI \-load\-ml\-object\ f +Load ML object file +.IR f . +.TP +.BI \-load\-ml\-source\ f +Load ML file +.IR f . +.TP +.BI \-l\ f ,\ \-load\-vernac\-source\ f +Load Coq file +.IR f .v +(Load +.IR f .). +.TP +.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f +Load Coq file +.IR f .v +(Load Verbose +.IR f .). +.TP +.BI \-load\-vernac\-object\ f +Load Coq object file +.IR f .vo. +.TP +.BI \-require\ f +Load Coq object file +.IR f .vo +and import it (Require +.IR f .). +.TP +.BI \-compile\ f +Compile Coq file +.IR f .v +(implies +.BR \-batch ). +.TP +.BI \-compile\-verbose\ f +Verbosely compile Coq file +.IR f .v +(implies +.BR -batch ). +.TP +.B \-opt +Run the native-code version of Coq or Coq_SearchIsos. +.TP +.B \-byte +Run the bytecode version of Coq or Coq_SearchIsos. +.TP +.B \-where +Print Coq's standard library location and exit. +.TP +.B -v +Print Coq version and exit. +.TP +.B \-q +Skip loading of rcfile. +.TP +.BI \-init\-file\ f +Set the rcfile to +.IR f . +.TP +.BI \-user\ u +Use the rcfile of user +.IR u . +.TP +.B \-batch +Batch mode (exits just after arguments parsing). +.TP +.B \-boot +Boot mode (implies +.B \-q +and +.BR \-batch ). +.TP +.B \-emacs +Tells Coq it is executed under Emacs. +.TP +.BI \-dump\-glob\ f +Dump globalizations in file +.I f +(to be used by +.BR coqdoc (1)). +.TP +.B \-impredicative\-set +Set sort Set impredicative. +.TP +.B \-dont\-load\-proofs +Don't load opaque proofs in memory. +.TP +.B \-xml +Export XML files either to the hierarchy rooted in +the directory +.B COQ_XML_LIBRARY_ROOT +(if set) or to stdout (if unset). + + +.SH SEE ALSO + +.BR coqc (1), +.BR coqtop (1), +.BR coq-tex (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual, +.I +The Coq web site: http://coq.inria.fr, +.I +/usr/share/doc/coqide/FAQ. + +.SH AUTHOR +This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>, +for the Debian project (but may be used by others). diff --git a/man/coqmktop.1 b/man/coqmktop.1 index 3640d439..1b9c9e2a 100644 --- a/man/coqmktop.1 +++ b/man/coqmktop.1 @@ -17,10 +17,10 @@ coqmktop \- The Coq Proof Assistant user-tactics linker .B coqmktop builds a new Coq toplevel extended with user-tactics. .IR files \& -are the Objective Caml object or library files (i.e. with suffix .cmo, -.cmx, .cma or .cmxa) to link with the Coq system. +are the Objective Caml object or library files +(i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the Coq system. The linker produces an executable Coq toplevel which can be called -directly or through coqc(1), using the -image option. +directly or through coqc(1), using the \-image option. .SH OPTIONS diff --git a/man/coqwc.1 b/man/coqwc.1 index 7011d148..4594aeec 100644 --- a/man/coqwc.1 +++ b/man/coqwc.1 @@ -44,4 +44,4 @@ Do not skip headers .SH BUGS Please report any bug to -.B coq-bugs@pauillac.inria.fr +.B coq\-bugs@pauillac.inria.fr diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 3aa51c53..4811c443 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id: prettyp.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: prettyp.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Pp open Util @@ -744,7 +744,7 @@ let print_path_between cls clt = let j = index_of_class clt in let p = try - lookup_path_between (i,j) + lookup_path_between_class (i,j) with _ -> errorlabstrm "index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 0bdae7c7..be73f573 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -60,10 +60,10 @@ let rec print_module name locals with_body mb = in let modtype = match mb.mod_type with None -> str "" - | Some t -> str": " ++ + | Some t -> spc () ++ str": " ++ print_modtype locals t in - hv 2 (str "Module " ++ name ++ spc () ++ modtype ++ body) + hv 2 (str "Module " ++ name ++ modtype ++ body) and print_modtype locals mty = match mty with @@ -102,7 +102,7 @@ and print_sig locals msid sign = | SFBconst {const_opaque=true} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " - | SFBalias (mp,_) -> str "Module" + | SFBalias (mp,_) -> str "Module " | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_spec sign @@ -114,7 +114,7 @@ and print_struct locals msid struc = | SFBconst {const_body=None} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " - | SFBalias (mp,_) -> str "Module" + | SFBalias (mp,_) -> str "Module " | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_body struc @@ -125,9 +125,9 @@ and print_modexpr locals mexpr = match mexpr with (* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env in *) let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in - hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ + hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++ str ":" ++ print_modtype locals mty.typ_expr ++ - str "]" ++ spc () ++ print_modexpr locals' mexpr) + str ")" ++ spc () ++ print_modexpr locals' mexpr) | SEBstruct (msid, struc) -> hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End") | SEBapply (mexpr,marg,_) -> diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b5a5709e..398da529 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: classops.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: classops.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Util open Pp @@ -128,6 +128,10 @@ let class_exists cl = Bijint.mem cl !class_tab let class_info_from_index i = Bijint.map i !class_tab +let cl_fun_index = fst(class_info CL_FUN) + +let cl_sort_index = fst(class_info CL_SORT) + (* coercion_info : coe_typ -> coe_info_typ *) let coercion_info coe = Gmap.find coe !coercion_tab @@ -136,32 +140,10 @@ let coercion_exists coe = Gmap.mem coe !coercion_tab let coercion_params coe_info = coe_info.coe_param -let lookup_path_between (s,t) = - Gmap.find (s,t) !inheritance_graph - -let lookup_path_to_fun_from s = - lookup_path_between (s,fst(class_info CL_FUN)) +(* find_class_type : env -> evar_map -> constr -> cl_typ * int *) -let lookup_path_to_sort_from s = - lookup_path_between (s,fst(class_info CL_SORT)) - -let lookup_pattern_path_between (s,t) = - let l = Gmap.find (s,t) !inheritance_graph in - List.map - (fun coe -> - let c, _ = - Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty - coe.coe_value - in - match kind_of_term c with - | Construct cstr -> - (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1) - | _ -> raise Not_found) l - -(* find_class_type : constr -> cl_typ * int *) - -let find_class_type t = - let t', args = decompose_app (Reductionops.whd_betaiotazeta t) in +let find_class_type env sigma t = + let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in match kind_of_term t' with | Var id -> CL_SECVAR id, args | Const sp -> CL_CONST sp, args @@ -178,7 +160,7 @@ let subst_cl_typ subst ct = match ct with | CL_CONST kn -> let kn',t = subst_con subst kn in if kn' == kn then ct else - fst (find_class_type t) + fst (find_class_type (Global.env()) Evd.empty t) | CL_IND (kn,i) -> let kn' = subst_kn subst kn in if kn' == kn then ct else @@ -188,19 +170,17 @@ let subst_cl_typ subst ct = match ct with to declare any term as a coercion *) let subst_coe_typ subst t = fst (subst_global subst t) -(* classe d'un terme *) - (* class_of : Term.constr -> int *) let class_of env sigma t = let (t, n1, i, args) = try - let (cl,args) = find_class_type t in + let (cl,args) = find_class_type env sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, args) with Not_found -> let t = Tacred.hnf_constr env sigma t in - let (cl, args) = find_class_type t in + let (cl, args) = find_class_type env sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, args) in @@ -208,7 +188,7 @@ let class_of env sigma t = let inductive_class_of ind = fst (class_info (CL_IND ind)) -let class_args_of c = snd (find_class_type c) +let class_args_of env sigma c = snd (find_class_type env sigma c) let string_of_class = function | CL_FUN -> "Funclass" @@ -222,6 +202,61 @@ let string_of_class = function let pr_class x = str (string_of_class x) +(* lookup paths *) + +let lookup_path_between_class (s,t) = + Gmap.find (s,t) !inheritance_graph + +let lookup_path_to_fun_from_class s = + lookup_path_between_class (s,cl_fun_index) + +let lookup_path_to_sort_from_class s = + lookup_path_between_class (s,cl_sort_index) + +(* advanced path lookup *) + +let apply_on_class_of env sigma t cont = + try + let (cl,args) = find_class_type env sigma t in + let (i, { cl_param = n1 } ) = class_info cl in + if List.length args <> n1 then raise Not_found; + t, cont i + with Not_found -> + (* Is it worth to be more incremental on the delta steps? *) + let t = Tacred.hnf_constr env sigma t in + let (cl, args) = find_class_type env sigma t in + let (i, { cl_param = n1 } ) = class_info cl in + if List.length args <> n1 then raise Not_found; + t, cont i + +let lookup_path_between env sigma (s,t) = + let (s,(t,p)) = + apply_on_class_of env sigma s (fun i -> + apply_on_class_of env sigma t (fun j -> + lookup_path_between_class (i,j))) in + (s,t,p) + +let lookup_path_to_fun_from env sigma s = + apply_on_class_of env sigma s lookup_path_to_fun_from_class + +let lookup_path_to_sort_from env sigma s = + apply_on_class_of env sigma s lookup_path_to_sort_from_class + +let get_coercion_constructor coe = + let c, _ = + Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty coe.coe_value + in + match kind_of_term c with + | Construct cstr -> + (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1) + | _ -> + raise Not_found + +let lookup_pattern_path_between (s,t) = + let i = inductive_class_of s in + let j = inductive_class_of t in + List.map get_coercion_constructor (Gmap.find (i,j) !inheritance_graph) + (* coercion_value : coe_index -> unsafe_judgment * bool *) let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } = @@ -255,11 +290,11 @@ let add_coercion_in_graph (ic,source,target) = try if i=j then begin if different_class_params i j then begin - let _ = lookup_path_between ij in + let _ = lookup_path_between_class ij in ambig_paths := (ij,p)::!ambig_paths end end else begin - let _ = lookup_path_between (i,j) in + let _ = lookup_path_between_class (i,j) in ambig_paths := (ij,p)::!ambig_paths end; false diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 1436a11b..a76fe75c 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classops.mli 10840 2008-04-23 21:29:34Z herbelin $ i*) +(*i $Id: classops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*) (*i*) open Names @@ -52,17 +52,17 @@ val class_info : cl_typ -> (cl_index * cl_info_typ) val class_exists : cl_typ -> bool val class_info_from_index : cl_index -> cl_typ * cl_info_typ -(* [find_class_type c] returns the head reference of c and its +(* [find_class_type env sigma c] returns the head reference of [c] and its arguments *) -val find_class_type : constr -> cl_typ * constr list +val find_class_type : env -> evar_map -> types -> cl_typ * constr list (* raises [Not_found] if not convertible to a class *) -val class_of : env -> evar_map -> constr -> constr * cl_index +val class_of : env -> evar_map -> types -> types * cl_index (* raises [Not_found] if not mapped to a class *) val inductive_class_of : inductive -> cl_index -val class_args_of : constr -> constr list +val class_args_of : env -> evar_map -> types -> constr list (*s [declare_coercion] adds a coercion in the graph of coercion paths *) val declare_coercion : @@ -75,11 +75,16 @@ val coercion_exists : coe_typ -> bool val coercion_value : coe_index -> (unsafe_judgment * bool) (*s Lookup functions for coercion paths *) -val lookup_path_between : cl_index * cl_index -> inheritance_path -val lookup_path_to_fun_from : cl_index -> inheritance_path -val lookup_path_to_sort_from : cl_index -> inheritance_path -val lookup_pattern_path_between : - cl_index * cl_index -> (constructor * int) list +val lookup_path_between_class : cl_index * cl_index -> inheritance_path + +val lookup_path_between : env -> evar_map -> types * types -> + types * types * inheritance_path +val lookup_path_to_fun_from : env -> evar_map -> types -> + types * inheritance_path +val lookup_path_to_sort_from : env -> evar_map -> types -> + types * inheritance_path +val lookup_pattern_path_between : + inductive * inductive -> (constructor * int) list (*i Crade *) open Pp diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3074c4c4..73fcd0ea 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Util open Names @@ -78,10 +78,6 @@ module Default = struct | App (f,l) -> mkApp (whd_evar sigma f,l) | _ -> whd_evar sigma t - let class_of1 env evd t = - let sigma = evars_of evd in - class_of env sigma (whd_app_evar sigma t) - (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = let rec apply_rec acc typ = function @@ -107,18 +103,16 @@ module Default = struct (* raise Not_found if no coercion found *) let inh_pattern_coerce_to loc pat ind1 ind2 = - let i1 = inductive_class_of ind1 in - let i2 = inductive_class_of ind2 in - let p = lookup_pattern_path_between (i1,i2) in + let p = lookup_pattern_path_between (ind1,ind2) in apply_pattern_coercion loc pat p (* appliquer le chemin de coercions p à hj *) - let apply_coercion env p hj typ_cl = + let apply_coercion env sigma p hj typ_cl = try fst (List.fold_left (fun (ja,typ_cl) i -> let fv,isid = coercion_value i in - let argl = (class_args_of typ_cl)@[ja.uj_val] in + let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in let jres = apply_coercion_args env argl fv in (if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } @@ -137,16 +131,15 @@ module Default = struct (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> (try - let t,i1 = class_of1 env evd j.uj_type in - let p = lookup_path_to_fun_from i1 in - (evd,apply_coercion env p j t) + let t,p = + lookup_path_to_fun_from env (evars_of evd) j.uj_type in + (evd,apply_coercion env (evars_of evd) p j t) with Not_found -> (evd,j)) let inh_tosort_force loc env evd j = try - let t,i1 = class_of1 env evd j.uj_type in - let p = lookup_path_to_sort_from i1 in - let j1 = apply_coercion env p j t in + let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in + let j1 = apply_coercion env (evars_of evd) p j t in let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in (evd,type_judgment env j2) with Not_found -> @@ -173,12 +166,12 @@ module Default = struct else let v', t' = try - let t1,i1 = class_of1 env evd c1 in - let t2,i2 = class_of1 env evd t in - let p = lookup_path_between (i2,i1) in + let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in match v with Some v -> - let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in + let j = + apply_coercion env (evars_of evd) p + {uj_val = v; uj_type = t} t2 in Some j.uj_val, j.uj_type | None -> None, t with Not_found -> raise NoCoercion diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2f507318..21e881b9 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reductionops.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: reductionops.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Pp open Util @@ -233,6 +233,7 @@ let evar = mkflags [fevar] let betaevar = mkflags [fevar; fbeta] let betaiota = mkflags [fiota; fbeta] let betaiotazeta = mkflags [fiota; fbeta;fzeta] +let betaiotazetaevar = mkflags [fiota; fbeta;fzeta;fevar] (* Contextual *) let delta = mkflags [fdelta;fevar] @@ -483,6 +484,12 @@ let whd_betaiotazeta_stack x = let whd_betaiotazeta x = app_stack (whd_betaiotazeta_state (x, empty_stack)) +let whd_betaiotazetaevar_state = whd_state_gen betaiotazetaevar +let whd_betaiotazetaevar_stack env sigma x = + appterm_of_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack)) +let whd_betaiotazetaevar env sigma x = + app_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack)) + let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e let whd_betaiotaevar_stack env sigma x = appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack)) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1ac36b2a..c026d9fe 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reductionops.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: reductionops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*) (*i*) open Names @@ -98,6 +98,7 @@ val whd_evar : evar_map -> constr -> constr val whd_beta : local_reduction_function val whd_betaiota : local_reduction_function val whd_betaiotazeta : local_reduction_function +val whd_betaiotazetaevar : contextual_reduction_function val whd_betadeltaiota : contextual_reduction_function val whd_betadeltaiota_nolet : contextual_reduction_function val whd_betaetalet : local_reduction_function @@ -105,17 +106,17 @@ val whd_betalet : local_reduction_function val whd_beta_stack : local_stack_reduction_function val whd_betaiota_stack : local_stack_reduction_function -val whd_betaiotazeta_stack : local_stack_reduction_function -val whd_betadeltaiota_stack : contextual_stack_reduction_function -val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function +val whd_betaiotazetaevar_stack : contextual_stack_reduction_function +val whd_betadeltaiota_stack : contextual_stack_reduction_function +val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function val whd_betaetalet_stack : local_stack_reduction_function val whd_betalet_stack : local_stack_reduction_function val whd_beta_state : local_state_reduction_function val whd_betaiota_state : local_state_reduction_function -val whd_betaiotazeta_state : local_state_reduction_function -val whd_betadeltaiota_state : contextual_state_reduction_function -val whd_betadeltaiota_nolet_state : contextual_state_reduction_function +val whd_betaiotazetaevar_state : contextual_state_reduction_function +val whd_betadeltaiota_state : contextual_state_reduction_function +val whd_betadeltaiota_nolet_state : contextual_state_reduction_function val whd_betaetalet_state : local_state_reduction_function val whd_betalet_state : local_state_reduction_function diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index e87a195f..2569b292 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqmktop.ml 11260 2008-07-24 20:53:12Z letouzey $ *) +(* $Id: coqmktop.ml 11380 2008-09-07 12:27:27Z glondu $ *) (* coqmktop is a script to link Coq, analogous to ocamlmktop. The command line contains options specific to coqmktop, options for the @@ -289,7 +289,8 @@ let main () = (* bytecode (we shunt ocamlmktop script which fails on win32) *) let ocamlmktoplib = " toplevellib.cma" in let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in - let ocamlccustom = ocamlcexec^" -custom -linkall" in + let ocamlccustom = Printf.sprintf "%s %s -linkall " + ocamlcexec Coq_config.coqrunbyteflags in (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom) in (* files to link *) diff --git a/test-suite/check b/test-suite/check index 571e7a67..47960e98 100755 --- a/test-suite/check +++ b/test-suite/check @@ -65,7 +65,7 @@ test_output() { done } -# La fonction suivante teste l'analyseur syntaxique fournit par "parser" +# La fonction suivante teste l'analyseur syntaxique fournit par "coq-parser" # Elle fonctionne comme test_output test_parser() { if [ -d $1 ]; then @@ -74,7 +74,7 @@ test_parser() { printf " "$f"..." tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` foutput=`dirname $f`/`basename $f .v`.out - echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1 + echo "parse_file 1 \"$f\"" | ../bin/coq-parser > $tmpoutput 2>&1 perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \ $tmpoutput 2>&1 | grep -i error > /dev/null if [ $? = 0 ] ; then @@ -250,8 +250,16 @@ echo "Interactive tests" test_interactive interactive echo "Micromega tests" test_success micromega -echo "Complexity tests" -test_complexity complexity + +# We give a chance to disable the complexity tests which may cause +# random build failures on build farms +if [ -z "$COQTEST_SKIPCOMPLEXITY" ]; then + echo "Complexity tests" + test_complexity complexity +else + echo "Skipping complexity tests" +fi + echo "Module tests" $coqtop -compile modules/Nat $coqtop -compile modules/plik diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index d652132e..525348de 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -61,3 +61,24 @@ Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)). End Q. +(* Combining class lookup and path lookup so that if a lookup fails, another + descent in the class can be found (see wish #1934) *) + +Record Setoid : Type := +{ car :> Type }. + +Record Morphism (X Y:Setoid) : Type := +{evalMorphism :> X -> Y}. + +Definition extSetoid (X Y:Setoid) : Setoid. +intros X Y. +constructor. +exact (Morphism X Y). +Defined. + +Definition ClaimA := forall (X Y:Setoid) (f: extSetoid X Y) x, f x= f x. + +Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True). + +Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x. + diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 94444f5b..05cd1892 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: FMapFacts.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: FMapFacts.v 11359 2008-09-04 09:43:36Z notin $ *) (** * Finite maps library *) @@ -975,7 +975,7 @@ Module WProperties (E:DecidableType)(M:WSfun E). fold (fun k e b => if f k e then true else b) m false. Definition partition (f : key -> elt -> bool)(m : t elt) := - (filter f m, filter (fun k e => negb (f k e))). + (filter f m, filter (fun k e => negb (f k e)) m). Section Specs. Variable f : key -> elt -> bool. diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index 3900987e..65c39b7a 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -24,7 +24,8 @@ body { padding: 0px 0px; #main{ display: block; padding: 10px; overflow: hidden; - font-size: 10pt } + font-size: 100%; + line-height: 80% } #main a.idref:visited {color : #416DFF; text-decoration : none; } #main a.idref:link {color : #416DFF; text-decoration : none; } @@ -39,16 +40,16 @@ body { padding: 0px 0px; #main .keyword { color : #cf1d1d } #main { color: black } -#main .section { background-color:#899BD6; - font-size : 20pt } +#main .section { background-color:#90bdff; + font-size : 175% } -#main code { font-family: monospace; - line-height: 50% } +#main code { font-family: monospace } #main .doc { margin: 0px; padding: 10px; font-family: sans-serif; - font-size: 11pt; + font-size: 100%; + line-height: 100%; font-weight:bold; color: black; background-color: #90bdff; @@ -58,7 +59,7 @@ body { padding: 0px 0px; /* Pied de page */ -#footer { font-size: 8pt; +#footer { font-size: 65%; font-family: sans-serif; } #footer a:visited { color: blue; } diff --git a/toplevel/class.ml b/toplevel/class.ml index 2c6a63b0..6ebc663b 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: class.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: class.ml 11343 2008-09-01 20:55:13Z herbelin $ *) open Util open Pp @@ -139,7 +139,7 @@ let get_source lp source = let (cl1,lv1) = match lp with | [] -> raise Not_found - | t1::_ -> find_class_type t1 + | t1::_ -> find_class_type (Global.env()) Evd.empty t1 in (cl1,lv1,1) | Some cl -> @@ -147,7 +147,7 @@ let get_source lp source = | [] -> raise Not_found | t1::lt -> try - let cl1,lv1 = find_class_type t1 in + let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in if cl = cl1 then cl1,lv1,(List.length lt+1) else raise Not_found with Not_found -> aux lt @@ -157,7 +157,7 @@ let get_target t ind = if (ind > 1) then CL_FUN else - fst (find_class_type t) + fst (find_class_type (Global.env()) Evd.empty t) let prods_of t = let rec aux acc d = match kind_of_term d with @@ -225,8 +225,9 @@ let build_id_coercion idf_opt source = match idf_opt with | Some idf -> idf | None -> + let cl,_ = find_class_type (Global.env()) Evd.empty t in id_of_string ("Id_"^(ident_key_of_class source)^"_"^ - (ident_key_of_class (fst (find_class_type t)))) + (ident_key_of_class cl)) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry |