Rapid slow down of Proof General interactions with OCaml 5.x

[fdupress]

This is reviving the OG #390, which I had prematurely conflated with the general memory consumption issues related to OCaml 5.0 (now fixed with OCaml 5.1).

In particular, the following still occurs in interactive usage.

Triggering this requires a large context I cannot include here, and only affects interactive usage of EasyCrypt—while pretty-printing large proof goals for display. As far as I can tell, it cannot be triggered through non-interactive testing.

I have tried bisecting recent commits on pretty printing to no avail, then tested different versions of ocaml, since only one of my computers displayed the behaviour.

For constant easycrypt version, computer, proof context and printed goal:

With ocaml 4.14.2, printing is instant. With ocaml 5.1.0, printing takes an increasing amount of time, which grows quickly with the number of "printful" interactions.

To reproduce:

0. Install EC and necessary dependencies in an OCaml 5.1.0 switch,
1. pick a somewhat large file,
2. open it in emacs with PG;
3. pick a proof point (ideally, not an SMT call) late in the file, and hit Ctrl-B. So far so good.
4. Repeatedly undo and redo a proof step.

Expected behaviour: The proof step gets undone and redone with no perceptible performance change.

Observed behaviour: The time it takes to both undo and redo will increase rapidly. Memory used by EC goes up with each interaction (by a few 10s of MB!), but not sufficiently to justify the massive slow down.

Changing the proof step to be a trivial failure halves the wait time, which seems to indicate that something is going on both in parsing and formatting messages for emacs. This may also affect print-heavy non-interactive behaviour, but I have not tested.

Performing step 0 with an OCaml 4.14.2 switch yields the expected behaviour.

Thanks to @alleystoughton for reporting and early investigation. This was confirmed on a Mac M1 (by Alley) and Linux (by me).

[fdupress]

Hold on to your hats: the issue does not occur if emacs is running in TUI mode. (I was trying to record the behaviour.)

I'm looking into the emacs angle. @alleystoughton can you please confirm your emacs version, and that you're on the latest PG? (I still don't understand why switching ocaml compiler would make a difference, but we'll figure that out later.)

[alleystoughton]

I'm running GNU Emacs 29.1 from https://emacsformacosx.com

[alleystoughton]

And yes, on latest PG from opam.

[fdupress]

Thanks. Sorry for the red herring: the issue does pop up regardless of emacs interface (phew! that would have been a real puzzler).

Recording here, after a few tries so it starts already quite slow.

The proof is irrelevant. The left-most buffer is the *easycrypt* buffer, and it clearly shows that the message is slow to print, but even slower to end. Most of the slow down is due to increasingly long delays in finishing the message once all printing is done.

Failures fail quickly, so it looks like something in goal printing whose complexity grows with the number of calls that have been made to the goal printing function.

[strub]

This has nothing to do with ProofGeneral. I just noticed that having a tight-loop with a lot of printing (cumulatively) slow-down things too.

[alleystoughton]

Seems it might be possible to send the OCaml developers a self-contained program illustrating the bug?

[strub]

Self-contained, but far from being minimal. I don't even understand what is, as of today, the best way to profile an OCaml program.

[strub]

See #517

[strub]

Is this issue been fixed by #517?

[fdupress]

Yes.

[strub]

Closing then.