36 % - prints and marks TEXT for the main index
40 % - marks TEXT,SUBTEXT and SUBTEXT,TEXT for the main index
48 % - prints \emph{TEXT} and marks TEXT for the main index
53 % - marks \Gram{TEXT} for the Symbol Index, sorted as TEXT
72 \title{CASL libraries on the web}
78 \section{What the \CASL summary says}
81 A library may be located at a particular \emphindex{site} on the
84 the location and perhaps identifies a particular version of the
92 independently of their registration in the global directory.
105 A direct link to a library is simply written as the URI of the
107 access not only to the individual specifications defined by the
108 current version of the library but also to previously-defined
117 by the current global library directory.
121 following the key words `\Gram{library}' and `\Gram{from}' in
124 \QUERY{The \Gram{PATH-CHAR} characters include all the `safe' and `extra' 
125 characters, plus the `reserved' character `\Gram{:}' and the `national' 
148 \section{Proposal for implementation in the Heterogeneous Tool Set (\Hets)}
161 for indicating the language of the subsequent specification text.
165 Now the proposal how to implement the \CASL library mechanism
170 The global directory for the indirect links is accessed by a list of
176 later based on the UniForm Workbench). 
181 following the versioning scheme below.
183 used by \Hets (and both the http interface and \Hets should do some
184 caching). For directly browsing through the libraries viewcvs should
186 is too much for the moment.
192 or \texttt{../path}. They are interpreted relative to the URI
193 of the referencing library.
197 (otherwise the first name in \texttt{path} it is interpreted as a hostname).
205 Versioning: should the location of a library be a directory
206 containing all the versions (which means that library
208 and the current version via \texttt{path/name/name}), 
209 or should the version be appended to the name of the library (which
211 \texttt{path/name\_v\_nnn}, and the current version
214 A decision in favour of the former approach is taken in the summary,
215 the main argument being all the versions and development graphs, proof
216 object, proof scripts etc.\ that shall be stored together with the
217 library. On the other hand, editing and browsing will be easier with
218 the latter approach, because fewer subdirectories have to be entered. 
220 language take the latter approach, and their integration into \Hets
221 should be eased. Hence, the following reconcilation of the appraoches
226    the same name (but without the ending) contains previously-defined
227    versions of the library, various indexes, tool-generated information
233 For heterogeneous libraries, the ending is ``.het''\footnote{``.spec''
235 with a standard mode for these.}, indicating that the needed
236 logic(s) have to specified within the library itself.
239 orders tags alphabetically. This coincides with the intended lexikographic version
242 consecutively, while \CASL version numbers are chosen by the user).
245 versions, named by the above versioning scheme.
247 of individual version via cgi scripts. However, the advantage
248 is that the versioning scheme is simple, such that it also
251 scripts or use cvs: they can just manually create the needed directories
253 a different versioning scheme, with the file name and version
254 number added as parameters to the URL, using, say, ?name and ?version.)
257 together with the particular libray version they belong to.
259 \item What happens if different versions of the same specification
261 should issue a warning. But still the user could get confused
262 by the fact that (s)he has to work with, say, two different
264 between the two copies. Hence, an alternative might be to
267 project, or a standard package like the collection of libraries
271 Packages ease the download of library versions that
273 the user who does not want to use latest versions but rather particular
274 fixed versions would have to care about the fact that say StructuredDatatypes
277 to avoid having two different copies of the Numbers. It is much easier
278 if the Basic Datatypes have global version numbers which are the same
281 for the Basic Datatypes, but it would be easier if also \Hets would
287 the cvs tag is set, but also the version numbers used in the CASL
290 Note that this is a tools issue that should not affect the summary.
294 \item URNs are not needed: the syntax of usual URIs suffices, and moreover,

Indexes created Tue Jul 24 14:28:13 CEST 2018