1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
<html>
<head><title>FULL-BOOK-NAME.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>FULL-BOOK-NAME</h2>book naming conventions assumed by ACL2
<pre>Major Section: <a href="BOOKS.html">BOOKS</a>
</pre><p>
For this discussion we assume that the resident operating system is
Unix (trademark of AT&T), but analogous remarks apply to other
operating systems supported by ACL2, in particular, the Macintosh
operating system where `<code>:</code>' plays roughly the role of `<code>/</code>' in
Unix; see <a href="PATHNAME.html">pathname</a>.<p>
ACL2 defines a ``full book name'' to be an ``absolute filename
string,'' that may be divided into contiguous sections: a
``directory string'', a ``familiar name'' and an ``extension''.
See <a href="PATHNAME.html">pathname</a> for the definitions of ``absolute,'' ``filename
string,'' and other notions pertaining to naming files. Below we
exhibit the three sections of one such string:
<pre>
"/usr/home/smith/project/arith.lisp"<p>
"/usr/home/smith/project/" ; directory string
"arith" ; familiar name
".lisp" ; extension
<p>
</pre>
The sections are marked by the rightmost slash and rightmost dot,
as shown below.
<pre>
"/usr/home/smith/project/arith.lisp"
| |
slash dot
| |
"/usr/home/smith/project/" ; directory string
"arith" ; familiar name
".lisp" ; extension
</pre>
The directory string includes (and terminates with) the rightmost
slash. The extension includes (and starts with) the rightmost dot.
The dot must be strictly to the right of the slash so that the
familiar name is well-defined and nonempty.<p>
If you are using ACL2 on a system in which file names do not have
this form, please contact the authors and we'll see what we can do
about generalizing ACL2's conventions.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
