diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-01-19 14:23:51 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-01-19 14:23:51 +0100 |
commit | f22969902223ab54f56f25583b24dc27c4cd6f4e (patch) | |
tree | 09c893b1dd14c9b2b38067a01486fc61452d0209 | |
parent | 34c19354c9997621a40ad053a2a12edcd8c5b5e4 (diff) | |
parent | 8d783c10d9505cbc1beb1c8e3451ea5dd567f260 (diff) |
Merge branch 'v8.6'
-rw-r--r-- | CHANGES | 10 | ||||
-rw-r--r-- | Makefile.doc | 6 | ||||
-rw-r--r-- | configure.ml | 24 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86_abs_ocaml.bat | 10 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86_installer.bat | 8 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86_installer_32.bat | 8 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat | 10 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86beta1_installer.bat | 8 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86beta1_installer_32.bat | 8 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat | 10 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86rc1_installer.bat | 8 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_86rc1_installer_32.bat | 8 | ||||
-rw-r--r-- | doc/refman/RefMan-syn.tex | 2 | ||||
-rw-r--r-- | doc/tutorial/Tutorial.tex | 61 | ||||
-rw-r--r-- | ide/ide_slave.ml | 3 | ||||
-rw-r--r-- | kernel/byterun/coq_interp.c | 63 | ||||
-rw-r--r-- | kernel/pre_env.ml | 3 | ||||
-rw-r--r-- | lib/aux_file.ml | 4 | ||||
-rw-r--r-- | lib/system.ml | 7 | ||||
-rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 11 | ||||
-rw-r--r-- | stm/stm.ml | 6 | ||||
-rw-r--r-- | tools/coq_makefile.ml | 2 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 6 |
23 files changed, 215 insertions, 71 deletions
@@ -7,6 +7,16 @@ Tactics functional extensionality in H supposed to be a quantified equality until giving a bare equality. +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 ============================== diff --git a/Makefile.doc b/Makefile.doc index cdd9852e8..9ae20ba76 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: diff --git a/configure.ml b/configure.ml index f75bbb538..48e167c99 100644 --- a/configure.ml +++ b/configure.ml @@ -12,10 +12,10 @@ open Printf let coq_version = "trunk" -let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of +let coq_macos_version = "8.6.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) -let vo_magic = 8591 -let state_magic = 58591 +let vo_magic = 8691 +let state_magic = 58691 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] @@ -509,6 +509,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 @@ -523,7 +537,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 @@ -544,7 +558,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" 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 000000000..50483c4d4 --- /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 000000000..263520ff1 --- /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 000000000..14921dd7c --- /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
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 000000000..914c332f4 --- /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 000000000..76a5bb35a --- /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 000000000..f53232b65 --- /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_coq32_86beta1_inst ^
+ -destcoq=%ROOTPATH%\coq32_86beta1_inst
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 000000000..c0669f01d --- /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 000000000..66234ebbd --- /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 000000000..96f43e16a --- /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_coq32_86rc1_inst ^
+ -destcoq=%ROOTPATH%\coq32_86rc1_inst
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 1fcc1c0df..21c39de96 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*} diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 973a0b75e..0d537256b 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 diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 48fd0a93e..ae3dcd94a 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -393,7 +393,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/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 5dec3b785..af89712d5 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; } diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 72de2f1a6..d14a254d3 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -157,7 +157,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); diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 17f55330d..1b6651a55 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" diff --git a/lib/system.ml b/lib/system.ml index 74dd224a0..e0e2c829d 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 ())) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 0d4be72d9..fc988a2c5 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -391,7 +391,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 *) @@ -525,7 +526,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 diff --git a/stm/stm.ml b/stm/stm.ml index f7569d257..6f34c8dbc 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; diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index eab909f5b..b7dd5f2a1 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 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8ce13c69a..a2f2ded32 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -571,10 +571,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 |