# Changeset 8

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

Final version of D6.1.

Location:
Deliverables
Files:
2 edited

### Legend:

Unmodified
 r7 \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\\ \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} \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} \end{center} \vspace*{6cm} \vspace*{\fill} \noindent Project Acronym: \cerco{}\\ 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 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 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 \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} 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} 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} \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 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 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} 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. \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}