search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 88 forks source link

Indentation issue: "by" #453

Open RalfJung opened 4 years ago

RalfJung commented 4 years ago

The following code:

Proof using Fcontr.
  induction k as [|k IH]; simpl.
  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
    apply (contractive_0 map).
  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
    by apply (contractive_S map).
Qed.

gets auto-indented (select it, and hit "Tab") to

Proof using Fcontr.
  induction k as [|k IH]; simpl.
  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
    apply (contractive_0 map).
  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
      by apply (contractive_S map).
Qed.

Notice how the line starting with "by" got indented, for no apparent reason.

cpitclaudel commented 4 years ago

for no apparent reason.

The reason is that rewrite xyz by tactic (without the dot) is also valid, and that could reasonably be considered to need indentation. (I can't comment on how easy it would be to fix the issue)

RalfJung commented 3 years ago

The reason is that rewrite xyz by tactic (without the dot) is also valid, and that could reasonably be considered to need indentation.

I don't understand why by would be special here. IMO indentation (by exactly 2 spaces) should happen whenever this is a continuation of the tactic on the previous line, i.e. whenever the previous line does not end in a .. rewrite X by Y is not special here, e.g. the same should happen in

rewrite X Y Z
  Q.

(imagine those being long lemma names)

proux01 commented 3 years ago

I've added the following line to my .emacs to "fix" that issue

 '(coq-smie-user-tokens (quote (("by" . "now"))))
Matafou commented 3 years ago

The reason is that rewrite xyz by tactic (without the dot) is also valid, and that could reasonably be considered to need indentation.

I don't understand why by would be special here. IMO indentation (by exactly 2 spaces) should happen whenever this is a continuation of the tactic on the previous line, i.e. whenever the previous line does not end in a .. rewrite X by Y is not special here, e.g. the same should happen in

rewrite X Y Z
  Q.

(imagine those being long lemma names)

Coming back to this remark. Actually it would get indented like this(1) (both with current engine and the new one):

rewrite X Y Z
        B Q.

Whereas if "by" is known as a (infix) keyword then we have:

rewrite X Y Z
  by Q.

(1) for technical reason it is still the same in the new indentation engine.