/usr/share/acl2-6.5/books/fix-cert/fix-cert.lisp is in acl2-books-source 6.5-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 | (in-package "ACL2")
; fix-cert.lisp - Written by Peter Dillinger
; Copyright (C) 2007-2009 Northeastern University
; This program is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
;--------------------------------------------------------------------------
; After books have been moved, this file can update .cert files to reflect
; their new location. There are potential reliability and soundness issues
; (see make-certificate-file in ACL2 sources), but it should work fine on
; the system books.
;
; This file should be loadable with LD and should not include any books, so
; that it is available to be used even if .cert files are messed up.
(program)
(set-state-ok t)
;==========================================================================
; Code to create empty packages from those in a .cert file, so that it can
; be read.
; ch is in the middle of reading portcullis commands
(defun create-pkgs-for-cert-file1 (file1 file2 ch
known-pkgs new-pkgs-sofar
ctx state)
(mv-let
(eofp cmd state)
(state-global-let* ((infixp nil)) (read-object ch state))
(cond (eofp (ill-formed-certificate-er ctx 'create-pkgs-for-cert-file1
file1 file2))
((eq cmd :end-portcullis-cmds)
(value new-pkgs-sofar))
((and (consp cmd)
(eq (car cmd) 'defpkg)
(consp (cdr cmd))
(stringp (cadr cmd)))
(let ((pkg (cadr cmd)))
(if (member-equal pkg known-pkgs)
(create-pkgs-for-cert-file1 file1 file2 ch known-pkgs
new-pkgs-sofar ctx state)
(er-progn
(defpkg-fn pkg nil state nil nil nil
`(defpkg ,pkg nil))
(create-pkgs-for-cert-file1 file1 file2 ch known-pkgs
(cons pkg new-pkgs-sofar)
ctx state)))))
(t
(create-pkgs-for-cert-file1 file1 file2 ch known-pkgs
new-pkgs-sofar ctx state)))))
(defun set-current-package1 (val state)
(mv-let (erp v state)
(set-current-package val state)
(declare (ignore v erp))
state))
(defconst *fix-cert-suspect-book-action-alist*
'((:uncertified-okp . nil)
(:defaxioms-okp . t)
(:skip-proofs-okp . t)))
(defun create-pkgs-for-cert-file (file1 ctx state)
(let ((file2 (convert-book-name-to-cert-name file1 t)))
(mv-let
(ch state)
(open-input-channel file2 :object state)
(if (null ch)
(include-book-er file1 file2
"There is no certificate on file for ~x0."
:uncertified-okp
*fix-cert-suspect-book-action-alist*
ctx state)
(er-let*
((pkg
(state-global-let*
((infixp nil))
(chk-in-package ch file2 nil ctx state))))
(if (not (equal pkg "ACL2"))
(ill-formed-certificate-er ctx 'create-pkgs-for-cert-file{1}
file1 file2 pkg)
(state-global-let*
((current-package "ACL2" set-current-package1))
(mv-let (error-flg val state)
(mv-let
(eofp version state)
(state-global-let* ((infixp nil))
(read-object ch state))
(if (or eofp (not (stringp version)))
(ill-formed-certificate-er
ctx 'create-pkgs-for-cert-file{2} file1 file2)
(mv-let
(eofp key state)
(state-global-let* ((infixp nil))
(read-object ch state))
(if (or eofp (not (eq key :begin-portcullis-cmds)))
(ill-formed-certificate-er
ctx 'create-pkgs-for-cert-file{3} file1 file2)
(create-pkgs-for-cert-file1
file1 file2 ch
(strip-cars (known-package-alist state))
nil ctx state)))))
(pprogn (close-input-channel ch state)
(mv error-flg val state))))))))))
;==========================================================================
; Code for actually fixing certificate files based on their new location.
(defun fix-cert-fn (user-book-name dir ctx state)
;; user-book-name and dir are as given by a user to include-book
(er-let*
((dir-value
(cond (dir (include-book-dir-with-chk soft ctx dir))
(t (value (cbd))))))
(mv-let
(new-full-book-name new-directory-name-with-slash new-familiar-name)
(parse-book-name
dir-value
(prog2$ (cw "~%Fixing .cert file for ~x0~%" user-book-name)
user-book-name)
".lisp" ctx state)
(declare (ignorable new-directory-name-with-slash new-familiar-name))
(er-let*
((new-pkg-lst (create-pkgs-for-cert-file new-full-book-name ctx state))
(cert-obj (chk-certificate-file new-full-book-name
new-directory-name-with-slash
'certify-book ; gives light-chkp = t
ctx state
*fix-cert-suspect-book-action-alist* nil)))
(let* ((portcullis (cons (access cert-obj cert-obj :cmds)
(access cert-obj cert-obj :pre-alist)))
(post-alist (access cert-obj cert-obj :post-alist))
(expansion-alist (access cert-obj cert-obj :expansion-alist))
(pcert-info (access cert-obj cert-obj :pcert-info))
(expansion-alist-nonelided (and (consp pcert-info) pcert-info))
(old-full-book-name (caar post-alist))
(old-directory-name (remove-after-last-directory-separator
old-full-book-name))
(new-directory-name (remove-after-last-directory-separator
new-full-book-name)))
(if (equal old-full-book-name new-full-book-name)
(value :not-needed)
(make-certificate-file-relocated
new-full-book-name portcullis
(convert-book-name-to-cert-name new-full-book-name t)
post-alist expansion-alist expansion-alist-nonelided
old-directory-name new-directory-name
nil ctx state)))))))
; Beware that in order to create packages before they are needed,
; the order of the books to be fixed needs to satisfy the dependencies.
(defun fix-certs-fn (user-book-names dir ctx state)
(if (not (consp user-book-names))
(if (stringp user-book-names)
(fix-cert-fn user-book-names dir ctx state)
(value :done))
(mv-let (er-flag val state)
(fix-cert-fn (car user-book-names) dir ctx state)
(declare (ignore er-flag val))
(fix-certs-fn (cdr user-book-names) dir ctx state))))
(defmacro fix-cert (user-book-name-or-lst &key dir)
`(fix-certs-fn
,(if (quotep user-book-name-or-lst)
user-book-name-or-lst
`',user-book-name-or-lst)
',dir
'fix-cert
state))
; so that we can also load this book with LD without complications
(logic)
(set-state-ok nil)
|