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
|
; To reproduce the results shown in the paper, get the following files from
; this directory
; tjvm.lisp
; examples.lisp
; tjvm-examples.lisp
; mod-1-property.lisp
; report.lisp
; The top level results are in report.lisp.
; The Makefile allows you to type make to certify all the books. Otherwise,
; you can follow the original instructions, included here now:
; To recertify all these books, edit the form below, replacing the full
; path names by the full path of the directory on which you have down loaded
; these files. Then execute the expression below in an ACL2 in which the
; connected book directory is set to the full path name of that directory.
(ld '(
(certify-book "defpun")
(ubt! 1)
(DEFPKG "TJVM"
(set-difference-equal
(union-eq '(ASSOC-EQUAL LEN NTH ZP SYNTAXP
QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<)
(union-eq *acl2-exports*
*common-lisp-symbols-from-main-lisp-package*))
'(PC PROGRAM PUSH POP REVERSE STEP ++)))
(certify-book "tjvm" 1)
(ubt! 1)
(include-book "/dir/tjvm")
(certify-book "examples" 1)
(ubt! 1)
(include-book "/dir/examples")
(certify-book "tjvm-examples" 1)
(ubt! 1)
(certify-book "mod-1-property")
(ubt! 1)
(certify-book "report")
(ubt! 1))
:ld-pre-eval-print t)
|
