gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Gcl-devel] Re: address@hidden: Re: ACL2 Version 4.0]


From: Matt Kaufmann
Subject: Re: [Gcl-devel] Re: address@hidden: Re: ACL2 Version 4.0]
Date: Sun, 18 Jul 2010 15:49:49 -0500

Hi --

Since you mention "trad and ansi" and also "acl2", I thought it best
for me to reply with a reminder that ACL2 builds with non-ANSI GCL but
does not build with ANSI GCL.  If you think ANSI GCL is ready for
ACL2, I could give that a try sometime (it will almost certainly
involve some ACL2 source code modification).

Regards,
Matt
   From: Camm Maguire <address@hidden>
   Date: Thu, 15 Jul 2010 23:06:30 -0400
   X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6 (newer, 2)
   Cc: address@hidden
   Sender: address@hidden
   X-SpamAssassin-Status: No, hits=-2.4 required=5.0
   X-UTCS-Spam-Status: No, hits=-297 required=165

   Great!  I had to upgade the gmp sources in the stable Version_2_6_8pre
   branch for mac os x.  I think mingw uses the loca sources too.  It
   would be great if you could build this branch to ensure all is well,
   both trad and ansi, report the number of ansi-test failures, and build
   maxima,acl2 and axiom.  Of course if only some of this is possible,
   that is great too.  Thanks so much, and please let me know if you run
   into difficulties.

   Donald Winiecki <address@hidden> writes:

   > Hi Camm,
   >
   > I can continue building GCL on Windows for the project, so if you get 
there I'll produce an executable for
   > whoever is out there.
   >
   > _don
   >
   > On Thu, Jul 15, 2010 at 11:49 AM, Camm Maguire <address@hidden> wrote:
   >
   >     Great!  acl2-4.0 test builds are in progress on bbh and the x86 mac
   >     axiom provides.  One last porting nightmare is windows/mingw, if
   >     anyone still cares/uses this.  I believe you have had a test box at
   >     your cite once in the past.  If this support is of interest to you and
   >     you could reactivate this machine, please let me know.
   >    
   >     Take care,
   >    
   >     "David L. Rager" <address@hidden> writes:
   >    
   >     > Hi Camm,
   >     >
   >     > Okay, good.  I think for now, if you're happy we're happy.  Please 
let
   >     > me know if you need something else.
   >     >
   >     > Thanks,
   >     > David
   >     >
   >     > On Sun, Jul 11, 2010 at 4:37 PM, Camm Maguire <address@hidden> wrote:
   >     >> "David L. Rager" <address@hidden> writes:
   >     >>
   >     >>> Hello Camm,
   >     >>>
   >     >>> Matt was able to grant me root access on bbh earlier today, and I 
was
   >     >>> able install gcc-4.2 and g++4.2.  I tested gcc with a simple C 
program
   >     >>> and it worked.  g++ couldn't compile the same program, but unless 
you
   >     >>> actually need g++, I'm okay leaving g++ [potentially] broken.
   >     >>>
   >     >>> which gcc-4.2
   >     >>> ==>
   >     >>> /usr/bin/gcc-4.2
   >     >>>
   >     >>> which g++-4.2
   >     >>> ==>
   >     >>> /usr/bin/g++-4.2
   >     >>>
   >     >>> I didn't install the xcode package, because I think it contains
   >     >>> significantly more than we need, and the xcode installer wanted a 
gui
   >     >>> when I tried earlier (which I don't have at the moment).  The 4.2
   >     >>> version of GCC looks to be the most recent version available for 
OS-X,
   >     >>> or, at least, it was the most recent version that ATT labs had
   >     >>> available.  I did go through the process to "become an apple
   >     >>> developer", so if it turns out you'd like the disk image necessary 
to
   >     >>> install xcode, I'll happily send you the 700 megabyte file.
   >     >>>
   >     >>> Please let me know if you need something else.
   >     >>
   >     >> Thank you so much!  I think this suffices.  On ppc, 4.0 and 4.2
   >     >> relocations appear identical so all is good.  However, I thought I'd
   >     >> let you know that there was soe problem with the 4.2 installation on
   >     >> bbh.
   >     >>
   >     >> 1) Cannot compile with -g:
   >     >>
   >     >> bbh:~/ngcl/o camm$ gcc-4.2  -c -mlongcall -g -O2  -Wall 
