path: root/doc/Changes.tex

\documentclass[11pt]{article}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}

\input{./title}
\input{./macros}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Changes 6.3.1 ===> 7.0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\shorttitle{Changes from {\Coq} V6.3.1 to {\Coq} V7}

This document describes the main differences between Coq V7 and
V6.3.1. This new version of Coq is characterized by fixed bugs, and
improvement of implicit arguments synthesis and speed in tactic
applications.

\section{Changes overview}

The new major version number is explained by a deep restructuration of
the implementation code of Coq. From a user point of view, Coq V7 is
characterized by the following novelties:

\begin{itemize}
\item A mini-language to write tactics with high-level
pattern-matching on goals  (see section \ref{Tactics})

\item A primitive let-in constructions (see section \ref{Metatheory})
\item Structuration of the name space and access to names by the dot notation (see section \ref{Metatheory})
\item A command to export theories to XML to be used with rendering
tools by Bologna University (see section \ref{Tools})
\item Various improvements, including a search facilities by pattern
provided by Yves Bertot (see section \ref{Tools})
\item As usual, several bugs fixed and a lot of new ones introduced
\end{itemize}

Incompatibilities are described in section
\ref{Incompatibilities}. Please notice that extraction and the
{\texttt Program/Realizer} tactic are unavailable in Coq V7.
Developpers of tactics in ML are invited to read section
\ref{Developers}.

\section{Tactics}
\label{Tactics}
\def\ltac{{\cal L}_{tac}}

\begin{description}

\item[The main novelty is $\ltac$,] a mini-language contributed
by David Delahaye to write tactics with high-level pattern-matching on
goals. A separate documentation entitled $\ltac$ is available
in the archive or at the author page
http://logical.inria.fr/~delahaye.


\item[Other changes]

  \begin{itemize}

  \item {\texttt Tauto} and {\texttt Intuition} has been rewritten in
$\ltac$. This has introduced some changes in the hypotheses names
generated by {\texttt Intuition}. The previous versions of {\texttt
Tauto} and {\texttt Intuition} remains available under the names ???.\\

  \item	Redondant or incompatible instantiations in {\texttt
  Apply ... with ...} now correctly trapped

  \end{itemize}

  \item[Program/Realizer] is unavailable in Coq V7.

\end{description}

\section{Toplevel commands}

\begin{description}
    
\item[New searching mechanism by pattern] contributed by Yves Bertot

\begin{itemize}

\item {\texttt SearchPattern {\term}.}

This command displays the name and type of all theorems of the current
context whose statement's conclusion matches the expression {\term}
where holes in the latter are denoted by ``{\texttt ?}''.

\begin{coq_example}
Require Arith.
SearchPattern (plus ? ?)=?.
\end{coq_example}

