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
|
<html>
<head><title>PATHNAME.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>PATHNAME</h2>introduction to filename conventions in ACL2
<pre>Major Section: <a href="BOOKS.html">BOOKS</a>
</pre><p>
The notion of pathname objects from Common Lisp is not supported in
ACL2, nor is the function <code>pathname</code>. However, ACL2 supports file
operations, using conventions for naming files based on those of the
Unix (trademark of AT&T) operating system, so that the character <code>/</code>
is used to terminate directory names. Some file names are ``absolute''
(complete) descriptions of a file or directory; others are
``relative'' to the current working directory or to the connected
book directory (see <a href="CBD.html">cbd</a>). We emphasize that even for users of
Windows-based systems or Macintosh computers, ACL2 file names are in
the Unix style. We will call these <em>ACL2 pathnames</em>, often
omitting the ``ACL2.''
<p>
Pathnames starting with the directory separator (<code>/</code>) are absolute
pathnames. All other pathnames are relative pathnames. An
exception is in the Microsoft Windows operating system, where the
drive may be included, e.g., <code>"c:/home/smith/acl2/book-1.lisp"</code>.
In fact, the drive <em>must</em> be included in the portcullis of a book;
see <a href="PORTCULLIS.html">portcullis</a>.<p>
Consider the following examples. The filename string
<pre>
"/home/smith/acl2/book-1.lisp"
</pre>
is an absolute pathname, with top-level directory <code>"home"</code>,
under that the directory <code>"smith"</code> and then the directory
<code>"acl2"</code>, and finally, within that directory the file
<code>"book-1.lisp"</code>. If the connected book directory is
<code>"/home/smith/"</code> (see <a href="CBD.html">cbd</a>), then the filename string above
also corresponds to the relative filename string "acl2/book1.lisp".
<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>
|
