Highlighting of evars

[proofgeneral]

Highlighting of evars

[jonleivent]

On 11/22/2015 09:48 PM, Clément Pit--Claudel wrote:

Evars are currently using a pretty agressive highlighting scheme
(heavy orange background). It's nice, but it's apply to slightly too
many things. In particular, it also ctaches Ltac binders ( as in
match _ with ?x = ?y). This is particulary unpleasant when reading
a large match-goal form using Print Ltac.

It used to be easy to fix the problem, since evars always used
numbers. In 8.5, however, evars now keep their names. If there was a
way to tell evars from non-evars I'd be all for highlighting them
differently, but I don't think there is such a way anymore; is
there?

Company-coq currently highlights ltac binders as variables in Coq
buffers. Maybe we should justhiglight all patterns like ?abc as
variables, instead of the heavy orange highlighting? It might even
make the new style evars more readable.

My $0.02: A goal that contains evars usually has to be handled very
differently from one that doesn't. How differently depends on where the
evars occur. So, it is very helpful if evars are highlighted
differently from normal variables.

Personally, I don't like the fact that evars have the same syntax as
pattern match variables - and have complained about this elsewhere.

However, if the ?id syntax is going to remain for both, then I'd mind it
less if match pattern variables shared the same highlighting as evars
than I would if evars shared the same highlighting as normal vars. I
print Ltac very rarely - mostly because it is far more useful to examine
a whole file of related Ltac than just a single tactic.

-- Jonathan

[cpitclaudel]

Hi @jonleivent,

I'd mind it less if match pattern variables shared the same highlighting as evars than I would if evars shared the same highlighting as normal vars.

This is currently the case. Here's the proposed change (left: original; right: new)

Can you comment on this specific change?

I print Ltac very rarely - mostly because it is far more useful to examine a whole file of related Ltac than just a single tactic.

Interesting; I don't examine whole files of tactics very often myself: instead, I very often copy an Ltac definition from the response buffer and redefine it.

[jonleivent]

You don't show what a normal var looks like in those samples, so I cannot tell the difference between the right sample's evars and what normal vars would look like in that color scheme. However, I like the background highlighting of evars because of how much it stands out. Maybe have this as a user-settable option?

[cpitclaudel]

You don't show what a normal var looks like in those samples, so I cannot tell the difference between the right sample's evars and what normal vars would look like in that color scheme.

Here it is:

The more I look at it and the more I find the background version hard to read, actually. For the printing Ltacs case, on the other hand, contrast

with

Maybe have this as a user-settable option?

It already is a user-settable option actually :) (and I already have this option set on my machine). My concern is just that PG devs end up living in a world quite different from that of other users, with enough options set that their PG doesn't look much like the standard PG. It happens often enough to me that someone looks at my emacs and says "wait how did you get PG to do that" that I want to implement better defaults.

[jonleivent]