Patterns need not be linear: you can express that the same
expression must occur in two places by using indexed `{\texttt ?}''.

\begin{coq_example}
Require Arith.
SearchPattern (plus ?1 ?)=?1.
\end{coq_example}

\item {\texttt SearchRewrite {\term}.}

This command displays the name and type of all theorems of the current
context whose statement's conclusion is an equality of which one side matches
the expression {\term =}. Holes in {\term} are denoted by ``{\texttt ?}''.

\begin{coq_example}
Require Arith.
SearchRewrite (plus ? ?).
\end{coq_example}
\end{itemize}

\begin{Variants}
\item {\tt SearchPattern {\term} inside {\module$_1$}...{\module$_n$}}\\
  This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.

\item {\tt SearchPattern {\term} outside {\module}.}\\
  This restricts the search to constructions not defined in modules
{\module$_1$}...{\module$_n$}.

\item {\tt SearchRewrite {\term} inside
{\module$_1$}...{\module$_n$}.}\\
  This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}.

\item {\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.}\\
  This restricts the search to constructions not defined in modules {\module$_1$}...{\module$_n$}.

\end{Variants}

\item {\texttt Search {\ident}} has been extended to accept qualified
identifiers and the {\tt inside} and {\tt outside} restrictions as
{\texttt SearchPattern} and {\texttt SearchRewrite}.

\end{description}

\section{Language}
\label{Language}

\subsection{Names}

\begin{description}

\item[Structured absolute names] The naming strategy for constructions
has been made clearer. A Coq name is now unique and has the form

\begin{quote}
{\texttt Coq.Init.Logic.Equality.eq}
\end{quote}

{\texttt eq} is the name of the construction.

{\texttt Coq} means {\texttt eq} is a construction of the standard library of
Coq.

{\texttt Init} means it is defined in directory {\texttt Init} of the
standard library of Coq.

{\texttt Logic} means it is defined in file {\texttt Logic.v} of the
directory {\texttt Init} in the standard library of Coq.

{\texttt Equality} means it is defined in section {\texttt Equality}
of the file {\texttt Logic.v} in the directory {\texttt Init} of the
standard library of Coq.

Of course, there is no limit to the number of directory to traverse to
find the corresponding file and no limit to the number of section to
traverse in the file to find the corresponding definition.

\item[Dot notation] Almost all commands accept the ``.'' notation to
write absolute names.

\item[Open mechanism] Usually all required modules ({\texttt .vo}
files) and closed sections are ``open'' by default. This means that
constructions there can be accessed just by their identifier.


\item[Bug] with identifiers ended by a number greater than $2^{31}$ fixed.

\end{description}

\section{Tools}
\label{Tools}

\begin{description}

\item[Consistency check for {\texttt .vo} files] A check-sum test
avoids to require inconsistent {\texttt .vo} files.

\item[Optimal compiler] If your architecture supports it, the native
version of {\texttt coqtop} and {\texttt coqc} is used by default.

\item[Miscellaneous]

\begin{itemize}
\item {\texttt do\_Makefile} is now called {\texttt coq\_makefile}.

\end{itemize}
\end{description}

\section{Incompatibilities}
\label{Incompatibilities}

  You could have to modify your vernacular source for the following
  reasons:

  \begin{itemize}
 
  \item {\texttt Intuition} now remove true hypotheses.

  \item In all cases, the ``.vo'' files are not compatible and should
  be recompiled.

  \item[Extraction] is currently unavailable in Coq V7.

  \item[Program/Realizer] tactics are currently unavailable in Coq V7.

  \item[Linear] tactic is discontinued.

  \end{itemize}

\section{New users contributions}

  \begin{description}

  \item[Binary Decision Diagrams] provided by Kumar Verma (Dyade)

  \item[A distributed reference counter] (part of a
  garbage collector) provided by Jean Duprat (ENS-Lyon)

\end{description}

\section{Installation procedure}

\subsection{Uninstalling Coq}

\paragraph{Warning} 
It is strongly recommended to clean-up the V6.3 Coq library directory
before you install the new version.
Use the option to coqtop \texttt{-uninstall} that will remove
the binaries and the library files of Coq V6.3 on a Unix system.

\subsection{OS Issues -- Requirements}

\subsubsection{Unix users}
You need Objective Caml version 2.01 or later, and the corresponding 
Camlp4 version to compile the system. Both are available by anonymous ftp
at: \\
\verb|ftp://ftp.inria.fr/Projects/Cristal|.
\bigskip

\noindent
Binary distributions are available for the following architectures:

\bigskip
\begin{tabular}{l|c|r}
{\bf OS } & {\bf Processor} & {name of the package}\\
\hline
Linux & 80386 and higher & coq-6.3.1-Linux-i386.tar.gz \\
Solaris & Sparc & coq-6.3.1-solaris-sparc.tar.gz\\
Digital & Alpha & coq-6.3.1-OSF1-alpha.tar.gz\\
\end{tabular}
\bigskip

There is also rpm packages for Linux.

\bigskip

If your configuration is in the above list, you don't need to install
Caml and Camlp4 and to compile the system: 
just download the package and install the binaries in the right place.

\subsubsection{MS Windows users}

A binary distribution is available for PC under MS Windows 95/98/NT.
The package is named coq-6.3.1-win.zip.

For installation information see the 
files INSTALL.win and README.win.

\end{document}

% Local Variables: 
% mode: LaTeX
% TeX-master: t
% End: 


% $Id$