Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Create a coq formatter #158

Open
ogiekako opened this issue Sep 3, 2020 · 4 comments
Open

Create a coq formatter #158

ogiekako opened this issue Sep 3, 2020 · 4 comments
Labels
enhancement New feature or request

Comments

@ogiekako
Copy link

ogiekako commented Sep 3, 2020

Reproduction:

  1. Open foo.v, which is not formatted, e.g.
Inductive day : Type :=
  | monday
    | tuesday
  | wednesday
    | thursday
  | friday
  | saturday
  | sunday.
  1. Press F1 && Format Document.

Got:

  • The source code isn't formatted.
  • VS Code show the message "There is no formater for 'coq' files installed".
  • I press the button "Install Formatter..." on the message, but no candidates are listed.

Expected:
The source code is formatted.

@Zimmi48
Copy link
Member

Zimmi48 commented Sep 7, 2020

But there is no formatter for Coq source code, so I don't see why you would expect a different behavior. Furthermore, this is not really related to VsCoq, is it? The "Format Document" command is provided by default by VsCode.

@gares
Copy link
Member

gares commented Sep 8, 2020

The I guess this bug can be turned into a feature request...

@artagnon
Copy link

Once rocq-archive/coq-serapi#191 is fixed, it'll be trivial to write a vscode extension that calls the formatter.

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 31, 2020

There are good chances though that the beautifier will not be a satisfying formatter (at least not before many fixes). It has hardly been maintained at all.

@fakusb fakusb added the enhancement New feature or request label Dec 17, 2020
@rtetley rtetley changed the title Format Document doesn't work Create a coq formatter Sep 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

5 participants