Automatically insert Coq output as a comment

[whonore]

@whonore Is there a way to insert the output of coq inside the current buffer after the line that was just executed?

Originally posted by @ju-sh in https://github.com/whonore/Coqtail/issues/39#issuecomment-809239615

For example,

Check nat.

could become

Check nat.
(*
nat
     : Set
*)

after execution.

The content that appear in the info panel appearing as a comment right after the block that produced that output.

[whonore]

This is an interesting idea for a feature, but there's a few details that need to be worked out before we could add it.

1. If you check multiple sentences with CoqToLine does it insert the output under each sentence, or at the end of the whole block?
2. What if there are multiple sentences on a line and you step over them one at a time? E.g., given

Check nat. Check bool.

should :CoqNext | CoqNext give

Check nat. Check bool.
(* 
nat
      : Set
*)
(* 
bool
      : Set
*)

or

Check nat. Check bool.
(* 
bool
      : Set
*)
(* 
nat
      : Set
*)

3. Does this need to be interactive (comments are inserted as you call CoqNext or CoqToLine) or is it sufficient to have a CoqCommentFile command that does the whole file at once?

As suggested in https://github.com/whonore/Coqtail/issues/39#issuecomment-809908833,

call append('.', ['(*'] + getbufline(b:coqtail_panel_bufs['info'], 1, '$') + ['*)'])

could be a temporary workaround that gets you a similar behavior.

[ju-sh]

I'm a beginner in coq and I haven't done any complex stuff yet. Based on my limited experience, I think

1. If multiple sentences are check with CoqToLine, the output may be inserted under each sentence instead of the whole block.

Like,

Check nat.
Check I.

when executed with CoqToLine could produce

Check nat.
(*
nat
     : Set
*)
Check I.
(*
I
     : True
*)

---

2. If there are multiple sentences on a line like

Check nat. Check bool.

having the output in the same order like

(*
nat
      : Set
*)
(*
bool
      : Set
*)

looks better. But would it be trickier to implement?

---

3. Allowing interaction would be cool.

But a command to do the commenting at once could come helpful as well maybe?

Or would it be sufficient to do something like CoqToLine at the end of the file so that the same effect can be obtained?

[whonore]

I'll have to keep thinking about this and how best to implement it, if at all. One issue with comments is they can go out of sync with the code so I'm wondering if using something like popups or 'balloonexpr' would be better. Also, have you taken a look at Alectryon to see if it does what you need?

[ju-sh]

I'll have to keep thinking about this and how best to implement it, if at all.

Yeah, if it's doable and someone finds time to do it :-)

have you taken a look at Alectryon

Didn't even know about it. Gotta check it out. Thanks!

One issue with comments is they can go out of sync with the code

How do you mean? Like in the case with multiple commands on the same line or something? (I'm new to this :-D Just to know).

[whonore]

How do you mean?

For example if you have

Check nat.
(* 
nat
      : Set
*)

But then you change nat to bool and forget to recheck the line the comment will remain and be wrong. Of course it's not hard to fix, but it would be nice to have something that automatically updates itself when the code changes.

[ju-sh]

Okay, I think the 'comment going out of sync' problem is about updating the 'output-comment' when the input changes.

How about making this 'output as comment' feature just as something to help the user without the feature itself assuming too many responsibilities?

I mean, the user has the option to insert the output as a comment right after the input line being checked (maybe as a function that coqtail exposes or something).

The feature itself is not responsible for maintaining that result. It just inserts the output right after the line being checked. Whether a 'comment-output' already existed there doesn't matter as far as the feature is concerned.

If we take that approach, we also needn't worry checking if a comment that the user manually inserted was an 'output-comment' as well.

[whonore]

That's definitely also an option and could be implemented pretty easily with the workaround suggested earlier using append and b:coqtail_panel_bufs.