Feature requests for the new indentation engine

[cpitclaudel]

Hi @Matafou

Thanks for your work on the new indentation engine! Here are a few things that could be improved.

The following samples are indented how I would expect them; PG's new indentation changes them:

Instance spec_of_upstr : spec_of "upstr" :=
  fnspec! "upstr" s_ptr wlen / (s : list byte) R,
    { requires tr mem :=
        wlen = word.of_Z (Z.of_nat (length s));
      ensures tr' mem' :=
        tr' = tr }.

Goal forall x,
    x =
    x.

Goal (True /\
      True /\
      True).

Lemma t :
  (forall x,
     x = x).
Qed.

match x with
| ABC =>
  DEF
end

[monnier]

Goal forall x,
    x =
    x.

While I can agree with (or understand) the other choices, FWIW, the above looks wrong to me.

Goal (True /\
      True /\
      True).

And here, I'll note that the GNU coding convention recommends breaking the line before infix operators rather than after them. I found it odd, to be honest, but it's growing on me (tho still definitely not for the , and ;).

[cpitclaudel]

While I can agree with (or understand) the other choices, FWIW, the above looks wrong to me.

That's how PG used to do it; not sure if it's the "right" way, but it lines things up nicely (often you have roughly the same thing before and after the equal, modulo some tweak)

[cpitclaudel]

And here, I'll note that the GNU coding convention recommends breaking the line before infix operators rather than after them.

yes, I dislike this convention for the same reason: things don't line up:

uint32_t x = ((x0 << 24)
              | (x1 << 16)              
              | (x2 <<  8) 
              | (x3 <<  0));

vs.

uint32_t x = ((x0 << 24) |
              (x1 << 16) |
              (x2 <<  8) |
              (x3 <<  0));

Dafny does it better:

uint32_t x = (| (x0 << 24)
              | (x1 << 16)              
              | (x2 <<  8) 
              | (x3 <<  0));

(You're allowed to prefix one copy of the infix operator in a chain, which works nicely for && in particular)

[Matafou]

Hi! Nice to have feedback!

Hi @Matafou

Thanks for your work on the new indentation engine! Here are a few things that could be improved.

The following samples are indented how I would expect them; PG's new indentation changes them:

Instance spec_of_upstr : spec_of "upstr" :=
  fnspec! "upstr" s_ptr wlen / (s : list byte) R,
    { requires tr mem :=
        wlen = word.of_Z (Z.of_nat (length s));
      ensures tr' mem' :=
        tr' = tr }.

Goal forall x,
    x =
    x.

Goal (True /\
      True /\
      True).

Lemma t :
  (forall x,
     x = x).
Qed.

These 3 cases are the same problem: you want more "boxed" style-indentation but not everywhere. If you (setq coq-indent-box-style t) the indentation is like you want BUT you have boxed indentation everywhere. In non boxed indentation style the level of nesting is generally the rule:

   (forall x,
       x = x).

and

   (           forall x,
       x = x).

are both indented like if each nesting had its own line:

   (
     forall x,
       x = x).

I will think about doing an exception in this case, but I need to understand what is "this case" exactly. I have to understand when and when not to have boxed style.

match x with
| ABC =>
  DEF
end

I don't understand this one. To me the => is not symmetric (like = is). It is more like := to me.

[Matafou]

These 3 cases are the same problem

Sorry only the last case ((forallx,\n x = x) is about boxed style. The others should be easy to fix.

[cpitclaudel]

I don't understand this one. To me the => is not symmetric (like = is). It is more like := to me.

It's just a mater of saving horizontal space for long lines; the vertical bars already provide clear visibility on what is part of each case. But mostly it's that this is how things used to be, so it makes editing existing code more painful.

[cpitclaudel]

The others should be easy to fix.

Thanks!!

[cpitclaudel]

@monnier Here is a good example from my work today: I much prefer

    Lemma word_morph_eqb_u :
      (0 <= z1 < 2 ^ width /\
       0 <= z2 < 2 ^ width) \/
      (- 2 ^ (width-1) <= z1 < 2 ^ (width-1) /\
       - 2 ^ (width-1) <= z2 < 2 ^ (width-1)

over

    Lemma word_morph_eqb_u :
      (0 <= z1 < 2 ^ width /\
         0 <= z2 < 2 ^ width) \/
      (- 2 ^ (width-1) <= z1 < 2 ^ (width-1) /\
         - 2 ^ (width-1) <= z2 < 2 ^ (width-1)

[cpitclaudel]

Btw, one more thing that I've noticed is that the indentation engine now seems to be more "global" For example I commonly write things like this:

Module A.
Section A.
  Context ….

  Definition ….
End A.
End A.

I usually don't indent the inner section, and previously the indentation engine aligned all top-level statements in the section based on my (manual) indentation of the first one. But not it wants to indent all top-level statements "correctly" (two levels deep), even if the preceding ones are indented just one level deep).

[Matafou]

I don't see this behaviour. If the line "Context" is shifted then so are the others.

[cpitclaudel]

I don't see this behaviour. If the line "Context" is shifted then so are the others.

You're right… Where did I get that idea from? Sorry :/

[Matafou]

Instance spec_of_upstr : spec_of "upstr" :=
  fnspec! "upstr" s_ptr wlen / (s : list byte) R,
    { requires tr mem :=
        wlen = word.of_Z (Z.of_nat (length s));
      ensures tr' mem' :=
        tr' = tr }.

This one is fixed by PR #647.

I am not sure to strongly try the remaining ones, even if this one

Lemma t :
  (forall x,
       x = x).
Qed.

is indeed quite ugly imho.