-DVOL=volatile -fsigned-char -pipe -g   -I/
   >     Users/camm/gcl-2.6.8pre/o -I../h -I../gcl-tk plttest.c
   >     >> {standard input}:3:unknown section attribute: debug
   >     >> {standard input}:3:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:4:unknown section attribute: debug
   >     >> {standard input}:4:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:5:unknown section attribute: debug
   >     >> {standard input}:5:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:6:unknown section attribute: debug
   >     >> {standard input}:6:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:7:unknown section attribute: debug
   >     >> {standard input}:7:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:8:unknown section attribute: debug
   >     >> {standard input}:8:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:9:unknown section attribute: debug
   >     >> {standard input}:9:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:10:unknown section attribute: debug
   >     >> {standard input}:10:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:11:unknown section attribute: debug
   >     >> {standard input}:11:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:12:unknown section attribute: debug
   >     >> {standard input}:12:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:13:unknown section attribute: debug
   >     >> {standard input}:13:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:15:unknown section attribute: debug
   >     >> {standard input}:15:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:16:unknown section attribute: debug
   >     >> {standard input}:16:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:17:unknown section attribute: debug
   >     >> {standard input}:17:Rest of line ignored. 1st junk character valued 
76 (L).
   >     >> {standard input}:533:unknown section attribute: debug
   >     >> {standard input}:533:Rest of line ignored. 1st junk character 
valued 76 (L).
   >     >> {standard input}:589:unknown section attribute: debug
   >     >> {standard input}:589:Rest of line ignored. 1st junk character 
valued 76 (L).
   >     >> {standard input}:677:unknown section attribute: debug
   >     >> {standard input}:677:Rest of line ignored. 1st junk character 
valued 32 ( ).
   >     >> {standard input}:1063:Complex expression. Absolute segment assumed.
   >     >> {standard input}:1072:Complex expression. Absolute segment assumed.
   >     >> {standard input}:1079:Complex expression. Absolute segment assumed.
   >     >> {standard input}:1086:Complex expression. Absolute segment assumed.
   >     >> {standard input}:1098:Complex expression. Absolute segment assumed.
   >     >> {standard input}:1129:Complex expression. Absolute segment assumed.
   >     >> {standard input}:1150:unknown section attribute: debug
   >     >> {standard input}:1150:Rest of line ignored. 1st junk character 
valued 32 ( ).
   >     >> {standard input}:1408:unknown section attribute: debug
   >     >> {standard input}:1408:Rest of line ignored. 1st junk character 
valued 32 ( ).
   >     >> {standard input}:1416:unknown section attribute: debug
   >     >> {standard input}:1416:Rest of line ignored. 1st junk character 
valued 32 ( ).
   >     >> {standard input}:1436:unknown section attribute: debug
   >     >> {standard input}:1436:Rest of line ignored. 1st junk character 
valued 32 ( ).
   >     >> {standard input}:1449:unknown section attribute: debug
   >     >> {standard input}:1449:Rest of line ignored. 1st junk character 
valued 32 ( ).
   >     >>
   >     >>
   >     >> 2) Doing the final link with 4.2 apparently brings in a bogus execve
   >     >> from libc:
   >     >>
   >     >> gcc-4.2  -o raw_gcl  -L.    -lgcl `echo -lm  -lreadline -lz | sed 
-e 's/-lncurses/ /'` -lc -lgclp
   >     >> ...
   >     >>
   >     >> init_darwin_zone_compat(): execv() failed
   >     >> make: *** [saved_gcl] Error 1
   >     >>
   >     >> gcc-4.0  -o raw_gcl  -L.    -lgcl `echo -lm  -lreadline -lz | sed 
-e 's/-lncurses/ /'` -lc -lgclp
   >     >>
   >     >> OK
   >     >>
   >     >> I think I've tested this enough to determine what I was looking for,
   >     >> so you really don't have to bother any further unless you want to.
   >     >> But just a heads up that 4.2 on this box is not useable as is.
   >     >>
   >     >> Take care,
   >     >>
   >     >>>
   >     >>> Thanks!
   >     >>> David
   >     >>>
   >     >>> On Fri, Jul 9, 2010 at 5:31 AM, Camm Maguire <address@hidden> 
wrote:
   >     >>>> Greetings!
   >     >>>>
   >     >>>> "David L. Rager" <address@hidden> writes:
   >     >>>>
   >     >>>>> Greetings Camm,
   >     >>>>>
   >     >>>>> I just wanted to let you know that I'm looking into updating gcc 
on
   >     >>>>> Matt's mac.  I'm guessing that the current version of gcc is too 
