Request: Semantic highlighting

[sethomsen]

I have a background writing Idris, but recently transferred to Coq. In both Idris and Agda they have semantic highlighting which I have come to miss.

The semantic highlighting in Idris is somewhat documented at the following pages: http://docs.idris-lang.org/en/latest/reference/semantic-highlighting.html https://github.com/idris-hackers/idris-mode

@spitters and I are both wondering if there are plans/work on extending company-coq with such semantic highlighting?

[cpitclaudel]

Not at the moment. Most of the syntax highlighting is done by Proof-General, and it's based on regular expressions, not on proper parsing.

One issue is that semantic highlighting is only well-defined for complete programs, and most of the time (in a non-structured editor) the contents of the current file do not form a complete program.

Last time I used Agda, the Emacs mode worked around this issue by only syntax-highlighting well-formed code. Has this improved since? Does Idris do better?

[spitters]

Not sure whether this is related, but it gives some background on the idris editor and related work: https://cattheory.com/extensibleTypeDirectedEditing.pdf

On Thu, Sep 6, 2018 at 5:37 PM Clément Pit-Claudel notifications@github.com wrote:

Not at the moment. Most of the syntax highlighting is done by Proof-General, and it's based on regular expressions, not on proper parsing.

One issue is that semantic highlighting is only well-defined for complete programs, and most of the time (in a non-structured editor) the contents of the current file do not form a complete program.

Last time I used Agda, the Emacs mode worked around this issue by only syntax-highlighting well-formed code. Has this improved since? Does Idris do better?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/cpitclaudel/company-coq/issues/207#issuecomment-419140643, or mute the thread https://github.com/notifications/unsubscribe-auth/AAM2zvw7UTK6MWxAwwd_bkaidOG6siLtks5uYUE-gaJpZM4Wcrdg .

[sethomsen]

For Agda i dont know, but Idris is still relying on the code to be well-formed to do semantic highlighting.

Idris do however have a very well developed hole-mechanism (a mechanism for making a introducing a placeholder for non-finished definitions, which the type-checker treats as a wildcard). For details on "holes" see Brady's original paper on Idris: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf.

The intended workflow in Idris (as least the workflow advocated by Brady) is to write functions incrementally using these "holes" for non-finished parts, and let the remaining implementation be guided by the types.
Therefore is the program being written, nearly at all times well-formed and the semantic-highlighting can thus guide you.

[cpitclaudel]

Right, that's what I meant by "structured editor" above. We don't really have this for Coq, unfortunately (or fortunately? I'm not a huge fan of that experience ^^)

[spitters]

How about this? https://stackoverflow.com/questions/41837820/agda-like-programming-in-coq-proof-general

or even the new Equations plug in ?

On Thu, Sep 6, 2018 at 9:30 PM Clément Pit-Claudel notifications@github.com wrote:

Right, that's what I meant by "structured editor" above. We don't really have this for Coq, unfortunately (or fortunately? I'm not a huge fan of that experience ^^)

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/cpitclaudel/company-coq/issues/207#issuecomment-419214032, or mute the thread https://github.com/notifications/unsubscribe-auth/AAM2zjWxEVd-fDgikl2feJk_EyE3OSNzks5uYXe6gaJpZM4Wcrdg .

[cpitclaudel]

Hmm, maybe I wasn't clear. I'm not talking about a limitation of Coq, I'm talking about the way PG works. Concretely, when you write lambda, you tend to type ( f u n = > …some stuff here… ). For most of that time, your file is not in a consistent state.

A structured editor would force you to always have matched braces, and so on.

In other words, with the current PG, the question is: how would we highlight specialize (fun x (y: na?

[spitters]

I seem to recall that lean just considers this a spelling error (using flyspeck). https://github.com/leanprover/lean-mode

On Thu, Sep 6, 2018 at 10:07 PM Clément Pit-Claudel < notifications@github.com> wrote:

Hmm, maybe I wasn't clear. I'm not talking about a limitation of Coq, I'm talking about the way PG works. Concretely, when you write lambda, you tend to type ( f u n = > …some stuff here… ). For most of that time, your file is not in a consistent state.

A structured editor would force you to always have matched braces, and so on.

In other words, with the current PG, the question is: how would we highlight specialize (fun x (y: na?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/cpitclaudel/company-coq/issues/207#issuecomment-419224233, or mute the thread https://github.com/notifications/unsubscribe-auth/AAM2zob8jT98Yv0ln1eQ5K0xAeyDKZqZks5uYYB5gaJpZM4Wcrdg .

[cpitclaudel]

I seem to recall that lean just considers this a spelling error

Sure, but it still highlights the code. IOW, it does the same thing as PG, doesn't it?

flyspeck

:) I think you mean Flycheck, but I actually find the name flyspeck a lot cuter ^^

[simongregersen]

I suppose that the straightforward way to go would be to do semantic highlighting of code that is actually loaded by the Coq process (and hence complete and type checked) and fall back to syntax-directed highlighting of code not loaded yet? But yes, this might be a PG issue rather than company-coq.

[cpitclaudel]

I suppose that the straightforward way to go would be to do semantic highlighting of code that is actually loaded by the Coq process

Indeed, that would be completely feasible.