diff --git a/doc/api.tex b/doc/api.tex new file mode 100644 index 0000000000000000000000000000000000000000..4b7610a4a02a328d62b60fd58e82664d40134bde --- /dev/null +++ b/doc/api.tex @@ -0,0 +1,15 @@ +\chapter{The Why3 Application Programming Interface} + +\section{Building Terms and Formulas} + +\section{Building Theories} + +\section{Buildings Tasks and calling External Provers} + +\section{Applying transformations} + +%%% Local Variables: +%%% mode: latex +%%% TeX-PDF-mode: t +%%% TeX-master: "manual" +%%% End: diff --git a/doc/ide.tex b/doc/ide.tex index b861f3ff0f5ac2986239e6e9156235ec75c52d6a..c427062d33e3a6a6f5c265b34d1d278bf9d71fcc 100644 --- a/doc/ide.tex +++ b/doc/ide.tex @@ -3,3 +3,10 @@ \section{IDE} hello + + +%%% Local Variables: +%%% mode: latex +%%% TeX-PDF-mode: t +%%% TeX-master: "manual" +%%% End: diff --git a/doc/manpages.tex b/doc/manpages.tex new file mode 100644 index 0000000000000000000000000000000000000000..82e5fbe6b9e1c08aba95833fe4a8a019759cc9a3 --- /dev/null +++ b/doc/manpages.tex @@ -0,0 +1,18 @@ +\chapter{Reference manuals for the Why3 tools} + +\section{Compilation, Installation} + +\section{The \texttt{why.conf} configuration file} + +\section{The \texttt{why3} command-line tool} + +\section{The \texttt{why3ml} tool} + +\section{The \texttt{why3ide} tool} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-PDF-mode: t +%%% TeX-master: "manual" +%%% End: diff --git a/doc/manual.tex b/doc/manual.tex index c821794125701b08cf5f4e3b00e1731b4429b3c0..2225c4d1a4272f9121afea009e94438c28127f7e 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -2,8 +2,26 @@ \begin{document} -\chapter{Syntax} +\title{Why3 manual} +\author{F. Bobot \and J.-C. Filli\^atre \and C. March\'e \and A. Paskevich} +\maketitle + +\cleardoublepage + +\tableofcontents + +\input{syntax.tex} \input{ide.tex} +\input{api.tex} + +\input{manpages.tex} + \end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-PDF-mode: t +%%% TeX-master: t +%%% End: diff --git a/doc/syntax.tex b/doc/syntax.tex new file mode 100644 index 0000000000000000000000000000000000000000..c8cb199c6a47ca4944909d8b62fda0f57dda80cb --- /dev/null +++ b/doc/syntax.tex @@ -0,0 +1,15 @@ +\chapter{Syntax} + +This chapter describes the input syntax, and informally gives its semantics, +illustrated by examples. + +\section{Terms and Formulas} + +\section{Declarations, Theories} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-PDF-mode: t +%%% TeX-master: "manual" +%%% End: