Stream: Proof General users

Topic: Better emacs indentation

Daniel Hilst Selli (Mar 14 2022 at 20:11):

Not sure if this is offtopic but. How can I make emacs stop aligning the current line based on the previous line.

If I have something like this

Foo.Bar.Tar(
Zar

And I press tab on the second line I get

Foo.Bar.Tar(
            Zar

While I want

Foo.Bar.Tar.(
  Zar

(2 spaces)

This is particularly bad with Coq mode because I have long module names, today I'm indenting line by line manually to keep this style, any ideas on how to configure this?

Notification Bot (Mar 14 2022 at 20:18):

This topic was moved here from #Coq users > Better emacs indentation by Karl Palmskog.

Ana de Almeida Borges (Mar 14 2022 at 20:18):

Yup, this is super annoying. I don't know how to stop it from happening, the best I have is disabling the aggressiveness, but you don't mention it, so perhaps you already fixed that part of the problem.

Ana de Almeida Borges (Mar 14 2022 at 20:22):

I just remembered that link is still in private beta. Basically what I mean by aggressiveness is that after the text gets indented and you fix it, it gets unfixed automatically as soon as you leave the line. You can avoid it by adding the following to your user-config:

(eval-after-load "proof-script"
  '(progn
     (setq electric-indent-mode nil)
     ))

Daniel Hilst Selli (Mar 14 2022 at 20:32):

Thank you Ana, I put it on my config. My problem seems not to be with electric-indent-mode though, is more by the way that the indentation align columns. I'm looking on internet but couldn't find anything, people usually like this way, but for coq is being terrible for me, because it makes keeping the 80 columns limit much harder

Ana de Almeida Borges (Mar 14 2022 at 20:46):

Yeah, I'm 100% in agreement with you and I also couldn't find anything.

Ali Caglayan (Mar 14 2022 at 21:35):

I see something here: https://proofgeneral.github.io/doc/master/userman/Customizing-Proof-General/#User-options

Ali Caglayan (Mar 14 2022 at 21:35):

An option called PA-script-indent?

Ali Caglayan (Mar 14 2022 at 21:36):

By default it is enabled, does disabling it solve this issue?

Stefan Monnier (Mar 14 2022 at 22:28):

The "aggressive" reindentation described by Ana is unknown to me and I don't know what might trigger it, so I suggest trying to reproduce it with a a vanilla config and if you can still reproduce it, report it as a bug. Similarly, the indentation right after an open paren (which I call "a hanging open paren") should not be as you've shown, so I suggest you file a bug report for that as well.

Ana de Almeida Borges (Mar 14 2022 at 22:39):

As far as I can tell the aggressiveness is just electric-indent-mode in action. Perhaps I explained badly: the problem is not that it's literally impossible to change emacs' preferred indentation; the problem is that every time you click Enter both the line you left and the line you reach get indented, regardless of whether you'd previously manually indented it or not. Thus it feels aggressive to me because my default is to press Enter, fix the indentation, write whatever I want to write, press Enter, and lose the indentation I had just fixed.

Ana de Almeida Borges (Mar 14 2022 at 23:08):

Ali Caglayan said:

By default it is enabled, does disabling it solve this issue?

No, I don't see any difference in behavior after disabling it :/

Ana de Almeida Borges (Mar 14 2022 at 23:18):

There are a number of options that seem very promising for editing indenting behavior but get completely ignored by my setup, no matter their value. Examples are the coq-script-indent mentioned by Ali, coq-indent-box-style, which according to its documentation sets precisely what kind of indentation is preferred after a hanging open paren, and others I also tested for sanity checks such as coq-indent-proofstart.

Ana de Almeida Borges (Mar 14 2022 at 23:19):

My working assumption right now is that I have some setting that is overshadowing all of these options.

James Wood (Mar 15 2022 at 09:12):

I think "indentation respects α-equivalence" is a common and well defined enough desideratum that one would expect it to be supported.

Daniel Hilst Selli (Mar 15 2022 at 13:30):

Yeah, to me that align behavior seems to be hard coded, for example in this picture, I would like the indented line to be on the purple square image.png

Daniel Hilst Selli (Mar 15 2022 at 13:32):

I think the only way to get this working would be hacking the indentation el files by hand, but back to emacs about some weeks after years not using, maybe I'm missing some new feature

Jaehwang Jung (Mar 15 2022 at 14:49):

A solution I came up with is to map tab to a very simple indentation function (tab-to-tab-stop) and map another key to PG's indentation function (smie-indent-line). Then you can use tab most of the time without surprise and can still use PG's indenting when you really want it. https://github.com/tomtomjhj/init.el/blob/c621df748838e5d8ae32bca381cf50c1b52eb852/init.el#L433

Pierre Courtieu (Mar 19 2022 at 14:48):

Daniel Hilst Selli said:

...
And I press tab on the second line I get

Foo.Bar.Tar(
            Zar

I get

Foo.Bar.Tar.(
    Zar

(4 spaces)

What version of proofgeneral do you have?

Pierre Courtieu (Mar 21 2022 at 12:08):

By the way, before this indentation is fixed (working on it) you can use a trick to make indentation not indent a given line: put a comment with the word fixindent in it.

Pierre Courtieu (Mar 29 2022 at 21:59):

This is now fixed in pg master branch (and today's elpa package).

Andrey Klaus (Mar 30 2022 at 05:46):

cool! Thanks! already downloading it

Last updated: Oct 13 2024 at 01:02 UTC