[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

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
         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

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

Getting through these, I ran aground at:

;;; Fasl write complete
[Loading efile #>E"tdefun.fasl" as file
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))
                         (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
failed with error: no suitable image found.  Did find:
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!