Changeset 8


Ignore:
Timestamp:
Jun 15, 2010, 11:27:04 PM (7 years ago)
Author:
sacerdot
Message:

Final version of D6.1.

Location:
Deliverables
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D6.1/report.tex

    r7 r8  
    11\documentclass[11pt,epsf,a4wide]{article}
    2 %\usepackage[a4paper=true,  bookmarks=true, linkcolor=black, citecolor=black, urlcolor=black,colorlinks=true,pagecolor=black, breaklinks=true, bookmarksopen=true]{hyperref}
    3 \usepackage{latexsym, amssymb, amsfonts}
    4 %\usepackage{equation}
    52\usepackage{../style/cerco}
    63
    7 %\addtolength{\topmargin}{-1.7cm}
    8 %\addtolength{\oddsidemargin}{-1.5cm}
    9 %\addtolength{\evensidemargin}{-1.5cm}
    10 %\addtolength{\textwidth}{3cm}
    11 %\addtolength{\textheight}{3.4cm}
    12 
    13 \title{INFORMATION AND COMMUNICATION TECHNOLOGIES\\
     4\title{
     5INFORMATION AND COMMUNICATION TECHNOLOGIES\\
    146(ICT)\\
    157PROGRAMME\\
     
    2012
    2113\begin{document}
     14\thispagestyle{empty}
     15
     16\vspace*{-1cm}
     17\begin{center}
     18\includegraphics[width=0.6\textwidth]{cerco_logo.png}
     19\end{center}
     20
     21\begin{minipage}{\textwidth}
    2222\maketitle
    23 
    24 \thispagestyle{empty}
    25 
    26 
    27 %\vspace*{-1cm}
    28 %\begin{center}
    29 %\includegraphics[width=0.6\textwidth]{istlogo.eps}
    30 %\end{center}
    31 %\centerline{\epsfbox[width=0.8\textwidth]{istlogo.eps}}
     23\end{minipage}
     24
    3225
    3326\vspace*{0.5cm}
     
    3629\bf
    3730Report n. D6.1\\
    38 Project Wet Site and Software Repository
     31Project Web Site and Software Repository\\
    3932\end{LARGE}
    4033\end{center}
    4134
    4235\vspace*{2cm}
     36\begin{center}
     37\begin{large}
     38Version 1.0
     39\end{large}
     40\end{center}
     41
     42\vspace*{0.5cm}
    4343\begin{center}
    4444\begin{large}
     
    4848\end{center}
    4949
    50 \vspace*{6cm}
     50\vspace*{\fill}
    5151\noindent
    5252Project Acronym: \cerco{}\\
     
    5454Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
    5555
    56 \newpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
     56\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
    5757
    5858\tableofcontents
     
    7777research results of \cerco{}, and it must also provide the means for direct
    7878communication and resource sharing among partners. Moreover, UNIBO will provide
    79 to the other partners the Matita interactive theorem prover that will be used
     79to the other partners the Matita\cite{matita} interactive theorem prover that will be used
    8080to obtain the certified \cerco{} compiler. We expect to make Matita evolve during
    8181the project timeframe in order to fix bugs that are critical for \cerco{} and in
     
    8585introduction. Therefore, we plan to achieve a strict integration between
    8686the technological infrastructure for the development of Matita and the one for
    87 \cerco{}.
     87\cerco.
    8888
    8989In order to target the previous
     
    100100\begin{description}
    101101 \item[cerco.cs.unibo.it] This virtual machine hosts the ``project web site''
    102    (actually, a Trac instance) and
     102   (actually, a Trac instance~\cite{trac}) and
    103103   the software repository. These services are discussed in
    104104   Sections~\ref{site} and~\ref{repo}. We installed on it the \emph{stable}
     
    109109   We installed on it the \emph{unstable} version of the Debian distribution
    110110   in order to immediately exploit the most recent developments of the software
    111    library that will be used in \cerco{}.
     111   library that will be used in \cerco.
    112112 \item[maelstrom.helm.cs.unibo.it] This is the development virtual machine of
    113    \cerco{}. It is open to all project participants in order to do remote
     113   \cerco. It is open to all project participants in order to do remote
    114114   development and testing in a controlled environment that has all the
    115    required libraries and tools. It is also base on the \emph{unstable} version
    116    of the Debian distribution.
     115   required libraries and tools. It is also based on the \emph{unstable} version
     116   of the Debian distribution and it is configured with all the libraries
     117   required by Matita and the OCaml ones we plan to use for CerCo .
    117118\end{description}
    118119
     
    139140was decided to prefer a Wiki-centred solution to a traditional Web Site.
    140141Our choice has been to install a personalised version of the
    141 Integrated SCM \& Project Management tool Trac (http://trac.edgewall.org).
     142Integrated SCM \& Project Management tool Trac~\cite{trac}, accessible at
     143\url{http://cerco.cs.unibo.it}.
    142144Trac provides in an integrated and lightweight solution:
    143145 \begin{enumerate}
     
    159161\section{Software Repository}\label{repo}
    160162After considering several alternatives, it was decided to use a centralised
    161 software repository for the \cerco{} project, and we installed Subversion on the
     163software repository for the \cerco{} project, and we installed Subversion~\cite{subversion} on the
    162164\cerco{} server. Project members that prefer a distributed solution or that are
    163165used to work without network connectivity are advised to use the svn-git
     
    177179be heavily used in Matita to reduce the proving effort. Moreover, as already
    178180explained, we expect to observe a continuous evolution of Matita (and its
    179 standard library) to parallel the development of the \cerco{}. Each change in
     181standard library) to parallel the development of the \cerco. Each change in
    180182the code of Matita must trigger not only the checking for regressions on the
    181183\cerco{} code, but also on all the existent developments made in Matita (in order
     
    191193the \cerco{} prototype. Performance checks are meaningful only if systematically
    192194repeated always on the same machine and with reproducible load conditions.
    193 Hence we put up an ad-hoc continuous building system for Matita+CerCo that
     195Hence we put up an ad-hoc continuous building system for Matita+\cerco{} that
    194196supports the following workflow:
    195197\begin{itemize}
     
    201203   repository (using git-svn), but are discouraged on the central repository.
    202204 \item Every night the CBS virtual machine is brought back to a pristine
    203    condition and a script checks-out the latest version of the Matita and CerCo
     205   condition and a script checks-out the latest version of the Matita and \cerco{}
    204206   code, compiles the code of Matita, verifies the standard library, all
    205    the contribs of Matita and the certified CerCo code, and run all the
     207   the contribs of Matita and the certified \cerco{} code, and run all the
    206208   regression tests on both the certified and un-certified code. All faults
    207209   are recorded, as well as the performance of Matita on each source file.
     
    244246\cerco{} prototype.
    245247
     248\begin{thebibliography}{9}
     249\bibitem{matita} The Interactive Theorem Prover Matita,
     250 \url{http://matita.cs.unibo.it}
     251\bibitem{subversion}The Version Control System Subversion,
     252 \url{http://subversion.apache.org}
     253\bibitem{trac}The Integrated SCM \& Project Management tool Trac,
     254 \url{http://trac.edgewall.org}
     255\end{thebibliography}
     256
    246257\end{document}
  • Deliverables/style/cerco.sty

    r6 r8  
    33\pdfcompresslevel9
    44\usepackage[pdftex]{graphicx}
     5\usepackage{latexsym, amssymb, amsfonts}
    56
    67\usepackage[a4paper=true,  bookmarks=true, linkcolor=black, citecolor=black, urlcolor=black,colorlinks=true,pagecolor=black, breaklinks=true, bookmarksopen=true]{hyperref}
Note: See TracChangeset for help on using the changeset viewer.