search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
336 stars 68 forks source link

Formatting Proof view #749

Closed oddcoder closed 4 months ago

oddcoder commented 7 months ago

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

image

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 commented 7 months ago

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 commented 6 months ago

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 commented 6 months ago

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 commented 6 months ago

Bug: Screenshot from 2024-03-22 10-33-51 Expected: Screenshot from 2024-03-22 10-34-23 Documentation of the box module Coq uses behind the scenes: https://v2.ocaml.org/api/Format.html