Formatter can't handle proofs consisting only of `Admitted.` or (I think) proofs which don't start with a tactic

[BridgeTheMasterBuilder]

121 does not fully fix the issue raised by #119. E.g. proofs which are only Admitted. (to be implemented with PR #124)

Generally speaking, I feel like the current heuristic of VernacStartTheoremProof followed by a tactic is not good. After all, a proof may very well start with something other than a tactic. However, removing the is_tactic guard from the match arm makes a bunch of tests fail so I left it alone.

Adding another heuristic such as is_admitted (which I have already done in my local fork) on top of that is a hack at best, I think a more robust solution to this problem is required.

[toku-sa-n]

Yes, that was an ad-hoc way. Honestly, I don't know what the best way here is, but I think adding more heuristics is better because we can't list all the possible values that require an extra indent due to VernacExtend.

[BridgeTheMasterBuilder]

Yes, that was an ad-hoc way. Honestly, I don't know what the best way here is, but I think adding more heuristics is better because we can't list all the possible values that require an extra indent due to VernacExtend.

Could you elaborate? Why is it not possible to make it so that starting a proof increases the indentation level unconditionally except in the only two (?) edge cases of it being a definition of an "axiom" with immediate invocation of Admitted. or an immeditely abandoned proof with Abort.? I can't think of any other case where Coq will allow you to complete empty proofs, but I might be overlooking something.

[toku-sa-n]

My concern was that a VernacExtend might contain things that usually don't need an extra indent. Currently we assume that a VernacExtend only contains a ltac tactic, but in fact it may contain other things. Also it seems that users can add things by writing a Coq plugin, and I think the parser will represent them as VernacExtends. I totally don't know about Coq's plugin system, but if we can say a VernacExtend never contains such things, things will be easy.

Btw,

Why is it not possible to make it so that starting a proof increases the indentation level unconditionally except in the only two (?) edge cases of it being a definition of an "axiom" with immediate invocation of Admitted. or an immeditely abandoned proof with Abort.?

In fact, there are other cases where indent is not required. For example, an Example can define something like a Definition. The following is a valid Coq code.

Example foo := 4.

Definition bar := 4.

[BridgeTheMasterBuilder]

My concern was that a VernacExtend might contain things that usually don't need an extra indent. Currently we assume that a VernacExtend only contains a ltac tactic, but in fact it may contain other things. Also it seems that users can add things by writing a Coq plugin, and I think the parser will represent them as VernacExtends. I totally don't know about Coq's plugin system, but if we can say a VernacExtend never contains such things, things will be easy.

Btw,

Why is it not possible to make it so that starting a proof increases the indentation level unconditionally except in the only two (?) edge cases of it being a definition of an "axiom" with immediate invocation of Admitted. or an immeditely abandoned proof with Abort.?

In fact, there are other cases where indent is not required. For example, an Example can define something like a Definition. The following is a valid Coq code.

Example foo := 4.

Definition bar := 4.

Actually, Coq treats Example exactly the same as a Definition as far as I can tell, as VernacDefinition, not as a VernacStartTheoremProof (that applies to Examples that are proofs and definitions, just like Definition can have a DefineBody or a ProveBody, it's the same thing with Example):

(* test.v *)
Example foo := 4.

sercomp --mode=sexp --printer=human test.v
((v
  ((control ()) (attrs ())
   (expr
    (VernacDefinition (NoDischarge Example)
     (((v (Name (Id foo)))
       (loc
        (((fname (InFile (dirpath ()) (file test.v)))
          (line_nb 1) (bol_pos 0) (line_nb_last 1)
          (bol_pos_last 0) (bp 8) (ep 11)))))
      ())
     (DefineBody () ()
      ((v (CPrim (Number (SPlus ((int 4) (frac "") (exp ""))))))
       (loc
        (((fname (InFile (dirpath ()) (file test.v)))
          (line_nb 1) (bol_pos 0) (line_nb_last 1)
          (bol_pos_last 0) (bp 15) (ep 16)))))
      ())))))
 (loc
  (((fname (InFile (dirpath ()) (file test.v))) (line_nb 1)
    (bol_pos 0) (line_nb_last 1) (bol_pos_last 0)
    (bp 0) (ep 17)))))

So, that does not affect treatment of VernacStartTheoremProof in this case with regards to indentation handling AFAICT.

[toku-sa-n]

Ah, thanks. I wasn't aware of that. On second thought, I think it's ok to indent unconditionally unless the next is either a VernacEndProof or a VernacAbort.

(I said we can't guess what a VernacExtend has, but actually we can in a sense, because serapi provides a limited set of serializers/deserializers, and we can pp if a VernacExtend has things supported by serapi, or have to say "Sorry, your plugin is not supported.")

[toku-sa-n]

@BridgeTheMasterBuilder Will you send a PR, or can I do it?

[BridgeTheMasterBuilder]

@BridgeTheMasterBuilder Will you send a PR, or can I do it?

Unfortunately I am a bit busy the next two weeks so I won't have a lot of time to work on it, so feel free to do it yourself. But if you want to work on something else I can get around to it eventually.

[toku-sa-n]

@BridgeTheMasterBuilder Could you check #163 when you have time?

[BridgeTheMasterBuilder]

@BridgeTheMasterBuilder Could you check #163 when you have time?

Everything looks good to me :)  

[toku-sa-n]

OK, thanks!