The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 2016-09-12 15:14, Beta Ziliani wrote:
> Dear Clément,

Dear Beta,

Thanks for the example.

> Coq Indent Box Style: off (nil)
> Coq Script Indent: off (nil)

Sorry; I meant to ask how you set the settings: through the Emacs "customize" 
interface, or using a plain setq in your .emacs?

The first setting is unrelated to the indentation of the example below (see 
its docs with C-h v); it seems that the second one is broken, however; a bug 
report would be useful.  It would also help if you pointed out which parts 
are different from old releases of PG.

> Example indent_test : True.

The fact that the code in question contains multiple keywords (is, and) 
doesn't help, but I can answer some of the questions :)

> Proof.
>   let why_this_is_indentend :=

I think you're looking for coq-indent-proofstart:

  (setq coq-indent-proofstart 0)

>       and why this is here in

I don't think we have a setting for continuation lines of ‘let’s.

>   x <- some MetaCoq code;
>     y <- ouch this shouldnt be indented;
>     ret why_isnt_this_indented_BTW.

Would (setq coq-indent-semicolon-tactical 0) help?

    Number of spaces used to indent after the first tactical semi colon of a 
serie.
      If set to 0, indetation is as follows:
       tac1;
       tac2;
       tac3;
       tac4.

       if set to 2 (default):

       tac1;
         tac2;
         tac3;
         tac4.

Otherwise, adding a parens fixes it: (x <- …). In general, I don't think you 
can expect PG to indent your notations properly, at least not without support 
from Coq.

> I prefer to set the tab as two spaces, and mange it myself. But Proof
> General is inserting its own indentation

Correct.  What do you usually bind TAB to? Rebinding it Coq mode should work 
too.

> (and sometimes in a weird way, see e.g. the two lines ending with ;).

This is expected; see the documentation that I pasted above :)

> And what is really pissing me off is that it is changing the
> indentation I wrote. For instance, if I decide to move the y <- ouch
> ... code so it is aligned with the previous line, after hitting enter
> PG will move it back to where it is in the code above. Maybe there are
> some other options I’m missing?

Are you using electric-indent-mode maybe?  That would explain the behavior of 
RET.  (PG doesn't do anything like this)

Cheers,
Clément.

> On Mon, Sep 12, 2016 at 3:58 PM, Clément Pit--Claudel
> <clement.pit AT gmail.com>
>  wrote:
>> Hi Beta,
>>
>> How do you set these settings? Can you share a snippet and show the 
>> expected indentation?
>>
>> Cheers,
>> Clément.
>>
>> On 2016-09-12 14:47, Beta Ziliani wrote:
>>> Hi list,
>>>
>>> I updated PG and now it is indenting my code in a way I don't want it
>>> to. I'm aware of the options Coq Script Indent and Coq Indent Box
>>> Style, however they seem to have no effect whatsoever. Any clues?
>>>
>>> Thanks,
>>> Beta
>>>
>>
>

Attachment: signature.asc
Description: OpenPGP digital signature