[Gcl-devel] Re: address@hidden: Re: address@hidden: differences between 2.9 and 2.9.2]]

[Camm Maguire]

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 <address@hidden> 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 <address@hidden> 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 <address@hidden>
> > > Subject: Re: address@hidden: differences between 2.9 and 2.9.2]
> > > To: Matt Kaufmann <address@hidden>
> > > cc: address@hidden, Jared Davis <address@hidden>
> > > Date: Wed, 31 Aug 2005 10:54:32 -0500 (CDT)
> > > Reply-To: Rex Page <address@hidden>
> > >
> > > 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 <address@hidden>
> > > > X-X-Sender: address@hidden
> > > > Reply-To: Rex Page <address@hidden>
> > > > To: ACL2 Help List <address@hidden>
> > > > Subject: differences between 2.9 and 2.9.2
> > > > Content-Type: TEXT/PLAIN; charset=US-ASCII
> > > > Sender: address@hidden
> > > > 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                                                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