[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Re: address@hidden: Re: ACL2 Version 4.0]
|
From: |
Camm Maguire |
|
Subject: |
Re: [Gcl-devel] Re: address@hidden: Re: ACL2 Version 4.0] |
|
Date: |
Mon, 19 Jul 2010 12:11:01 -0400 |
|
User-agent: |
Gnus/5.11 (Gnus v5.11) Emacs/22.2 (gnu/linux) |
Greetings!
Matt Kaufmann <address@hidden> writes:
> 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).
>
Thanks Matt. GCL is continuing the policy of supporting both flavors
for the foreseeable future. acl2 and axiom use trad, maxima uses
ansi. Bob Boyer had told me nqthm needed no modification to run under
ansi. Of course if one is not using pcl, its just bloat.
I had put in a note to David Ranger about possible windows remote ssh
access at your site, as a backup to the very helpful services Donald
is providing. Of course, there is no reason to go out of the way here
unless there are people at ut who want to use gcl and what is builds
under windows. But if there are, and if they have a spare machine
they could make available, that would be useful. Hadn't heard back
from David in this regard yet.
acl2 is running fine on intel and ppc mac with both C compilers. I
have noticed that on machines where sgc is not available, and
si::*optimize-maximum-pages* is set (default), the standard MAXPAGE
setting is insufficient to certify all the books. Two in particular
fail (I can tell you which if you want to know), "Symbol pages
exhausted", with a simple workaround of writing a little acl2 file
turning off si::*optimize-maximum-pages* for these certs only.
Don't worry about this stuff while on vacation!!!!
Take care,
> 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
>
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah