[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Re: gcl/acl2
From: |
Camm Maguire |
Subject: |
Re: [Gcl-devel] Re: gcl/acl2 |
Date: |
17 Nov 2002 16:34:43 -0500 |
Greetings, and thanks as always for your feedback!
Matt Kaufmann <address@hidden> writes:
> Hi --
>
> I just downloaded the following to my Redhat Linux 7.3 home machine; some
> comments are below.
>
> http://incoming.debian.org/acl2_2.6-14_i386.deb
> http://incoming.debian.org/acl2-doc_2.6-14_all.deb
>
> I unpacked acl2_2.6-14_i386.deb using "ar x acl2_2.6-14_i386.deb" followed by
> "tar zxf data.tar.gz", into a directory /home/kaufmann/apps/acl2/v2-6/. I
> also
> created a doc/ subdirectory, /home/kaufmann/apps/acl2/v2-6/doc/, and similarly
> unpacked acl2-doc_2.6-14_all.deb there. I'll refer below to
> /home/kaufmann/apps/acl2/v2-6 as "....".
>
> 1. The books reside in ..../usr/share/acl2-2.6/books/, but
> /home/kaufmann/apps/acl2/v2-6/usr/lib/acl2-2.6/books/ has just a portion of
> the
> book directories, perhaps because you haven't yet included a full make in the
> process. (Or maybe that make was intended to be done as part of Debian
> package
> installation?? -- which I'm avoiding since I have a Redhat machine.)
>
This is correct. The package build pushes whatever .o files it finds
under books to /usr/lib/acl2-2.6, making whatever directories
necessary in the process, and linking back to /usr/share. When the
full build is run, presumably all directories will appear in /usr/lib.
> 2. The .cert files are invalid, as they need correct absolute pathnames, which
> were incorrect for my machine, e.g. (from
> ..../usr/share/acl2-2.6/books/arithmetic/abs.cert):
>
> /fix/t1/camm/tmp/acl2-2.6/books/arithmetic/abs.lisp
>
I received your subsequent note indicating that include-books still
works. Nevertheless, I've just added a bit to debian/rules to insert
the correct final path into these files. In general, no references to
the build directory should exist in the package. I haven't double
checked everything on this score yet.
> I think that the book certification will have to be done at installation time
> rather than on your machine. That probably means that there's no reason for
> you to distribute the .o files for the books, since they will be re-created at
> certification time.
>
> It may be possible in some future ACL2 release to modify the nature of .cert
> files so that they can refer to a system directory that avoids the need to
> place those absolute pathnames in the .cert file. With such a change, I think
> you would be able to distribute .cert files. Let me know if you think that is
> important, in which case I'll put that on our "to do" list.
>
> 3. There is no need to distribute ..../usr/share/acl2-2.6/TMP1.lisp.
>
OK, removed!
> 4. I'm not so sure about moving some of the stuff into doc. For example,
> ..../doc/usr/share/doc/acl2-doc/books/arithmetic/README
> talks about "contents of this directory", yet there are no such
> contents -- the contents are in ..../usr/share/acl2-2.6/books/*/.
>
I wasn't too sure about this either -- however, this is *definitely*
the standard place for Debian documentation, and all users will look
there. No one by default will ever think of looking for anything
under /usr/share, unless they are a sysadmin or something. Which is
again interesting given that the .lisp files are here. But I don't
think there is any better place for these.
> 5. I didn't immediately find ..../doc/usr/share/info/. But maybe Debian users
> would know to look there.
>
All info reading tools, (e.g. emacs, info) look here. On a Debian
box, you can just fire up emacs and do a C-h i to see the info pages.
Take care,
> -- Matt
> Cc: address@hidden, address@hidden, address@hidden
> From: Camm Maguire <address@hidden>
> Date: 17 Nov 2002 12:52:11 -0500
>
> Greetings!
>
> Matt Kaufmann <address@hidden> writes:
>
> > Hi --
> >
> > I hadn't realized that an ACL2 Debian package is on the Web. After
> getting
> > your email I did a google search and found
> > http://packages.debian.org/unstable/math/acl2.html; is that the right
> place to
> > look? (It seems to point to version -11 rather than -12.)
> >
>
> Yes this is the right place for the 'unstable' distribution. In
> general, packages flow through Debian as follows:
>
> On upload, in http://incoming.debian.org
> After a day or so, at http://packages.debian.org/unstable/math/acl2.html
> After 10 days, if no critical bugs filed, at
> http://packages.debian.org/testing/math/acl2.html
> After ~ 6mos to 1 year, when a new stable is released, at
> http://packages.debian.org/stable/math/acl2.html
>
> Take care,
>
> > Thanks --
> > -- Matt
> > Cc: address@hidden, address@hidden, address@hidden
> > From: Camm Maguire <address@hidden>
> > Date: 17 Nov 2002 00:11:50 -0500
> >
> > Greetings! Just a note that I'm uploading version -12 of the package
> > now. It should be in the archives in a day or so. I've tried to
> > address all the points you raise below. I'd greatly appreciate a
> > knowledgeable person's feedback.
> >
> > Barring the unforeseen, I hope to release -13 in a few days with the
> > sole change that the package will certify all the books. By then 2.7
> > should be ready and hopefully the package structure will be finalized.
> >
> > Take care,
> >
> > Matt Kaufmann <address@hidden> writes:
> >
> > > Hi, and thank YOU again for all your great GCL work --
> > >
> > > As you requested, I have taken a look at the Debian ACL2 package
> that you
> > > constructed. Thanks for your work! Here are some comments.
> > >
> > > I downloaded
> http://ftp.debian.org/debian/pool/main/a/acl2/acl2_2.6-6_i386.deb
> > > to my RedHat 7.3 laptop and then followed the instructions in
> > > http://ftp.gnu.org/gnu/gcl/cvs/HOWTO-UNPACK-DEBS. (By the way, I
> had to become
> > > root to do that; perhaps you could mention that in
> HOWTO-UNPACK-DEBS.) I then
> > > issued the command "acl2" at the shell and it seemed to work
> perfectly! In
> > > order to run ACL2 proof trees (meta-x proof-tree) in emacs, though,
> I needed to
> > > execute the following forms in emacs (which I have added to my
> .emacs file).
> > >
> > > (defvar *acl2-interface-dir* "/usr/share/emacs/site-lisp/acl2/")
> > >
> > > (autoload 'start-proof-tree
> > > (concat *acl2-interface-dir* "top-start-shell-acl2")
> > > "Enable proof tree logging in a prooftree buffer."
> > > t)
> > >
> > > But then they worked great; thanks.
> > >
> > > Also, a file was missing in /usr/share/emacs/site-lisp/acl2/:
> > > load-shell-acl2.el. (That directory comes from the ACL2
> interface/emacs/
> > > directory.) I went ahead and copied it over manually (as root).
> File
> > > load-inferior-acl2.el was also missing, as were README, README.doc,
> README.mss,
> > > and README.ps.
> > >
> > > More importantly, several ACL2 directories (and their
> subdirectories) were
> > > missing from the extraction. In order of importance (most to
> least), they are
> > > as follows, where acl2-sources is the top-level ACL2 source
> directory:
> > >
> > > acl2-sources/ [users need to be able to browse the sources]
> > > acl2-sources/books/ [these are like "libraries" -- pre-proved
> theorems etc.]
> > > acl2-sources/doc/ [HTML, Emacs info, and Postscript
> documentation]
> > > acl2-sources/emacs/ [Some emacs utilities]
> > > acl2-sources/interface/infix/
> > >
> > > I don't know enough about traditional file organization to suggest
> where these
> > > should go in a Debian package. Our method has been to allow ACL2
> users to
> > > download ACL2 and put the acl2-sources directory anywhere they want,
> > > maintaining the structure that we provide under acl2-sources/.
> Under that
> > > method, one of the first things to do is to run the "make
> certify-books"
> > > command from acl2-sources/, in order to "certify" the many .lisp
> files under
> > > acl2-sources/books/ (i.e., run them through ACL2). This process
> compiles files
> > > and, more importantly, writes out .cert files that have absolute
> pathnames. I
> > > don't know how that would fit into a Debian installation process.
> > >
> > > >> > By the way, I'm hoping that we will release the next version
> (2.7) of ACL2
> > > >> > later this month. (It's been a year since we released ACL2
> 2.6.)
> > > >> >
> > > >>
> > > >> Great! Any surprises?
> > >
> > > I don't think so. The set of files has changed slightly, and of
> course the
> > > contents of files have changed somewhat, but the basic structure is
> the same.
> > >
> > > Thanks --
> > > -- Matt
> > > Cc: address@hidden, address@hidden
> > > From: Camm Maguire <address@hidden>
> > > Date: 01 Nov 2002 19:41:24 -0500
> > >
> > > Greetings, and thanks for your reply!
> > >
> > > Matt Kaufmann <address@hidden> writes:
> > >
> > > > Hi, Camm --
> > > >
> > > > That's really great that GCL is in such good shape!
> > > >
> > > > I've added two targets to the top-level ACL2 Makefile for you,
> so that you can
> > > > easily run short tests. In both cases, the exit status should
> be 0 if the test
> > > > succeeded and non-zero otherwise. Two files need to be
> edited: Makefile and
> > > > books/Makefile. At the end below are editing instructions,
> but if you'd rather
> > > > I just email you the entire files, let me know.
> > > >
> > >
> > > Many thanks! I've added these. BTW, Debian's autobuilders
> expect
> > > *some* output from the build at least every 15 minutes. For
> > > potentially long running tests with redirected standard output, I
> > > usually use this trick:
> > >
> > > $(MAKE) short-test-aux > short-test.log 2> short-test.log &
> j=$$! ; \
> > > tail -f --pid=$$j --retry short-test.log & wait $$j
> > >
> > >
> > > > >> Lastly, I'd be most appreciate if you or some other
> knowledgeable acl2
> > > > >> user could look at the package and comment as to whether
> everything is
> > > > >> available and in the right place.
> > > >
> > > > Sure. Please point me to where it is. I don't know anything
> about Debian
> > > > packages but I'll try to find someone who does. Or would it
> suffice to follow
> > > > the instructions at
> http://ftp.gnu.org/gnu/gcl/cvs/HOWTO-UNPACK-DEBS and build
> > > > it on my Redhat 7.3 laptop?
> > > >
> > >
> > > http://ftp.debian.org/debian/pool/main/a/acl2/
> > >
> > > > By the way, I'm hoping that we will release the next version
> (2.7) of ACL2
> > > > later this month. (It's been a year since we released ACL2
> 2.6.)
> > > >
> > >
> > > Great! Any surprises?
> > >
> > > > Finally, regarding your emacs point:
> > > >
> > > > >> Also, a Debian user has already brought up a minor issue in
> the emacs
> > > > >> lisp interface regarding differences between xemacs and GNU
> emacs. He
> > > > >> is suggesting the following:
> > > > >>
> > > > >>
> =============================================================================
> > > > >> (defun acl2-shared-lisp-mode-map ()
> > > > >> "Return the shared lisp-mode-map, independent of Emacs
> version."
> > > > >> (if (boundp 'shared-lisp-mode-map)
> > > > >> shared-lisp-mode-map
> > > > >> lisp-mode-shared-map))
> > > > >>
> > > > >> and replacing references to shared-lisp-mode-map with
> > > > >> (acl2-shared-lisp-mode-map) ought to work. (I actually
> even tested
> > > > >> the approach with GNU Emacs 20, GNU Emacs 21, and XEmacs 21
> this
> > > > >> time; I get byte-compiler warnings, but that's all. ;-))
> > > > >>
> =============================================================================
> > > > >>
> > > > >> Do you have any thoughts here?
> > > >
> > > > Thanks very much. I guess you're referring to directory
> interface/emacs/ in
> > > > the ACL2 distribution; is that right? Your solution looks
> reasonable to me.
> > > >
> > >
> > > OK, its in.
> > >
> > >
> > > Thanks again!
> > >
> > >
> > > --
> > > Camm Maguire
> address@hidden
> > >
> ==========================================================================
> > > "The earth is but one country, and mankind its citizens." --
> Baha'u'llah
> > >
> > >
> > > _______________________________________________
> > > Gcl-devel mailing list
> > > address@hidden
> > > http://mail.gnu.org/mailman/listinfo/gcl-devel
> > >
> > >
> >
> > --
> > 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://mail.gnu.org/mailman/listinfo/gcl-devel
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
- Re: [Gcl-devel] Re: gcl/acl2, (continued)
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/15
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/15
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Camm Maguire, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2, Matt Kaufmann, 2002/11/17
- Re: [Gcl-devel] Re: gcl/acl2,
Camm Maguire <=