Formatting Proof view

[oddcoder]

Legacy vscoq allows proofs to be formatted nicely, But this is no the case for the current vscoq as shown below:

This is makes it extremely hard to follow computer science related proofs as the induction principles generated are very large and wordy. I often find myself having to copy paste it to a new tab and reformatting it by hand just to understand what I am trying to do.

[rtetley]

Hi and thanks for reporting ! Coud you give me an example to work with ? As far as I remember we had fixed the formatting issues when we switched to using ppstrings.

[Lee-Janggun]

https://gitlab.mpi-sws.org/iris/examples should work. Before, both the coq context and the proof goals were formatted nicely with good indentations. However, now there are no indentations.

[gares]

Hi and thanks for reporting ! Coud you give me an example to work with ? As far as I remember we had fixed the formatting issues when we switched to using ppstrings.

I can reproduce the same bug without Iris, it is sufficient to have a large goal.
I believe this is a regression, it seems formatting (like applying the box language) is not performed anymore.

[gares]

Bug:

Expected:

Documentation of the box module Coq uses behind the scenes:
https://v2.ocaml.org/api/Format.html