trace output gets error when certain lisp objects encountered

[bendyarm]

Even when I go into lisp mode with :q and use the Common Lisp trace, this gets an error.

ACL2 !>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
? (zippy:with-zip-file (zip-file "~/kestrel-acl2/tmpzippy2/src.zip") 
  (let ((entry (aref (zippy:entries zip-file) 18821)))
     (zippy::entry-to-vector entry)))
#<VECTOR 14995 type (UNSIGNED-BYTE 8), simple>
? *package*
#<Package "ACL2">
? (in-package :cl-user)
#<Package "COMMON-LISP-USER">
? (trace 3bz:decompress)
(3BZ:DECOMPRESS)
? (zippy:with-zip-file (zip-file "~/kestrel-acl2/tmpzippy2/src.zip") 
  (let ((entry (aref (zippy:entries zip-file) 18821)))
     (zippy::entry-to-vector entry)))
1> (3BZ::DECOMPRESS 
> Error: Prin1$ called on an illegal object #<OCTET-VECTOR-CONTEXT #x30200758489D>
>        
>        .
> While executing: PRIN1$, in process listener(1).
> Type :POP to abort, :R for a list of available restarts.
> Type :? for other options.
1 > 

[bendyarm]

Hopefully there is nothing dependent on ACL2's exact trace$ output. If we made trace$ output just use Common Lisp's printer when an illegal object is encountered, that would be good so we could trace things from ACL2 without this sort of error.
However, if the exact trace$ output would be logically compromised by such a change, then at least it would be good if the raw lisp version would not get an error, as shown in the transcript above.

[MattKaufmann]

A new trace$ printing option may be possible. In the meantime, the following from :DOC trace$ may be helpful, to overcome ACL2's hijacking of trace and untrace.

If you need the original trace utility supplied for those Lisps,
quit the ACL2 loop with :q and call old-trace and old-untrace in raw
Lisp where you would otherwise call trace and untrace.

[MattKaufmann]

@bendyarm In principle, using option :evisc-tuple :print does what you want; see :DOC trace$. It doesn't quite do what I'd expect though; I plan to fix that tomorrow.

[MattKaufmann]

@bendyarm I've improved trace$ option :evisc-tuple :print as per the following from :DOC note-8-6.

  The [trace$] option :evisc-tuple :print, which continues to use raw
  Lisp printing, has undergone the following improvements when
  printing entry and exit values.  Thanks to Eric McCarthy for a
  query that led to these improvements.

    * Values are now pretty-printed.
    * Array values are no longer displayed as [stobj]s.  (This includes
      stobjs themselves, since they are arrays.)