Re: [PVS-Help] compilation problems under debian etch

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Hendrik,

I don't know exactly where this is happening, but a symbol such as
you show is usually gotten by interning a carriage return, e.g.,

pvs(276): (intern (format nil "~%"))
|
|
nil
pvs(277):

What I usually do in these cases is start up CMU Lisp in Emacs (from the
PVS directory), (load "pvs.system"), and then run

(operate-on-system :pvs :lf)

Then when it runs into such problems, I can more easily backtrace and
debug them.

If you do get a backtrace, that at least will tell you where the problem
variable is.

Let me know what you find.

Regards,
Sam

Hendrik Tews <H.Tews@cs.ru.nl> wrote:

> Hi,
> 
> after removing the -lbsd in BDD/ix86-Linux/Makefile I could
> successfully build pvs with cmucl on
> - debian sarge (kernel 2.6.8)
> - mixed debian sarge/etch running a 2.6.15 kernel
> - Fedora Core release 5 (Bordeaux)
> 
> However, on my own machine, running debian etch (kernel 2.6.18-3)
> I only get until
> 
>     ;;;; Loading #P"/home/tews/src/pvs/ess/box-defs.lisp".
>     ; [GC threshold exceeded with 15,718,168 bytes in use.  Commencing GC.]
>     ; [GC completed with 5,043,712 bytes retained and 10,674,456 bytes freed.]
>     ; [GC will next occur when at least 17,043,712 bytes are in use.]
>     ; 
>     Error in KERNEL::UNBOUND-SYMBOL-ERROR-HANDLER:  the variable |
>     | is unbound.
>        [Condition of type UNBOUND-VARIABLE]
> 
>     Restarts:
>       0: [ABORT] Skip remaining initializations.
> 
>     Debug  (type H for help)
> 
>     (EVAL |
>     |)
>     Source: Error finding source: 
>     Error in function DEBUG::GET-FILE-TOP-LEVEL-FORM:  Source file no longer exists:
>       target:code/eval.lisp.
>     0] 
> 
> (full make log attached) I tried different lisp versions (debian
> cmucl, original 19d, original 19c), with a different kernel
> (vanilla 2.6.15.7), and different gcc's (3.4 and debian 4.1.2).
> The result is always the same.
> 
> Any ideas?
> 
> Bye,
> 
> Hendrik