[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: Problem to get a Function Admitted by ACL2
From: |
Camm Maguire |
Subject: |
[Gcl-devel] Re: Problem to get a Function Admitted by ACL2 |
Date: |
12 Dec 2003 10:01:53 -0500 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
Greetings!
>camm,
>can you give a few more details about what exactly you want to do?
>Maybe the function definition that was rejected would be useful.
Unfortunately I doubt my attempted function would be of much use to
anyone. I was looking into the possibility of shipping working,
pre-built .cert files for acl2's "books" in the Debian ACL2 package.
Its quite simple in principle if I can navigate around ACL2's
restrictions on lisp:
;; in other-events.lisp...
(defun new-alist (alist old new)
(let (new-list)
(do ((al alist (cdr al)))
((not (consp al))
(let ((res (nreverse new-list)))
(when al
(setf (cdr (last res)) al))
res))
(let ((a (car al)))
(cond ((consp a)
(push (new-alist a old new) new-list))
((and (stringp a)
(> (length a) (length old))
(equal old (subseq a 0 (length old))))
(push (concatenate 'string new (subseq a (length old)))
new-list))
(t
(push a new-list)))))))
(defun make-certificate-file-with-final-path (file portcullis post-alist1
post-alist2 state old new)
(let* ((certification-file (convert-book-name-to-cert-name file))
(post-alist3 (mark-local-included-books post-alist1 post-alist2))
;;;
;;; only changed lines are below
;;;
(certification-file (concatenate 'string certification-file ".final"))
(post-alist3 (lisp::new-alist post-alist3 old new)))
;; rest same as make-certificate-file
;; ......
))
;; Then in certify-book-fn:
;; ....
(er-progn
(make-certificate-file full-book-name
portcullis
post-alist1
post-alist2
state)
(let ((bdir (si::getenv "BUILDDIR"))
(fdir (si::getenv "FINALDIR")))
(when (and bdir fdir)
(make-certificate-file-with-final-path
full-book-name
portcullis
post-alist1
post-alist2
state
bdir
fdir)))
"Matt Kaufmann" <address@hidden> writes:
> Camm --
>
> In case Bogo's excellent reply didn't fully answer your particular question:
> I'm wondering if the following is the sort of problem you found, where you use
> a function defined in Common Lisp that is unknown to ACL2.
>
> ACL2 !>(defun my-princ (x)
> (princ x))
>
>
> ACL2 Error in ( DEFUN MY-PRINC ...): The symbol PRINC (in package
> "COMMON-LISP") has neither a function nor macro definition in ACL2.
> Please define it.
>
Yep. If I recall, this was triggered in the example above with "DO".
Also, I couldn't figure out how to try a simple change to
other-events.lisp, and recompile only that file -- instead each
modification required a rebuild of all of ACL2 from what I could
discern.
> Perhaps we should create a documentation topic ("lisp-analogues"?) that
> associates ACL2 functions with Common Lisp functions, e.g.:
>
> princ --> princ$
> format --> fms, fmt, fmt1
> pairlis --> pairlis$
>
> and so on. Would anyone find that useful?
>
Might be helpful, but please don't launch this solely on my account,
as I imagine my application here is a bit uncommon.
Take care,
> -- Matt
> cc: address@hidden
> From: "Camm Maguire" <address@hidden>
> Date: 11 Dec 2003 21:02:43 -0500
> User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> Reply-to: address@hidden
> Sender: address@hidden
> X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
> X-WSS-ID: 13C7FE754525471-01-01
> Content-Type: text/plain;
> charset=us-ascii
>
> Greetings! On an unrelated issue, I too was trying to write a lisp
> function for use inside ACL2, and ran into the "~ not defined for use
> in ACL2" error message. Anyway, I too would like to know how to do
> this (i.e. write lisp functions for use in ACL2).
>
> Take care,
> --
> Camm Maguire address@hidden
> ==========================================================================
> "The earth is but one country, and mankind its citizens." -- Baha'u'llah
>
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
- [Gcl-devel] Re: Problem to get a Function Admitted by ACL2,
Camm Maguire <=