Simple query prints raw Pretype_errors.Pretype error, produces 18MB of output

[cpitclaudel]

The following input to sertop produces 18MB of output (81MB in --human mode) and takes 1.5 seconds to run:

(query0 (Add () "(* test *)\nGoal 1 = True.")) 
(query1 (Exec 2))

It looks like printing the internals of the Pretype_errors.PretypeError object yields about 1.5 million lines of sexps in --human mode. This is mostly funny, but Alectryon takes 6 seconds to parse through that, which is less funny. Amy change to improve that output?

[ejgallego]

Umm, we had some code workarounding this problem, see:

  Conv.Exn_converter.add [%extension_constructor Pretype_errors.PretypeError] (function
      (* Pretype Errors XXX what to do with _env, _envmap *)
      | Pretype_errors.PretypeError(_env, _evmap, pterr) ->
        List [Atom "Pretype_errors.PretypeError";
              List [Ser_pretype_errors.sexp_of_pretype_error pterr]]

Maybe changes in sexplib have broken this? I'll have a look.

I thought we had already opened an issue for the general problem, but indeed, I was aware of it, and a systematic solution should hopefully happen.

• [errors] Introduce error registration API rocq-prover/rocq#12602 should allow us to mark all the exceptions that carry an env
• and a way to provide handles to large objects so they can be queried lazily, or to simulate sharing in some way.

Now that I think of it, I guess that we should add a flag to serlib/ser_environ.ml to avoid this by default, as uses of environment serialization are very special.

[ejgallego]

Sorry for the delay, I've confirmed the bug.