prevent ++ from becoming ⧺ when it is a proof script bullet

[jonleivent]

The second level proof script bullet ++ shouldn't get folded into ⧺, as this both looks strange and confuses indenting. Can symbol folding get turned off in certain spots?

Ideally, it would be nice to have proof script bullets highlighted in some way so that they look like buttons - and when depressed, they hide/show that part of the proof script tree. I know hide/show and outline minor modes are supposed to do this, but have they ever worked with Coq proof scripts?

[cpitclaudel]

Hey Jonathan,

Thanks a lot for the cool feedback!

The second level proof script bullet ++ shouldn't get folded into ⧺, as this both looks strange and confuses indenting. Can symbol folding get turned off in certain spots?

I don't use bullets in that way; when do you use ++? (Could you give me a small example? I'll add it to my tests!)

More generally, I'm updating this list of bindings soon, based on the experience gathered since launch. The new list I'm going to use is this:

(defcustom company-coq-prettify-symbols-alist '(("|-" . ?⊢) ("True" . ?⊤) ("False" . ?⊥)
                                     ("->" . ?→) ("-->" . ?⟶) ("<-" . ?←)
                                     ("<--" . ?⟵) ("<->" . ?↔) ("<-->" . ?⟷)
                                     ("=>" . ?⇒) ("==>" . ?⟹) ("<==" . ?⟸)
                                     ("~~>" . ?⟿) ("<~~" . ?⬳) ("fun" . ?λ)
                                     ("forall" . ?∀) ("exists" . ?∃) ("/\\" . ?∧)
                                     ("\\/" . ?∨) ("~" . ?¬) ("+-" . ?±)
                                     ("<=" . ?≤) (">=" . ?≥) ("<>" . ?≠) ("*" . ?×)
                                     ;; ("++" . ?⧺) ;; Not present in TeX fonts
                                     ;; ("nat" . ?𝓝) ("Prop" . ?𝓟) ;; Rather uncommon
                                     ;; ("N" . ?ℕ) ("Z" . ?ℤ) ("Q" . ?ℚ) ;; Too invasive
                                     ("nat" . ?ℕ) ("Prop" . ?ℙ) ("Real" . ?ℝ) ("bool" . ?𝔹))
  "An alist of symbols to prettify.
Assigned to `prettify-symbols-alist' in Emacs >= 24.4."
  :group 'company-coq
  :type 'alist)

It uses more common symbols (fixing the other problem you reported). It doesn't include ⧺, either, so maybe this problem will just go away :)

Emacs 25 has a way to fine-tune prettification, but it's not available in Emacs 24.4, unfortunately.

[cpitclaudel]

I know hide/show and outline minor modes are supposed to do this, but have they ever worked with Coq proof scripts?

Company-coq does set up outline-mode, but outline mode just has a notion of "titles"; it doesn't have much in the way of proper folding (you can try it with C-c C-/ and C-c C-\, although the first command is disabled by default due to its potential for confusion).

`hide-show' is a better candidate, and I have had local support for it for a while, but I haven't pushed it to master yet (due to the refactoring I alluded to). I just cleaned it up and pushed it to my working branch.

Ideally, it would be nice to have proof script bullets highlighted in some way so that they look like buttons - and when depressed, they hide/show that part of the proof script tree.

I actually really like this clicking idea! I've implemented it for bullets (I'll look at braces later). Here's how it looks:

Would you be interested in helping me test this feature (and the general refactoring)? It's on the massive-cleanup branch of the repo.

[jonleivent]

Here's an example of ++ used as a proof script bullet:

which is from https://github.com/jonleivent/mindless-coding-phase2

My proofs get pretty heavily nested, as they correspond to programs, so maybe I'm using the new multiple-levels-of-bullets more than most would. But, as you see, I also use ++ as an operator (list append - or in this case - erasable list append), so I appreciate folding it to make it look nicer. Although, I find that I often need a space after it to make it fold (if the next char is an operator char, as with my use of the "^" operator as an erased list singleton "[ .. ]"). I guess that's the standard folding mechanism - and maybe it is properly encouraging me to put spaces into these terms to make them more readable. Maybe I will revisit the notation I use for erased singleton lists as well.

The bullet clicking looks great in your example! I would like to try it out. Currently, my emacs is using the MELPA version of company-coq, but I have cloned the git repo, so I should switch over to test this out. Does it unfold if you step into that part of the proof? That would be very nice.

However, one issue I see: Coq's "Proof with tactic" command will make ellipses often appear at the end of proof script lines - so using ellipses for hiding sub-bullets might confuse, unless it is highlighted in some special way. Maybe a box around the ellipses?.

[cpitclaudel]

Thanks a lot for the example! I haven't had much experience with 8.5 yet.