Well, as long as it is a user-settable option (and it's name is??), I can't complain. Especially if it appears in a Customize Emacs options page, where I won't forget it.

As for devs living in a different world - maybe consider adding a test user login to your machine which uses a bare-bones ~/.emacs file?

[cpitclaudel]

Well, as long as it is a user-settable option (and it's name is??), I can't complain. Especially if it appears in a Customize Emacs options page, where I won't forget it.

M-x customize-face RET proof-eager-annotation-face RET :)

As for devs living in a different world - maybe consider adding a test user login to your machine which uses a bare-bones ~/.emacs file?

I have that too; hence my desire to change the defaults.

@Matafou, do you have strong feelings about this?

[jonleivent]

I wouldn't want to change proof-eager-annotation-face, as that is used for other messages. The point is really what binds that particular face to evars. Some poking around, and I see that it is hardcoded into coq-response-font-lock-keywords and coq-goals-font-lock-keywords. My point is that there perhaps should be a coq-evar-face, and use that within these functions.

[cpitclaudel]

I wouldn't want to change proof-eager-annotation-face, as that is used for other messages.

For eager warning messages, right?

My point is that there perhaps should be a coq-evar-face, and use that within these functions.

Sounds good, except for the name: that face covers more than evars :/

[jonleivent]

coq-existential-and-ltac-pattern-var-face?

[cpitclaudel]

Ah, looks like I pushed this at the same time you were commenting. I made it coq-question-mark-face. Presumably if the syntax change we'll also want to change how things are highlighted.

[cpitclaudel]

@jonleivent Thanks for your help with this. I've made question-mark-face inherit from variable-name-face, but this is not definitive. Trying it for a while should allow us to decide if it's best. I'd like to welcome future visitors to reopen this issue if they disagree with the change.

[cpitclaudel]

Also:

Well, as long as it is a user-settable option (and it's name is??), I can't complain.

Actually, complaining is crucial, and complaints are very welcome. It's hard to come up with good defaults otherwise.

Thanks again for your help.

[Matafou]

There may be some tricky thing to do with the output of evar names made by
coqtop (intially asked by Hendrik for proof-tree. Meanwhile setting this
face as a less visible one is ok with me. Actually,like Jonathan, I like to
have evar extremely visible. And I don't mindhaving the ltac pattern vars
being very visible too. Matter of taste.

I also agree that we should force ourselves into working with a nominal
proofgeneral for one hour from time to time.

P.

2015-11-23 19:40 GMT+01:00 Clément Pit--Claudel [email protected]:

Also:

Well, as long as it is a user-settable option (and it's name is??), I
can't complain.

Actually, complaining is crucial, and complaints are very welcome. It's
hard to come up with good defaults otherwise.

Thanks again for your help.

—
Reply to this email directly or view it on GitHub
#12 (comment).

[jonleivent]

Thanks. I did this:
Options->Customize Emacs->Specific Face... coq-question-mark-face

Hide Coq Question Mark Face face: [sample]
State : SAVED and set.
Face for Ltac binders and evars.
[X] Box around text: Value Menu Box:
Width: 1
Color: Value Menu Color: grey75 Choose (sample)
Style: Value Menu Sunken
[X] Foreground: magenta Choose (sample)
[X] Background: yellow Choose (sample)
Show All Attributes

This sunken box style is very visible and makes sense for evars (things that need to be filled).

[cpitclaudel]

Cool, thanks for sharing!

[jonleivent]

A final note about this - maybe suitable for documentation purposes: if you print out Ltac, there are more places than just match patterns where ?id can appear. It can also appear in intro patterns (like intros ?H0) and rewrite tactics (rewrite ?rule).

I was once told by Pierre Courtieu that a possible future project for PG would be to interface with Coq's Print Grammar support, and drive PG syntax highlighting from those rules. Until then, chaos...

[cpitclaudel]

company-coq already parses parts of the output of Print Grammar, to create autocompletion entries with holes for tactics and tactic notations (the implementation is in https://github.com/cpitclaudel/company-coq/blob/master/company-coq-tg.el). I don't really like this approach though (I chose it because there are too many people using old version for an implementation based on new commands in Coq to be immediately useful).

In my ideal world, Coq would expose a good IDE-oriented API, and could for example annotate fragments of code (solving indentation and highlighting issues), as well as return context-sensitive completions. Until then, chaos indeed :)

[Matafou]

Let us try to convince people that evars should be written another way in
next version of coq... Or hope to have time to use the ide protocol...

P.

2015-11-24 23:23 GMT+01:00 Clément Pit--Claudel [email protected]:

company-coq already parses parts of the output of Print Grammar, to
create autocompletion entries with holes for tactics and tactic notations
(the implementation is in
https://github.com/cpitclaudel/company-coq/blob/master/company-coq-tg.el).
I don't really like this approach though (I chose it because there are too
many people using old version for an implementation based on new commands
in Coq to be immediately useful).

In my ideal world, Coq would expose a good IDE-oriented API, and could for
example annotate fragments of code (solving indentation and highlighting
issues), as well as return context-sensitive completions. Until then, chaos
indeed :)

—
Reply to this email directly or view it on GitHub
#12 (comment).