Re: [Gcl-devel] Windows stuff

[Matt Kaufmann]

Hi, Camm --

I see the problem: when the second argument to canonical-unix-pathname
is true, then the input pathname must end in "/".  I think the
following log will clarify.  But I'm not aware of any ill-formed calls
of canonical-unix-pathname in the ACL2 sources.  If this wasn't your
own call causing the problem, could you point me to where the bad call
might be coming from?

  ACL2 !>:q

  Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
  ACL2>(let* ((x (namestring (truename ".")))
              (y (pathname-unix-to-os x *the-live-state*))
              (z (canonical-unix-pathname y t *the-live-state*))) (list x y z))

  ("/v/filer4b/v11q002/acl2space/acl2/devel"
   "/v/filer4b/v11q002/acl2space/acl2/devel" NIL)

  ACL2>(let* ((x (namestring (truename ".")))
              (y (pathname-unix-to-os x *the-live-state*))
              (z (canonical-unix-pathname y nil *the-live-state*))) (list x y 
z))

  ("/v/filer4b/v11q002/acl2space/acl2/devel"
   "/v/filer4b/v11q002/acl2space/acl2/devel"
   "/v/filer4b/v11q002/acl2space/acl2/devel")

  ACL2>(let* ((x (namestring (truename ".")))
              (x (if (eql (char x (1- (length x))) #\/)
                     x
                   (concatenate 'string x "/")))
              (y (pathname-unix-to-os x *the-live-state*))
              (z (canonical-unix-pathname y t *the-live-state*))) (list x y z))

  ("/v/filer4b/v11q002/acl2space/acl2/devel/"
   "/v/filer4b/v11q002/acl2space/acl2/devel/"
   "/v/filer4b/v11q002/acl2space/acl2/devel/")

  ACL2>

My expert on 2) has replied to your maguirefamily.org address.  For
now, if you tell me which version of ACL2 you're using, I can send you
a couple of files, together with instructions, that may provide a
workaround.  (I'll leave it to you whether to continue to copy
gcl-devel on the current thread.)

-- Matt
   From: Camm Maguire <address@hidden>
   Date: Wed, 16 Oct 2013 10:21:15 -0400

   Matt Kaufmann <address@hidden> writes:

   > Hi, Camm --
   > 
   > For 1), I'd appreciate your running the following experiment: in your
   > local copy of books/Makefile, change the line
   > 
   > SHELL := $(shell which bash)
   > 
   > to:
   > 
   > SHELL := $(shell which sh)

   Thanks!  Had done this, and it appears to work up to the perl failure.

   > 
   > or just explicitly define SHELL to be the full pathname of the sh
   > executable.
   > 
   > If that works, I'll think about how to allow such overrides without
   > editing that Makefile.  (I don't want to use "?=" in place of ":=",
   > since otherwise SHELL might be modified by accident.)
   > 
   > For 2), I'll get with the person who kind of maintains that Perl
   > stuff.
   > 

   Thanks!

   > >> Is there a way to certify just using make as in the past, just so I can
   > >> test the integrity of this image?
   > 
   > I hope so, once we've dealt with 1) and 2).
   > 
   > For state, please try:
   > 
   >   *the-live-state*

   OK, your input and output forms are at

   http://paste.debian.net/58363
   and
   http://paste.debian.net/58364

   > 
   > Thanks for keeping at this --

   And you too!

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