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

[PVS-Help] Configure problems on 64-bit mac -- partially solved butnot totally



OK, I have managed to wrestle myself a little further into the configure
problem mentioned in my last email.

Here's the problem:

My emacs path is as follows:

checking for emacs... /Applications/Aquamacs
Emacs.app/Contents/MacOS/Aquamacs Emacs

Unfortunately, the presence of spaces in the pathname causes configure
to cack, now a little further on:

checking for /Applications/Aquamacs Emacs.app/Contents/MacOS/Aquamacs
Emacs version >= 19... ./configure: line 2988: /Applications/Aquamacs:
No such file or directory

My best guess is that it is trying to call

/Applications/Aquamacs Emacs.app/Contents/MacOS/Aquamacs Emacs --version

and there isn't enough magic quotification to keep the shell from
getting confused.

Setting up a symlink from ~/bin/aquamacs to the above path fixes that
problem.



With that fixed, I still have a problem with ld.  First, it does not
support the --version command line option that the configure script
expects.  Then, when I substitute the -v option that it DOES accept, it
prints the following nastiness instead of a real version number:

[rpgoldman-2:~/lisp/pvs-4.2-source] rpg% ld -v
@(#)PROGRAM:ld  PROJECT:ld64-77

The script seems to complete anyway and write a makefile.

Then I get the following error in the Lisp:

Warning: An error occurred
         (Attempt to take the value of the unbound variable
          `*pvs-binary-type*'.)
         during the reading or evaluation of -e "(load \"pvs.system\")"
Warning: An error occurred
         (Package "mk" not found. [file position = 207]) during the
         reading or evaluation of -e
         "(let ((code 1)                           (*load-pvs-prelude*
nil))                       (unwind-protect
(multiple-value-bind (v err)                             (ignore-errors
(mk:operate-on-system :pvs :compile))                                (if
err                                    (let ((*print-readably* nil))
                                  (format t \"~a\" err))
                    (setq code 0))))                         (excl:exit
code)))"

Adding this line to the definition of *pvs-binary-type* seems to fix the
fact that pvs-config.lisp doesn't support 64-bit macs:

  #+(and allegro macosx x86-64) "fasl"

I'd suggest modifying the pvs-config file additionally to put a line in
there to check for an unset *pvs-binary-type* file, and throw an
informative error message to the effect that the user is attempting to
use an unanticipated form of CL.

The same addition needs to be made in
/Users/rpg/lisp/pvs-4.2-source/ess/sys/tools/rel/box-system.lisp

Getting through these, I ran aground at:

;;; Fasl write complete
[Loading efile #>E"tdefun.fasl" as file
"/Users/rpg/lisp/pvs-4.2-source/ess/sys/ergolisp/rel/tdefun.fasl".]
cannot find foreign file; Exiting
make: *** [bin/ix86-MacOSX/devel/pvs-allegro] Error 1

I don't believe that it is actually the attempt to load tdefun.fasl
that's failed --- this doesn't look like it attempts to load anything
foreign; it's just a few macros.  That suggests to me that there is
something AFTER this that has failed.

Looking into this, it looks like the problem comes because the binary
files aren't set.  I tried to fix this by modifying the following block
in pvs.system (see starred line):

 #+(and allegro dynload)
                  (let* ((platform #+(and sun4 sunos4) "sun4-SunOS4"
                                   #+(and sun4 (not sunos4)) "sun4-SunOS5"
                                   #+(and x86 (not macosx)) "ix86-Linux"
                                   #+(and macosx powerpc) "powerpc-MacOSX"
 ***                                  #+(and macosx (or x86 x86-64))
"ix86-MacOSX"
                                   )
                         (utilpath (concatenate 'string
                                     *pvs-path* "/src/utils/" platform))
                         (bddpath (concatenate 'string
                                    *pvs-path* "/BDD/" platform))
                         (ws1spath (concatenate 'string
                                     *pvs-path* "/src/WS1S/" platform)))

But now I think I lose because either I am not compiling the right
binary files from foreign libraries, or because the right binary files
must be distributed with PVS and aren't:

; Foreign loading
/Users/rpg/lisp/pvs-4.2-source/src/utils/ix86-MacOSX/file_utils.dylib.
Loading
/Users/rpg/lisp/pvs-4.2-source/src/utils/ix86-MacOSX/file_utils.dylib
failed with error: no suitable image found.  Did find:
	/Users/rpg/lisp/pvs-4.2-source/src/utils/ix86-MacOSX/file_utils.dylib:
mach-o, but wrong architecture.; Exiting


I think I compiled that file myself, so I bet that the
configure/makefile doesn't consider the possbility that I should be
building an x86-64 binary instead of an i86 one.  I'm a little surprised
by this, though --- I thought that the x86-64 was supposed to be able to
run 32-bit binaries.

Any suggestions would be much appreciated!