← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/doc/top.lisp

  • 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/doc/top.lisp
29
29
; Original author: Jared Davis <jared@centtech.com>
30
30
 
31
31
(in-package "ACL2")
32
 
(set-inhibit-warnings "ttags")
33
32
 
34
33
(make-event
35
34
 
45
44
   (value '(value-triple nil))))
46
45
 
47
46
(include-book "centaur/misc/memory-mgmt" :dir :system)
48
 
(value-triple (set-max-mem (* 10 (expt 2 30))))
 
47
(value-triple (set-max-mem (* 4 (expt 2 30))))
49
48
 
50
49
(include-book "relnotes")
51
50
(include-book "practices")
81
80
(include-book "centaur/clex/example" :dir :system)
82
81
(include-book "centaur/nrev/demo" :dir :system)
83
82
 
84
 
(include-book "cgen/top" :dir :system)
85
 
 
86
83
(include-book "centaur/defrstobj/defrstobj" :dir :system)
87
84
 
88
85
(include-book "centaur/esim/stv/stv-top" :dir :system)
103
100
 
104
101
(include-book "centaur/satlink/top" :dir :system)
105
102
(include-book "centaur/satlink/check-config" :dir :system)
 
103
(include-book "centaur/satlink/benchmarks" :dir :system)
 
104
 
 
105
(include-book "centaur/depgraph/top" :dir :system)
 
106
 
 
107
(include-book "centaur/quicklisp/top" :dir :system)
106
108
 
107
109
(include-book "centaur/misc/top" :dir :system)
108
110
(include-book "centaur/misc/smm" :dir :system)
113
115
(include-book "centaur/misc/load-stobj-tests" :dir :system)
114
116
(include-book "centaur/misc/count-up" :dir :system)
115
117
(include-book "centaur/misc/fast-alist-pop" :dir :system)
 
118
(include-book "centaur/misc/spacewalk" :dir :system)
116
119
 
117
120
;; BOZO conflicts with something in 4v-sexpr?
118
121
 
159
162
(include-book "centaur/vl/transforms/xf-propagate" :dir :system)
160
163
(include-book "centaur/vl/transforms/xf-expr-simp" :dir :system)
161
164
(include-book "centaur/vl/transforms/xf-inline" :dir :system)
162
 
(include-book "centaur/vl/mlib/sub-counts" :dir :system)
163
165
 
164
166
;; BOZO these are incompatible?  which is right?
165
167
(include-book "centaur/vl/util/prefix-hash" :dir :system)
170
172
 
171
173
(include-book "hacking/all" :dir :system)
172
174
(include-book "hints/consider-hint" :dir :system)
 
175
 
 
176
(include-book "ordinals/e0-ordinal" :dir :system)
 
177
 
173
178
(include-book "tools/do-not" :dir :system)
174
179
(include-book "tools/plev" :dir :system)
175
180
(include-book "tools/plev-ccl" :dir :system)
199
204
 
200
205
(include-book "centaur/fty/deftypes" :dir :system)
201
206
 
 
207
(include-book "misc/find-lemmas" :dir :system)
 
208
(include-book "misc/simp" :dir :system)
 
209
(include-book "misc/without-waterfall-parallelism" :dir :system)
 
210
(include-book "misc/with-waterfall-parallelism" :dir :system)
 
211
(include-book "misc/seq" :dir :system)
 
212
(include-book "misc/seqw" :dir :system)
 
213
 
 
214
(include-book "centaur/memoize/old/profile" :dir :system)
 
215
(include-book "centaur/memoize/old/watch" :dir :system)
 
216
 
 
217
; The following include-book causes a name conflict for set-equal, which is
 
218
; defined both in arithmetic-5/lib/basic-ops/building-blocks.lisp and in
 
219
; data-structures/set-defuns.lisp.  So for now, at least, it is commented out.
 
220
; (include-book "data-structures/top" :dir :system)
 
221
 
 
222
;Put ACL2s doc last, since ccg.lisp inclusion might cause problems -- harshrc
 
223
(include-book "acl2s/doc" :dir :system)
 
224
 
202
225
#||
203
226
 
204
227
;; This is a nice place to put include-book scanner hacks that trick cert.pl
235
258
 
236
259
||#
237
260
 
 
261
(defpointer assocs patbind-assocs)
 
262
 
238
263
; Historically we had a completely ad-hoc organization that grew organically as
239
264
; topics were added.  This turned out to be a complete mess.  To make the
240
265
; manual more approachable and relevant, we now try to impose a better
241
266
; hierarchy and add some context.
242
267
 
 
268
(defxdoc acl2::|Building the ACL2+Books Manual|
 
269
  :parents (documentation)
 
270
  :short "How to build the ACL2+Books Manual."
 
271
 
 
272
  :long "<p>If you just want to get a copy of the ACL2+Books manual for local
 
273
viewing, you probably <b>don't need to build it yourself</b> because you can
 
274
just <a href='download/'>download</a> a copy.</p>
 
275
 
 
276
 
 
277
<h4>Quick Instructions</h4>
 
278
 
 
279
<p>This should work on CCL on Linux and Mac OS X.  It <b>may not work</b> for
 
280
other OS/Lisp combinations.  In particular, building the manual requires some
 
281
features from @(see oslib) and @(see quicklisp) that may not be available on
 
282
other systems; see <a href='https://github.com/acl2/acl2/issues/189'>Issue
 
283
189</a>.</p>
 
284
 
 
285
<p>You need a copy of <b>ACL2(h)</b>.  Then, just run:</p>
 
286
 
 
287
@({
 
288
    cd acl2-sources/books
 
289
    make manual ACL2=my-acl2h
 
290
})
 
291
 
 
292
<p>The resulting manual may be found in:</p>
 
293
 
 
294
@({
 
295
    acl2-sources/books/doc/manual/index.html
 
296
})
 
297
 
 
298
<p>For more detailed instructions, see @(see books-certification).</p>
 
299
 
 
300
<h4>Other Manuals</h4>
 
301
 
 
302
<p>See @(see acl2::acl2-doc) for details about how to build your own
 
303
Emacs-based manual.</p>
 
304
 
 
305
<p>See @(see xdoc::save) for general information about how to build and
 
306
distribute custom XDOC manuals.  For instance, you can build manuals that are
 
307
extended to cover proprietary libraries.</p>")
 
308
 
 
309
 
243
310
(defsection arithmetic
244
311
  :parents (top)
245
312
  :short "Libraries for reasoning about basic arithmetic, bit-vector
358
425
; have XDOC topics for their parents.  So, get them all loaded and converted
359
426
; into proper XDOC topics, then move them around where we want them.
360
427
 
 
428
#+acl2-legacy-doc
361
429
(xdoc::import-acl2doc)
362
430
 
363
431
(include-book "xdoc/topics" :dir :system)
369
437
; we'll do them globally, so they'll be included, e.g., in the Emacs version of
370
438
; the combined manual.
371
439
(xdoc::change-parents ihs (arithmetic))
372
 
(xdoc::change-parents data-definitions (macro-libraries projects debugging))
373
 
(xdoc::change-parents with-timeout (data-definitions))
374
 
(xdoc::change-parents data-structures (macro-libraries))
 
440
; data-definitions went away.  It might be reasonable to place with-timeout
 
441
; under defdata, if that still exists.
 
442
;(xdoc::change-parents data-definitions (macro-libraries projects debugging))
 
443
;(xdoc::change-parents with-timeout (data-definitions))
 
444
;(xdoc::change-parents testing (cgen))
 
445
;; (xdoc::change-parents data-structures (macro-libraries))
375
446
(xdoc::change-parents hacker (interfacing-tools))
376
447
(xdoc::change-parents witness-cp (proof-automation))
377
 
(xdoc::change-parents testing (debugging))
 
448
 
378
449
 
379
450
(xdoc::change-parents leftist-trees (projects))
380
451
(xdoc::change-parents ltree-sort (leftist-trees))
381
452
(xdoc::change-parents how-many-lt (leftist-trees))
382
453
 
383
454
(xdoc::change-parents consideration (hints))
384
 
(xdoc::change-parents do-not-hint (hints))
385
455
(xdoc::change-parents untranslate-patterns (macros user-defined-functions-table))
386
456
 
387
457
#!XDOC
425
495
     (xdoc::change-parents bdd (boolean-reasoning proof-automation))
426
496
     (xdoc::change-parents books (top))
427
497
 
428
 
     ;; bozo where should this go... Matt suggests maybe interfacing-tools?
429
 
     ;; But by the same token, maybe programming, maybe lots of places...
430
 
     (xdoc::change-parents unsound-eval (miscellaneous))
431
 
 
432
498
     ))
433
499
 
434
500
(local
564
630
      "new-doc.lsp")
565
631
     (xdoc::save "./manual"
566
632
                 :import nil
567
 
                 :redef-okp t
568
 
                 :expand-level 2)
 
633
                 :redef-okp t)
569
634
     (value `(value-triple :manual)))))
570
635
 
571
636
 
606
671
 
607
672
 
608
673
(collect-topics-with-name 'acl2::add-listfix-rule (get-xdoc-table (w state)))
609
 
||#
 
 
b'\\ No newline at end of file'
 
674
||#