Greetings! I believe this is because you are in the acl2 repl. YOu need :q first. THen you can resume acl2 with (in-package 'acl2)(lp).
Thanks for the note re: XP. Perhaps we can try some runtime toggling of the variable, though I don't know how precisely as I don't use Windows. Mike? Rex Page <[EMAIL PROTECTED]> writes: > Camm > > When I tried the incantation in your note, it failed on the in-package > command, on the excuse that 'compiler is not a string. Then, the let* > also failed, saying some sort of guard failed. (I've pasted the > response at the end of this note, but I don't think it matters because > I had to add a right paren to the let* to get it to go, even though > the parens apper to me to be balanced.) > > I've decide to revert to 2.9. > > For the record, the problem seems to go away on XP. That is, when I > try to certify my book on W2K, ACL2 2.9.2, it fails, but the book > certifies without a problem on XP, ACL2 2.9.2. > > Rex > > ------------ response to let* ----- > (LET* ((X '|-FNO-ZERO-INITIALIZED-IN-BSS| > '(I #)) > (SETQ *CC* > (CONCATENATE 'STRING > (SUBSEQ *CC* 0 I) > (SUBSEQ *CC* #))))) > the guard, > (IF (SYMBOL-ALISTP BINDINGS) > (IF (CONSP DECL-BODY) > (IF (EQ (CDR DECL-BODY) 'NIL) > (EQ (CDR DECL-BODY) 'NIL) > (IF (EQ # #) (# # BINDINGS FORM) 'NIL)) > 'NIL) > 'NIL), > for LET* failed. > ---------end of response ---------- > > > On Fri, 2 Sep 2005, Camm Maguire wrote: > > > Greetings, and please excuse my delayed reply. > > > > I think you can just do this from lisp: > > > > (in-package 'compiler) > > (let* ((x `-fno-zero-initialized-in-bss') > > (i (search x *cc*))) > > (setq *cc* (concatenate 'string (subseq *cc* 0 i) (subseq *cc* (+ i > > (length x)))))) > > > > Please let me know if problems persist. > > > > Mike, what is the deal with this flag? > > > > Take care, > > > > Matt Kaufmann <[EMAIL PROTECTED]> writes: > > > > > Hi, Jared -- > > > > > > In case you check your Rockwell account more often than your CS account, > > > I'm > > > forwarding this. I don't have anything to add about the Windows side of > > > things > > > and the GCL upgrade, so I'm passing Rex's questions along to you.... > > > > > > Thanks -- > > > -- Matt > > > From: Rex Page <[EMAIL PROTECTED]> > > > Subject: Re: [EMAIL PROTECTED]: differences between 2.9 and 2.9.2] > > > To: Matt Kaufmann <[EMAIL PROTECTED]> > > > cc: [EMAIL PROTECTED], Jared Davis <[EMAIL PROTECTED]> > > > Date: Wed, 31 Aug 2005 10:54:32 -0500 (CDT) > > > Reply-To: Rex Page <[EMAIL PROTECTED]> > > > > > > Matt > > > > > > Thanks for taking time out from your vacation to help me out. I'm > > > sending this reply in case you decide to go beyond the call of duty > > > again. > > > > > > I upgraded to 2.9.2 for class this fall because that's the release you > > > get to when you follow the current links to Jared's Windows > > > installers: http://www.cs.utexas.edu/users/jared/acl2/ > > > > > > I still have a copy of the old 2.9 installer, but thought it would be > > > best to have students download directly from the ACL2 website instead > > > of using something I downloaded in January. > > > > > > It appears that 2.9 for Windows (via Jared's prepackaged installer) > > > used GCL 2.6.5, but 2.9.2 uses GCL 2.6.6. If that is the case, maybe > > > the problem I ran into when trying to certify a book that worked with > > > 2.9 has something to do with GCL 2.6.6. > > > > > > There doesn't seem to be a Windows installer, yet, for 2.9.3, so my > > > safest alternative (at least for this fall's class) may be to have > > > students uninstall 2.9.2 and install 2.9 using the old 2.9 installer > > > that I downloaded in January. > > > > > > This is just a guess, though. Please let me know if you think this > > > would be ill advised. I'd rather stick with 2.9.2 if I can get ACL2 to > > > certify the books containing the ACL2 software I supply for the class. > > > > > > Rex > > > > > > > > > On Wed, 31 Aug 2005, Matt Kaufmann wrote: > > > > > > > Hi, Camm -- > > > > > > > > Can you help Rex with his question, below? It looks like a compiler > > > > sort of > > > > thing. > > > > > > > > By the way, Rex, you might want to upgrade all the way to ACL2 2.9.3 (by > > > > following the "Recent Changes" link from the ACL2 home page). You can > > > > see > > > > changes from one version to the next with :doc note-2-9-2 etc. > > > > > > > > -- Matt [typing from England, on vacation!] > > > > ------- Start of forwarded message ------- > > > > X-IronPort-MID: 1710767823 > > > > X-SBRS: None > > > > X-BrightmailFiltered: true > > > > X-Brightmail-Tracker: AAAAAA== > > > > X-Ironport-AV: i="3.96,156,1122872400"; > > > > d="scan'208"; a="1710767823:sNHT13805992" > > > > X-Authentication-Warning: turing.cs.ou.edu: rlpage owned process doing > > > > -bs > > > > Date: Tue, 30 Aug 2005 20:54:28 -0500 (CDT) > > > > From: Rex Page <[EMAIL PROTECTED]> > > > > X-X-Sender: [EMAIL PROTECTED] > > > > Reply-To: Rex Page <[EMAIL PROTECTED]> > > > > To: ACL2 Help List <[EMAIL PROTECTED]> > > > > Subject: differences between 2.9 and 2.9.2 > > > > Content-Type: TEXT/PLAIN; charset=US-ASCII > > > > Sender: [EMAIL PROTECTED] > > > > X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN > > > > X-SpamAssassin-Status: No, hits=-2.6 required=5.0 > > > > X-UTCS-Spam-Status: No, hits=-212 required=180 > > > > > > > > I'm trying to certify a book that goes through with no problem on 2.9, > > > > but fails on 2.9.2 (after admitting the first function in the book) > > > > with the error report shown below. > > > > > > > > Is there something I need to update in addition to running the Windows > > > > installer code for 2.9.2? > > > > > > > > Rex Page > > > > > > > > ---------- error report from cert attempt ---------------- > > > > > > > > cc1.exe: unrecognized option `-fno-zero-initialized-in-bss' > > > > > > > > Error: (SYSTEM "gcc -c -Wall -DVOL=volatile -fsigned-char -pipe > > > > - -fno-zero-initialized-in-bss -mms-bitfields -march=i386 > > > > - -IC:/PROGRA~1/ACL2-2.9.2/lib/gcl-2.6.6/ > > > > unixport/../h -O3 -c -w \"gazonk4.c\" -o \"gazonk4.o\"") returned a > > > > non-zero value 1. > > > > Fast links are on: do (si::use-fast-links nil) for debugging > > > > Error signalled by UNLESS. > > > > Broken at COND. Type :H for Help. > > > > ACL2>> > > > > ------- End of forwarded message ------- > > > > > > > ---------- > > > > > > > > > > > > > > > > -- > > Camm Maguire [EMAIL > > PROTECTED] > > ========================================================================== > > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > > > > > > -- Camm Maguire [EMAIL PROTECTED] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list [email protected] http://lists.gnu.org/mailman/listinfo/gcl-devel
