From 80bd0e81305abfc76831ff1c8361e01c4aabb68e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Dec 2016 12:34:35 +0100 Subject: ssrmatching: fix iter_constr_LR iterator wrt Proj --- plugins/ssrmatching/ssrmatching.ml4 | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 11f45d5d86..d21223d43d 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -390,7 +390,8 @@ let iter_constr_LR f c = match kind_of_term c with | Case (_, p, v, b) -> f v; f p; Array.iter f b | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) -> for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done - | _ -> () + | Proj(_,a) -> f a + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () (* The comparison used to determine which subterms matches is KEYED *) (* CONVERSION. This looks for convertible terms that either have the same *) @@ -524,7 +525,13 @@ let nb_cs_proj_args pc f u = try match kind_of_term f with | Prod _ -> na Prod_cs | Sort s -> na (Sort_cs (family_of_sort s)) - | Const (c',_) when Constant.equal c' pc -> Array.length (snd (destApp u.up_f)) + | Const (c',_) when Constant.equal c' pc -> + begin match kind_of_term u.up_f with + | App(_,args) -> Array.length args + | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be + the number of arguments including the projected *) + | _ -> assert false + end | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f)) | _ -> -1 with Not_found -> -1 -- cgit v1.2.3 From 04c3f08807e341273919556652525f8226e94b6d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 7 Dec 2016 14:52:29 +0100 Subject: A few words in CHANGES. --- CHANGES | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CHANGES b/CHANGES index ecbf82e69d..3cb0eaa216 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,13 @@ +Changes from V8.6beta1 to V8.6 +============================== + +Kernel + +- Fixed critical bug #5248 in VM long multiplication on 32-bit + architectures. Was there only since 8.6beta1, so no stable release impacted. + +Other bug fixes in universes, type class shelving,... + Changes from V8.5 to V8.6beta1 ============================== -- cgit v1.2.3 From 7037e2972828f395962284848ce167545253d910 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 7 Dec 2016 14:59:14 +0100 Subject: Set version number to 8.6rc1. --- configure.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/configure.ml b/configure.ml index b97bf9a71b..f1397e676d 100644 --- a/configure.ml +++ b/configure.ml @@ -12,10 +12,10 @@ open Printf let coq_version = "8.6beta1" -let coq_macos_version = "8.5.90" (** "[...] should be a string comprised of +let coq_macos_version = "8.6.00" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 8591 -let state_magic = 58591 +let vo_magic = 8600 +let state_magic = 58600 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] -- cgit v1.2.3 From b802f1789b59a93bb84783125f61794c00d6c940 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 7 Dec 2016 15:18:03 +0100 Subject: Add bat files for 8.6beta1 build. --- dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat | 10 ++++++++++ dev/build/windows/MakeCoq_86beta1_installer.bat | 8 ++++++++ dev/build/windows/MakeCoq_86beta1_installer_32.bat | 8 ++++++++ 3 files changed, 26 insertions(+) create mode 100644 dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat create mode 100644 dev/build/windows/MakeCoq_86beta1_installer.bat create mode 100644 dev/build/windows/MakeCoq_86beta1_installer_32.bat diff --git a/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat new file mode 100644 index 0000000000..914c332f46 --- /dev/null +++ b/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat @@ -0,0 +1,10 @@ +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=64 ^ + -mode=absolute ^ + -ocaml=Y ^ + -make=Y ^ + -coqver=8.6beta1 ^ + -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_abs ^ + -destcoq=%ROOTPATH%\coq64_86beta1_abs diff --git a/dev/build/windows/MakeCoq_86beta1_installer.bat b/dev/build/windows/MakeCoq_86beta1_installer.bat new file mode 100644 index 0000000000..76a5bb35ac --- /dev/null +++ b/dev/build/windows/MakeCoq_86beta1_installer.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=64 ^ + -installer=Y ^ + -coqver=8.6beta1 ^ + -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_inst ^ + -destcoq=%ROOTPATH%\coq64_86beta1_inst diff --git a/dev/build/windows/MakeCoq_86beta1_installer_32.bat b/dev/build/windows/MakeCoq_86beta1_installer_32.bat new file mode 100644 index 0000000000..ff83087e75 --- /dev/null +++ b/dev/build/windows/MakeCoq_86beta1_installer_32.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=32 ^ + -installer=Y ^ + -coqver=8.6beta1 ^ + -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_inst ^ + -destcoq=%ROOTPATH%\coq64_86beta1_inst -- cgit v1.2.3 From fddf3ca8f2499c14018c13417346c567971c0a23 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 7 Dec 2016 15:22:34 +0100 Subject: Add bat files for 8.6rc1 build. --- dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat | 10 ++++++++++ dev/build/windows/MakeCoq_86rc1_installer.bat | 8 ++++++++ dev/build/windows/MakeCoq_86rc1_installer_32.bat | 8 ++++++++ 3 files changed, 26 insertions(+) create mode 100644 dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat create mode 100644 dev/build/windows/MakeCoq_86rc1_installer.bat create mode 100644 dev/build/windows/MakeCoq_86rc1_installer_32.bat diff --git a/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat new file mode 100644 index 0000000000..c0669f01d2 --- /dev/null +++ b/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat @@ -0,0 +1,10 @@ +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=64 ^ + -mode=absolute ^ + -ocaml=Y ^ + -make=Y ^ + -coqver=8.6rc1 ^ + -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_abs ^ + -destcoq=%ROOTPATH%\coq64_86rc1_abs diff --git a/dev/build/windows/MakeCoq_86rc1_installer.bat b/dev/build/windows/MakeCoq_86rc1_installer.bat new file mode 100644 index 0000000000..66234ebbde --- /dev/null +++ b/dev/build/windows/MakeCoq_86rc1_installer.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=64 ^ + -installer=Y ^ + -coqver=8.6rc1 ^ + -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_inst ^ + -destcoq=%ROOTPATH%\coq64_86rc1_inst diff --git a/dev/build/windows/MakeCoq_86rc1_installer_32.bat b/dev/build/windows/MakeCoq_86rc1_installer_32.bat new file mode 100644 index 0000000000..50672a6b5d --- /dev/null +++ b/dev/build/windows/MakeCoq_86rc1_installer_32.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=32 ^ + -installer=Y ^ + -coqver=8.6rc1 ^ + -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_inst ^ + -destcoq=%ROOTPATH%\coq64_86rc1_inst -- cgit v1.2.3 From d24aaa4d0e45dc3ec31c5f576516b01ded403dd8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 7 Dec 2016 16:04:21 +0100 Subject: Commit bumping the version number was partial... The sad part of the story is that the script testing this version number is run after tagging by the coq-dev-tools Makefile... will fix that. --- configure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index f1397e676d..f4b18d9f70 100644 --- a/configure.ml +++ b/configure.ml @@ -11,7 +11,7 @@ #load "str.cma" open Printf -let coq_version = "8.6beta1" +let coq_version = "8.6rc1" let coq_macos_version = "8.6.00" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) let vo_magic = 8600 -- cgit v1.2.3 From fb637d483d3637f0cf81eed92467f1ff491add2a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 8 Dec 2016 10:30:26 +0100 Subject: Fix paths in 32-bit windows build scripts. --- dev/build/windows/MakeCoq_86beta1_installer_32.bat | 4 ++-- dev/build/windows/MakeCoq_86rc1_installer_32.bat | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/dev/build/windows/MakeCoq_86beta1_installer_32.bat b/dev/build/windows/MakeCoq_86beta1_installer_32.bat index ff83087e75..f53232b651 100644 --- a/dev/build/windows/MakeCoq_86beta1_installer_32.bat +++ b/dev/build/windows/MakeCoq_86beta1_installer_32.bat @@ -4,5 +4,5 @@ call MakeCoq_MinGW.bat ^ -arch=32 ^ -installer=Y ^ -coqver=8.6beta1 ^ - -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_inst ^ - -destcoq=%ROOTPATH%\coq64_86beta1_inst + -destcyg=%ROOTPATH%\cygwin_coq32_86beta1_inst ^ + -destcoq=%ROOTPATH%\coq32_86beta1_inst diff --git a/dev/build/windows/MakeCoq_86rc1_installer_32.bat b/dev/build/windows/MakeCoq_86rc1_installer_32.bat index 50672a6b5d..96f43e16a5 100644 --- a/dev/build/windows/MakeCoq_86rc1_installer_32.bat +++ b/dev/build/windows/MakeCoq_86rc1_installer_32.bat @@ -4,5 +4,5 @@ call MakeCoq_MinGW.bat ^ -arch=32 ^ -installer=Y ^ -coqver=8.6rc1 ^ - -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_inst ^ - -destcoq=%ROOTPATH%\coq64_86rc1_inst + -destcyg=%ROOTPATH%\cygwin_coq32_86rc1_inst ^ + -destcoq=%ROOTPATH%\coq32_86rc1_inst -- cgit v1.2.3 From fbde1bb856527cc152cd7daf99b85a8c76991a23 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 8 Dec 2016 16:03:33 +0100 Subject: Windows build scripts for 8.6 final. --- dev/build/windows/MakeCoq_86_abs_ocaml.bat | 10 ++++++++++ dev/build/windows/MakeCoq_86_installer.bat | 8 ++++++++ dev/build/windows/MakeCoq_86_installer_32.bat | 8 ++++++++ 3 files changed, 26 insertions(+) create mode 100644 dev/build/windows/MakeCoq_86_abs_ocaml.bat create mode 100644 dev/build/windows/MakeCoq_86_installer.bat create mode 100644 dev/build/windows/MakeCoq_86_installer_32.bat diff --git a/dev/build/windows/MakeCoq_86_abs_ocaml.bat b/dev/build/windows/MakeCoq_86_abs_ocaml.bat new file mode 100644 index 0000000000..50483c4d4a --- /dev/null +++ b/dev/build/windows/MakeCoq_86_abs_ocaml.bat @@ -0,0 +1,10 @@ +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=64 ^ + -mode=absolute ^ + -ocaml=Y ^ + -make=Y ^ + -coqver=8.6 ^ + -destcyg=%ROOTPATH%\cygwin_coq64_86_abs ^ + -destcoq=%ROOTPATH%\coq64_86_abs diff --git a/dev/build/windows/MakeCoq_86_installer.bat b/dev/build/windows/MakeCoq_86_installer.bat new file mode 100644 index 0000000000..263520ff14 --- /dev/null +++ b/dev/build/windows/MakeCoq_86_installer.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=64 ^ + -installer=Y ^ + -coqver=8.6 ^ + -destcyg=%ROOTPATH%\cygwin_coq64_86_inst ^ + -destcoq=%ROOTPATH%\coq64_86_inst diff --git a/dev/build/windows/MakeCoq_86_installer_32.bat b/dev/build/windows/MakeCoq_86_installer_32.bat new file mode 100644 index 0000000000..14921dd7c3 --- /dev/null +++ b/dev/build/windows/MakeCoq_86_installer_32.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=32 ^ + -installer=Y ^ + -coqver=8.6 ^ + -destcyg=%ROOTPATH%\cygwin_coq32_86_inst ^ + -destcoq=%ROOTPATH%\coq32_86_inst -- cgit v1.2.3 From 0d1438851ba3a0b9f76847abc42f3bf8ad26c4cb Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 8 Dec 2016 15:58:33 +0100 Subject: Set version to 8.6 in configure. --- configure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index f4b18d9f70..99f5ae5424 100644 --- a/configure.ml +++ b/configure.ml @@ -11,7 +11,7 @@ #load "str.cma" open Printf -let coq_version = "8.6rc1" +let coq_version = "8.6" let coq_macos_version = "8.6.00" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) let vo_magic = 8600 -- cgit v1.2.3 From 42f27beb63a629dcef514abb0b31dea193f35a38 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 16 Dec 2016 11:27:42 +0100 Subject: Fix incorrect documentation that prevents successful compilation (bug #5265). --- doc/refman/RefMan-syn.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 1fcc1c0df4..21c39de967 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -649,7 +649,7 @@ A recursive pattern for binders can be used in position of a recursive pattern for terms. Here is an example: \begin{coq_example*} -Notation ``'FUNAPP' x .. y , f'' := +Notation "'FUNAPP' x .. y , f" := (fun x => .. (fun y => (.. (f x) ..) y ) ..) (at level 200, x binder, y binder, right associativity). \end{coq_example*} -- cgit v1.2.3 From c793d102df3e007d824e79f499e71823207c301a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 19 Dec 2016 11:58:39 +0100 Subject: Avoid concurrent runs when producing html documentation (bug #5269). Make does not allow for rules that produce multiple outputs (unless they are pattern rules). As a consequence, the hacha rule could be run several times concurrently, thus causing doc/refman/html to be deleted under the feet of some runs. This commit fixes the issue by turning the rule into a single-output rule and adding a dummy rule to handle all the other indexes. Note that this is not a perfect solution since, if the user were to manually delete one of the auxiliary index, it would not be rebuilt until the main index is. --- Makefile.doc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Makefile.doc b/Makefile.doc index cdd9852e87..9ae20ba765 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -201,15 +201,17 @@ doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva $(INSTALLLIB) $< doc/refman INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html -ALLINDEXES:= doc/refman/html/index.html $(INDEXES) -refman-html-dir $(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ +refman-html-dir $(INDEXES): doc/refman/html/index.html ; + +doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html - rm -rf doc/refman/html $(MKDIR) doc/refman/html $(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html (cd doc/refman/html; $(HACHA) -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) $(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html + @touch $(INDEXES) -$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html refman-quick: -- cgit v1.2.3 From 021f94d7dfef5630e48e79c9238db3a24b2aa221 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 23 Dec 2016 09:28:47 +0100 Subject: Handle application of a primitive projection to a not yet evaluated cofixpoint (bug #5286). --- kernel/byterun/coq_interp.c | 63 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 48 insertions(+), 15 deletions(-) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 5dec3b785c..af89712d5e 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -891,25 +891,58 @@ value coq_interprete Instruct(PROJ){ + do_proj: print_instr("PROJ"); if (Is_accu (accu)) { - value block; - /* Skip over the index of projected field */ - pc++; - /* Create atom */ - Alloc_small(block, 2, ATOM_PROJ_TAG); - Field(block, 0) = Field(coq_global_data, *pc); - Field(block, 1) = accu; - accu = block; - /* Create accumulator */ - Alloc_small(block, 2, Accu_tag); - Code_val(block) = accumulate; - Field(block, 1) = accu; - accu = block; + *--sp = accu; // Save matched block on stack + accu = Field(accu, 1); // Save atom to accu register + switch (Tag_val(accu)) { + case ATOM_COFIX_TAG: // We are forcing a cofix + { + mlsize_t i, nargs; + sp -= 2; + // Push the current instruction as the return address + sp[0] = (value)(pc - 1); + sp[1] = coq_env; + coq_env = Field(accu, 0); // Pointer to suspension + accu = sp[2]; // Save accumulator to accu register + sp[2] = Val_long(coq_extra_args); // Push number of args for return + nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + // Push arguments to stack + CHECK_STACK(nargs + 1); + sp -= nargs; + for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2); + *--sp = accu; // Last argument is the pointer to the suspension + coq_extra_args = nargs; + pc = Code_val(coq_env); // Trigger evaluation + goto check_stack; + } + case ATOM_COFIXEVALUATED_TAG: + { + accu = Field(accu, 1); + ++sp; + goto do_proj; + } + default: + { + value block; + /* Skip over the index of projected field */ + ++pc; + /* Create atom */ + Alloc_small(accu, 2, ATOM_PROJ_TAG); + Field(accu, 0) = Field(coq_global_data, *pc++); + Field(accu, 1) = *sp++; + /* Create accumulator */ + Alloc_small(block, 2, Accu_tag); + Code_val(block) = accumulate; + Field(block, 1) = accu; + accu = block; + } + } } else { - accu = Field(accu, *pc++); + accu = Field(accu, *pc); + pc += 2; } - pc++; Next; } -- cgit v1.2.3 From ac9b9415e884dc478b1776b8792c690f61efd5ed Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 Dec 2016 16:57:35 +0100 Subject: Fix some typos in tutorial (bug #5294). This commit uses the proper url for bug reporting, marks urls as such, stops qualifying the Coq'Art book as new, and fix the spacing after the Coq name. --- doc/tutorial/Tutorial.tex | 61 ++++++++++++++++++++++++----------------------- 1 file changed, 31 insertions(+), 30 deletions(-) diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 973a0b75e0..0d537256bb 100644 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -3,6 +3,7 @@ \usepackage[utf8]{inputenc} \usepackage{textcomp} \usepackage{pslatex} +\usepackage{hyperref} \input{../common/version.tex} \input{../common/macros.tex} @@ -17,7 +18,7 @@ \chapter*{Getting started} -\Coq\ is a Proof Assistant for a Logical Framework known as the Calculus +\Coq{} is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications. It runs as a computer program @@ -29,7 +30,7 @@ possibilities of \Coq, but rather to present in the most elementary manner a tutorial on the basic specification language, called Gallina, in which formal axiomatisations may be developed, and on the main proof tools. For more advanced information, the reader could refer to -the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y. +the \Coq{} Reference Manual or the \textit{Coq'Art}, a book by Y. Bertot and P. Castéran on practical uses of the \Coq{} system. Coq can be used from a standard teletype-like shell window but @@ -39,9 +40,9 @@ and Pcoq.}. Instructions on installation procedures, as well as more comprehensive documentation, may be found in the standard distribution of \Coq, -which may be obtained from \Coq{} web site \texttt{http://coq.inria.fr}. +which may be obtained from \Coq{} web site \url{https://coq.inria.fr/}. -In the following, we assume that \Coq~ is called from a standard +In the following, we assume that \Coq{} is called from a standard teletype-like shell window. All examples preceded by the prompting sequence \verb:Coq < : represent user input, terminated by a period. @@ -51,10 +52,10 @@ users screen. When used from a graphical user interface such as CoqIde, the prompt is not displayed: user input is given in one window and \Coq's answers are displayed in a different window. -The sequence of such examples is a valid \Coq~ +The sequence of such examples is a valid \Coq{} session, unless otherwise specified. This version of the tutorial has been prepared on a PC workstation running Linux. The standard -invocation of \Coq\ delivers a message such as: +invocation of \Coq{} delivers a message such as: \begin{small} \begin{flushleft} @@ -67,17 +68,17 @@ Coq < \end{flushleft} \end{small} -The first line gives a banner stating the precise version of \Coq~ +The first line gives a banner stating the precise version of \Coq{} used. You should always return this banner when you report an anomaly to our bug-tracking system -\verb|http://logical.futurs.inria.fr/coq-bugs| +\url{https://coq.inria.fr/bugs/}. \chapter{Basic Predicate Calculus} \section{An overview of the specification language Gallina} A formal development in Gallina consists in a sequence of {\sl declarations} -and {\sl definitions}. You may also send \Coq~ {\sl commands} which are +and {\sl definitions}. You may also send \Coq{} {\sl commands} which are not really part of the formal development, but correspond to information requests, or service routine invocations. For instance, the command: \begin{verbatim} @@ -106,7 +107,7 @@ of the system, called respectively \verb:Prop:, \verb:Set:, and Every valid expression $e$ in Gallina is associated with a specification, itself a valid expression, called its {\sl type} $\tau(E)$. We write $e:\tau(E)$ for the judgment that $e$ is of type $E$. -You may request \Coq~ to return to you the type of a valid expression by using +You may request \Coq{} to return to you the type of a valid expression by using the command \verb:Check:: \begin{coq_eval} @@ -130,7 +131,7 @@ Check nat. The specification \verb:Set: is an abstract type, one of the basic sorts of the Gallina language, whereas the notions $nat$ and $O$ are notions which are defined in the arithmetic prelude, -automatically loaded when running the \Coq\ system. +automatically loaded when running the \Coq{} system. We start by introducing a so-called section name. The role of sections is to structure the modelisation by limiting the scope of parameters, @@ -206,7 +207,7 @@ We may optionally indicate the required type: Definition two : nat := S one. \end{coq_example} -Actually \Coq~ allows several possible syntaxes: +Actually \Coq{} allows several possible syntaxes: \begin{coq_example} Definition three := S two : nat. \end{coq_example} @@ -249,7 +250,7 @@ explicitly the type of the quantified variable. We check: Check (forall m:nat, gt m 0). \end{coq_example} We may revert to the clean state of -our initial session using the \Coq~ \verb:Reset: command: +our initial session using the \Coq{} \verb:Reset: command: \begin{coq_example} Reset Initial. \end{coq_example} @@ -340,7 +341,7 @@ assumption. \end{coq_example} The proof is now finished. We may either discard it, by using the -command \verb:Abort: which returns to the standard \Coq~ toplevel loop +command \verb:Abort: which returns to the standard \Coq{} toplevel loop without further ado, or else save it as a lemma in the current context, under name say \verb:trivial_lemma:: \begin{coq_example} @@ -414,7 +415,7 @@ backtrack one step, and more generally \verb:Undo n: to backtrack n steps. We end this section by showing a useful command, \verb:Inspect n.:, -which inspects the global \Coq~ environment, showing the last \verb:n: declared +which inspects the global \Coq{} environment, showing the last \verb:n: declared notions: \begin{coq_example} Inspect 3. @@ -429,7 +430,7 @@ their value (or proof-term) is omitted. \subsection{Conjunction} We have seen how \verb:intro: and \verb:apply: tactics could be combined -in order to prove implicational statements. More generally, \Coq~ favors a style +in order to prove implicational statements. More generally, \Coq{} favors a style of reasoning, called {\sl Natural Deduction}, which decomposes reasoning into so called {\sl introduction rules}, which tell how to prove a goal whose main operator is a given propositional connective, and {\sl elimination rules}, @@ -528,7 +529,7 @@ such a simple tautology. The reason is that we want to keep \subsection{Tauto} A complete tactic for propositional -tautologies is indeed available in \Coq~ as the \verb:tauto: tactic. +tautologies is indeed available in \Coq{} as the \verb:tauto: tactic. \begin{coq_example} Restart. tauto. @@ -555,7 +556,7 @@ The two instantiations are effected automatically by the tactic \verb:apply: when pattern-matching a goal. The specialist will of course recognize our proof term as a $\lambda$-term, used as notation for the natural deduction proof term through the Curry-Howard isomorphism. The -naive user of \Coq~ may safely ignore these formal details. +naive user of \Coq{} may safely ignore these formal details. Let us exercise the \verb:tauto: tactic on a more complex example: \begin{coq_example} @@ -579,7 +580,7 @@ argument fails. This may come as a surprise to someone familiar with classical reasoning. Peirce's lemma is true in Boolean logic, i.e. it evaluates to \verb:true: for every truth-assignment to \verb:A: and \verb:B:. Indeed the double negation -of Peirce's law may be proved in \Coq~ using \verb:tauto:: +of Peirce's law may be proved in \Coq{} using \verb:tauto:: \begin{coq_example} Abort. Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A). @@ -588,7 +589,7 @@ Qed. \end{coq_example} In classical logic, the double negation of a proposition is equivalent to this -proposition, but in the constructive logic of \Coq~ this is not so. If you +proposition, but in the constructive logic of \Coq{} this is not so. If you want to use classical logic in \Coq, you have to import explicitly the \verb:Classical: module, which will declare the axiom \verb:classic: of excluded middle, and classical tautologies such as de Morgan's laws. @@ -652,7 +653,7 @@ function and predicate symbols. \subsection{Sections and signatures} Usually one works in some domain of discourse, over which range the individual -variables and function symbols. In \Coq~ we speak in a language with a rich +variables and function symbols. In \Coq{} we speak in a language with a rich variety of types, so me may mix several domains of discourse, in our multi-sorted language. For the moment, we just do a few exercises, over a domain of discourse \verb:D: axiomatised as a \verb:Set:, and we consider two @@ -660,7 +661,7 @@ predicate symbols \verb:P: and \verb:R: over \verb:D:, of arities respectively 1 and 2. Such abstract entities may be entered in the context as global variables. But we must be careful about the pollution of our global environment by such declarations. For instance, we have already -polluted our \Coq~ session by declaring the variables +polluted our \Coq{} session by declaring the variables \verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:. \begin{coq_example} @@ -714,7 +715,7 @@ Check ex. \end{coq_example} and the notation \verb+(exists x:D, P x)+ is just concrete syntax for the expression \verb+(ex D (fun x:D => P x))+. -Existential quantification is handled in \Coq~ in a similar +Existential quantification is handled in \Coq{} in a similar fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by the proof combinator \verb:ex_intro:, which is invoked by the specific tactic \verb:Exists:, and its elimination provides a witness \verb+a:D+ to @@ -951,7 +952,7 @@ Abort. \subsection{Equality} -The basic equality provided in \Coq~ is Leibniz equality, noted infix like +The basic equality provided in \Coq{} is Leibniz equality, noted infix like \verb+x=y+, when \verb:x: and \verb:y: are two expressions of type the same Set. The replacement of \verb:x: by \verb:y: in any term is effected by a variety of tactics, such as \verb:rewrite: @@ -1208,7 +1209,7 @@ About prim_rec. Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we get an apparently more complicated expression. Indeed the type of \verb:prim_rec: is equivalent by rule $\beta$ to its expected type; this may -be checked in \Coq~ by command \verb:Eval Cbv Beta:, which $\beta$-reduces +be checked in \Coq{} by command \verb:Eval Cbv Beta:, which $\beta$-reduces an expression to its {\sl normal form}: \begin{coq_example} Eval cbv beta in @@ -1228,7 +1229,7 @@ That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n: according to its main constructor; when \verb:n = O:, we get \verb:m:; when \verb:n = S p:, we get \verb:(S rec):, where \verb:rec: is the result of the recursive computation \verb+(addition p m)+. Let us verify it by -asking \Coq~to compute for us say $2+3$: +asking \Coq{} to compute for us say $2+3$: \begin{coq_example} Eval compute in (addition (S (S O)) (S (S (S O)))). \end{coq_example} @@ -1275,7 +1276,7 @@ as subgoals the corresponding instantiations of the base case \verb:(P O): , and of the inductive step \verb+forall y:nat, P y -> P (S y)+. In each case we get an instance of function \verb:plus: in which its second argument starts with a constructor, and is thus amenable to simplification -by primitive recursion. The \Coq~tactic \verb:simpl: can be used for +by primitive recursion. The \Coq{} tactic \verb:simpl: can be used for this purpose: \begin{coq_example} simpl. @@ -1488,7 +1489,7 @@ Set Printing Width 60. \section{Opening library modules} -When you start \Coq~ without further requirements in the command line, +When you start \Coq{} without further requirements in the command line, you get a bare system with few libraries loaded. As we saw, a standard prelude module provides the standard logic connectives, and a few arithmetic notions. If you want to load and open other modules from @@ -1503,9 +1504,9 @@ Such a command looks for a (compiled) module file \verb:Arith.vo: in the libraries registered by \Coq. Libraries inherit the structure of the file system of the operating system and are registered with the command \verb:Add LoadPath:. Physical directories are mapped to -logical directories. Especially the standard library of \Coq~ is +logical directories. Especially the standard library of \Coq{} is pre-registered as a library of name \verb=Coq=. Modules have absolute -unique names denoting their place in \Coq~ libraries. An absolute +unique names denoting their place in \Coq{} libraries. An absolute name is a sequence of single identifiers separated by dots. E.g. the module \verb=Arith= has full name \verb=Coq.Arith.Arith= and because it resides in eponym subdirectory \verb=Arith= of the standard -- cgit v1.2.3 From 11bdfe88061c5bda160baec625b862a146809024 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 4 Jan 2017 19:15:26 +0100 Subject: Fixing another inconsistency when looking for camlp5o when camlp5dir is given. This was not fixed by b9a15a390f yet. --- configure.ml | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 99f5ae5424..42c2e2785d 100644 --- a/configure.ml +++ b/configure.ml @@ -514,6 +514,20 @@ let camltag = match caml_version_list with (** * CamlpX configuration *) (* Convention: we use camldir as a prioritary location for camlpX, if given *) +(* i.e., in the case of camlp5, we search for a copy of camlp5o which *) +(* answers the right camlp5 lib dir *) + +let strip_slash dir = + let n = String.length dir in + if n>0 && dir.[n - 1] = '/' then String.sub dir 0 (n-1) else dir + +let which_camlp5o_for camlp5lib = + let camlp5o = Filename.concat camlbin "camlp5o" in + let camlp5lib = strip_slash camlp5lib in + if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else + let camlp5o = which "camlp5o" in + if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else + die ("Error: cannot find Camlp5 binaries corresponding to Camlp5 library " ^ camlp5lib) let which_camlpX base = let file = Filename.concat camlbin base in @@ -528,7 +542,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with | Some dir -> if Sys.file_exists (dir/testcma) then let camlp5o = - try which_camlpX "camlp5o" + try which_camlp5o_for dir with Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" in dir, camlp5o else -- cgit v1.2.3 From 5391d15256af65a0ba0ead4ee6d1ec16f7e362cc Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 12 Jan 2017 14:03:47 +0100 Subject: Fix configure crash on some version strings of camlp5, e.g. "6.18-exp" (bug #5307). --- configure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 42c2e2785d..04b04979d9 100644 --- a/configure.ml +++ b/configure.ml @@ -563,7 +563,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with let check_camlp5_version camlp5o = let version_line, _ = run ~err:StdOut camlp5o ["-v"] in let version = List.nth (string_split ' ' version_line) 2 in - match string_split '.' version with + match numeric_prefix_list version with | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) -> printf "You have Camlp5 %s. Good!\n" version; version | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" -- cgit v1.2.3 From aa21c209f85f37b3d16ff499bbeac15e967bf78f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 13 Jan 2017 08:40:17 +0100 Subject: Fix broken .aux machinery. Coq expects aux_file_name_for to give the aux file corresponding to the input file whichever its Coq-related extension, be it .v or .vo or .vio. Commit 3e6fa1c broke this contract when fixing bug #5183. As a consequence, depending on the execution path, Coq would try to save or load from either .foo.aux or .foo.vo.aux or .foo.vio.aux. This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call chain by not initializing hints when the input file does not end with .v. This also restores 8.5 behavior with respect to aux file naming. --- ide/ide_slave.ml | 3 ++- lib/aux_file.ml | 4 ---- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 5b07d3ec3b..c0c4131ac5 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -392,7 +392,8 @@ let init = Stm.add false ~ontop:(Stm.get_current_state ()) 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) else Stm.get_current_state (), `NewTip in - Stm.set_compilation_hints file; + if Filename.check_suffix file ".v" then + Stm.set_compilation_hints file; Stm.finish (); initial_id end diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 0f0f09aa23..c6c7b42429 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -17,10 +17,6 @@ let version = 1 let oc = ref None -let chop_extension f = - if check_suffix f ".v" then chop_extension f - else f - let aux_file_name_for vfile = dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux" -- cgit v1.2.3 From 9568a34f665a6f3dca06271ffd6e914d9bd2a5ad Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 13 Jan 2017 08:42:13 +0100 Subject: Properly remove aux files in subdirectories (bug #5089). The aux file for foo/bar.v is foo/.bar.aux, not .foo/bar.aux. --- tools/coq_makefile.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index eab909f5b1..b7dd5f2a14 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -390,7 +390,7 @@ let clean sds sps = let () = if !some_vfile then let () = print "cleanall:: clean\n" in - print "\trm -f $(patsubst %.v,.%.aux,$(VFILES))\n\n" in + print "\trm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)\n\n" in print "archclean::\n"; print "\trm -f *.cmx *.o\n"; List.iter -- cgit v1.2.3 From 6424a49842ed9982c7edd1b847d88d66508f072b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 11 Jan 2017 13:59:54 +0100 Subject: Fix race condition in STM DAG generation (in debug mode). The same file name for .dot graphs could be used by concurrent processes. --- lib/system.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/lib/system.ml b/lib/system.ml index 4b99de707b..1817aed1fc 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -309,6 +309,7 @@ let with_time time f x = raise e let process_id () = - if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id - else Printf.sprintf "master:%d" (Thread.id (Thread.self ())) - + Printf.sprintf "%d:%s:%d" (Unix.getpid ()) + (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id + else "master") + (Thread.id (Thread.self ())) -- cgit v1.2.3 From 93ee722a9612d57a7928eaeb8ccede688214d158 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 16 Jan 2017 15:44:14 +0100 Subject: Fixing (part of) #5303 (clarifications around Record/Structure/Variant). - We fix the inconsistency of Structure and Record which according to doc are the same. - We improve the error message when not using { ... } for Record or Structure. --- toplevel/vernacentries.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 41ee165ff8..6736d83293 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -570,10 +570,10 @@ let vernac_inductive poly lo finite indl = | _ -> () (* dumping is done by vernac_record (called below) *) ) indl; match indl with - | [ ( _ , _ , _ ,Record, Constructors _ ),_ ] -> - CErrors.error "The Record keyword cannot be used to define a variant type. Use Variant instead." + | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] -> + CErrors.error "The Record keyword is for types defined using the syntax { ... }." | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> - CErrors.error "The Variant keyword cannot be used to define a record type. Use Record instead." + CErrors.error "The Variant keyword does not support syntax { ... }." | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> vernac_record (match b with Class _ -> Class false | _ -> b) poly finite id bl c oc fs -- cgit v1.2.3 From 23ffecc39a064775724ad524bd97f30fb8e763cd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 Jan 2017 10:47:34 +0100 Subject: STM: fix run-time classification of VernacInstance (fix #5313) --- stm/stm.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/stm/stm.ml b/stm/stm.ml index b4331dc460..f577994ffa 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2584,12 +2584,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty if not in_proof && Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - let opacity_of_produced_term = - match x.expr with + let rec opacity_of_produced_term = function (* This AST is ambiguous, hence we check it dynamically *) | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity + | VernacLocal (_,e) -> opacity_of_produced_term e | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term,[])); + VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[])); let proof_mode = default_proof_mode () in VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode; -- cgit v1.2.3 From 8d783c10d9505cbc1beb1c8e3451ea5dd567f260 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Jan 2017 11:23:48 +0100 Subject: Mapping named_context_val preserves sharing when possible. This was deactivated by 27c9346 and made an optimization moot in eauto. This optimization was physically checking for equality, but as lists where rebuilt by the mapping, this was never true. Some contribs were thus quite slower, including persistent-union-find which was twice slower. This 2-line patch fixes it by trying to preserve sharing as much as possible. Note that we should still do something about eauto, because it does redo useless work a lot whenever the environment only changes a bit, while we could cache this computation. --- kernel/pre_env.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 7be8606ef4..f211583e06 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -156,7 +156,8 @@ let map_named_val f ctxt = (accu, d') in let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in - { env_named_ctx = ctx; env_named_map = map } + if map == ctxt.env_named_map then ctxt + else { env_named_ctx = ctx; env_named_map = map } let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); -- cgit v1.2.3