diff options
| author |  Samuel Mimram <smimram@debian.org> | 2007-10-15 19:55:12 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2007-10-15 19:55:12 +0000 |
| commit | 4767d724d489a7ad67f696e9401e70b9f9ae2143 (patch) | |
| tree | 142a99bc1cd3beef403f1942908de090f70c5e07 | |
| parent | 72b9a7df489ea47b3e5470741fd39f6100d31676 (diff) | |
Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg
63 files changed, 1085 insertions, 613 deletions
@@ -378,7 +378,8 @@ contrib/cc/ccalgo.cmi: lib/util.cmi kernel/term.cmi lib/pp.cmi \ kernel/names.cmi contrib/cc/ccproof.cmi: kernel/term.cmi kernel/names.cmi \ contrib/cc/ccalgo.cmi -contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.cmi +contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.cmi \ + contrib/cc/ccproof.cmi contrib/correctness/past.cmi: lib/util.cmi interp/topconstr.cmi \ kernel/term.cmi kernel/names.cmi contrib/correctness/pcicenv.cmi: kernel/term.cmi kernel/sign.cmi \ @@ -2261,8 +2262,9 @@ toplevel/command.cmo: toplevel/vernacexpr.cmo lib/util.cmi kernel/typeops.cmi \ pretyping/indrec.cmi library/impargs.cmi library/global.cmi \ pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \ kernel/environ.cmi kernel/entries.cmi library/declare.cmi \ - kernel/declarations.cmi library/decl_kinds.cmo interp/constrintern.cmi \ - interp/constrextern.cmi toplevel/class.cmi toplevel/command.cmi + kernel/declarations.cmi library/decl_kinds.cmo interp/coqlib.cmi \ + interp/constrintern.cmi interp/constrextern.cmi toplevel/class.cmi \ + toplevel/command.cmi toplevel/command.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/typeops.cmx \ interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \ proofs/tacmach.cmx interp/syntax_def.cmx library/states.cmx \ @@ -2277,8 +2279,9 @@ toplevel/command.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/typeops.cmx \ pretyping/indrec.cmx library/impargs.cmx library/global.cmx \ pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \ kernel/environ.cmx kernel/entries.cmx library/declare.cmx \ - kernel/declarations.cmx library/decl_kinds.cmx interp/constrintern.cmx \ - interp/constrextern.cmx toplevel/class.cmx toplevel/command.cmi + kernel/declarations.cmx library/decl_kinds.cmx interp/coqlib.cmx \ + interp/constrintern.cmx interp/constrextern.cmx toplevel/class.cmx \ + toplevel/command.cmi toplevel/coqinit.cmo: toplevel/vernac.cmi toplevel/toplevel.cmi \ lib/system.cmi lib/pp.cmi lib/options.cmi kernel/names.cmi \ library/nameops.cmi toplevel/mltop.cmi config/coq_config.cmi \ @@ -2483,18 +2486,20 @@ toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \ interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \ proofs/pfedit.cmi parsing/pcoq.cmi lib/options.cmi library/nametab.cmi \ - kernel/names.cmi library/libnames.cmi parsing/lexer.cmi interp/genarg.cmi \ - kernel/environ.cmi parsing/egrammar.cmi library/dischargedhypsmap.cmi \ - pretyping/detyping.cmi interp/constrintern.cmi toplevel/command.cmi \ - toplevel/cerrors.cmi toplevel/whelp.cmi + kernel/names.cmi library/libnames.cmi parsing/lexer.cmi \ + library/goptions.cmi interp/genarg.cmi kernel/environ.cmi \ + parsing/egrammar.cmi library/dischargedhypsmap.cmi pretyping/detyping.cmi \ + interp/constrintern.cmi toplevel/command.cmi toplevel/cerrors.cmi \ + toplevel/whelp.cmi toplevel/whelp.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/termops.cmx kernel/term.cmx proofs/tacmach.cmx lib/system.cmx \ interp/syntax_def.cmx proofs/refiner.cmx pretyping/rawterm.cmx lib/pp.cmx \ proofs/pfedit.cmx parsing/pcoq.cmx lib/options.cmx library/nametab.cmx \ - kernel/names.cmx library/libnames.cmx parsing/lexer.cmx interp/genarg.cmx \ - kernel/environ.cmx parsing/egrammar.cmx library/dischargedhypsmap.cmx \ - pretyping/detyping.cmx interp/constrintern.cmx toplevel/command.cmx \ - toplevel/cerrors.cmx toplevel/whelp.cmi + kernel/names.cmx library/libnames.cmx parsing/lexer.cmx \ + library/goptions.cmx interp/genarg.cmx kernel/environ.cmx \ + parsing/egrammar.cmx library/dischargedhypsmap.cmx pretyping/detyping.cmx \ + interp/constrintern.cmx toplevel/command.cmx toplevel/cerrors.cmx \ + toplevel/whelp.cmi contrib/cc/ccalgo.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \ kernel/names.cmi library/goptions.cmi contrib/cc/ccalgo.cmi contrib/cc/ccalgo.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \ @@ -3503,40 +3508,6 @@ contrib/omega/g_omega.cmx: lib/util.cmx tactics/tacinterp.cmx \ toplevel/cerrors.cmx contrib/omega/omega.cmo: lib/util.cmi kernel/names.cmi contrib/omega/omega.cmx: lib/util.cmx kernel/names.cmx -contrib/recdef/recdef.cmo: toplevel/vernacinterp.cmi \ - toplevel/vernacentries.cmi lib/util.cmi pretyping/typing.cmi \ - kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ - kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ - proofs/tactic_debug.cmi pretyping/tacred.cmi proofs/tacmach.cmi \ - tactics/tacinterp.cmi kernel/safe_typing.cmi pretyping/reductionops.cmi \ - pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ - pretyping/pretyping.cmi parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi \ - parsing/pcoq.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \ - library/nameops.cmi library/libnames.cmi library/lib.cmi \ - tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \ - pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \ - kernel/entries.cmi tactics/elim.cmi parsing/egrammar.cmi \ - tactics/eauto.cmi library/declare.cmi kernel/declarations.cmi \ - library/decl_kinds.cmo interp/coqlib.cmi interp/constrintern.cmi \ - toplevel/command.cmi kernel/closure.cmi toplevel/cerrors.cmi \ - tactics/auto.cmi -contrib/recdef/recdef.cmx: toplevel/vernacinterp.cmx \ - toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \ - kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \ - kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ - proofs/tactic_debug.cmx pretyping/tacred.cmx proofs/tacmach.cmx \ - tactics/tacinterp.cmx kernel/safe_typing.cmx pretyping/reductionops.cmx \ - pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \ - pretyping/pretyping.cmx parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx \ - parsing/pcoq.cmx lib/options.cmx library/nametab.cmx kernel/names.cmx \ - library/nameops.cmx library/libnames.cmx library/lib.cmx \ - tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \ - pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \ - kernel/entries.cmx tactics/elim.cmx parsing/egrammar.cmx \ - tactics/eauto.cmx library/declare.cmx kernel/declarations.cmx \ - library/decl_kinds.cmx interp/coqlib.cmx interp/constrintern.cmx \ - toplevel/command.cmx kernel/closure.cmx toplevel/cerrors.cmx \ - tactics/auto.cmx contrib/ring/g_quote.cmo: lib/util.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo contrib/ring/quote.cmo parsing/pptactic.cmi lib/pp.cmi \ parsing/pcoq.cmi interp/genarg.cmi parsing/egrammar.cmi \ @@ -4001,6 +3972,10 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \ parsing/egrammar.cmx toplevel/cerrors.cmx contrib/xml/xml.cmo: contrib/xml/xml.cmi contrib/xml/xml.cmx: contrib/xml/xml.cmi +doc/refman/euclid.cmo: doc/refman/euclid.cmi +doc/refman/euclid.cmx: doc/refman/euclid.cmi +doc/refman/heapsort.cmo: doc/refman/heapsort.cmi +doc/refman/heapsort.cmx: doc/refman/heapsort.cmi ide/utils/config_file.cmo: ide/utils/config_file.cmi ide/utils/config_file.cmx: ide/utils/config_file.cmi ide/utils/configwin_html_config.cmo: ide/utils/configwin_types.cmo \ @@ -4154,39 +4129,38 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \ + /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ kernel/byterun/coq_fix_code.h coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_jumptbl.h coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \ - kernel/byterun/coq_interp.h + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_interp.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/local/lib/ocaml/caml/alloc.h @@ -1,3 +1,14 @@ +Changes from V8.1pl1 to V8.1pl2 +=============================== + +Installation + +- Support for compilation with ocaml 3.10 and (transitional) camlp5. + +Bug fixes + +- Many bugs have been fixed (cf coq-bugs web page) + Changes from V8.1 to V8.1pl1 ============================ @@ -5,16 +5,51 @@ WHAT DO YOU NEED ? ================== - Coq is designed to work on computers equipped with the Unix operating - system. In order to compile Coq V8.1 you need: + Coq is designed to work on computers equipped with a POSIX (Unix or + a clone) operating system. It also works under Microsoft Windows + (see INSTALL.win); for a precompiled MacOS X package, see + INSTALL.macosx. + + Coq is known to be actively used under GNU/Linux (i386, amd64 and + ppc) and FreeBSD. Automated tests are run under many, many + different architectures under GNU/Linux. + + Naturally, Coq will run faster on an architecture where OCaml can + compile to native code, rather than only bytecode. At time of + writing, that is IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64, + HPPA and StrongArm. See + http://caml.inria.fr/ocaml/portability.en.html for details. + + + Your OS may already contain Coq under the form of a precompiled + package or ready-to-compile port. In this case, and if the supplied + version suits you, follow the usual procedure for your OS to + install it. E.g.: + + - Debian GNU/Linux (or Debian GNU/k*BSD or ...): + + aptitude install coq + + - Gentoo GNU/Linux: emerge sci-mathematics/coq + + + Should you need or prefer to compile Coq V8.1 yourself, you need: - Objective Caml version 3.07 or later (available at http://caml.inria.fr/) - - Until now, it has mainly been tested on Sun workstations running Solaris, - and DEC alpha and Pentium workstations running Linux. By FTP, Coq - comes as a single compressed tar-file. You have probably already - decompressed it if you are reading this document. + + For Ocaml version >= 3.10.0, you also need to install camlp5 + version <= 4.08, or 5.01 transitional + (see http://pauillac.inria.fr/~ddr/camlp5/) + + - GNU Make + + - a C compiler + + - for Coqide, the Lablgtk development files, and the GTK libraries + + By FTP, Coq comes as a single compressed tar-file. You have + probably already decompressed it if you are reading this document. QUICK INSTALLATION PROCEDURE. diff --git a/INSTALL.ide b/INSTALL.ide index 0ca3d9e0..365f59ee 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -8,24 +8,66 @@ DISCLAIMER: CoqIde is ongoing work. Eventhough it should never let you loose a proof, you may encounter unexpected bugs. Do not hesitate to send suggestions/bug reports. +DISTRIBUTION PACKAGES + +Your POSIX operating system may already contain precompiled packages +for Coq, including CoqIde, or a ready-to-compile... If the version +provided there suits you, follow the usual procedure for your +operating system. + +E.g., on Debian GNU/Linux (or Debian GNU/k*BSD or ...), do: + aptitude install coqide +On Gentoo GNU/Linux, do: + USE=ide emerge sci-mathematics/coq + +Else, read the rest of this document to compile your own CoqIde. + REQUIREMENT: - OCaml >= 3.07 with native thread support. - make world must succeed. - The graphical toolkit Gtk 2.x. See http://www.gtk.org. - The official supported version is at least 2.2.x. - You may still compile CoqIde with older 2.0.x versions and + The official supported version is at least 2.8.x. + You may still compile CoqIde with older versions and use all features. Run "pkg-config --modversion gtk+-2.0" to check your version. - All recent distributions have precompiled packages. - Do not forget to install the developement headers packages. - As for Debian/woody, + All recent distributions have precompiled packages. + Do not forget to install the development headers packages. + As for Debian or Ubuntu, apt-get install libgtk2.0-dev - should be enough. + should be enough. + + - The OCaml bindings for for GTK+ 2.x, lablgtk2. + + Your distribution may contain precompiled packages. For + example, for Debian, run + aptitude install liblablgtk2-ocaml-dev + + If it does not, see + http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html . + + The latest official release of lablftk2 is here: + http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.10.0.tar.gz + + Note that even if its README requires ocaml > 3.07, it works + ok with 3.07. If you are in a hurry just run : + + cd /tmp && \ + wget \ + http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.10.0.tar.gz && \ + tar zxvf lablgtk-2.10.0.tar.gz && \ + cd lablgtk-2.10.0 && \ + ./configure && \ + make world && \ + make install + + You must have write access to the OCaml standard library path. + + If this fails, read lablgtk-2.10.0/README. INSTALLATION - 0) For optimal performance, OCaml must support native threads (aka pthreads). +0) For optimal performance, OCaml must support native threads (aka pthreads). If this not the case, this means that Coq computations will be slow and "make ide" will fail. Use "make bin/coqide.byte" instead. To fix this problem, just recompile OCaml from source and configure OCaml with : @@ -33,26 +75,7 @@ INSTALLATION In case you install over an existing copy of OCaml, you should better empty the OCaml installation directory. - 1) You need to install the OCaml stub library lablgtk2. See - http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html - The first official release of lablftk2 is here: - http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.2.0.tar.gz - Note that even if its README requires ocaml > 3.07, it works ok with 3.07. - If you are in a hurry just run : - -cd /tmp && \ -wget \ - http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk-2.2.0.tar.gz && \ -tar zxvf lablgtk-2.2.0.tar.gz && \ -cd lablgtk-2.2.0 && \ -./configure && \ -make world && \ -make install - - You must have write access to the OCaml standard library path. - If this fails read lablgtk-2.2.0/README. - -2) Go into your Coq source directory and, as usual, configure with: +1) Go into your Coq source directory and, as usual, configure with: ./configure @@ -68,7 +91,7 @@ make install In case you are upgrading from an old version you may need to run make clean-ide -3) You may now run bin/coqide +2) You may now run bin/coqide NOTES diff --git a/INSTALL.win b/INSTALL.win deleted file mode 100644 index f2cddb8a..00000000 --- a/INSTALL.win +++ /dev/null @@ -1,63 +0,0 @@ -***************************************************************** -* INSTALLATION PROCEDURE FOR THE COQ V8 SYSTEM UNDER WINDOWS OS * -***************************************************************** - - The binary distribution consists in a .zip archive file. This .zip contains -long filenames and cannot therefore be unpacked with pkunzip version 2. Use -either Winzip (shareware) or the Windows version of unzip (freeware): - - http://www.winzip.com/ - http://www.winimage.com/zLibDll/ - - Unzipping the distribution creates (among others) the following directories -and files: - - coq\bin\ The command-line tools - coq\lib\ The standard library files - coq\emacs A Coq mode for your Emacs - coq\man\man1 The man pages for the command-line tools - - There are two cases to consider : - -1. You unzip in the root of your drive (say C): -=============================================== - - Hence Coq will be installed in C:\coq - - You must add the C:\coq\bin path to your environment variable PATH. This is -done by adding the following line to your AUTOEXEC.BAT: - - set PATH=%PATH%;C:\coq\bin - - You may also want to specify where Coq has to look for your configuration -file .coqrc (not mandatory), e.g.: - - set HOME=C:\My_Documents\Coq - -2. You unzip in some other place (say D:\My_Dir): -================================================= - - You must add the D:\My_Dir\coq\bin path to your environment variable PATH. -This is done by adding the following line to AUTOEXEC.BAT: - - set PATH=%PATH%;D:\My_Dir\coq\bin - - You must also set the environment variables COQBIN and COQLIB to tell Coq -that binaries and libraries are not in the default place. This is done by -adding the following lines to your AUTOEXEC.BAT: - - set COQBIN=D:\My_Dir\coq\bin - set COQLIB=D:\My_Dir\coq\lib - - You may also want to specify where Coq has to look for your configuration -file .coqrc (not mandatory), e.g.: - - set HOME=C:\My_Documents\Coq - -PROBLEMS: -========= - - If you have any trouble with this installation, please contact: -coq-bugs@pauillac.inria.fr. - - The Coq Team. @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 10014 2007-07-17 15:14:39Z notin $ +# $Id: Makefile 10216 2007-10-11 13:44:00Z notin $ # Makefile for Coq @@ -79,18 +79,19 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ -I contrib/field -I contrib/subtac -I contrib/rtauto \ -I contrib/recdef -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) +MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) $(COQIDEINCLUDES) OCAMLC += $(CAMLFLAGS) OCAMLOPT += $(CAMLFLAGS) BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) $(INLINEFLAG) $(USERFLAGS) -DEPFLAGS=$(LOCALINCLUDES) +DEPFLAGS= -slash $(LOCALINCLUDES) OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS) OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS) -CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo +CAMLP4EXTENSIONS=-I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo pa_macro.cmo +CAMLP4OPTIONS=$(CAMLP4COMPAT) -D$(CAMLVERSION) CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)|\1|p' COQINCLUDES= # coqtop includes itself the needed paths @@ -352,12 +353,6 @@ OBJSCMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \ CINCLUDES= -I $(CAMLHLIB) -ifeq ($(CAMLVERSION),OCAML307) - CFLAGS=-fno-defer-pop -Wall -Wno-unused -DOCAML_307 -else - CFLAGS=-fno-defer-pop -Wall -Wno-unused -endif - # libcoqrun.a $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) @@ -611,7 +606,7 @@ COQIDECMO=ide/utils/okey.cmo ide/utils/config_file.cmo \ ide/coq_tactics.cmo ide/command_windows.cmo ide/coqide.cmo COQIDECMX=$(COQIDECMO:.cmo=.cmx) -COQIDEFLAGS=-thread -I +lablgtk2 +COQIDEFLAGS=-thread $(COQIDEINCLUDES) BEFOREDEPEND+= ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml BEFOREDEPEND+= ide/config_parser.mli ide/config_parser.ml BEFOREDEPEND+= ide/utf8_convert.ml @@ -1168,7 +1163,7 @@ $(COQDEP): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS) -BEFOREDEPEND+= tools/coqdep_lexer.ml $(COQDEP) +BEFOREDEPEND+= tools/coqdep_lexer.ml GALLINACMO=tools/gallina_lexer.cmo tools/gallina.cmo @@ -1262,6 +1257,7 @@ install-tools:: $(MKDIR) $(FULLBINDIR) # recopie des fichiers de style pour coqide $(MKDIR) $(FULLCOQLIB)/tools/coqdoc + touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715) cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc cp $(TOOLS) $(FULLBINDIR) @@ -1483,7 +1479,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)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ @@ -1500,15 +1496,15 @@ ML4FILES +=parsing/g_minicoq.ml4 \ parsing/g_decl_mode.ml4 -# BEFOREDEPEND+= $(GRAMMARCMO) +BEFOREDEPEND+= $(GRAMMARCMO) # BEFOREDEPEND+= parsing/pcoq.ml parsing/extend.ml -# File using pa_ifdef and only necessary for parsing ml files +# File using pa_macro and only necessary for parsing ml files parsing/q_coqast.cmo: parsing/q_coqast.ml4 $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo $(CAMLP4COMPAT) -impl" -c -impl $< + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(CAMLP4OPTIONS) -impl" -c -impl $< # toplevel/mltop.ml4 (ifdef Byte) @@ -1522,11 +1518,11 @@ toplevel/mltop.cmx: toplevel/mltop.optml toplevel/mltop.byteml: toplevel/mltop.ml4 $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo -DByte -impl $< > $@ || rm -f $@ toplevel/mltop.optml: toplevel/mltop.ml4 $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -impl $< > $@ || rm -f $@ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo -impl $< > $@ || rm -f $@ ML4FILES += toplevel/mltop.ml4 @@ -1571,11 +1567,11 @@ ML4FILES += lib/pp.ml4 lib/compat.ml4 lib/compat.cmo: lib/compat.ml4 $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $< + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(CAMLP4OPTIONS) -impl" -c -impl $< lib/compat.cmx: lib/compat.ml4 $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $< + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(CAMLP4OPTIONS) -impl" -c -impl $< # files compiled with camlp4 because of streams syntax @@ -1591,11 +1587,11 @@ ML4FILES += contrib/xml/xml.ml4 \ parsing/lexer.cmx: parsing/lexer.ml4 $(SHOW)'OCAMLOPT4 $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $< + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo `$(CAMLP4DEPS) $<` -impl" -c -impl $< parsing/lexer.cmo: parsing/lexer.ml4 $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` pr_o.cmo -impl" -c -impl $< + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo `$(CAMLP4DEPS) $<` -impl" -c -impl $< # pretty printing of the revision number when compiling a checked out # source tree @@ -1647,17 +1643,11 @@ archclean:: .ml4.cmx: $(SHOW)'OCAMLOPT4 $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) `$(CAMLP4DEPS) $<` $(CAMLP4OPTIONS) -impl" -c -impl $< .ml4.cmo: $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< - -%.ml: %.ml4 - $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ - -#.v.vo: -# $(BOOTCOQTOP) -compile $* + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) `$(CAMLP4DEPS) $<` $(CAMLP4OPTIONS) -impl" -c -impl $< .el.elc: echo "(setq load-path (cons \".\" load-path))" > $*.compile @@ -1721,8 +1711,8 @@ cleanconfig:: alldepend: depend dependcoq -dependcoq: - $(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \ +dependcoq: $(BEFOREDEPEND) $(COQDEP) + $(COQDEP) -slash -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \ $(ALLFSETS:.vo=.v) $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq # Build dependencies ignoring failures in building ml files from ml4 files @@ -1745,30 +1735,43 @@ ML4FILESML = $(ML4FILES:.ml4=.ml) # Expresses dependencies of the .ml4 files w.r.t their grammars .PHONY: dependp4 -dependp4: $(ML4FILES) +dependp4: rm -f .depend.camlp4 for f in $(ML4FILES); do \ printf "%s" `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4; \ echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \ done +# Produce the .ml files using Makefile.dep +.PHONY: ml4filesml +ml4filesml:: .depend.camlp4 parsing/grammar.cma + $(MAKE) -f Makefile.dep $(ML4FILESML) + + .PHONY: depend -depend: $(BEFOREDEPEND) dependp4 $(ML4FILESML) +depend: dependp4 ml4filesml $(BEFOREDEPEND) # 1. We express dependencies of the .ml files w.r.t their grammars # 2. Then we are able to produce the .ml files using Makefile.dep # 3. We compute the dependencies inside the .ml files using ocamldep $(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend # 4. We express dependencies of .cmo and .cmx files w.r.t their grammars for f in $(ML4FILES); do \ - printf "%s" `dirname $$f`/`basename $$f .ml4`".cmo: " >> .depend; \ - echo `$(CAMLP4DEPS) $$f` >> .depend; \ - printf "%s" `dirname $$f`/`basename $$f .ml4`".cmx: " >> .depend; \ - echo `$(CAMLP4DEPS) $$f` >> .depend; \ + bn=`dirname $$f`/`basename $$f .ml4`; \ + deps=`$(CAMLP4DEPS) $$f`; \ + if [[ $${deps} != "" ]]; then \ + /bin/mv -f .depend .depend.tmp; \ + sed -e "\|^$${bn}.cmo|s|^$${bn}.cmo: \(.*\)$$|$${bn}.cmo: $${deps} \1|" \ + -e "\|^$${bn}.cmx|s|^$${bn}.cmx: \(.*\)$$|$${bn}.cmx: $${deps} \1|" \ + .depend.tmp > .depend; \ + /bin/rm -f .depend.tmp; \ + fi; \ done # 5. We express dependencies of .o files - $(CC) -I $(CAMLHLIB) -MM kernel/byterun/*.c >> .depend + $(CC) -MM -isystem $(CAMLHLIB) kernel/byterun/*.c >> .depend # 6. Finally, we erase the generated .ml files rm -f $(ML4FILESML) +# and the .cmo and .cmi files needed by grammar.cma + rm -f rm parsing/*.cm[io] lib/pp.cm[io] lib/compat.cm[io] # 7. Since .depend contains correct dependencies .depend.devel can be deleted # (see dev/Makefile.dir for details about this file) if [ -e makefile ]; then >.depend.devel; else rm -f .depend.devel; fi @@ -1787,7 +1790,6 @@ devel: -include .depend -include .depend.coq --include .depend.camlp4 clean:: find . -name "\.#*" -exec rm -f {} \; diff --git a/Makefile.dep b/Makefile.dep index 93ca6dfa..8569dfbf 100644 --- a/Makefile.dep +++ b/Makefile.dep @@ -12,4 +12,4 @@ include Makefile include .depend.camlp4 .ml4.ml: - $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ + $(CAMLP4O) $(CAMLP4EXTENSIONS) pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ diff --git a/PROBLEMES b/PROBLEMES new file mode 100644 index 00000000..4e522a8a --- /dev/null +++ b/PROBLEMES @@ -0,0 +1,54 @@ +Intuition plante en 7.1 à certains endroits où il réussissait en 6.3. +Y a-t-il une explication ? (cf contrib sheaves de Chicli - HH) + +---------------------------------------------------------------------- +Theorem toto : (A:Prop)A->A. +Refine [A;x]?. +produit le message "type_of: this is not a well-typed term. Please report." + +---------------------------------------------------------------------- +"Intro until 1" plante avec le message +"Error: Internal tactic intro cannot be applied to intro until #GENTERM 1" +--> intro est répété + GENTERM + +---------------------------------------------------------------------- +La synthèse du ? dans l'exemple suivant se fait en V6 mais pas en V7: + +Inductive Prod : Type := Pair : Set->Set->Prod. +Definition Pfst := [p:Prod](let (x, _) = p in x). +Variable P : Prod->Type. +Variable i : Set->(P (Pair nat nat)). +Variable j : (X:Prod)(Pfst X)->(P X)->Prop. +Variable k : nat. +Variable l : (P (Pair nat nat)). +Check (!j ? k (i nat)). (* Marche en V6, pas en V7 *) +Check (!j ? k l). (* Ne marche ni en V6 !!! ni en V7 *) + +---------------------------------------------------------------------- +Des CASTEDCOMMAND s'affiche dans les scripts de preuves. + +---------------------------------------------------------------------- +Probleme d'affichage des scripts de preuve (disparition des THEN) +Compute affiche Cbv Beta Iota + +---------------------------------------------------------------------- +Variable + Record => clash. Exemple: + +Section S. +Variable F:Set. +Record R [ F:Set; x:F ] : Set := { c : x=x }. + => Error: new_isevar_sign: two vars have the same name + +---------------------------------------------------------------------- +Declaration de Local a l'interieur d'un but ... + +---------------------------------------------------------------------- +Certains Clear deviennent impossible car la variable apparait dans +un lemme local, c'est plutot sain ... + +---------------------------------------------------------------------- +l'entree numarg de g_tactic.ml4 accepte aussi des id... (pour les +binding je pense) d'ou des erreurs de syntaxe ... pure_numarg est +plus sûr +REPONSE PROVISOIRE: si c'est pour Specialize, faudrait en changer la +syntaxe, elle est incompatible avec L_tac. @@ -6,7 +6,12 @@ THE COQ V8.1 SYSTEM INSTALLATION. ============= - See the file INSTALL.win for installation procedure. + The Coq package for Windows comes with an auto-installer. It will +install Coq binaries and libraries under any directory you specify +(C:\Program Files\Coq is the default path). It also creates shortcuts +in the Windows menus. Alternatively, you can launch Coq using Coq.bat +and Coqide.bat in the installation directory (C:\Program Files\Coq by +default). COMPILATION. ============ @@ -15,25 +20,34 @@ COMPILATION. distribution. If you really need to recompile under Windows, here are some indications: - 1- Install ocaml version 3.07 or later, Visual C++ (needed - for the -custom option of ocaml) and MASM (needed if you want - to produce a native version). + 1- Install ocaml for Windows (MinGW port), preferably version 3.09.3. + See: http://caml.inria.fr - 2- Install a complete set of Unix utilities (used by Makefiles). - See: http://sources.redhat.com/cygwin/. + 2- Install a shell environment with at least: + - a C compiler (gcc), + - the GNU make utility - 3- Under cygwin, type successively + The Cygwin environment is well suited for compiling Coq + (official packages are made using Cygwin) See: + http://www.cygwin.com + + 3- In order to compile Coqide, you will need the LablGTK library + See: http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html + + You also need to install the GTK libraries for Windows (see the + installation instruction for LablGTK) + + 4- In a shell window, type successively ./configure make world make install - make clean - 4- Though not nescessary, you can find useful: + 5- Though not nescessary, you can find useful: - Windows version of (X)Emacs: it is a powerful environment for developpers with coloured syntax, modes for compilation and debug, and many more. It is free. See: http://www.gnu.org/software. - - Windows cvs client (very useful if you have access to the Coq + - Windows subversion client (very useful if you have access to the Coq archive). Good luck :-) @@ -0,0 +1,51 @@ +Langage: + +Distribution: + +Environnement: + +- Porter SearchIsos + +Noyau: + +Tactic: + +- Que contradiction raisonne a isomorphisme pres de False + +Vernac: + +- Print / Print Proof en fait identiques ; Print ne devrait pas afficher + les constantes opaques (devrait afficher qqchose comme <opaque>) + +Theories: + +- Rendre transparent tous les theoremes prouvant {A}+{B} +- Faire demarrer PolyList.nth a` l'indice 0 + Renommer l'actuel nth en nth1 ?? + +Doc: + +- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection +- Documenter le filtrage sur les types inductifs avec let-ins (dont la + compatibilite V6) + +- Ajouter let dans les règles du CIC + -> FAIT, mais reste a documenter le let dans les inductifs + et les champs manifestes dans les Record +- revoir le chapitre sur les tactiques utilisateur +- faut-il mieux spécifier la sémantique de Simpl (??) + +- Préciser la clarification syntaxique de IntroPattern +- preciser que Goal vient en dernier dans une clause pattern list et + qu'il doit apparaitre si il y a un "in" + +- Omega Time debranche mais Omega System et Omega Action remarchent ? +- Ajout "Replace in" (mais TODO) +- Syntaxe Conditional tac Rewrite marche, à documenter +- Documenter Dependent Rewrite et CutRewrite ? +- Ajouter les motifs sous-termes de ltac + +- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) +- mettre à jour la doc de induction (arguments multiples) (Pierre C.) +- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) +--> mettre à jour le CHANGES (vers la ligne 72) diff --git a/config/Makefile.template b/config/Makefile.template index 3ea7c7c9..1e611356 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -31,7 +31,7 @@ EMACSLIB="EMACSLIBDIRECTORY" EMACS=EMACSCOMMAND # Path to Coq distribution -COQTOP=COQTOPDIRECTORY +COQSRC=COQSRCDIRECTORY VERSION=COQVERSION # Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH @@ -48,6 +48,9 @@ CAMLP4O=CAMLP4TOOL CAMLP4COMPAT=CAMLP4COMPATFLAGS MYCAMLP4LIB="CAMLP4LIBDIRECTORY" +# LablGTK +COQIDEINCLUDES=LABLGTKINCLUDES + # Objective-Caml compile command OCAMLC="BYTECAMLC" OCAMLOPT="NATIVECAMLC" @@ -62,7 +65,7 @@ CAMLOPTLINK="NATIVECAMLC" CAMLMKTOP="CAMLMKTOPEXEC" # Caml flags -CAMLFLAGS=CAMLANNOTATEFLAG +CAMLFLAGS=-rectypes CAMLANNOTATEFLAG # Compilation debug flag CAMLDEBUG=COQDEBUGFLAG @@ -73,16 +76,15 @@ INLINEFLAG=COQINLINEFLAG # User compilation flag USERFLAGS= +# Flags for GCC +CFLAGS=CCOMPILEFLAGS + # Compilation profile flag CAMLTIMEPROF=COQPROFILEFLAG # The best compiler: native (=opt) or bytecode (=byte) if no native compiler BEST=BESTCOMPILER -# For Camlp4 use -P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing -P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep - # Your architecture # Can be obtain by UNIX command arch ARCH=ARCHITECTURE diff --git a/config/coq_config.mli b/config/coq_config.mli index c214344e..bf77f0f3 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 9115 2006-09-01 13:47:00Z notin $ i*) +(*i $Id: coq_config.mli 10185 2007-10-06 18:05:13Z herbelin $ i*) val local : bool (* local use (no installation) *) @@ -18,6 +18,7 @@ val coqtop : string (* where are the sources *) val camldir : string (* base directory of OCaml binaries *) val camllib : string (* for Dynlink *) +val camlp4 : string (* exact name of camlp4: either "camlp4" ou "camlp5" *) val camlp4lib : string (* where is the library of Camlp4 *) val best : string (* byte/opt *) @@ -6,8 +6,8 @@ # ################################## -VERSION=8.1pl1 -DATE="Jul. 2007" +VERSION=8.1pl2 +DATE="Oct. 2007" # a local which command for sh which () { @@ -42,7 +42,11 @@ usage () { echo "-coqdocdir" echo -e "\tSpecifies where Coqdoc style files are to be installed\n" echo "-camldir" - echo -e "\tTells configure where to look for OCaml files\n" + echo -e "\tSpecifies the path to the OCaml library\n" + echo "-lablgtkdir" + echo -e "\tSpecifies the path to the Lablgtk library\n" + echo "-camlp5dir" + echo -e "\tSpecifies where to look for the Camlp5 library and tells to use it\n" echo "-arch" echo -e "\tSpecifies the architecture\n" echo "-opt" @@ -86,6 +90,7 @@ coq_profile_flag= coq_annotate_flag= coq_inline_flag= best_compiler=opt +cflags="-fno-defer-pop -Wall -Wno-unused" gcc_exec=gcc ar_exec=ar @@ -100,6 +105,7 @@ mandir_spec=no emacslib_spec=no emacs_spec=no camldir_spec=no +lablgtkdir_spec=no coqdocdir_spec=no fsets_opt=no fsets=all @@ -109,7 +115,6 @@ arch_spec=no coqide_spec=no with_geoproof=false -# COQTOP=`pwd` COQSRC=`pwd` # Parse command-line arguments @@ -126,7 +131,7 @@ while : ; do reals_opt=yes reals=all;; -src|--src) src_spec=yes - COQTOP="$2" + COQSRC="$2" shift;; -bindir|--bindir) bindir_spec=yes bindir="$2" @@ -149,6 +154,12 @@ while : ; do -camldir|--camldir) camldir_spec=yes camldir="$2" shift;; + -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes + lablgtkdir="$2" + shift;; + -camlp5dir|--camlp5dir) + camlp5dir="$2" + shift;; -arch|--arch) arch_spec=yes arch=$2 shift;; @@ -229,6 +240,8 @@ case $arch_spec in # cygwin returns a name of the form /cygdrive/c/... # that coqc does not understand; need to transform it COQTOP=`echo $COQTOP | sed -e "s#.*cygdrive.\(.\)#\1:#"` + elif test -x /bin/uname ; then + ARCH=`/bin/uname -s` elif test -x /usr/bin/uname ; then ARCH=`/usr/bin/uname -s` else @@ -274,7 +287,7 @@ fi case $camldir_spec in no) CAMLC=`which $bytecamlc` case "$CAMLC" in - "") echo "$bytecamlc is not present in your path !" + "") echo "$bytecamlc is not present in your path!" echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: " read CAMLC @@ -306,6 +319,11 @@ if test ! -f "$CAMLC" ; then exit 1 fi +# Under Windows, OCaml only understands Windows filenames (C:\...) +case $ARCH in + win32) CAMLBIN=`cygpath -w ${CAMLBIN}`;; +esac + # this fixes a camlp4 bug under FreeBSD # ("native-code program cannot do a dynamic load") if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi @@ -313,24 +331,28 @@ if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi CAMLVERSION=`"$bytecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` case $CAMLVERSION in - 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.08.0) + 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.08.0) echo "Your version of Objective-Caml is $CAMLVERSION." if [ "$CAMLVERSION" = "3.08.0" ] ; then - echo "You need Objective-Caml 3.06 or later (to the exception of 3.08.0)!" + echo "You need Objective-Caml 3.07 or later (to the exception of 3.08.0)!" else - echo "You need Objective-Caml 3.06 or later!" + echo "You need Objective-Caml 3.07 or later!" fi echo "Configuration script failed!" exit 1;; - 3.06|3.07*|3.08*) - echo "You have Objective-Caml $CAMLVERSION. Good!" - coq_inline_flag="-inline 0";; + 3.07*) + cflags="$cflags -DOCAML_307" + coq_inline_flag="-inline 0" + echo "You have Objective-Caml $CAMLVERSION. Good!";; + 3.08*) + coq_inline_flag="-inline 0" + echo "You have Objective-Caml $CAMLVERSION. Good!";; ?*) CAMLP4COMPAT="-loc loc" echo "You have Objective-Caml $CAMLVERSION. Good!";; *) echo "I found the Objective-Caml compiler but cannot find its version number!" - echo "Is it installed properly ?" + echo "Is it installed properly?" echo "Configuration script failed!" exit 1;; esac @@ -342,11 +364,19 @@ CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"` if [ "$best_compiler" = "opt" ] ; then if test -e `which "$nativecamlc"` ; then CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` - if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then - echo "native and bytecode compilers do not have the same version!"; fi + if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then + case $CAMLOPTVERSION in + 3.09.3|3.1?*) ;; + *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3," + best_compiler=byte + echo "only the bytecode version of Coq will be available." + esac + elif [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then + echo "Native and bytecode compilers do not have the same version!"; + fi echo "You have native-code compilation. Good!" else - best_compiler=byte ; + best_compiler=byte echo "You have only bytecode compilation." fi fi @@ -354,19 +384,54 @@ fi # For coqmktop & bytecode compiler -CAMLLIB=`"$CAMLC" -where` +case $ARCH in + win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB + CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;; + *) + CAMLLIB=`"$CAMLC" -where` + esac + + +# Camlp4 / Camlp5 configuration +# Very basic for the moment: if camlp5 exists, we use it... + +if [ "$camlp5dir" != "" ]; then + CAMLP4=camlp5 + CAMLP4LIB=$camlp5dir + camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` +elif [ "$CAMLTAG" = "OCAML310" ]; then + if [ -x "${CAMLLIB}/camlp5" ]; then + CAMLP4LIB=+camlp5 + elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then + CAMLP4LIB=+site-lib/camlp5 + else + echo "Objective Caml 3.10 found but no Camlp5 installed." + echo "Configuration script failed!" + exit 1 + fi + CAMLP4=camlp5 + camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` +else + CAMLP4=camlp4 + CAMLP4LIB=+camlp4 +fi + +if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then + echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK." + echo "Configuration script failed!" + exit 1 +fi + -# Camlp4 (greatly simplified since merged with ocaml) +case $CAMLP4LIB in + +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;; + *) FULLCAMLP4LIB=$CAMLP4LIB;; +esac +# Assume that camlp(4|5) binaries are at the same place as ocaml ones +# (this should become configurable some day) CAMLP4BIN=${CAMLBIN} -#case $OS in -# Win32) - CAMLP4LIB=+camlp4 -# ;; -# *) -# CAMLP4LIB=${CAMLLIB}/camlp4 -#esac # OS dependent libraries @@ -380,7 +445,8 @@ case $ARCH in esac;; alpha) OSDEPLIBS="-cclib -lunix";; win32) OS="Win32" - OSDEPLIBS="-cclib -lunix";; + OSDEPLIBS="-cclib -lunix" + cflags="-mno-cygwin $cflags";; *) OSDEPLIBS="-cclib -lunix" esac @@ -396,24 +462,50 @@ fi # Which coqide is asked ? which one is possible ? if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then - echo "CoqIde disabled as requested" -elif [ ! -x "${CAMLLIB}/lablgtk2" ]; then - echo "LablGtk2 not found: CoqIde will not be available" - COQIDE=no -elif [ -z "`grep -w convert_with_fallback ${CAMLLIB}/lablgtk2/glib.mli`" ]; then - echo "LablGtk2 found but too old: CoqIde will not be available" - COQIDE=no; -elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then - echo "LablGtk2 found, bytecode CoqIde will be used as requested" - COQIDE=byte -elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then - echo "LablGtk2 found, no native threads: bytecode CoqIde will be available" - COQIDE=byte -else - echo "LablGtk2 found, native threads: native CoqIde will be available" - COQIDE=opt + echo "CoqIde disabled as requested." +else + case $lablgtkdir_spec in + no) + if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then + lablgtkdir=${CAMLLIB}/lablgtk2 + elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then + lablgtkdir=${CAMLLIB}/site-lib/lablgtk2 + fi;; + yes) + if [ ! -f "$lablgtkdir/glib.mli" ]; then + echo "Incorrect LablGtk2 library (glib.mli not found)." + echo "Configuration script failed!" + exit 1 + fi;; + esac + if [ "$lablgtkdir" = "" ]; then + echo "LablGtk2 not found: CoqIde will not be available." + COQIDE=no + elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then + echo "LablGtk2 found but too old: CoqIde will not be available." + COQIDE=no; + elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then + echo "LablGtk2 found, bytecode CoqIde will be used as requested." + COQIDE=byte + elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then + echo "LablGtk2 found, no native threads: bytecode CoqIde will be available." + COQIDE=byte + else + echo "LablGtk2 found, native threads: native CoqIde will be available." + COQIDE=opt + fi fi +case $COQIDE in + byte|opt) + case $lablgtkdir_spec in + no) LABLGTKLIB=+lablgtk2 # Pour le message + LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile + yes) LABLGTKLIB="$lablgtkdir" # Pour le message + LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile + esac;; + no) LABLGTKINCLUDES="";; +esac # Tell on windows if ocaml understands cygwin or windows path formats @@ -442,14 +534,13 @@ esac ########################################### # bindir, libdir, mandir, etc. -canonical_pwd () { -ocaml 2>&1 1>/dev/null <<EOF - prerr_endline(Sys.getcwd());; -EOF -} - case $src_spec in - no) COQTOP=`canonical_pwd` + no) COQTOP=${COQSRC} +esac + +# OCaml only understand Windows filenames (C:\...) +case $ARCH in + win32) COQTOP=`cygpath -w ${COQTOP}` esac case $ARCH in @@ -578,6 +669,9 @@ echo " Objective-Caml/Camlp4 version : $CAMLVERSION" echo " Objective-Caml/Camlp4 binaries in : $CAMLBIN" echo " Objective-Caml library in : $CAMLLIB" echo " Camlp4 library in : $CAMLP4LIB" +if test "$COQIDE" != "no"; then +echo " Lablgtk2 library in : $LABLGTKLIB" +fi if test "$fsets" = "all"; then echo " FSets theory : All" else @@ -609,13 +703,35 @@ escape_var () { EOF } -export COQTOP BINDIR LIBDIR CAMLBIN CAMLLIB -ESCCOQTOP="`VAR=COQTOP escape_var`" -ESCBINDIR="`VAR=BINDIR escape_var`" -ESCLIBDIR="`VAR=LIBDIR escape_var`" -ESCCAMLDIR="`VAR=CAMLBIN escape_var`" -ESCCAMLLIB="`VAR=CAMLLIB escape_var`" -ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4 +# damned backslashes under M$Windows +case $ARCH in + win32) + ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'` + ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` + ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` + ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'` + ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'` + ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` + ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` + ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'` + ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'` + ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'` + ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'` + ;; + *) + ESCCOQTOP="$COQTOP" + ESCBINDIR="$BINDIR" + ESCLIBDIR="$LIBDIR" + ESCCAMLDIR="$CAMLBIN" + ESCCAMLLIB="$CAMLLIB" + ESCMANDIR="$MANDIR" + ESCEMACSLIB="$EMACSLIB" + ESCCOQDOCDIR="$COQDOCDIR" + ESCCAMLP4BIN="$CAMLP4BIN" + ESCCAMLP4LIB="$CAMLP4LIB" + ESCLABLGTKINCLUDES="$LABLGTKINCLUDES" + ;; +esac mlconfig_file="$COQSRC/config/coq_config.ml" rm -f $mlconfig_file @@ -628,6 +744,7 @@ let coqlib = "$ESCLIBDIR" let coqtop = "$ESCCOQTOP" let camldir = "$ESCCAMLDIR" let camllib = "$ESCCAMLLIB" +let camlp4 = "$CAMLP4" let camlp4lib = "$ESCCAMLP4LIB" let best = "$best_compiler" let arch = "$ARCH" @@ -666,29 +783,8 @@ chmod a-w "$mlconfig_file" rm -f "$COQSRC/config/Makefile" -# damned backslashes under M$Windows (bis) -case $ARCH in - win32) - ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'` - ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'` - ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'` - ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'` - ;; - *) - ESCCOQTOP="$COQTOP" - ESCBINDIR="$BINDIR" - ESCLIBDIR="$LIBDIR" - ESCMANDIR="$MANDIR" - ESCEMACSLIB="$EMACSLIB" - ESCCOQDOCDIR="$COQDOCDIR" - ESCCAMLP4BIN="$CAMLP4BIN" ;; -esac - sed -e "s|LOCALINSTALLATION|$local|" \ - -e "s|COQTOPDIRECTORY|$ESCCOQTOP|" \ + -e "s|COQSRCDIRECTORY|$COQSRC|" \ -e "s|COQVERSION|$VERSION|" \ -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \ -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \ @@ -706,10 +802,12 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ -e "s|CAMLP4TOOL|$camlp4oexec|" \ -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \ + -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ -e "s|COQINLINEFLAG|$coq_inline_flag|" \ -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \ + -e "s|CCOMPILEFLAGS|$cflags|" \ -e "s|BESTCOMPILER|$best_compiler|" \ -e "s|EXECUTEEXTENSION|$EXE|" \ -e "s|BYTECAMLC|$bytecamlc|" \ @@ -735,19 +833,14 @@ chmod a-w "$COQSRC/config/Makefile" # Building the $COQTOP/dev/ocamldebug-coq file ################################################## -OCAMLDEBUGCOQ=$COQTOP/dev/ocamldebug-coq +OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq if test "$coq_debug_flag" = "-g" ; then rm -f $OCAMLDEBUGCOQ - if [ "$CAMLP4LIB" = "+camlp4" ] ; then - CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4 - else - CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB - fi sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ -e "s|COQLIBDIRECTORY|$LIBDIR|" \ -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ - -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIBFORCAMLDEBUG|" \ + -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\ $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ chmod a-w,a+x $OCAMLDEBUGCOQ fi @@ -757,7 +850,7 @@ fi #################################################### if [ ! "$COQIDE" = "no" ]; then - if grep "class view " "$CAMLLIB/lablgtk2/gText.mli" | grep -q "\[>" ; then + if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli else cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli @@ -773,4 +866,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 10039 2007-07-20 22:04:33Z notin $ +# $Id: configure 10215 2007-10-11 13:13:51Z herbelin $ diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index 86251254..dc0dec0e 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *) +(* $Id: cctac.ml 10121 2007-09-14 09:45:40Z corbinea $ *) (* This file is the interface between the c-c algorithm and Coq *) @@ -199,7 +199,7 @@ let build_projection intype outtype (cstr:constructor) special default gls= let ind=destInd h in let types=Inductiveops.arities_of_constructors env ind in let lp=Array.length types in - let ci=(snd cstr)-1 in + let ci=pred (snd cstr) in let branch i= let ti=Term.prod_appvect types.(i) argv in let rc=fst (Sign.decompose_prod_assum ti) in @@ -247,7 +247,7 @@ let rec proof_tac p gls = and tx2=constr_of_term p2.p_rhs in let typf = pf_type_of gls tf1 in let typx = pf_type_of gls tx1 in - let typfx = prod_applist typf [tx1] in + let typfx = pf_type_of gls (mkApp (tf1,[|tx1|])) in let id = pf_get_new_id (id_of_string "f") gls in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli index 97fa4d77..ffc4b9c4 100644 --- a/contrib/cc/cctac.mli +++ b/contrib/cc/cctac.mli @@ -6,11 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cctac.mli 9151 2006-09-19 13:32:22Z corbinea $ *) +(* $Id: cctac.mli 10121 2007-09-14 09:45:40Z corbinea $ *) open Term open Proof_type +val proof_tac: Ccproof.proof -> Proof_type.tactic + val cc_tactic : int -> constr list -> tactic val cc_fail : tactic diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index e31b701c..825b3554 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.ml 9486 2007-01-15 19:11:28Z letouzey $ i*) +(*i $Id: extract_env.ml 10209 2007-10-09 21:49:37Z letouzey $ i*) open Term open Declarations @@ -92,7 +92,8 @@ module Visit : VISIT = struct let needed_kn kn = KNset.mem kn v.kn let needed_con c = Cset.mem c v.con let needed_mp mp = MPset.mem mp v.mp - let add_mp mp = v.mp <- MPset.union (prefixes_mp mp) v.mp + let add_mp mp = + check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c) let add_ref = function diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 6fd4a3cc..6982ffc6 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml 9456 2006-12-17 20:08:38Z letouzey $ i*) +(*i $Id: extraction.ml 10195 2007-10-08 01:47:55Z letouzey $ i*) (*i*) open Util @@ -31,10 +31,6 @@ open Mlutil exception I of inductive_info -(* A set of all inductive currently being computed, - to avoid loops in [extract_inductive] *) -let internal_call = ref KNset.empty - (* A set of all fixpoint functions currently being extracted *) let current_fixpoints = ref ([] : constant list) @@ -303,13 +299,15 @@ and extract_type_scheme env db c p = (*S Extraction of an inductive type. *) and extract_ind env kn = (* kn is supposed to be in long form *) - try - if KNset.mem kn !internal_call then lookup_ind kn (* Already started. *) - else if visible_kn kn then lookup_ind kn (* Standard situation. *) - else raise Not_found (* Never trust the table for a internal kn. *) + let mib = Environ.lookup_mind kn env in + try + (* For a same kn, we can get various bodies due to module substitutions. + We hence check that the mib has not changed from recording + time to retrieving time. Ideally we should also check the env. *) + let (mib0,ml_ind) = lookup_ind kn in + if not (mib = mib0) then raise Not_found; + ml_ind with Not_found -> - internal_call := KNset.add kn !internal_call; - let mib = Environ.lookup_mind kn env in (* First, if this inductive is aliased via a Module, *) (* we process the original inductive. *) option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; @@ -335,7 +333,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ip_types = t }) mib.mind_packets in - add_ind kn + add_ind kn mib {ind_info = Standard; ind_nparams = npar; ind_packets = packets; @@ -425,8 +423,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ind_packets = packets; ind_equiv = mib.mind_equiv} in - add_ind kn i; - internal_call := KNset.remove kn !internal_call; + add_ind kn mib i; i (*s [extract_type_cons] extracts the type of an inductive diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index b1a3cb31..6d39faee 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml 9310 2006-10-28 19:35:09Z herbelin $ i*) +(*i $Id: table.ml 10209 2007-10-09 21:49:37Z letouzey $ i*) open Names open Term @@ -60,7 +60,6 @@ let at_toplevel mp = let visible_kn kn = at_toplevel (base_mp (modpath kn)) let visible_con kn = at_toplevel (base_mp (con_modpath kn)) - (*S The main tables: constants, inductives, records, ... *) (*s Constants tables. *) @@ -77,9 +76,9 @@ let lookup_type kn = Cmap.find kn !types (*s Inductives table. *) -let inductives = ref (KNmap.empty : ml_ind KNmap.t) +let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t) let init_inductives () = inductives := KNmap.empty -let add_ind kn m = inductives := KNmap.add kn m !inductives +let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives let lookup_ind kn = KNmap.find kn !inductives (*s Recursors table. *) @@ -124,11 +123,24 @@ let reset_tables () = let id_of_global = function | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l - | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename - | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) + | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename + | ConstructRef ((kn,i),j) -> + (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) | _ -> assert false -let pr_global r = pr_id (id_of_global r) +let pr_global r = + try Printer.pr_global r + with _ -> pr_id (id_of_global r) + +(* idem, but with qualification, and only for constants. *) + +let pr_long_global r = + try Printer.pr_global r + with _ -> match r with + | ConstRef kn -> + let mp,_,l = repr_con kn in + str ((string_of_mp mp)^"."^(string_of_label l)) + | _ -> assert false (*S Warning and Error messages. *) @@ -150,13 +162,13 @@ let warning_log_ax r = spc () ++ str "may lead to incorrect or non-terminating ML terms.") let check_inside_module () = - try - ignore (Lib.what_is_opened ()); - Options.if_verbose warning - ("Extraction inside an opened module is experimental.\n"^ - "In case of problem, close it first.\n"); - Pp.flush_all () - with Not_found -> () + if Lib.is_modtype () then + err (str "You can't do that within a Module Type." ++ fnl () ++ + str "Close it and try again.") + else if Lib.is_module () then + msg_warning + (str "Extraction inside an opened module is experimental.\n" ++ + str "In case of problem, close it first.\n") let check_inside_section () = if Lib.sections_are_opened () then @@ -164,10 +176,10 @@ let check_inside_section () = str "Close it and try again.") let error_constant r = - err (Printer.pr_global r ++ str " is not a constant.") + err (pr_global r ++ str " is not a constant.") let error_inductive r = - err (Printer.pr_global r ++ spc () ++ str "is not an inductive type.") + err (pr_global r ++ spc () ++ str "is not an inductive type.") let error_nb_cons () = err (str "Not the right number of constructors.") @@ -187,23 +199,23 @@ let error_scheme () = err (str "No Scheme modular extraction available yet.") let error_not_visible r = - err (Printer.pr_global r ++ str " is not directly visible.\n" ++ + err (pr_global r ++ str " is not directly visible.\n" ++ str "For example, it may be inside an applied functor." ++ str "Use Recursive Extraction to get the whole environment.") -let error_unqualified_name s1 s2 = - err (str (s1 ^ " is used in " ^ s2 ^ " where it cannot be disambiguated\n" ^ - "in ML from another name sharing the same basename.\n" ^ - "Please do some renaming.\n")) - let error_MPfile_as_mod d = err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^ "Extraction cannot currently deal with this situation.\n")) let error_record r = - err (str "Record " ++ Printer.pr_global r ++ str " has an anonymous field." ++ fnl () ++ + err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++ str "To help extraction, please use an explicit name.") +let check_loaded_modfile mp = match base_mp mp with + | MPfile dp -> if not (Library.library_is_loaded dp) then + err (str ("Please load library "^(string_of_dirpath dp^" first."))) + | _ -> () + (*S The Extraction auxiliary commands *) (*s Extraction AutoInline *) @@ -310,7 +322,7 @@ let _ = declare_summary "Extraction Lang" { freeze_function = (fun () -> !lang_ref); unfreeze_function = ((:=) lang_ref); init_function = (fun () -> lang_ref := Ocaml); - survive_module = false; + survive_module = true; survive_section = true } let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) @@ -342,28 +354,21 @@ let (inline_extraction,_) = load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); export_function = (fun x -> Some x); classify_function = (fun (_,o) -> Substitute o); - (*CSC: The following substitution may istantiate a realized parameter. - The right solution would be to make the substitution erase the - realizer from the table. However, this is not allowed by Coq. - In this particular case, though, keeping the realizer is place seems - to be harmless since the current code looks for a realizer only - when the constant is a parameter. However, if this behaviour changes - subtle bugs can happear in the future. *) subst_function = - (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))} + (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) + } let _ = declare_summary "Extraction Inline" { freeze_function = (fun () -> !inline_table); unfreeze_function = ((:=) inline_table); init_function = (fun () -> inline_table := empty_inline_table); - survive_module = false; + survive_module = true; survive_section = true } (* Grammar entries. *) let extraction_inline b l = check_inside_section (); - check_inside_module (); let refs = List.map Nametab.global l in List.iter (fun r -> match r with @@ -380,11 +385,11 @@ let print_extraction_inline () = (str "Extraction Inline:" ++ fnl () ++ Refset.fold (fun r p -> - (p ++ str " " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++ + (p ++ str " " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++ str "Extraction NoInline:" ++ fnl () ++ Refset.fold (fun r p -> - (p ++ str " " ++ Printer.pr_global r ++ fnl ())) n (mt ())) + (p ++ str " " ++ pr_long_global r ++ fnl ())) n (mt ())) (* Reset part *) @@ -423,20 +428,23 @@ let (in_customs,_) = {(default_object "ML extractions") with cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); - export_function = (fun x -> Some x)} + export_function = (fun x -> Some x); + classify_function = (fun (_,o) -> Substitute o); + subst_function = + (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) + } let _ = declare_summary "ML extractions" { freeze_function = (fun () -> !customs); unfreeze_function = ((:=) customs); init_function = (fun () -> customs := Refmap.empty); - survive_module = false; + survive_module = true; survive_section = true } (* Grammar entries. *) let extract_constant_inline inline r ids s = check_inside_section (); - check_inside_module (); let g = Nametab.global r in match g with | ConstRef kn -> @@ -455,7 +463,6 @@ let extract_constant_inline inline r ids s = let extract_inductive r (s,l) = check_inside_section (); - check_inside_module (); let g = Nametab.global r in match g with | IndRef ((kn,i) as ip) -> diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 66662138..c9a4e8da 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli 6441 2004-12-09 02:27:09Z letouzey $ i*) +(*i $Id: table.mli 10209 2007-10-09 21:49:37Z letouzey $ i*) open Names open Libnames open Miniml +open Declarations val id_of_global : global_reference -> identifier @@ -27,11 +28,11 @@ val error_unknown_module : qualid -> 'a val error_toplevel : unit -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a -val error_unqualified_name : string -> string -> 'a val error_MPfile_as_mod : dir_path -> 'a val error_record : global_reference -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit +val check_loaded_modfile : module_path -> unit (*s utilities concerning [module_path]. *) @@ -55,8 +56,8 @@ val lookup_term : constant -> ml_decl val add_type : constant -> ml_schema -> unit val lookup_type : constant -> ml_schema -val add_ind : kernel_name -> ml_ind -> unit -val lookup_ind : kernel_name -> ml_ind +val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit +val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index b55c5443..d8bb9eae 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -152,8 +152,15 @@ Ltac ParseRingComponents lemma := (* ring tactics *) +Ltac relation_carrier req := + let ty := type of req in + match eval hnf in ty with + ?R -> _ => R + | _ => fail 1000 "Equality has no relation type" + end. + Ltac FV_hypo_tac mkFV req lH := - let R := match type of req with ?R -> _ => R end in + let R := relation_carrier req in let FV_hypo_l_tac h := match h with @mkhypo (req ?pe _) _ => mkFV pe end in let FV_hypo_r_tac h := diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index f963fc9c..134ba1a8 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: newring.ml4 9968 2007-07-11 15:49:07Z barras $ i*) +(*i $Id: newring.ml4 10047 2007-07-24 17:55:18Z barras $ i*) open Pp open Util @@ -465,7 +465,8 @@ let op_smorph r add mul req m1 m2 = let default_ring_equality (r,add,mul,opp,req) = let is_setoid = function - {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true + {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> + eq_constr req rel (* Qu: use conversion ? *) | _ -> false in match default_relation_for_carrier ~filter:is_setoid r with Leibniz _ -> @@ -625,6 +626,7 @@ let interp_sign env sign = (* Same remark on ill-typed terms ... *) let add_theory name rth eqth morphth cst_tac (pre,post) power sign = + check_required_library (cdir@["Ring_base"]); let env = Global.env() in let sigma = Evd.empty in let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in @@ -986,6 +988,7 @@ let default_field_equality r inv req = inv_m.lem let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign = + check_required_library (cdir@["Field_tac"]); let env = Global.env() in let sigma = Evd.empty in let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 44680d6d..2d1c6289 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -7,7 +7,11 @@ export COQLIB=COQLIBDIRECTORY export COQTH=$COQLIB/theories CAMLBIN=CAMLBINDIRECTORY OCAMLDEBUG=$CAMLBIN/ocamldebug -export CAMLP4LIB=`$CAMLBIN/camlp4 -where` +if [ -x "$CAMLBIN/camlp5" ]; then + export CAMLP4LIB=`$CAMLBIN/camlp5 -where` +else + export CAMLP4LIB=`$CAMLBIN/camlp4 -where` +fi exec $OCAMLDEBUG \ -I $CAMLP4LIB \ diff --git a/doc/Makefile b/doc/Makefile index 403e2047..5158fbeb 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -1,6 +1,6 @@ # Makefile for the Coq documentation -# COQTOP needs to be set to a coq source repository +# COQSRC needs to be set to a coq source repository # To compile documentation, you need the following tools: # Dvi: latex (latex2e), bibtex, makeindex @@ -18,9 +18,9 @@ PDFLATEX=pdflatex HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea TEXINPUTS=$(HEVEALIB):.: -DOCCOQTOP=$(COQTOP)/bin/coqtop -COQTEX=$(COQTOP)/bin/coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small -COQDOC=$(COQTOP)/bin/coqdoc +COQTOP=$(COQSRC)/bin/coqtop +COQTEX=$(COQSRC)/bin/coq-tex -n 72 -image $(COQTOP) -v -sl -small +COQDOC=$(COQSRC)/bin/coqdoc #VERSION=POSITIONNEZ-CETTE-VARIABLE @@ -76,7 +76,7 @@ rectutorial:\ clean: rm -f */*.dvi */*.aux */*.log */*.bbl */*.blg */*.toc \ */*.idx */*~ */*.ilg */*.ind */*.dvi.gz */*.ps.gz */*.pdf.gz\ - */*.???idx */*.???ind */*.v.tex */*.atoc */*.lof\ + */*.???idx */*.???ind */*.v.tex */*.atoc */*.lof \ */*.hatoc */*.haux */*.hcomind */*.herrind */*.hidx */*.hind \ */*.htacind */*.htoc */*.v.html rm -f stdlib/index-list.html stdlib/index-body.html \ @@ -211,7 +211,7 @@ faq/html/index.html: faq/FAQ.v.html # Standard library ###################################################################### -GLOBDUMP=$(COQTOP)/glob.dump +GLOBDUMP=$(COQSRC)/glob.dump LIBDIRS= Logic Bool Arith ZArith QArith Reals Lists Sets Relations Sorting Wellfounded IntMap FSets @@ -222,11 +222,11 @@ stdlib/index-body.html: $(GLOBDUMP) mkdir stdlib/html (cd stdlib/html;\ $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\ - -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v) + -R $(COQSRC)/theories Coq $(COQSRC)/theories/*/*.v) mv stdlib/html/index.html stdlib/index-body.html stdlib/index-list.html: stdlib/index-list.html.template - COQTOP=$(COQTOP) ./stdlib/make-library-index stdlib/index-list.html + COQTOP=$(COQSRC) ./stdlib/make-library-index stdlib/index-list.html stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/index-trailer.html cat stdlib/index-list.html > $@ @@ -238,8 +238,8 @@ stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/ind stdlib/Library.coqdoc.tex: (for dir in $(LIBDIRS) ; do \ $(COQDOC) -q --gallina --body-only --latex --stdout \ - --coqlib_path $(COQTOP) \ - -R $(COQTOP)/theories Coq "$(COQTOP)/theories/$$dir/"*.v >> $@ ; done) + --coqlib_path $(COQSRC) \ + -R $(COQSRC)/theories Coq "$(COQSRC)/theories/$$dir/"*.v >> $@ ; done) stdlib/Library.dvi: $(COMMON) stdlib/Library.coqdoc.tex stdlib/Library.tex (cd stdlib;\ @@ -282,8 +282,8 @@ install-doc: install-meta install-doc-html install-doc-printable install-meta: mkdir $(DOCDIC) cp LICENCE $(DOCDIC)/LICENCE.doc -# cp $(COQTOP)/LICENCE $(COQTOP)/CREDITS $(COQTOP)/COPYRIGHT $(DOCDIC) -# cp $(COQTOP)/README $(COQTOP)/CHANGES $(DOCDIC) +# cp $(COQSRC)/LICENCE $(COQSRC)/CREDITS $(COQSRC)/COPYRIGHT $(DOCDIC) +# cp $(COQSRC)/README $(COQSRC)/CHANGES $(DOCDIC) install-doc-html: all-html mkdir $(HTMLINSTALLDIR) diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 768d125c..937098b7 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command_windows.ml 9189 2006-09-29 12:39:24Z notin $ *) +(* $Id: command_windows.ml 10197 2007-10-08 13:52:35Z notin $ *) class command_window () = let window = GWindow.window @@ -69,9 +69,10 @@ object(self) val notebook = notebook method window = window method new_command ?command ?term () = + let appendp x = ignore (notebook#append_page x) in let frame = GBin.frame ~shadow_type:`ETCHED_OUT - ~packing:notebook#append_page + ~packing:appendp () in notebook#goto_page (notebook#page_num frame#coerce); @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 9537 2007-01-26 10:05:04Z corbinea $ *) +(* $Id: coq.ml 10174 2007-10-04 13:52:23Z vsiles $ *) open Vernac open Vernacexpr @@ -152,6 +152,7 @@ let interp verbosely s = | VernacFixpoint _ | VernacCoFixpoint _ | VernacEndProof _ + | VernacScheme _ -> Options.make_silent (not verbosely) | _ -> () end; diff --git a/ide/coqide.ml b/ide/coqide.ml index fb650cbf..fdc344e8 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 9307 2006-10-28 18:48:48Z herbelin $ *) +(* $Id: coqide.ml 10220 2007-10-12 13:25:54Z notin $ *) open Preferences open Vernacexpr @@ -1719,9 +1719,10 @@ let create_input_tab filename = let v_box = GPack.hbox ~homogeneous:false () in let _ = GMisc.image ~packing:v_box#pack () in let _ = GMisc.label ~text:filename ~packing:v_box#pack () in + let appendp x = ignore ((notebook ())#append_page + ~tab_label:v_box#coerce x) in let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT - ~packing:((notebook ())#append_page - ~tab_label:v_box#coerce) () + ~packing:appendp () in let sw1 = GBin.scrolled_window ~vpolicy:`AUTOMATIC @@ -2035,8 +2036,8 @@ let main files = !flash_info "Cannot print: this buffer has no name" | Some f -> let cmd = - "cd " ^ Filename.dirname f ^ "; " ^ - !current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^ + "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ + !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^ " | " ^ !current.cmd_print in let s,_ = run_command av#insert_message cmd in @@ -2063,8 +2064,8 @@ let main files = | _ -> assert false in let cmd = - "cd " ^ Filename.dirname f ^ "; " ^ - !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef + "cd " ^ (Filename.quote (Filename.dirname f)) ^ "; " ^ + !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) in let s,_ = run_command av#insert_message cmd in !flash_info (cmd ^ @@ -2411,7 +2412,7 @@ let main files = | Some f -> save_f (); let l,r = !current.cmd_editor in - let _ = run_command av#insert_message (l ^ f ^ r) in + let _ = run_command av#insert_message (l ^ (Filename.quote f) ^ r) in av#revert) in let _ = edit_f#add_separator () in @@ -2857,7 +2858,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); | Some f -> let s,res = run_command av#insert_message - (!current.cmd_coqc ^ " " ^ f) + (!current.cmd_coqc ^ " " ^ (Filename.quote f)) in if s = Unix.WEXITED 0 then !flash_info (f ^ " successfully compiled") @@ -2877,11 +2878,17 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let make_f () = let v = get_active_view () in let av = out_some v.analyzed_view in + match av#filename with + | None -> + !flash_info "Cannot print: this buffer has no name" + | Some f -> + let cmd = + "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in (* save_f (); *) av#insert_message "Command output:\n"; - let s,res = run_command av#insert_message !current.cmd_make in + let s,res = run_command av#insert_message cmd in last_make := res; last_make_index := 0; !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") @@ -2937,9 +2944,15 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let coq_makefile_f () = let v = get_active_view () in let av = out_some v.analyzed_view in - let s,res = run_command av#insert_message !current.cmd_coqmakefile in - !flash_info - (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") + match av#filename with + | None -> + !flash_info "Cannot make makefile: this buffer has no name" + | Some f -> + let cmd = + "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in + let s,res = run_command av#insert_message cmd in + !flash_info + (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f in @@ -3313,7 +3326,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); \nContributors : Jean-Christophe Filliâtre\ \n Pierre Letouzey, Claude Marché\n\ \nFeature wish or bug report: use Web interface\n\ - \n\thttp://coq.inria.fr/bin/coq-bugs\n\ + \n\thttp://logical.futurs.inria.fr/coq-bugs\n\ \nVersion information\ \n-------------------\n" in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 349e8629..b9d7694f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrextern.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: constrextern.ml 10135 2007-09-21 14:28:12Z herbelin $ *) (*i*) open Pp @@ -923,6 +923,8 @@ let rec raw_of_pat env = function | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) -> let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b) + | PCase (_,PMeta None,tm,[||]) -> + RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[]) | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) -> let brs = Array.to_list (Array.map (raw_of_pat env) bv) in let brns = Array.to_list cstr_nargs in diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 79a217a1..0c3ffd0c 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqlib.ml 8866 2006-05-28 16:21:04Z herbelin $ *) +(* $Id: coqlib.ml 10067 2007-08-09 17:13:16Z msozeau $ *) open Util open Pp @@ -236,6 +236,7 @@ let coq_I = lazy_init_constant ["Logic"] "I" (* Connectives *) let coq_not = lazy_init_constant ["Logic"] "not" let coq_and = lazy_init_constant ["Logic"] "and" +let coq_conj = lazy_init_constant ["Logic"] "conj" let coq_or = lazy_init_constant ["Logic"] "or" let coq_ex = lazy_init_constant ["Logic"] "ex" @@ -246,6 +247,7 @@ let build_coq_I () = Lazy.force coq_I let build_coq_False () = Lazy.force coq_False let build_coq_not () = Lazy.force coq_not let build_coq_and () = Lazy.force coq_and +let build_coq_conj () = Lazy.force coq_conj let build_coq_or () = Lazy.force coq_or let build_coq_ex () = Lazy.force coq_ex diff --git a/interp/coqlib.mli b/interp/coqlib.mli index c81d72de..7254800c 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqlib.mli 8688 2006-04-07 15:08:12Z msozeau $ i*) +(*i $Id: coqlib.mli 10067 2007-08-09 17:13:16Z msozeau $ i*) (*i*) open Names @@ -129,6 +129,7 @@ val build_coq_not : constr delayed (* Conjunction *) val build_coq_and : constr delayed +val build_coq_conj : constr delayed (* Disjunction *) val build_coq_or : constr delayed diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 2f17d659..00901686 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductive.ml 9421 2006-12-08 16:00:53Z barras $ *) +(* $Id: inductive.ml 10173 2007-10-04 13:02:56Z herbelin $ *) open Util open Names @@ -656,21 +656,32 @@ let check_one_fix renv recpos def = let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in match kind_of_term f with | Rel p -> - List.iter (check_rec_call renv) l; (* Test if [p] is a fixpoint (recursive call) *) if renv.rel_min <= p & p < renv.rel_min+nfi then - (* the position of the invoked fixpoint: *) - let glob = renv.rel_min+nfi-1-p in - (* the decreasing arg of the rec call: *) - let np = recpos.(glob) in - if List.length l <= np then error_partial_apply renv glob - else - (match list_chop np l with - (la,(z::lrest)) -> - (* Check the decreasing arg is smaller *) - if not (check_is_subterm renv z) then - error_illegal_rec_call renv glob z - | _ -> assert false) + begin + List.iter (check_rec_call renv) l; + (* the position of the invoked fixpoint: *) + let glob = renv.rel_min+nfi-1-p in + (* the decreasing arg of the rec call: *) + let np = recpos.(glob) in + if List.length l <= np then error_partial_apply renv glob + else + match list_chop np l with + (la,(z::lrest)) -> + (* Check the decreasing arg is smaller *) + if not (check_is_subterm renv z) then + error_illegal_rec_call renv glob z + | _ -> assert false + end + else + begin + match pi2 (lookup_rel p renv.env) with + | None -> + List.iter (check_rec_call renv) l + | Some c -> + try List.iter (check_rec_call renv) l + with FixGuardError _ -> check_rec_call renv (applist(c,l)) + end | Case (ci,p,c_0,lrest) -> List.iter (check_rec_call renv) (c_0::p::l); @@ -736,9 +747,19 @@ let check_one_fix renv recpos def = let renv' = push_fix_renv renv recdef in Array.iter (check_rec_call renv') bodies - | (Ind _ | Construct _ | Var _ | Sort _) -> + | (Ind _ | Construct _ | Sort _) -> List.iter (check_rec_call renv) l + | Var id -> + begin + match pi2 (lookup_named id renv.env) with + | None -> + List.iter (check_rec_call renv) l + | Some c -> + try List.iter (check_rec_call renv) l + with (FixGuardError _) -> check_rec_call renv (applist(c,l)) + end + (* l is not checked because it is considered as the meta's context *) | (Evar _ | Meta _) -> () diff --git a/lib/compat.ml4 b/lib/compat.ml4 index 7ea3ff66..372d2be3 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -8,10 +8,24 @@ (* Compatibility file depending on ocaml version *) -(* IFDEF not available in 3.06; use ifdef instead *) - (* type loc is different in 3.08 *) -ifdef OCAML_308 then + +IFDEF OCAML309 THEN DEFINE OCAML308 END + +IFDEF CAMLP5 THEN +module M = struct +type loc = Stdpp.location +let dummy_loc = Stdpp.dummy_loc +let make_loc = Stdpp.make_loc +let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc +let join_loc loc1 loc2 = + if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc + else Stdpp.encl_loc loc1 loc2 +type token = string*string +type lexer = token Token.glexer +let using l x = l.Token.tok_using x +end +ELSE IFDEF OCAML308 THEN module M = struct type loc = Token.flocation let dummy_loc = Token.dummy_loc @@ -24,16 +38,34 @@ let unloc (b,e) = assert (dummy_loc = (b,e) or make_loc loc = (b,e)); *) loc +let join_loc loc1 loc2 = + if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc + else (fst loc1, snd loc2) +type token = Token.t +type lexer = Token.lexer +let using l x = l.Token.using x end -else +ELSE module M = struct type loc = int * int let dummy_loc = (0,0) let make_loc x = x let unloc x = x +let join_loc loc1 loc2 = + if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc + else (fst loc1, snd loc2) +type token = Token.t +type lexer = Token.lexer +let using l x = l.Token.using x end +END +END type loc = M.loc let dummy_loc = M.dummy_loc let unloc = M.unloc let make_loc = M.make_loc +let join_loc = M.join_loc +type token = M.token +type lexer = M.lexer +let using = M.using diff --git a/lib/options.ml b/lib/options.ml index c46857e3..53a7e9cf 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: options.ml 9191 2006-09-29 15:45:42Z courtieu $ *) +(* $Id: options.ml 10105 2007-08-30 16:53:32Z herbelin $ *) open Util @@ -121,4 +121,4 @@ let browser_cmd_fmt = Not_found -> if Sys.os_type = "Win32" then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", "" - else "netscape -remote \"OpenURL(", ")\"" + else "firefox -remote \"OpenURL(", ")\"" diff --git a/lib/util.ml b/lib/util.ml index bf70acc7..16d73430 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: util.ml 9766 2007-04-13 13:26:28Z herbelin $ *) +(* $Id: util.ml 10185 2007-10-06 18:05:13Z herbelin $ *) open Pp @@ -32,9 +32,7 @@ type 'a located = loc * 'a let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm)) let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm)) let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) -let join_loc loc1 loc2 = - if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc - else (fst loc1, snd loc2) +let join_loc = Compat.join_loc (* Like Exc_located, but specifies the outermost file read, the filename associated to the location of the error, and the error itself. *) diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 12c0ea1d..2731fc90 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: argextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *) +(* $Id: argextend.ml4 10185 2007-10-06 18:05:13Z herbelin $ *) open Genarg open Q_util open Q_coqast -let join_loc (deb1,_) (_,fin2) = (deb1,fin2) +let join_loc = Util.join_loc let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> @@ -226,7 +226,7 @@ EXTEND let t, g = interp_entry_name loc e sep in (g, Some (s,t)) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then - Pcoq.lexer.Token.using ("", s); + Compat.using Pcoq.lexer ("", s); (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None) ] ] ; diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 5dda69ba..4216899b 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: egrammar.mli 9147 2006-09-15 21:49:56Z herbelin $ i*) +(*i $Id: egrammar.mli 10185 2007-10-06 18:05:13Z herbelin $ i*) (*i*) open Util @@ -45,7 +45,7 @@ val extend_grammar : all_grammar_command -> unit type grammar_tactic_production = | TacTerm of string | TacNonTerm of - loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option + loc * (Compat.token Gramext.g_symbol * Genarg.argument_type) * string option val extend_tactic_grammar : string -> grammar_tactic_production list list -> unit @@ -61,7 +61,7 @@ val get_extend_vernac_grammars : (* val reset_extend_grammars_v8 : unit -> unit *) -val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol +val interp_entry_name : int -> string -> entry_type * Compat.token Gramext.g_symbol val recover_notation_grammar : notation -> (precedence * tolerability list) -> notation_grammar diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 6a9388b2..cdd484e7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_vernac.ml4 9977 2007-07-12 12:18:46Z msozeau $ *) +(* $Id: g_vernac.ml4 10067 2007-08-09 17:13:16Z msozeau $ *) (*i camlp4deps: "parsing/grammar.cma" i*) open Pp @@ -143,7 +143,9 @@ GEXTEND Gram VernacFixpoint (recs,Options.boxed_definitions()) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> VernacCoFixpoint (corecs,false) - | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ] + | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l + | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; + l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] ; gallina_ext: [ [ b = record_token; oc = opt_coercion; name = identref; diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 2f31c0b6..ce284454 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_xml.ml4 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: g_xml.ml4 10090 2007-08-24 10:53:53Z herbelin $ *) open Pp open Util diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index f7adfdd8..bf3cb084 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.ml4 9333 2006-11-02 13:59:14Z barras $ i*) +(*i $Id: pcoq.ml4 10185 2007-10-06 18:05:13Z herbelin $ i*) open Pp open Util @@ -29,6 +29,29 @@ open Ppextend we unfreeze the state of the lexer. This restores the behaviour of the lexer. B.B. *) +IFDEF CAMLP5 THEN + +let lexer = { + Token.tok_func = Lexer.func; + Token.tok_using = Lexer.add_token; + Token.tok_removing = (fun _ -> ()); + Token.tok_match = Token.default_match; + (* Token.parse = Lexer.tparse; *) + Token.tok_comm = None; + Token.tok_text = Lexer.token_text } + +module L = + struct + type te = string * string + let lexer = lexer + end + +(* The parser of Coq *) + +module G = Grammar.GMake(L) + +ELSE + let lexer = { Token.func = Lexer.func; Token.using = Lexer.add_token; @@ -45,6 +68,8 @@ module L = module G = Grammar.Make(L) +END + let grammar_delete e rls = List.iter (fun (_,_,lev) -> @@ -95,7 +120,7 @@ type ext_kind = | ByGrammar of grammar_object G.Entry.e * Gramext.position option * (string option * Gramext.g_assoc option * - (Token.t Gramext.g_symbol list * Gramext.g_action) list) list + (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list | ByGEXTEND of (unit -> unit) * (unit -> unit) let camlp4_state = ref [] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 1fe8c122..681a6b2c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 9333 2006-11-02 13:59:14Z barras $ i*) +(*i $Id: pcoq.mli 10185 2007-10-06 18:05:13Z herbelin $ i*) open Util open Names @@ -20,9 +20,9 @@ open Libnames (* The lexer and parser of Coq. *) -val lexer : Token.lexer +val lexer : Compat.lexer -module Gram : Grammar.S with type te = Token.t +module Gram : Grammar.S with type te = Compat.token (* The superclass of all grammar entries *) type grammar_object @@ -42,7 +42,7 @@ val get_constr_entry : val grammar_extend : grammar_object Gram.Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * - (Token.t Gramext.g_symbol list * Gramext.g_action) list) list + (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list -> unit val remove_grammars : int -> unit @@ -210,7 +210,7 @@ module Vernac_ : (* Binding entry names to campl4 entries *) val symbol_of_production : Gramext.g_assoc option -> constr_entry -> - bool -> constr_production_entry -> Token.t Gramext.g_symbol + bool -> constr_production_entry -> Compat.token Gramext.g_symbol (* Registering/resetting the level of an entry *) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 275e179e..92c6715e 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: ppconstr.ml 10087 2007-08-24 10:39:30Z herbelin $ *) (*i*) open Util @@ -95,9 +95,9 @@ let pr_patnotation = pr_notation_gen decode_patlist_value let pr_delimiters key strm = strm ++ str ("%"^key) -let pr_located pr ((b,e),x) = - if Options.do_translate() && (b,e)<>dummy_loc then - let (b,e) = unloc (b,e) in +let pr_located pr (loc,x) = + if Options.do_translate() && loc<>dummy_loc then + let (b,e) = unloc loc in comment b ++ pr x ++ comment e else pr x @@ -142,7 +142,7 @@ let pr_opt_type_spc pr = function | CHole _ -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t -let pr_lident (b,_ as loc,id) = +let pr_lident (loc,id) = if loc <> dummy_loc then let (b,_) = unloc loc in pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index f9b8c425..77f0d5cb 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 9562 2007-01-31 09:00:36Z msozeau $ *) +(* $Id: ppvernac.ml 10087 2007-08-24 10:39:30Z herbelin $ *) open Pp open Names @@ -28,7 +28,7 @@ open Tacinterp let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr -let pr_lident (b,_ as loc,id) = +let pr_lident (loc,id) = if loc <> dummy_loc then let (b,_) = unloc loc in pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) @@ -39,7 +39,7 @@ let string_of_fqid fqid = let pr_fqid fqid = str (string_of_fqid fqid) -let pr_lfqid (_,_ as loc,fqid) = +let pr_lfqid (loc,fqid) = if loc <> dummy_loc then let (b,_) = unloc loc in pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid) @@ -602,6 +602,11 @@ let rec pr_vernac = function | VernacScheme l -> hov 2 (str"Scheme" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l) + | VernacCombinedScheme (id, l) -> + hov 2 (str"Combined Scheme" ++ spc() ++ + pr_lident id ++ spc() ++ str"from" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) + (* Gallina extensions *) | VernacRecord (b,(oc,name),ps,s,c,fs) -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 23787f4c..9f828c96 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_coqast.ml4 9551 2007-01-29 15:13:35Z bgregoir $ *) +(* $Id: q_coqast.ml4 10185 2007-10-06 18:05:13Z herbelin $ *) open Util open Names @@ -19,13 +19,18 @@ let purge_str s = if String.length s == 0 || s.[0] <> '$' then s else String.sub s 1 (String.length s - 1) +IFDEF OCAML308 THEN DEFINE NOP END +IFDEF OCAML309 THEN DEFINE NOP END +IFDEF CAMLP5 THEN DEFINE NOP END + let anti loc x = let e = let loc = - ifdef OCAML_308 then + IFDEF NOP THEN loc - else - (1, snd loc - fst loc) + ELSE + (1, snd loc - fst loc) + END in <:expr< $lid:purge_str x$ >> in <:expr< $anti:e$ >> diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 2ef56907..552c144a 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_util.ml4 9333 2006-11-02 13:59:14Z barras $ *) +(* $Id: q_util.ml4 10087 2007-08-24 10:39:30Z herbelin $ *) (* This file defines standard combinators to build ml expressions *) @@ -37,18 +37,18 @@ let mlexpr_of_list f l = List.fold_right (fun e1 e2 -> let e1 = f e1 in - let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in + let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< [$e1$ :: $e2$] >>) l (let loc = dummy_loc in <:expr< [] >>) let mlexpr_of_pair m1 m2 (a1,a2) = let e1 = m1 a1 and e2 = m2 a2 in - let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in + let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in - let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in + let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in <:expr< ($e1$, $e2$, $e3$) >> (* We don't give location for tactic quotation! *) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 73d41465..2dfe489e 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *) +(* $Id: tacextend.ml4 10089 2007-08-24 10:49:43Z herbelin $ *) +open Util open Genarg open Q_util open Q_coqast open Argextend -let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 7cf542fe..4847f385 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernacextend.ml4 9265 2006-10-24 08:35:38Z herbelin $ *) +(* $Id: vernacextend.ml4 10089 2007-08-24 10:49:43Z herbelin $ *) +open Util open Genarg open Q_util open Q_coqast open Argextend -let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = Util.dummy_loc let default_loc = <:expr< Util.dummy_loc >> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 58dda021..1f7bdad3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 9215 2006-10-05 15:40:31Z herbelin $ *) +(* $Id: cases.ml 10071 2007-08-10 15:34:41Z herbelin $ *) open Util open Names @@ -1021,18 +1021,18 @@ let abstract_predicate env sigma indf cur tms = function (* Depending on whether the predicate is dependent or not, and has real args or not, we lift it to make room for [sign] *) (* Even if not intrinsically dep, we move the predicate into a dep one *) - let sign,k = + let sign,q = if names = [] & n <> 1 then (* Real args were not considered *) (if dep<>Anonymous then - ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1) + (let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign) else - (sign,n)) + sign),n else (* Real args are OK *) - (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign, - if dep<>Anonymous then 0 else 1) in - let pred = lift_predicate k pred in + (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,1) in + let q,k = if dep <> Anonymous then (q-1,2) else (q,1) in + let pred = liftn_predicate q k pred in let pred = extract_predicate [] (pred,tms) in (true, it_mkLambda_or_LetIn_name env pred sign) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 4a2e5ee3..29ec7904 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: detyping.ml 10135 2007-09-21 14:28:12Z herbelin $ *) open Pp open Util @@ -241,7 +241,9 @@ and align_tree nal isgoal (e,c as rhs) = match nal with | [] -> [[],rhs] | na::nal -> match kind_of_term c with - | Case (ci,_,c,cl) when c = mkRel (list_index na (snd e)) -> + | Case (ci,p,c,cl) when c = mkRel (list_index na (snd e)) + & (* don't contract if p dependent *) + computable p (ci.ci_pp_info.ind_nargs) -> let clauses = build_tree na isgoal e ci cl in List.flatten (List.map (fun (pat,rhs) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 92617820..64e9ebec 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 9762 2007-04-13 12:46:50Z herbelin $ *) +(* $Id: tacred.ml 10135 2007-09-21 14:28:12Z herbelin $ *) open Pp open Util @@ -358,12 +358,11 @@ let reduce_fix_use_function f whfun fix stack = Reduced (contract_fix_use_function f fix,stack') | _ -> NotReducible) -let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) = +let contract_cofix_use_function f (bodynum,(_names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = match f j with | None -> mkCoFix(j,typedbodies) | Some c -> c in -(* match List.nth names j with Name id -> f id | _ -> assert false in*) let subbodies = list_tabulate make_Fi nbodies in substl (List.rev subbodies) bodies.(bodynum) @@ -372,19 +371,27 @@ let reduce_mind_case_use_function func env mia = | Construct(ind_sp,i) -> let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1), real_cargs) - | CoFix (_,(names,_,_) as cofix) -> - let build_fix_name i = - match names.(i) with - | Name id -> - if isConst func then - let (mp,dp,_) = repr_con (destConst func) in - let kn = make_con mp dp (label_of_id id) in - (match constant_opt_value env kn with - | None -> None - | Some _ -> Some (mkConst kn)) - else None - | Anonymous -> None in - let cofix_def = contract_cofix_use_function build_fix_name cofix in + | CoFix (bodynum,(names,_,_) as cofix) -> + let build_cofix_name = + if isConst func then + let (mp,dp,_) = repr_con (destConst func) in + fun i -> + if i = bodynum then Some func + else match names.(i) with + | Anonymous -> None + | Name id -> + (* In case of a call to another component of a block of + mutual inductive, try to reuse the global name if + the block was indeed initially built as a global + definition *) + let kn = make_con mp dp (label_of_id id) in + try match constant_opt_value env kn with + | None -> None + | Some _ -> Some (mkConst kn) + with Not_found -> None + else + fun _ -> None in + let cofix_def = contract_cofix_use_function build_cofix_name cofix in mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index cb46ab19..3cb3c11b 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqmktop.ml 9496 2007-01-17 15:22:11Z herbelin $ *) +(* $Id: coqmktop.ml 10192 2007-10-08 00:33:39Z letouzey $ *) (* coqmktop is a script to link Coq, analogous to ocamlmktop. The command line contains options specific to coqmktop, options for the @@ -32,7 +32,10 @@ let ide = split_list Tolink.ide (* 3. Toplevel objects *) let camlp4topobjs = - ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] + if Coq_config.camlp4 = "camlp5" then + ["camlp5_top.cma"; "camlp5o.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] + else + ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] let topobjs = camlp4topobjs let gramobjs = [] @@ -310,7 +313,7 @@ let main () = (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *) let args = if !top then args @ [ "topstart.cmo" ] else args in (* Now, with the .cma, we MUST use the -linkall option *) - let command = String.concat " " (prog::args) in + let command = String.concat " " (prog::"-rectypes"::args) in if !echo then begin print_endline command; diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index c14462eb..9c23dda5 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: setoid_replace.ml 9853 2007-05-23 14:25:47Z letouzey $ *) +(* $Id: setoid_replace.ml 10213 2007-10-10 13:05:59Z letouzey $ *) open Tacmach open Proof_type @@ -819,15 +819,16 @@ let new_morphism m signature id hook = try find_relation_class output' with Not_found -> errorlabstrm "Add Morphism" (str "Not a valid signature: " ++ pr_lconstr output' ++ - str " is neither a registered relation nor the Leibniz " ++ - str " equality.") in + str " is neither a registered relation nor the Leibniz " ++ + str " equality.") in let rel_a,rel_quantifiers_no = match rel with Relation rel -> rel.rel_a, rel.rel_quantifiers_no | Leibniz (Some t) -> t, 0 - | Leibniz None -> assert false in + | Leibniz None -> let _,t = decompose_prod typ in t, 0 in let rel_a_n = - clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in + clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a + in try let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in let argsrev,_ = decompose_prod output_rel_a_n in @@ -1890,47 +1891,49 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_ | Some tac -> Tacticals.tclTRY (Tacticals.tclCOMPLETE tac ) in try - let relation = - match relation with - Some rel -> - (try - match find_relation_class rel with - Relation sa -> sa - | Leibniz _ -> raise Optimize - with - Not_found -> - errorlabstrm "Setoid_rewrite" - (pr_lconstr rel ++ str " is not a registered relation.")) - | None -> - match default_relation_for_carrier (pf_type_of gl c1) with - Relation sa -> sa - | Leibniz _ -> raise Optimize - in - let eq_left_to_right = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in - let eq_right_to_left = mkApp (relation.rel_aeq, [| c2 ; c1 |]) in - let replace dir eq = - tclTHENS (assert_tac false Anonymous eq) - [onLastHyp (fun id -> - tclTHEN - (rewrite_tac dir (mkVar id) ~new_goals) - (clear [id])); - try_prove_eq_tac] - in - tclORELSE - (replace true eq_left_to_right) (replace false eq_right_to_left) gl - with - Optimize -> (* (!replace tac_opt c1 c2) gl *) - let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in - tclTHENS (assert_tac false Anonymous eq) - [onLastHyp (fun id -> - tclTHEN - (rewrite_tac false (mkVar id) ~new_goals) - (clear [id])); - try_prove_eq_tac] gl + let carrier,args = decompose_app (pf_type_of gl c1) in + let relation = + match relation with + Some rel -> + (try + match find_relation_class rel with + Relation sa -> if not (eq_constr carrier sa.rel_a) then + errorlabstrm "Setoid_rewrite" + (str "the carrier of " ++ pr_lconstr rel ++ + str " does not match the type of " ++ pr_lconstr c1); + sa + | Leibniz _ -> raise Optimize + with + Not_found -> + errorlabstrm "Setoid_rewrite" + (pr_lconstr rel ++ str " is not a registered relation.")) + | None -> + match default_relation_for_carrier (pf_type_of gl c1) with + Relation sa -> sa + | Leibniz _ -> raise Optimize + in + let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in + let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in + let replace dir eq = + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN + (rewrite_tac dir (mkVar id) ~new_goals) + (clear [id])); + try_prove_eq_tac] + in + tclORELSE + (replace true eq_left_to_right) (replace false eq_right_to_left) gl + with + Optimize -> (* (!replace tac_opt c1 c2) gl *) + let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN + (rewrite_tac false (mkVar id) ~new_goals) + (clear [id])); + try_prove_eq_tac] gl - - - let setoid_replace = general_setoid_replace general_s_rewrite let setoid_replace_in tac_opt id relation c1 c2 ~new_goals gl = general_setoid_replace (general_s_rewrite_in id) tac_opt relation c1 c2 ~new_goals gl @@ -1970,11 +1973,22 @@ let setoid_symmetry gl = Optimize -> symmetry_red true gl let setoid_symmetry_in id gl = - let new_hyp = - let _,he,c1,c2 = analyse_hypothesis gl (mkVar id) in - mkApp (he, [| c2 ; c1 |]) - in - cut_replacing id new_hyp (tclTHEN setoid_symmetry) gl + let ctype = pf_type_of gl (mkVar id) in + let binders,concl = Sign.decompose_prod_assum ctype in + let (equiv, args) = decompose_app concl in + let rec split_last_two = function + | [c1;c2] -> [],(c1, c2) + | x::y::z -> let l,res = split_last_two (y::z) in x::l, res + | _ -> error "The term provided is not an equivalence" + in + let others,(c1,c2) = split_last_two args in + let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in + let new_hyp' = mkApp (he, [| c2 ; c1 |]) in + let new_hyp = it_mkProd_or_LetIn new_hyp' binders in + tclTHENS (cut new_hyp) + [ intro_replacing id; + tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ] + gl let setoid_transitivity c gl = try diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ac6a396f..37b3cbcb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: tacinterp.ml 10135 2007-09-21 14:28:12Z herbelin $ *) open Constrintern open Closure @@ -436,9 +436,16 @@ let rec intern_intro_pattern lf ist = function and intern_case_intro_pattern lf ist = List.map (List.map (intern_intro_pattern lf ist)) -let intern_quantified_hypothesis ist x = - (* We use identifier both for variables and quantified hyps (no way to - statically check the existence of a quantified hyp); thus nothing to do *) +let intern_quantified_hypothesis ist = function + | AnonHyp n -> AnonHyp n + | NamedHyp id -> + (* Uncomment to disallow "intros until n" in ltac when n is not bound *) + NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*)) + +let intern_binding_name ist x = + (* We use identifier both for variables and binding names *) + (* Todo: consider the body of the lemma to which the binding refer + and if a term w/o ltac vars, check the name is indeed quantified *) x let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c = @@ -453,7 +460,7 @@ let intern_type = intern_constr_gen true (* Globalize bindings *) let intern_binding ist (loc,b,c) = - (loc,intern_quantified_hypothesis ist b,intern_constr ist c) + (loc,intern_binding_name ist b,intern_constr ist c) let intern_bindings ist = function | NoBindings -> NoBindings @@ -1465,8 +1472,17 @@ let interp_quantified_hypothesis ist = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id) - with Not_found - | Stdpp.Exc_located (_, UserError _) | UserError _ (*Compat provisoire*) + with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _ + -> NamedHyp id + +let interp_binding_name ist = function + | AnonHyp n -> AnonHyp n + | NamedHyp id -> + (* If a name is bound, it has to be a quantified hypothesis *) + (* user has to use other names for variables if these ones clash with *) + (* a name intented to be used as a (non-variable) identifier *) + try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id) + with Not_found | Stdpp.Exc_located (_, UserError _) | UserError _ -> NamedHyp id (* Quantified named or numbered hypothesis or hypothesis in context *) @@ -1495,7 +1511,7 @@ let interp_induction_arg ist gl = function (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id))))) let interp_binding ist gl (loc,b,c) = - (loc,interp_quantified_hypothesis ist b,pf_interp_constr ist gl c) + (loc,interp_binding_name ist b,pf_interp_constr ist gl c) let interp_bindings ist gl = function | NoBindings -> NoBindings @@ -2349,7 +2365,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l) | TacCut c -> TacCut (subst_rawconstr subst c) - | TacAssert (b,na,c) -> TacAssert (b,na,subst_rawconstr subst c) + | TacAssert (b,na,c) -> + TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c) | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp) diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index 42df990f..fecc8977 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -77,3 +77,22 @@ Theorem discr2 : Some true = Some false -> False. intros. congruence. Qed. + +Set Implicit Arguments. + +Parameter elt: Set. +Parameter elt_eq: forall (x y: elt), {x = y} + {x <> y}. +Definition t (A: Set) := elt -> A. +Definition get (A: Set) (x: elt) (m: t A) := m x. +Definition set (A: Set) (x: elt) (v: A) (m: t A) := + fun (y: elt) => if elt_eq y x then v else m y. +Lemma gsident: + forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m. +Proof. + intros. unfold get, set. case (elt_eq j i); intro. + congruence. + auto. +Qed. + + +
\ No newline at end of file diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index cd9d3669..b6af3abc 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_makefile.ml4 8840 2006-05-22 13:51:14Z notin $ *) +(* $Id: coq_makefile.ml4 10185 2007-10-06 18:05:13Z herbelin $ *) (* créer un Makefile pour un développement Coq automatiquement *) @@ -175,8 +175,8 @@ let variables l = | _ :: r -> var_aux r in section "Variables definitions."; - print "CAMLP4LIB=`camlp4 -where`\n"; -(* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *) + print "CAMLP4LIB=`camlp5 -where 2> /dev/null || camlp4 -where`\n"; + print "CAMLP4=`basename $CAMLP4LIB`\n"; print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ -I $(COQTOP)/library -I $(COQTOP)/parsing \\ -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\ @@ -204,8 +204,8 @@ let variables l = print "CAMLOPTLINK=ocamlopt\n"; print "COQDEP=$(COQBIN)coqdep -c\n"; print "GRAMMARS=grammar.cma\n"; - print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n"; - print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; + print "CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; + print "PP=-pp \"$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; var_aux l; print "\n" diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 89f39b22..e787cdb3 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 9808 2007-04-29 07:15:18Z herbelin $ *) +(* $Id: coqdep.ml 10196 2007-10-08 13:50:39Z notin $ *) open Printf open Coqdep_lexer @@ -108,12 +108,12 @@ let absolute_dir dir = let absolute_file_name basename odir = let dir = match odir with Some dir -> dir | None -> "." in - absolute_dir dir / basename + absolute_dir dir // basename let file_name = function | (s,None) -> file_concat s | (s,Some ".") -> file_concat s - | (s,Some d) -> d / file_concat s + | (s,Some d) -> d // file_concat s let traite_fichier_ML md ext = try @@ -165,7 +165,7 @@ let cut_prefix p s = if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s let canonize f = - let f' = absolute_dir (Filename.dirname f) / Filename.basename f in + let f' = absolute_dir (Filename.dirname f) // Filename.basename f in match List.filter (fun (_,full) -> f' = full) !vAccu with | (f,_) :: _ -> f | _ -> f @@ -411,7 +411,7 @@ let all_subdirs root_dir log_dir = let f = readdir dirh in if f <> "." && f <> ".." then let file = dir@[f] in - let filename = phys_dir/f in + let filename = phys_dir//f in if (stat filename).st_kind = S_DIR then begin add (filename,file); traverse filename file @@ -429,7 +429,7 @@ let usage () = exit 1 let add_coqlib_known dir_name f = - let complete_name = dir_name/f in + let complete_name = dir_name//f in let lib_name = Filename.basename dir_name in match try (stat complete_name).st_kind with _ -> S_BLK with | S_REG -> @@ -458,7 +458,7 @@ let coqdep () = match (old_dirname,new_dirname) with | (d, ".") -> d | (None,d) -> Some d - | (Some d1,d2) -> Some (d1/d2) + | (Some d1,d2) -> Some (d1//d2) in let complete_name = file_name ([name],dirname) in match try (stat complete_name).st_kind with _ -> S_BLK with @@ -468,7 +468,7 @@ let coqdep () = let newdirname = match dirname with | None -> name - | Some d -> d/name + | Some d -> d//name in try while true do treat (Some newdirname) (readdir dir) done @@ -490,7 +490,7 @@ let coqdep () = | _ -> () in let add_known phys_dir log_dir f = - let complete_name = phys_dir/f in + let complete_name = phys_dir//f in match try (stat complete_name).st_kind with _ -> S_BLK with | S_REG -> if Filename.check_suffix f ".ml" then @@ -505,7 +505,7 @@ let coqdep () = else if Filename.check_suffix f ".v" then let basename = Filename.chop_suffix f ".v" in let name = log_dir@[basename] in - let file = phys_dir/basename in + let file = phys_dir//basename in let paths = [name;[basename]] in List.iter (fun n -> safe_addQueue clash_v vKnown (n,file)) paths @@ -546,11 +546,11 @@ let coqdep () = parse (List.tl (Array.to_list Sys.argv)); List.iter (fun (s,_) -> add_coqlib_directory s) - (all_subdirs (!coqlib/"theories") "Coq"); + (all_subdirs (!coqlib//"theories") "Coq"); List.iter (fun (s,_) -> add_coqlib_directory s) - (all_subdirs (!coqlib/"contrib") "Coq"); - add_coqlib_directory (!coqlib/"user-contrib"); + (all_subdirs (!coqlib//"contrib") "Coq"); + add_coqlib_directory (!coqlib//"user-contrib"); mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu); mlKnown := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu); warning_mult ".mli" !mliKnown; diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index c63a6a9b..2bf615d3 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 10017 2007-07-18 13:23:55Z notin $ i*) +(*i $Id: pretty.mll 10074 2007-08-13 12:19:44Z notin $ i*) (*s Utility functions for the scanners *) @@ -367,7 +367,7 @@ rule coq_bol = parse coq_bol lexbuf } | space* "(*" { let eol = comment lexbuf in - if eol then coq_bol lexbuf else coq lexbuf } + if eol then begin line_break(); coq_bol lexbuf end else coq lexbuf } | eof { () } | _ @@ -578,7 +578,7 @@ and body = parse | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true } | '.' space+ { char '.'; char ' '; false } | "(*" { let eol = comment lexbuf in - if eol then body_bol lexbuf else body lexbuf } + if eol then begin line_break(); body_bol lexbuf end else body lexbuf } | identifier { let s = lexeme lexbuf in ident s (lexeme_start lexbuf); diff --git a/toplevel/command.ml b/toplevel/command.ml index a1860329..a8e0133e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: command.ml 10067 2007-08-09 17:13:16Z msozeau $ *) open Pp open Util @@ -657,6 +657,58 @@ let build_scheme lnamedepindsort = let _ = List.fold_right2 declare listdecl lrecnames [] in if_verbose ppnl (recursive_message Fixpoint lrecnames) +let rec get_concl n t = + if n = 0 then t + else + match kind_of_term t with + Prod (_,_,t) -> get_concl (pred n) t + | _ -> raise (Invalid_argument "get_concl") + +let cut_last l = + let rec aux acc = function + hd :: [] -> List.rev acc, hd + | hd :: tl -> aux (hd :: acc) tl + | [] -> raise (Invalid_argument "cut_last") + in aux [] l + +let build_combined_scheme name schemes = + let env = Global.env () in + let defs = + List.map (fun x -> + let refe = Ident x in + let qualid = qualid_of_reference refe in + let cst = Nametab.locate_constant (snd qualid) in + qualid, cst, Typeops.type_of_constant env cst) + schemes + in + let (qid, c, t) = List.hd defs in + let nargs = + let (_, arity, _) = destProd t in + nb_prod arity + in + let prods = nb_prod t - nargs in + let defs, (qid, c, t) = cut_last defs in + let (args, concl) = decompose_prod_n prods t in + let concls = List.map (fun (_, cst, t) -> cst, get_concl prods t) defs in + let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in + let relargs = rel_vect 0 prods in + let concl_typ, concl_bod = + List.fold_right + (fun (cst, x) (acct, accb) -> + mkApp (coqand, [| x; acct |]), + mkApp (coqconj, [| x; acct; mkApp(mkConst cst, relargs); accb |])) + concls (concl, mkApp (mkConst c, relargs)) + in + let ctx = List.map (fun (x, y) -> x, None, y) args in + let typ = it_mkProd_wo_LetIn concl_typ ctx in + let body = it_mkLambda_or_LetIn concl_bod ctx in + let ce = { const_entry_body = body; + const_entry_type = Some typ; + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() } in + let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in + if_verbose ppnl (recursive_message Fixpoint [snd name]) + (* 4| Goal declaration *) let start_proof id kind c hook = diff --git a/toplevel/command.mli b/toplevel/command.mli index e043f354..d15e90cb 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) +(*i $Id: command.mli 10067 2007-08-09 17:13:16Z msozeau $ i*) (*i*) open Util @@ -53,6 +53,8 @@ val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit val build_scheme : (identifier located * bool * reference * rawsort) list -> unit +val build_combined_scheme : identifier located -> identifier located list -> unit + val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 3dcb1f58..13f1f1da 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 9333 2006-11-02 13:59:14Z barras $ *) +(* $Id: metasyntax.ml 10192 2007-10-08 00:33:39Z letouzey $ *) open Pp open Util @@ -28,7 +28,7 @@ open Notation (**********************************************************************) (* Tokens *) -let cache_token (_,s) = Pcoq.lexer.Token.using ("", s) +let cache_token (_,s) = Compat.using Pcoq.lexer ("", s) let (inToken, outToken) = declare_object {(default_object "TOKEN") with @@ -739,7 +739,9 @@ let set_entry_type etyps (x,typ) = let check_rule_productivity l = if List.for_all (function NonTerminal _ -> true | _ -> false) l then - error "A notation must include at least one symbol" + error "A notation must include at least one symbol"; + if (match l with SProdList _ :: _ -> true | _ -> false) then + error "A recursive notation must start with at least one symbol" let is_not_printable = function | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 4e6058be..2185d2a0 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mltop.ml4 9397 2006-11-21 21:50:54Z herbelin $ *) +(* $Id: mltop.ml4 10185 2007-10-06 18:05:13Z herbelin $ *) open Util open Pp @@ -98,7 +98,7 @@ let dir_ml_load s = str s; str" to Coq code." >]) (* TO DO: .cma loading without toplevel *) | WithoutTop -> - ifdef Byte then + IFDEF Byte THEN let _,gname = where_in_path !coq_mlpath_copy s in try Dynlink.loadfile gname; @@ -108,7 +108,7 @@ let dir_ml_load s = [Filename.dirname gname] with | Dynlink.Error a -> errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >] - else () + ELSE () END | Native -> errorlabstrm "Mltop.no_load_object" [< str"Loading of ML object file forbidden in a native Coq" >] diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 39106bbf..fdd30711 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 9432 2006-12-12 09:07:36Z courtieu $ *) +(* $Id: toplevel.ml 10087 2007-08-24 10:39:30Z herbelin $ *) open Pp open Util @@ -139,16 +139,16 @@ let print_highlight_location ib loc = (* Functions to report located errors in a file. *) -let print_location_in_file s inlibrary fname (bp,ep) = +let print_location_in_file s inlibrary fname loc = let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in - if (bp,ep) = dummy_loc then + if loc = dummy_loc then (errstrm ++ str", unknown location." ++ fnl ()) else if inlibrary then (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ - str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ()) + str" characters " ++ Cerrors.print_loc loc ++ fnl ()) else - let (bp,ep) = unloc (bp,ep) in + let (bp,ep) = unloc loc in let ic = open_in fname in let rec line_of_pos lin bol cnt = if cnt < bp then @@ -172,15 +172,16 @@ let print_command_location ib dloc = str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ()) | None -> (mt ()) -let valid_loc dloc (b,e) = - (b,e) <> dummy_loc +let valid_loc dloc loc = + loc <> dummy_loc & match dloc with - | Some (bd,ed) -> bd<=b & e<=ed + | Some dloc -> + let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed | _ -> true -let valid_buffer_loc ib dloc (b,e) = - valid_loc dloc (b,e) & - let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e +let valid_buffer_loc ib dloc loc = + valid_loc dloc loc & + let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e (*s The Coq prompt is the name of the focused proof, if any, and "Coq" otherwise. We trap all exceptions to prevent the error message printing diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fb719a21..dd6d7e25 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 9874 2007-06-04 13:46:11Z soubiran $ i*) +(*i $Id: vernacentries.ml 10067 2007-08-09 17:13:16Z msozeau $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -359,6 +359,8 @@ let vernac_cofixpoint = build_corecursive let vernac_scheme = build_scheme +let vernac_combined_scheme = build_combined_scheme + (**********************) (* Modules *) @@ -1137,6 +1139,7 @@ let interp c = match c with | VernacFixpoint (l,b) -> vernac_fixpoint l b | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b | VernacScheme l -> vernac_scheme l + | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l (* Modules *) | VernacDeclareModule (export,(_,id),bl,mtyo) -> diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 4c671787..9f51841d 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 9481 2007-01-11 19:17:56Z herbelin $ i*) +(*i $Id: vernacexpr.ml 10067 2007-08-09 17:13:16Z msozeau $ i*) open Util open Names @@ -199,6 +199,7 @@ type vernac_expr = | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool | VernacScheme of (lident * bool * lreference * sort_expr) list + | VernacCombinedScheme of lident * lident list (* Gallina extensions *) | VernacRecord of bool (* = Record or Structure *) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 0e17df28..b067ba1f 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: whelp.ml4 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: whelp.ml4 10105 2007-08-30 16:53:32Z herbelin $ *) open Options open Pp @@ -32,8 +32,30 @@ open Tacmach (* Coq interface to the Whelp query engine developed at the University of Bologna *) +let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080" +let getter_server_name = ref "http://mowgli.cs.unibo.it:58081" + +open Goptions + +let _ = + declare_string_option + { optsync = false; + optname = "Whelp server"; + optkey = (SecondaryTable ("Whelp","Server")); + optread = (fun () -> !whelp_server_name); + optwrite = (fun s -> whelp_server_name := s) } + +let _ = + declare_string_option + { optsync = false; + optname = "Whelp getter"; + optkey = (SecondaryTable ("Whelp","Getter")); + optread = (fun () -> !getter_server_name); + optwrite = (fun s -> getter_server_name := s) } + + let make_whelp_request req c = - "http://mowgli.cs.unibo.it/forward/58080/apply?xmluri=http%3A%2F%2Fmowgli.cs.unibo.it%3A58081%2Fgetempty¶m.profile=firewall&profile=firewall¶m.keys=d_c%2CC1%2CHC2%2CL¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thkeys=T1%2CT2%2CL%2CE¶m.prooftreekeys=HAT%2CG%2CHAO%2CL¶m.media-type=text%2Fhtml¶m.thmedia-type=&prooftreemedia-type=¶m.doctype-public=¶m.encoding=¶m.thencoding=¶m.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE¶m.expression=" ^ c ^ "¶m.action=" ^ req + !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty¶m.profile=firewall&profile=firewall¶m.keys=d_c%2CC1%2CHC2%2CL¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thkeys=T1%2CT2%2CL%2CE¶m.prooftreekeys=HAT%2CG%2CHAO%2CL¶m.media-type=text%2Fhtml¶m.thmedia-type=&prooftreemedia-type=¶m.doctype-public=¶m.encoding=¶m.thencoding=¶m.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE¶m.expression=" ^ c ^ "¶m.action=" ^ req let b = Buffer.create 16 |