İdris2 language syntax highlighting support needed.

[omentic]

For syntax highlighting, a tree-sitter grammar and associated queries are needed. I can't seem to find an Idris2 grammar except this one: https://github.com/gwerbin/tree-sitter-idris2, which seems abandoned.

[omentic]

Looking through the Idris Discord, it appears there are some serious ambiguity issues that make Haskell grammars a pain and would probably limit the usefulness of a grammar for Idris. I suppose anything is better than nothing, though.

Queries are pretty straightforward to write (I'll write them if there's a semi-working grammar available, I've wanted to get more acquainted with Idris) but the grammar is the real doozy.

[tarikozkanli]

Hello, There is idris2 vim plugin which provides syntax highlighting. https://github.com/edwinb/idris2-vim

Regards.

On Tue, 9 May 2023 at 11:53, JJ @.***> wrote:

For syntax highlighting, a tree-sitter grammar and associated queries are needed. I can't seem to find an Idris2 grammar except this one: https://github.com/gwerbin/tree-sitter-idris2, which seems abandoned.

— Reply to this email directly, view it on GitHub https://github.com/helix-editor/helix/issues/6997#issuecomment-1539292412, or unsubscribe https://github.com/notifications/unsubscribe-auth/AD54S56VWKM5WAVE73DG2B3XFIAYZANCNFSM6AAAAAAX2GWGYU . You are receiving this because you authored the thread.Message ID: @.***>

[tarikozkanli]

Idris community says that :

Do be aware that Idris' semantic highlighting is type-directed and cannot be replicated with a grammar-based approach.

Actually all dependently types programming languages have the same issue. Maybe some general approach is needed for this kind of language.

Regards.

On Tue, 9 May 2023 at 11:53, JJ @.***> wrote:

For syntax highlighting, a tree-sitter grammar and associated queries are needed. I can't seem to find an Idris2 grammar except this one: https://github.com/gwerbin/tree-sitter-idris2, which seems abandoned.

— Reply to this email directly, view it on GitHub https://github.com/helix-editor/helix/issues/6997#issuecomment-1539292412, or unsubscribe https://github.com/notifications/unsubscribe-auth/AD54S56VWKM5WAVE73DG2B3XFIAYZANCNFSM6AAAAAAX2GWGYU . You are receiving this because you authored the thread.Message ID: @.***>

[SomeGuyNamedMay]

im not a contributer to the project in any way but i just want to mention that the main thing keeping me on emacs atm is mostly its support for proof assistents like idris and coq, so maybe the topic of integrating proof assistent support into helix could be its own issue?

[omentic]

@SomeGuyNamedMy do you think you could write a little bit about how the emacs integration works? i'm aware that coq and agda (and idris) are essentially emacs (or vscode) exclusive languages because of it, but i've only learned idris with the interactive cli, have yet to learn emacs, am curious on what i'm missing, and also agree it'd be a good start for a separate issue and good to put here

[SomeGuyNamedMay]

im actually more or less a newb when it comes to theorem proving, i just finished my discrete mathematics course which taught coq, but the interface for theorem prover interfaces in emacs like in Proof General tend to use a three pane layout, one for the actual file, one for the goal, and one for the response. the response pane is used for things like error messages and proof searchs. example image:

[SomeGuyNamedMay]

it would also be nice to have a uniform method of input for unicode symbols like agdas emacs mode does were you can type in a sequence of characters after a backslash. so for example \bN produces ℕ. some docs on agdas emacs mode can also be found here

[omentic]

ah interesting, thanks! also relevant: #4465

re: custom input + integration, cc. #133 and #3366. i would love to see support for custom modes. it is unfortunately definitely blocked behind #122 which afaik no progress has been made on.

i might work on patching in unicode input, actually. i was poking around the codebase a while back and think adding a new unicode input mode would be straightforward enough: or perhaps better, a normal mode command? (\ is currently unused). i'll lyk if anything comes of it

[SomeGuyNamedMay]

regarding #122 i would actually think this would be a good opertunity to try to standardize the interface that you actually interact with theorem provers with by integrating it into the main project. emacs for proof assistent overall has been a decent experience for me (for being emacs, configuring emacs is a nightmare) but i do wish the interfaces were a little more consisten as they all do things slightly differently. id image this would make helix a lot more attractive to academic types as well.

[omentic]

consistent in what way, like consistent keybindings across panes? i think for a far-down-the-road proof assistant mode, i was imagining something akin to the debug mode redesign, at least aesthetics-wise: #5950

[SomeGuyNamedMay]

the different modes in emacs across the board do this not just the stuff related to proof assistents, things like keybindings, unicode input, and interacting with the proof goal are not very well standardized, also the debug mode redesign look more or less perfect for this purpose.

[tarikozkanli]

Hi,

There is an idris2 language server project and it seems it partially works with Helix. Although it is not live anymore it seems

https://github.com/idris-community/idris2-lsp

No syntax coloring and highlighting though.

Regards.

On Tue, 16 May 2023 at 08:59, Mason Dear @.***> wrote:

the different modes in emacs across the board do this not just the stuff related to proof assistents do this, things like keybindings, unicode input, and interacting with the proof goal are not very well standardized, also the debug mode redesign look more or less perfect for this purpose.

— Reply to this email directly, view it on GitHub https://github.com/helix-editor/helix/issues/6997#issuecomment-1549037876, or unsubscribe https://github.com/notifications/unsubscribe-auth/AD54S542FOLAXKTYWC7EDTTXGMJUPANCNFSM6AAAAAAX2GWGYU . You are receiving this because you authored the thread.Message ID: @.***>

[foxyseta]

idris2-lsp seems alive again, but tree-sitter-idris2 is most certainly still abandoned.

Do be aware that Idris' semantic highlighting is type-directed and cannot be replicated with a grammar-based approach. Actually all dependently types programming languages have the same issue. Maybe some general approach is needed for this kind of language.

Where can I read more about this problem? Would limited syntax highlighting still be possible using grammars? Doesn't Agda (which also features dependent type) have proper syntax highliting based on its grammar (https://github.com/tree-sitter/tree-sitter-agda)?