\documentclass{article}
\addtolength\textheight{0.8cm}
\parindent 0pt
\parskip 5pt
\usepackage{xspace}
\RequirePackage{alltt}
\usepackage{casl}
\usepackage{url}
\renewcommand{\index}[1]{}
\newcommand{\QUERY}[1]
{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
\newenvironment{Grammar}
{\small% svmono sets \footnotesize to \small
\begin{alltt}}{\end{alltt}\ignorespacesafterend}
\newenvironment{AbstractGrammar}
{\par\smallskip\samepage\begin{Grammar}}{\end{Grammar}\noindent
\ignorespacesafterend}
\newenvironment{ConcreteDisplay}
{\nopagebreak\begin{quote}\casl}{\end{quote}\noindent
\ignorespacesafterend}
\newcommand{\Meta}[1]{\mbox{$\it#1$}}
\newcommand{\Metasub}[2]{\mbox{$\it#1_{#2}$}}
\newcommand{\Metasubsub}[2]{\mbox{$\scriptstyle\it#1_{#2}$}}
\newcommand{\Gram}[1]{{\textup{\texttt{#1}}}}
% \textindex{TEXT}
% - prints and marks TEXT for the main index
\newcommand{\textindex}[1]{#1\index{#1}}
% \bothindex{TEXT}{SUBTEXT}
% - marks TEXT,SUBTEXT and SUBTEXT,TEXT for the main index
\newcommand{\bothindex}[2]{\index{#1!#2}\index{#2!#1}}
% \textbothindex{TEXT}{SUBTEXT}
% - prints TEXT SUBTEX and marks both TEXT,SUBTEXT and SUBTEXT,TEXT
\newcommand{\textbothindex}[2]{#1 #2\index{#1!#2}\index{#2!#1}}
% \emphindex{TEXT}
% - prints \emph{TEXT} and marks TEXT for the main index
\newcommand{\emphindex}[1]{\emph{#1}\index{#1}}
% \gramindex{TEXT}
% - marks \Gram{TEXT} for the Symbol Index, sorted as TEXT
\newcommand{\gramindex}[1]{\texttt{#1}}
\newcommand{\CASL}{\textmd{\textsc{Casl}}\xspace }
\newcommand{\HasCASL}{\textmd{\textsc{HasCasl}}\xspace }
\newcommand{\LBCASL}{\textmd{\textsc{Lb-Casl}}\xspace }
\newcommand{\SBCASL}{\textmd{\textsc{Sb-Casl}}\xspace }
\newcommand{\CspCASL}{\textmd{\textsc{Csp-Casl}}\xspace }
\newcommand{\CspCFOL}{\textmd{\textsc{Csp}-$CFOL^=$}\xspace }
\newcommand{\CASLLtl}{\textmd{\textsc{Casl-Ltl}}\xspace }
\newcommand{\CFOLLtl}{\textmd{$CFOL^=$-\textsc{Ltl}}\xspace }
\newcommand{\CATS}{\textmd{\textsc{Cats}}\xspace }
\newcommand{\Hets}{\textmd{\textsc{Hets}}\xspace }
\newcommand{\MAYA}{\textmd{\textsc{Maya}}\xspace }
\newcommand{\HOLCASL}{\textmd{\textsc{Hol-Casl}}\xspace }
\newcommand{\ELANCASL}{\textmd{\textsc{Elan-Casl}}\xspace }
\begin{document}
\title{CASL libraries on the web}
\author{Till Mossakowski}
\date{Version 0.3\\[1ex] \today}
\maketitle
\section{What the \CASL summary says}
\begin{quote}
A library may be located at a particular \emphindex{site} on the
Internet.
The library is referenced from other sites by a name which determines
the location and perhaps identifies a particular version of the
library. To allow libraries to be relocated without this invalidating
existing references to them, library names may be interpreted relative
to a \emph{\textbothindex{global}{directory}} that maps names to URIs.
\QUERY{CASL/Summary 9, \ldots:\\
URL changed to URI.}
Libraries
may also be referenced directly by their (relative or absolute) URIs,
independently of their registration in the global directory.
\begin{AbstractGrammar}
\gramindex{LIB-NAME} ::= LIB-ID | LIB-VERSION
\gramindex{LIB-VERSION} ::= lib-version LIB-ID VERSION-NUMBER
\gramindex{VERSION-NUMBER} ::= version-number NUMBER+
\end{AbstractGrammar}
\begin{AbstractGrammar}
\gramindex{LIB-ID} ::= DIRECT-LINK | INDIRECT-LINK
\gramindex{DIRECT-LINK} ::= direct-link URI
\gramindex{INDIRECT-LINK} ::= indirect-link PATH
\end{AbstractGrammar}
A direct link to a library is simply written as the URI of the
library. The location of a library is always a directory, giving
access not only to the individual specifications defined by the
current version of the library but also to previously-defined
versions, various indexes, and perhaps other documentation.
An indirect link is written:
\begin{ConcreteDisplay}
\Metasub{FI}{1}/\ldots/\Metasub{FI}{n}
\end{ConcreteDisplay}
where each file identifier \Metasub{FI}{i} is a valid file name, as
for use in a path in a URI. An indirect link is interpreted as a URI
by the current global library directory.
\Gram{URI} and \Gram{PATH} are recognized as lexical symbols only directly
following the key words `\Gram{library}' and `\Gram{from}' in
specification libraries. The following grammar provides a minimal
syntax for \Gram{URI}: further forms may be recognized and supported.
\QUERY{The \Gram{PATH-CHAR} characters include all the `safe' and `extra'
characters, plus the `reserved' character `\Gram{:}' and the `national'
character `\Gram{\textasciitilde}'.}
%
\begin{quote}
\begin{Grammar}
\gramindex{PATH-CHAR} ::= A |...| Z | a |...| z | 0 |...| 9
| \$ | - | \_ | @ | . | & | + | ! | *
| '"' | "'" | ( | ) | , | : | \textasciitilde
| \% HEX-CHAR HEX-CHAR
\gramindex{HEX-CHAR} ::= A |...| F | a |...| f | 0 |...| 9
\gramindex{PATH-WORD} ::= PATH-CHAR ... PATH-CHAR
\gramindex{PATH} ::= PATH-WORD /.../ PATH-WORD
\gramindex{URI} ::= http:// PATH
| ftp:// PATH
| file:/// PATH
\end{Grammar}
\end{quote}
\end{quote}
\section{Proposal for implementation in the Heterogeneous Tool Set (\Hets)}
Briefly some words about what \Hets is:
\Hets (\url{http://www.tzi.de/cofi/hets}) is a tool combining various
tools for different specification languages, thus providing a tool for
a heterogeneous specification language. The structuring constructs of
this language are those of \CASL, plus some new heterogeneous
constructs like
\begin{verbatim}
logic <language-name>
\end{verbatim}
for indicating the language of the subsequent specification text.
Languages currently supported by \Hets are \CASL, \HasCASL, \CspCASL
and Haskell.
Now the proposal how to implement the \CASL library mechanism
in \Hets:
\begin{enumerate}
\item
The global directory for the indirect links is accessed by a list of
mirror sites that can be obtained from
\begin{quote}\texttt{www.cofi.info/Libraries}.\end{quote}
The
mirror sites are copied from a central server (initially
later based on the UniForm Workbench).
The central server can be accessed through an http interface.
\item
The http interface provides access to versioned libraries,
following the versioning scheme below.
The http interface is
used by \Hets (and both the http interface and \Hets should do some
caching). For directly browsing through the libraries viewcvs should
suffice. Setting up an Apache server in order to be able to use cvsweb
is too much for the moment.
\label{global-server}
\item
Direct absolute URIs are taken as such.
Direct relative URIs are written \texttt{./path}
or \texttt{../path}. They are interpreted relative to the URI
of the referencing library.
Local files can be accessed via \texttt{file://path}.
\texttt{path} must begin with a \texttt{/}
(otherwise the first name in \texttt{path} it is interpreted as a hostname).
Often, it will be more convenient to access local files
via \texttt{./path} or \texttt{../path}. Should \texttt{./path} then
also be allowed as defining library name in a local library
(and only there)?
\item
Versioning: should the location of a library be a directory
containing all the versions (which means that library
\texttt{name} in path \texttt{path} version \texttt{nnn} is accessed via \texttt{path/name/v\_nnn},
and the current version via \texttt{path/name/name}),
or should the version be appended to the name of the library (which
means that library \texttt{name} in path \texttt{path} version \texttt{nnn} is accessed via
\texttt{path/name\_v\_nnn}, and the current version
via \texttt{path/name}) ?
A decision in favour of the former approach is taken in the summary,
the main argument being all the versions and development graphs, proof
object, proof scripts etc.\ that shall be stored together with the
library. On the other hand, editing and browsing will be easier with
the latter approach, because fewer subdirectories have to be entered.
Moreover, many other specification and programming
language take the latter approach, and their integration into \Hets
should be eased. Hence, the following reconcilation of the appraoches
is proposed:
\begin{quote}
A CASL library is stored in a file ending ``.casl''. A directory having
the same name (but without the ending) contains previously-defined
versions of the library, various indexes, tool-generated information
and perhaps other documentation.
\end{quote}
For files with a language-specific module mechanism, a language-specific
ending is chosen (e.g.\ ``.hs'' for Haskell).
For heterogeneous libraries, the ending is ``.het''\footnote{``.spec''
is already reserved for RPM specification files, and Emacs comes
with a standard mode for these.}, indicating that the needed
logic(s) have to specified within the library itself.
\item The versioning is realized in cvs with tags\footnote{Probably, viewcvs
orders tags alphabetically. This coincides with the intended lexikographic version
ordering only if main version numbers are not greater than 9.} , one for each version
(note that one cannot use cvs version numbers, because they are numbered
consecutively, while \CASL version numbers are chosen by the user).
The versioning scheme shall be supported by a shell script that in
connection with cvs automatically generates all available
versions, named by the above versioning scheme.
This solution uses more disk space than a dynamic checkout
of individual version via cgi scripts. However, the advantage
is that the versioning scheme is simple, such that it also
can be simulated by people who want to provide access to their
libraries via direct links but who do not want to install cgi
scripts or use cvs: they can just manually create the needed directories
and files. (By constrast, using cgi scripts would require
a different versioning scheme, with the file name and version
number added as parameters to the URL, using, say, ?name and ?version.)
A further advantage is that it is easy to store
development graphs, proof object, proof scripts
together with the particular libray version they belong to.
\item What happens if different versions of the same specification
are imported (via different import paths)? At least, \Hets
should issue a warning. But still the user could get confused
by the fact that (s)he has to work with, say, two different
copies of \texttt{Nat} and cannot interchange theorems and proofs
between the two copies. Hence, an alternative might be to
require global version numbers for each package of libraries.
Here, a package is a collection of libraries needed for a specific
project, or a standard package like the collection of libraries
of basic datatypes. \Hets should provide some means of
specifying which libraries belong to a package.
Packages ease the download of library versions that
together form a consistent global configuration. It would be bad if
the user who does not want to use latest versions but rather particular
fixed versions would have to care about the fact that say StructuredDatatypes
version 0.9 uses Numbers version 0.7, and therefore (s)he also should use
Numbers version 0.7 when importing StructuredDatatypes version 0.9 in order
to avoid having two different copies of the Numbers. It is much easier
if the Basic Datatypes have global version numbers which are the same
for each library, such that StructuredDatatypes version 0.9 uses
Numbers version 0.9. Actually, we are following this policy already
for the Basic Datatypes, but it would be easier if also \Hets would
support some kind of configuration management along these lines.
cvs uses tags for this, and since these shall correspond to \CASL
version numbers, perhaps a package is just a cvs project or folder
in such a project, and we just should provide a mechanism for
globally tagging such a folder, which would mean that not only
the cvs tag is set, but also the version numbers used in the CASL
libraries are updated accordingly.
Note that this is a tools issue that should not affect the summary.
\item URNs are not needed: the syntax of usual URIs suffices, and moreover,
these are directly understood by browsers and web servers.
%\item We should have a look at VSE to get feeling for a realistic system
%(however, VSE does not have version control).
%Unfortunately, currently, VSE needs Solaris 5 or SunOS 5.6. In Bremen, we only have Solaris 8 and 9.
\end{enumerate}
\section*{Acknowledgements}
Thanks to Christoph L\"uth, Klaus L\"uttich, Achim Mahnke and Peter D.\ Mosses for
useful discussions and comments on earlier versions of this note.
\end{document}