Changeset 7


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

ispelled

File:
1 edited

Legend:

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

    r6 r7  
    7676technological infrastructure for the advertisement and dissemination of the
    7777research results of \cerco{}, and it must also provide the means for direct
    78 communication and resource sharing among parterns. Moreover, UNIBO will provide
     78communication and resource sharing among partners. Moreover, UNIBO will provide
    7979to the other partners the Matita interactive theorem prover that will be used
    8080to obtain the certified \cerco{} compiler. We expect to make Matita evolve during
     
    103103   the software repository. These services are discussed in
    104104   Sections~\ref{site} and~\ref{repo}. We installed on it the \emph{stable}
    105    version of the Debian distribution of Linux in order to maximize
     105   version of the Debian distribution of Linux in order to maximise
    106106   availability.
    107107 \item[cbs.helm.cs.unibo.it] This virtual machine hosts the continuous building
     
    122122project members only.
    123123
    124 To maximize fault tolerance, we configured the server with RAID 5, so that
    125 the loss of one hard disk does not compromize the data. Morevoer, we provide
    126 incremental nighly backups of all the sensible data and we store the backups
     124To maximise fault tolerance, we configured the server with RAID 5, so that
     125the loss of one hard disk does not compromise the data. Moreover, we provide
     126incremental nightly backups of all the sensible data and we store the backups
    127127on a different physical machine. The main motivation is to be able to recover
    128128accidentally deleted files or old machine configurations.
     
    132132Bologna) that can also be used for \cerco{} development.
    133133
    134 We discuss now the implementation of the ``Web Site'', Softare Repository and
     134We discuss now the implementation of the ``Web Site'', Software Repository and
    135135Continuous Building System.
    136136
    137137\section{Project ``Web Site'' (Trac)}\label{site}
    138138In order to ease the creation of a community around the \cerco{} prototype, it
    139 was decided to prefer a Wiki-centered solution to a traditional Web Site.
    140 Our choice has been to install a personalized version of the
     139was decided to prefer a Wiki-centred solution to a traditional Web Site.
     140Our choice has been to install a personalised version of the
    141141Integrated SCM \& Project Management tool Trac (http://trac.edgewall.org).
    142142Trac provides in an integrated and lightweight solution:
     
    146146  \item An issue tracking system that subsumes a bug tracking system and
    147147    provides a basic control over the project advancement.
    148   \item An on-line, simplified Web interface to the softare repository.
     148  \item An on-line, simplified Web interface to the software repository.
    149149  \item A flexible system of plug-ins to add new functionalities or modify
    150     the beaviour of the basic ones.
     150    the behaviour of the basic ones.
    151151 \end{enumerate}
    152152By means of additional plug-ins, we have integrated the public part of the
    153153Wiki with a private one. The private part is meant to integrate the mailing
    154154list in facilitating the discussion between the project developers. Moreover,
    155 since it is integrated with the softare repository and Issue tracking systems,
     155since it is integrated with the software repository and Issue tracking systems,
    156156it is possible to create hyper-links to or to embed in discussion pages
    157157both code fragments and description of issues.
    158158
    159159\section{Software Repository}\label{repo}
    160 After considering several alternatives, it was decided to use a centralized
     160After considering several alternatives, it was decided to use a centralised
    161161software repository for the \cerco{} project, and we installed Subversion on the
    162162\cerco{} server. Project members that prefer a distributed solution or that are
    163163used to work without network connectivity are advised to use the svn-git
    164 software to mirror the centralized repository.
     164software to mirror the centralised repository.
    165165
    166166The repository is open in read mode to anonymous users, and in write mode to
     
    169169
    170170\section{Continuous Building System}\label{cbs}
    171 In \cerco{} we will develp both certified code (in Matita) and standard one
     171In \cerco{} we will develop both certified code (in Matita) and standard one
    172172(mainly in OCaml). We plan to adopt traditional testing methods (e.g. unit
    173173testing) to control bug regressions in the standard code, while the certified
    174174code will be checked by asking Matita to verify all the definitions and proofs
    175175of correctness. The last operation in particular can require quite a lot of
    176 time (in the order of at most a few hours), expecially if proof automation will
     176time (in the order of at most a few hours), especially if proof automation will
    177177be heavily used in Matita to reduce the proving effort. Moreover, as already
    178178explained, we expect to observe a continuous evolution of Matita (and its
     
    180180the code of Matita must trigger not only the checking for regressions on the
    181181\cerco{} code, but also on all the existent developments made in Matita (in order
    182 to avoid the possibility of introducing a bug that jeopardize the whole
     182to avoid the possibility of introducing a bug that jeopardise the whole
    183183project or that will later require other changes before the next official
    184184release of Matita).
     
    200200   regressions. Development branches are encouraged on personal copies of the
    201201   repository (using git-svn), but are discouraged on the central repository.
    202  \item Every night the CBS virtual machine is bringed back to a pristine
     202 \item Every night the CBS virtual machine is brought back to a pristine
    203203   condition and a script checks-out the latest version of the Matita and CerCo
    204204   code, compiles the code of Matita, verifies the standard library, all
Note: See TracChangeset for help on using the changeset viewer.