<commit_before>\documentclass[11pt,a4paper]{book}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{pslatex}

\input{../common/version.tex}
\input{../common/macros.tex}
\input{../common/title.tex}

%\makeindex

\begin{document}
\coverpage{A Tutorial}{<NAME>, <NAME> and <NAME>}{}

%\tableofcontents

\chapter*{Getting started}

\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
on many architectures.
%, and mainly on Unix machines. 
It is available with a variety of user interfaces. The present
document does not attempt to present a comprehensive view of all the
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.
Bertot and <NAME> on practical uses of the \Coq{} system.

We assume here that the potential user has installed \Coq~ on his workstation,
that he calls \Coq~ from a standard teletype-like shell window, and that
he does not use any special interface.
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}.

In the following, all examples preceded by the prompting sequence
\verb:Coq < : represent user input, terminated by a period. The
following lines usually show \Coq's answer as it appears on the users
screen. 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:

\begin{small}
\begin{flushleft}
\begin{verbatim}
unix:~> coqtop
Welcome to Coq 8.0 (Mar 2004)

Coq < 
\end{verbatim}<commit_msg>Mention de coqide, proof general et pcoq<commit_after>\documentclass[11pt,a4paper]{book}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{pslatex}

\input{../common/version.tex}
\input{../common/macros.tex}
\input{../common/title.tex}

%\makeindex

\begin{document}
\coverpage{A Tutorial}{<NAME>, <NAME> and <NAME>}{}

%\tableofcontents

\chapter*{Getting started}

\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
on many architectures.
%, and mainly on Unix machines. 
It is available with a variety of user interfaces. The present
document does not attempt to present a comprehensive view of all the
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.
Bertot and <NAME> on practical uses of the \Coq{} system.

Coq can be used from a standard teletype-like shell window but
preferably through the graphical user interface
CoqIde\footnote{Alternative graphical interfaces exist: Proof General
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}.

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. 

The following lines usually show \Coq's answer as it appears on the
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~
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:

\begin{small}
\begin{flushleft}
\begin{verbatim}
unix:~> coqtop
Welcome to Coq 8.0 (Mar 2004)

Coq < 
\end{verbatim}
{'fraction_non_alphanumeric': 0.07245753601376048, 'fraction_numerical': 0.004730165555794453, 'mean_word_length': 4.714987714987715, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5184385', 'n_tokens_mistral': 1354, 'n_tokens_neox': 1255, 'n_words': 633}