old.
   >     >>>>> It's looking like it'll be a couple hours worth of work (and I'm
   >     >>>>> uncertain at the moment whether I'll be able to get it done), so 
I
   >     >>>>> thought I would ask that question first.
   >     >>>>>
   >     >>>>
   >     >>>> The current version works fine.  Its just that I am finalizing 
mac osx
   >     >>>> support for gcl, and on the intel mac at least, the relocation 
records
   >     >>>> output by gcc-4.0 and gcc-4.2 are different.  I think these are 
the
   >     >>>> only two gcc versions supported on mac (can you verify this?)  I'd
   >     >>>> just like to ensure that the patch I have will work with both 
versions
   >     >>>> on both cpus to head off future user complaints.
   >     >>>>
   >     >>>> If it is too difficult, we can just forget about it and require
   >     >>>> gcc-4.0 only on ppc.  On the intel, gcc-4.0 and 4.2 can coexist 
-- the
   >     >>>> default compiler is not changed.  Does that simplify anything?
   >     >>>>
   >     >>>> Take care,
   >     >>>>
   >     >>>>> Thanks,
   >     >>>>> David
   >     >>>>>
   >     >>>>>> On Thu, Jul 8, 2010 at 9:30 PM, Matt Kaufmann <address@hidden> 
wrote:
   >     >>>>>>> Hi, David --
   >     >>>>>>>
   >     >>>>>>> Camm Maguire (the GCL "god") just sent me a request (see thread
   >     >>>>>>> below).  Would you be willing to help him?  Someone in the 
Tower has a
   >     >>>>>>> key to my office (probably Robert).  But I don't know if 
you're in
   >     >>>>>>> town, have time, or know how to do this sort of thing.
   >     >>>>>>>
   >     >>>>>>> Xcode might already be installed on bbh, since we do have 
"make" on
   >     >>>>>>> that machine, but I'm not sure.  I don't know anything about
   >     >>>>>>> installing gcc on a Mac but maybe the latest version is 
included with
   >     >>>>>>> Xcode.  It would be good to help Camm, but I know it's not on 
the path
   >     >>>>>>> to your dissertation....
   >     >>>>>>>
   >     >>>>>>> Feel free to reply directly to Camm, and to CC me if you 
remember and
   >     >>>>>>> don't mind.  Or if you're not going to do it, please let me 
know and
   >     >>>>>>> I'll tell him that I can't help him.
   >     >>>>>>>
   >     >>>>>>> Thanks --
   >     >>>>>>> -- Matt
   >     >>>>>>> ------- Start of forwarded message -------
   >     >>>>>>> Date: 8 Jul 2010 14:27:14 -0500
   >     >>>>>>> From: Matt Kaufmann <address@hidden>
   >     >>>>>>> To: address@hidden
   >     >>>>>>> In-reply-to: <address@hidden> (message from Camm Maguire on
   >     >>>>>>>        Thu, 08 Jul 2010 15:18:32 -0400)
   >     >>>>>>> Subject: Re: ACL2 Version 4.0
   >     >>>>>>>
   >     >>>>>>> Hi, Camm --
   >     >>>>>>>
   >     >>>>>>> Unfortunately, I'm not in my office -- instead I'm packing for 
a trip
   >     >>>>>>> to the UK -- leaving tomorrow (Friday) and returning September 
15.  I
   >     >>>>>>> expect to be connected while I'm away (including email), but I 
don't
   >     >>>>>>> know how to install stuff on a Mac unless I'm at the terminal.
   >     >>>>>>>
   >     >>>>>>> I know someone who might be able to help -- I'll email him.
   >     >>>>>>>
   >     >>>>>>> Sorry I can't be more helpful --
   >     >>>>>>> - -- Matt
   >     >>>>>>>   From: Camm Maguire <address@hidden>
   >     >>>>>>>   Date: Thu, 08 Jul 2010 15:18:32 -0400
   >     >>>>>>>   X-MagicMail-UUID: efd06ae4-8ac5-11df-9e93-000c29c6406d
   >     >>>>>>>   X-SpamAssassin-Status: No, hits=-2.6 required=5.0
   >     >>>>>>>   X-UTCS-Spam-Status: No, hits=-272 required=165
   >     >>>>>>>
   >     >>>>>>>   Greetings again!  One last item -- could you look into 
perhaps
   >     >>>>>>>   installing the latest gcc available for your ppc mac?  I 
think at
   >     >>>>>>>   least 4.2 should be in 'xcode', whatever that is.
   >     >>>>>>>
   >     >>>>>>>   Thanks!
   >     >>>>>>>   --
   >     >>>>>>>   Camm Maguire                                     
address@hidden
   >     >>>>>>>   
==========================================================================
   >     >>>>>>>   "The earth is but one country, and mankind its citizens."  
--  Baha'u'llah
   >     >>>>>>> ------- 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
   >     >>
   >     >
   >     >
   >     >
   >     >
   >    
   >     --
   >     Camm Maguire                                       address@hidden
   >     
==========================================================================
   >     "The earth is but one country, and mankind its citizens."  --  
Baha'u'llah
   >    
   >     _______________________________________________
   >     Gcl-devel mailing list
   >     address@hidden
   >     http://lists.gnu.org/mailman/listinfo/gcl-devel
   >

   -- 
   Camm Maguire                                     address@hidden
   ==========================================================================
   "The earth is but one country, and mankind its citizens."  --  Baha'u'llah

   _______________________________________________
   Gcl-devel mailing list
   address@hidden
   http://lists.gnu.org/mailman/listinfo/gcl-devel



reply via email to

[Prev in Thread] Current Thread [Next in Thread]