← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2007/dillinger-et-al/code/Readme.lsp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2007/dillinger-et-al/code/Readme.lsp
 
1
; NOTE: This directory has been superseded by directory books/hacking/
 
2
; of the ACL2 release.
 
3
 
 
4
((:FILES "
 
5
.:
 
6
Makefile
 
7
Readme.lsp
 
8
all.acl2
 
9
all.lisp
 
10
bridge.acl2
 
11
bridge.lisp
 
12
certify-all.lsp
 
13
defcode-macro.acl2
 
14
defcode-macro.lisp
 
15
defcode.acl2
 
16
defcode.lisp
 
17
defstruct-parsing.acl2
 
18
defstruct-parsing.lisp
 
19
hacker-pkg.lsp
 
20
hacker.acl2
 
21
hacker.lisp
 
22
raw.acl2
 
23
raw.lisp
 
24
redefun.acl2
 
25
redefun.lisp
 
26
rewrite-code.acl2
 
27
rewrite-code.lisp
 
28
subsumption.acl2
 
29
subsumption.lisp
 
30
table-guard.acl2
 
31
table-guard.lisp
 
32
"
 
33
)
 
34
 (:TITLE    "Hacking & Extending ACL2")
 
35
 (:AUTHOR/S "Peter C. Dillinger") ; With guidance & advice from Matt Kaufmann and Panagiotis Manolios
 
36
 (:KEYWORDS ; non-empty list of keywords, case-insensitive
 
37
   "book contributions" "contributed books"
 
38
   "hacking" "system" "defcode" "redefun" "trust tags" "ttags"
 
39
   "extensions" "raw mode" "raw lisp"
 
40
   )
 
41
 (:ABSTRACT
 
42
"NOTE: This directory has been superseded by directory books/hacking/
 
43
of the ACL2 release.
 
44
 
 
45
This support code is intended as a library to those who wish to use
 
46
trust tags to modify or extend core ACL2 behavior.  We add some other
 
47
constructs to the set of low-level tools enabled by trust tags that make
 
48
system modifications easier to specify and keep track of.  We also offer
 
49
some high-level tools that offer significant benefits (in both ease &
 
50
soundness) over more direct methods of overriding behavior.  See the
 
51
comments in Readme.lsp and individual files for more info.
 
52
")
 
53
 (:PERMISSION ; author/s permission for distribution and copying:
 
54
"Copyright (C) 2007 Peter C. Dillinger, the Georgia Tech Research Corporation,
 
55
                    and Northeastern University
 
56
 
 
57
This program is free software; you can redistribute it and/or
 
58
modify it under the terms of the GNU General Public License
 
59
as published by the Free Software Foundation; either version 2
 
60
of the License, or (at your option) any later version.
 
61
 
 
62
This program is distributed in the hope that it will be useful,
 
63
but WITHOUT ANY WARRANTY; without even the implied warranty of
 
64
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
65
GNU General Public License for more details.
 
66
 
 
67
You should have received a copy of the GNU General Public License
 
68
along with this program; if not, write to the Free Software
 
69
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
 
70
02110-1301, USA."))
 
71
 
 
72
#|
 
73
Supporting materials for "Hacking & Extending ACL2" for 2007 ACL2 Workshop
 
74
 
 
75
By Peter Dillinger
 
76
With guidance & advice from Matt Kaufmann and Panagiotis Manolios
 
77
 
 
78
Note that the tops of most of these files will look funny unless edited in
 
79
ACL2s.  The "preamble" (which generates the .acl2 file) is embedded in a
 
80
special comment in the .lisp file.
 
81
 
 
82
 
 
83
certify-all.lsp
 
84
    ACL2 input to certify all these books
 
85
 
 
86
hacker-pkg.lsp
 
87
    Package & documentation topic/section used in preambles
 
88
 
 
89
 
 
90
all.lisp
 
91
    Book that includes all of the below
 
92
 
 
93
bridge.lisp
 
94
    Book for bridging the gap between ACL2 and raw Lisp
 
95
 
 
96
defcode.lisp
 
97
    Book for the DEFCODE construct (ttag required)
 
98
 
 
99
defcode-macro.lisp
 
100
    Used internally in defcode.lisp
 
101
 
 
102
defstruct-parsing.lisp
 
103
    Book for parsing defstruct calls
 
104
 
 
105
hacker.lisp
 
106
    Basic book with hacking constructs
 
107
 
 
108
raw.lisp
 
109
    Book for making raw definitions in a nice way
 
110
 
 
111
redefun.lisp
 
112
    Book for overriding and rewriting existing definitions
 
113
 
 
114
rewrite-code.lisp
 
115
    Book with tools for rewriting and copying existing code
 
116
    (used by redefun.lisp)
 
117
 
 
118
subsumption.lisp
 
119
    Book with constructs to do ttag subsumption
 
120
 
 
121
table-guard.lisp
 
122
    An example application of this stuff to allow extension of table
 
123
    guards, including the acl2-defaults-table.
 
124
|#