Support ssreflect-style indentation

[ejgallego]

Dear PG devs,

it would be great if proofgeneral coq could support ssreflect's style indentation.

In order to maximize horizontal proof space, the ssreflect library uses a more conservative indentation, for instance, this is typical code:

Section A.

Lemma a : P.
Proof.
case/orP=> ...
  by rewrite U.
exact: Pm.
Qed.

End A.

AFAICT, the current recommendation is to disable indentation which is a pity. IMHO we could:

• have an explicit variable use-ssreflect-indent.
• automatically detect the import of ssreflect and switch the variable on.

I would be happy to try to provide a patch if the PG devs agree on how they would like this feature to be integrated.

Thanks, Emilio

[Matafou]

I think this is what you are looking for:

(setq coq-indent-proofstart 0) (setq coq-indent-modulestart 0)

Please confirm before I close the bug.

Indeed this was asked by another ssreflect guy.

Be careful that ssreflect bullets may not be indented as you want.

Best, P.

[ejgallego]

Hi @Matafou , thanks, indeed I saw that advice in the mailing list some time ago. I'll check if the settings are enough.

IMHO it would be great to document the setting before closing the bug, if a specified switch is not desired.

E.

[cpitclaudel]

IIRC ssreflect already distributes a lisp file with a number of PG settings (like extra tactics to highlight). Should these be added there?

[ejgallego]

Hi @cpitclaudel , the file is this one:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/pg-ssr.el

It seems that at least part of it has already been merged, and it doesn't include documentation. I need to submit a patch to math comp for fixing their docs.

I'm currently testing @Matafou settings, will report back and close the bug if appropriate soon.

[ejgallego]

Hi, I have been testing this and so far looks good.

There is a small tweak to do thou, IMO both variables should be buffer local, to allow both styles to coexists. I should get a patch ready soon.

[Matafou]

Agreed, buffer local would be cool.

But how would you set it? Each time you open a file? Pretty painful. This is typically a setting that should be set by a .dir-locals.el written by library authors to enforce a homogeneous style in each library. That would become buffer local this way. And if one wants to set it really buffer per buffer then it should be set by a file variable.

Do you have something better in mind?

P.

[ejgallego]

Sounds good! I hope to have time in the next couple of weeks to test something like that.

[pi8027]

(setq coq-indent-proofstart 0) (setq coq-indent-modulestart 0)

Those settings do not seem to work in the current master branch of PG. Is there anyone who can confirm it?

[Matafou]

I confirm. It got removed in the refactoring of indentation. I will put this back quickly. Sorry for the inconvenience.

[Matafou]

By the way is this still open? Do we want these variables buffer local?