# Changeset 7

Ignore:
Timestamp:
Jun 15, 2010, 10:58:48 PM (8 years ago)
Message:

ispelled

File:
1 edited

### Legend:

Unmodified
 r6 technological infrastructure for the advertisement and dissemination of the research results of \cerco{}, and it must also provide the means for direct communication and resource sharing among parterns. Moreover, UNIBO will provide communication and resource sharing among partners. Moreover, UNIBO will provide to the other partners the Matita interactive theorem prover that will be used to obtain the certified \cerco{} compiler. We expect to make Matita evolve during the software repository. These services are discussed in Sections~\ref{site} and~\ref{repo}. We installed on it the \emph{stable} version of the Debian distribution of Linux in order to maximize version of the Debian distribution of Linux in order to maximise availability. \item[cbs.helm.cs.unibo.it] This virtual machine hosts the continuous building project members only. To maximize fault tolerance, we configured the server with RAID 5, so that the loss of one hard disk does not compromize the data. Morevoer, we provide incremental nighly backups of all the sensible data and we store the backups To maximise fault tolerance, we configured the server with RAID 5, so that the loss of one hard disk does not compromise the data. Moreover, we provide incremental nightly backups of all the sensible data and we store the backups on a different physical machine. The main motivation is to be able to recover accidentally deleted files or old machine configurations. Bologna) that can also be used for \cerco{} development. We discuss now the implementation of the Web Site'', Softare Repository and We discuss now the implementation of the Web Site'', Software Repository and Continuous Building System. \section{Project Web Site'' (Trac)}\label{site} In order to ease the creation of a community around the \cerco{} prototype, it was decided to prefer a Wiki-centered solution to a traditional Web Site. Our choice has been to install a personalized version of the 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). Trac provides in an integrated and lightweight solution: \item An issue tracking system that subsumes a bug tracking system and provides a basic control over the project advancement. \item An on-line, simplified Web interface to the softare repository. \item An on-line, simplified Web interface to the software repository. \item A flexible system of plug-ins to add new functionalities or modify the beaviour of the basic ones. the behaviour of the basic ones. \end{enumerate} By means of additional plug-ins, we have integrated the public part of the Wiki with a private one. The private part is meant to integrate the mailing list in facilitating the discussion between the project developers. Moreover, since it is integrated with the softare repository and Issue tracking systems, since it is integrated with the software repository and Issue tracking systems, it is possible to create hyper-links to or to embed in discussion pages both code fragments and description of issues. \section{Software Repository}\label{repo} After considering several alternatives, it was decided to use a centralized After considering several alternatives, it was decided to use a centralised software repository for the \cerco{} project, and we installed 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 software to mirror the centralized repository. software to mirror the centralised repository. The repository is open in read mode to anonymous users, and in write mode to \section{Continuous Building System}\label{cbs} In \cerco{} we will develp both certified code (in Matita) and standard one In \cerco{} we will develop both certified code (in Matita) and standard one (mainly in OCaml). We plan to adopt traditional testing methods (e.g. unit testing) to control bug regressions in the standard code, while the certified code will be checked by asking Matita to verify all the definitions and proofs of correctness. The last operation in particular can require quite a lot of time (in the order of at most a few hours), expecially if proof automation will time (in the order of at most a few hours), especially if proof automation will 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 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 to avoid the possibility of introducing a bug that jeopardize the whole to avoid the possibility of introducing a bug that jeopardise the whole project or that will later require other changes before the next official release of Matita). regressions. Development branches are encouraged on personal copies of the repository (using git-svn), but are discouraged on the central repository. \item Every night the CBS virtual machine is bringed back to a pristine \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 code, compiles the code of Matita, verifies the standard library, all