I've extended that feature to support all sorts of bullets. One disagreeable thing is that there will be false positives here and there; it's too costly performance wise to do a precise check to see whether e.g. a + is a bullet or an operator, so I went with a seemingly decent heuristic.

I'll investigate automatic unfolding. As for the ... symbol, I should be able to change it to another symbol by hacking into the buffer's display table (the dots are inserted by Emacs itself and are not directly user-customizable otherwise)

Thanks a lot for your feedback and suggestions!

[cpitclaudel]

Here's what things look like with a custom ... symbol:

(I've just pushed that)

[jonleivent]

I think that looks pretty good, even in the dark ;)

[jonleivent]

OK - now that I have massive-cleanup working, here are some suggestions:

• make Proof. a bullet that hides the entire proof.
• make hidden parts of the proof unhide when they are stepped into with the cursor for any reason (I see that it already does this for incremental search, but not for stepping the proof).
• if the first line of a subproof is long, then the ellipses is all the way at the end of the line, possibly even wrapped, and might not be easily noticed. Maybe the bullet itself should change somehow when the subproof is hidden?
• if the last bullet has unbulleted things after it (like Unshelve or Grab Existential Variables), they are hidden by that last bullet, and probably shouldn't be. That's probably really hard to prevent. Maybe at least for Grab Existential Variables, which can only be used when the proof is otherwise complete?
• I noticed cases where things that are not bullets are misidentified as bullets. Like a sumbool return type for a function where the line was broken at the + {...}. Is it the case that a bullet can be distinguished from these other cases by the fact that the previous line (modulo comments) must have ended with a "."? Or would such complex searches (not a simple regexp) really slow things down?

By the way, the local character folding stuff is now working for me in the goals window! All good!

[cpitclaudel]

Glad to here the branch is working :)

make Proof. a bullet that hides the entire proof.

Good idea. I just tried it, though, and it doesn't work that well; the issue is that hs-minor-mode is a bit primitive (it only lets you specify one pair of openers and closers. That feature is available through outline-mode though (using C-c C-/), so maybe it isn't that bad?

make hidden parts of the proof unhide when they are stepped into with the cursor for any reason (I see that it already does this for incremental search, but not for stepping the proof).

Definitely on my todo list. I'd also like a good keybinding for folding or unfolding the enclosing block (maybe S-TAB?).

if the first line of a subproof is long, then the ellipses is all the way at the end of the line, possibly even wrapped, and might not be easily noticed. Maybe the bullet itself should change somehow when the subproof is hidden?

That's probably a good idea, although I wonder how to implement this cleanly.

if the last bullet has unbulleted things after it (like Unshelve or Grab Existential Variables), they are hidden by that last bullet, and probably shouldn't be. That's probably really hard to prevent. Maybe at least for Grab Existential Variables, which can only be used when the proof is otherwise complete?

That's indeed really tricky. The current code relies on SMIE parsing to delimit bullet bodies; unless we can make SMIE aware of the special case of "stuff after the last bullets", it will be hard to support this.

I noticed cases where things that are not bullets are misidentified as bullets. Like a sumbool return type for a function where the line was broken at the + {...}.

Yes, I noticed that one too :/

Is it the case that a bullet can be distinguished from these other cases by the fact that the previous line (modulo comments) must have ended with a "."? Or would such complex searches (not a simple regexp) really slow things down?

Complex searches are tricky. I have one that never seem to make mistakes (essentially navigates back up all the way to the top, and checks for "Proof", but it's much too slow.
A good test there is really hard to come up with, so we have to make do with heuristics. It's frustrating (hopefully one day Coq itself can give us hints for highlighting and parsing). I'm a bit afraid of adding complexity to the font-locking, since coq-mode is already not the most responsive. I'd vote for waiting a bit, and seeing how broken the current heuristic is, before we add extra complexity.

By the way, the local character folding stuff is now working for me in the goals window! All good!

Brilliant! Thanks for testing!

[cpitclaudel]

make hidden parts of the proof unhide when they are stepped into with the cursor for any reason (I see that it already does this for incremental search, but not for stepping the proof).

Definitely on my todo list. I'd also like a good keybinding for folding or unfolding the enclosing block (maybe S-TAB?).

Done and done (using S-TAB). Incremental search unfolds temporarily; stepping in leaves the proof unfolded. At this point the feature feels pretty complete, so I'll close this issue :)

[jonleivent]

When the cursor is right at the end of the last line in the subgoal's script, S-Tab does nothing.

Stepping in via C-c C-n unfolds, but by toolbar next leaves it folded. Is there a way I can change that?

[cpitclaudel]

Thanks for spotting these issues! I don't have a good grasp on the first one yet unfortunately (I know why it happens, but not how to fix it yet. I opened a separate issue

The other one is fixed!

[jonleivent]

Thanks, Clément!