Changeset 8 for Deliverables/D6.1/report.tex

Timestamp:

Jun 15, 2010, 11:27:04 PM (10 years ago)

Author:

sacerdot

Message:

Final version of D6.1.

File:

• Deliverables/D6.1/report.tex (modified) (15 diffs)

Deliverables/D6.1/report.tex

@@ -1 +1 @@
 \documentclass[11pt,epsf,a4wide]{article}
-%\usepackage[a4paper=true,  bookmarks=true, linkcolor=black, citecolor=black, urlcolor=black,colorlinks=true,pagecolor=black, breaklinks=true, bookmarksopen=true]{hyperref}
-\usepackage{latexsym, amssymb, amsfonts}
-%\usepackage{equation}
 \usepackage{../style/cerco}
 
-%\addtolength{\topmargin}{-1.7cm}
-%\addtolength{\oddsidemargin}{-1.5cm}
-%\addtolength{\evensidemargin}{-1.5cm}
-%\addtolength{\textwidth}{3cm}
-%\addtolength{\textheight}{3.4cm}
-
-\title{INFORMATION AND COMMUNICATION TECHNOLOGIES\\
+\title{
+INFORMATION AND COMMUNICATION TECHNOLOGIES\\
 (ICT)\\
 PROGRAMME\\
@@ -20 +12 @@
 
 \begin{document}
+\thispagestyle{empty}
+
+\vspace*{-1cm}
+\begin{center}
+\includegraphics[width=0.6\textwidth]{cerco_logo.png}
+\end{center}
+
+\begin{minipage}{\textwidth}
 \maketitle
-
-\thispagestyle{empty}
-
-
-%\vspace*{-1cm}
-%\begin{center}
-%\includegraphics[width=0.6\textwidth]{istlogo.eps}
-%\end{center}
-%\centerline{\epsfbox[width=0.8\textwidth]{istlogo.eps}}
+\end{minipage}
+
 
 \vspace*{0.5cm}
@@ -36 +29 @@
 \bf
 Report n. D6.1\\
-Project Wet Site and Software Repository
+Project Web Site and Software Repository\\
 \end{LARGE} 
 \end{center}
 
 \vspace*{2cm}
+\begin{center}
+\begin{large}
+Version 1.0
+\end{large}
+\end{center}
+
+\vspace*{0.5cm}
 \begin{center}
 \begin{large}
@@ -48 +48 @@
 \end{center}
 
-\vspace*{6cm}
+\vspace*{\fill}
 \noindent
 Project Acronym: \cerco{}\\
@@ -54 +54 @@
 Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
 
-\newpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
+\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
 
 \tableofcontents
@@ -77 +77 @@
 research results of \cerco{}, and it must also provide the means for direct
 communication and resource sharing among partners. Moreover, UNIBO will provide
-to the other partners the Matita interactive theorem prover that will be used
+to the other partners the Matita\cite{matita} interactive theorem prover that will be used
 to obtain the certified \cerco{} compiler. We expect to make Matita evolve during
 the project timeframe in order to fix bugs that are critical for \cerco{} and in
@@ -85 +85 @@
 introduction. Therefore, we plan to achieve a strict integration between
 the technological infrastructure for the development of Matita and the one for
-\cerco{}.
+\cerco.
 
 In order to target the previous
@@ -100 +100 @@
 \begin{description}
  \item[cerco.cs.unibo.it] This virtual machine hosts the ``project web site''
-   (actually, a Trac instance) and
+   (actually, a Trac instance~\cite{trac}) and
    the software repository. These services are discussed in
    Sections~\ref{site} and~\ref{repo}. We installed on it the \emph{stable}
@@ -109 +109 @@
    We installed on it the \emph{unstable} version of the Debian distribution
    in order to immediately exploit the most recent developments of the software
-   library that will be used in \cerco{}.
+   library that will be used in \cerco.
  \item[maelstrom.helm.cs.unibo.it] This is the development virtual machine of
-   \cerco{}. It is open to all project participants in order to do remote
+   \cerco. It is open to all project participants in order to do remote
    development and testing in a controlled environment that has all the
-   required libraries and tools. It is also base on the \emph{unstable} version
-   of the Debian distribution.
+   required libraries and tools. It is also based on the \emph{unstable} version
+   of the Debian distribution and it is configured with all the libraries
+   required by Matita and the OCaml ones we plan to use for CerCo .
 \end{description}
 
@@ -139 +140 @@
 was decided to prefer a Wiki-centred solution to a traditional Web Site.
 Our choice has been to install a personalised version of the
-Integrated SCM \& Project Management tool Trac (http://trac.edgewall.org).
+Integrated SCM \& Project Management tool Trac~\cite{trac}, accessible at
+\url{http://cerco.cs.unibo.it}.
 Trac provides in an integrated and lightweight solution:
  \begin{enumerate}
@@ -159 +161 @@
 \section{Software Repository}\label{repo}
 After considering several alternatives, it was decided to use a centralised
-software repository for the \cerco{} project, and we installed Subversion on the
+software repository for the \cerco{} project, and we installed Subversion~\cite{subversion} on the
 \cerco{} server. Project members that prefer a distributed solution or that are
 used to work without network connectivity are advised to use the svn-git
@@ -177 +179 @@
 be heavily used in Matita to reduce the proving effort. Moreover, as already
 explained, we expect to observe a continuous evolution of Matita (and its
-standard library) to parallel the development of the \cerco{}. Each change in
+standard library) to parallel the development of the \cerco. Each change in
 the code of Matita must trigger not only the checking for regressions on the
 \cerco{} code, but also on all the existent developments made in Matita (in order
@@ -191 +193 @@
 the \cerco{} prototype. Performance checks are meaningful only if systematically
 repeated always on the same machine and with reproducible load conditions. 
-Hence we put up an ad-hoc continuous building system for Matita+CerCo that
+Hence we put up an ad-hoc continuous building system for Matita+\cerco{} that
 supports the following workflow:
 \begin{itemize}
@@ -201 +203 @@
    repository (using git-svn), but are discouraged on the central repository.
  \item Every night the CBS virtual machine is brought back to a pristine
-   condition and a script checks-out the latest version of the Matita and CerCo
+   condition and a script checks-out the latest version of the Matita and \cerco{}
    code, compiles the code of Matita, verifies the standard library, all
-   the contribs of Matita and the certified CerCo code, and run all the
+   the contribs of Matita and the certified \cerco{} code, and run all the
    regression tests on both the certified and un-certified code. All faults
    are recorded, as well as the performance of Matita on each source file.
@@ -244 +246 @@
 \cerco{} prototype. 
 
+\begin{thebibliography}{9}
+\bibitem{matita} The Interactive Theorem Prover Matita,
+ \url{http://matita.cs.unibo.it}
+\bibitem{subversion}The Version Control System Subversion,
+ \url{http://subversion.apache.org}
+\bibitem{trac}The Integrated SCM \& Project Management tool Trac,
+ \url{http://trac.edgewall.org}
+\end{thebibliography}
+
 \end{document}