Changeset 8 for Deliverables/D6.1/report.tex
- Timestamp:
- Jun 15, 2010, 11:27:04 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D6.1/report.tex
r7 r8 1 1 \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}5 2 \usepackage{../style/cerco} 6 3 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{ 5 INFORMATION AND COMMUNICATION TECHNOLOGIES\\ 14 6 (ICT)\\ 15 7 PROGRAMME\\ … … 20 12 21 13 \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} 22 22 \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 32 25 33 26 \vspace*{0.5cm} … … 36 29 \bf 37 30 Report n. D6.1\\ 38 Project We t Site and Software Repository31 Project Web Site and Software Repository\\ 39 32 \end{LARGE} 40 33 \end{center} 41 34 42 35 \vspace*{2cm} 36 \begin{center} 37 \begin{large} 38 Version 1.0 39 \end{large} 40 \end{center} 41 42 \vspace*{0.5cm} 43 43 \begin{center} 44 44 \begin{large} … … 48 48 \end{center} 49 49 50 \vspace*{ 6cm}50 \vspace*{\fill} 51 51 \noindent 52 52 Project Acronym: \cerco{}\\ … … 54 54 Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\ 55 55 56 \ newpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}56 \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881} 57 57 58 58 \tableofcontents … … 77 77 research results of \cerco{}, and it must also provide the means for direct 78 78 communication and resource sharing among partners. Moreover, UNIBO will provide 79 to the other partners the Matita interactive theorem prover that will be used79 to the other partners the Matita\cite{matita} interactive theorem prover that will be used 80 80 to obtain the certified \cerco{} compiler. We expect to make Matita evolve during 81 81 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 86 86 the technological infrastructure for the development of Matita and the one for 87 \cerco {}.87 \cerco. 88 88 89 89 In order to target the previous … … 100 100 \begin{description} 101 101 \item[cerco.cs.unibo.it] This virtual machine hosts the ``project web site'' 102 (actually, a Trac instance ) and102 (actually, a Trac instance~\cite{trac}) and 103 103 the software repository. These services are discussed in 104 104 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 110 110 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. 112 112 \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 remote113 \cerco. It is open to all project participants in order to do remote 114 114 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 . 117 118 \end{description} 118 119 … … 139 140 was decided to prefer a Wiki-centred solution to a traditional Web Site. 140 141 Our choice has been to install a personalised version of the 141 Integrated SCM \& Project Management tool Trac (http://trac.edgewall.org). 142 Integrated SCM \& Project Management tool Trac~\cite{trac}, accessible at 143 \url{http://cerco.cs.unibo.it}. 142 144 Trac provides in an integrated and lightweight solution: 143 145 \begin{enumerate} … … 159 161 \section{Software Repository}\label{repo} 160 162 After considering several alternatives, it was decided to use a centralised 161 software repository for the \cerco{} project, and we installed Subversion on the163 software repository for the \cerco{} project, and we installed Subversion~\cite{subversion} on the 162 164 \cerco{} server. Project members that prefer a distributed solution or that are 163 165 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 178 180 explained, we expect to observe a continuous evolution of Matita (and its 179 standard library) to parallel the development of the \cerco {}. Each change in181 standard library) to parallel the development of the \cerco. Each change in 180 182 the code of Matita must trigger not only the checking for regressions on the 181 183 \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 192 194 repeated always on the same machine and with reproducible load conditions. 193 Hence we put up an ad-hoc continuous building system for Matita+ CerCothat195 Hence we put up an ad-hoc continuous building system for Matita+\cerco{} that 194 196 supports the following workflow: 195 197 \begin{itemize} … … 201 203 repository (using git-svn), but are discouraged on the central repository. 202 204 \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 CerCo205 condition and a script checks-out the latest version of the Matita and \cerco{} 204 206 code, compiles the code of Matita, verifies the standard library, all 205 the contribs of Matita and the certified CerCocode, and run all the207 the contribs of Matita and the certified \cerco{} code, and run all the 206 208 regression tests on both the certified and un-certified code. All faults 207 209 are recorded, as well as the performance of Matita on each source file. … … 244 246 \cerco{} prototype. 245 247 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 246 257 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.