search

tamarin-prover / editors

Repository for text editor syntax highlighting
GNU General Public License v3.0
2 stars 5 forks source link

License Change towards support for Tamarin / .spthy Language & Syntax Recognition #8

Open JeuJeus opened 3 months ago

JeuJeus commented 3 months ago

In this Issue I describe the Goal of enabling Tamarin as a “supported”/recognized language on GitHub, as well as reasons for doing so and the necessary changes to start. At the same time I volunteer to implement the necessary steps.

Goal

It would be beneficial to have support for Tamarin or more specifically its security protocol theory files (.spthy) on GitHub.

This means having the Tamarin theories listed in the repositories languages (see Screenshot from tamarin-prover/tamarin-prover attached). image

As well as working Syntax highlighting in the GitHub Web interface for .spthy files in general.

Reasons for this

The inclusion of Tamarin into GitHubs supported languages provides benefits in the visibility and public appearance of Tamarin. Exemplary highlighting its presence in repositories of protocols/tools utilizing Tamarin to proof their security (random example, first one that appeared in my search cloudflare/odoh-analysis). At the same time, Tamarin would be highlighted on GitHub increasing exposure to potential new users. Additionally, the usability of Tamarin files on GitHub would be increased due to working Syntax highlighting. This would be largely beneficial for Diffs, Issues, and PRs. Whilst also improving studying examples/implementations online, without the need to clone a repo for syntax highlighting support.

Necessary Changes

The process of integrating a new language for GitHub is pretty straightforward with linguist (see Adding a language). The only real change would be the necessity to provide Syntax Highlighting and Example Code with a compatible license. The current GPL-3.0 license is not sufficient.

Let me know if additional information is necessary, feel free to reach out to me, I am looking forward to help.

rkunnema commented 3 months ago

Hi! Sounds cool to me! Do you plan to build the grammar from scratch? We've got a tree-sitter grammar and only three people were directly writing into it, so it should be easy to relicense that piece of code.

JeuJeus commented 3 months ago

When I was first looking into this and opened the Issue I skimmed the linguist documentation to validate whether this was viable. As far as I know, unfortunately, linguist does not support tree-sitter grammars, but : Syntax highlighting in GitHub is performed using TextMate-compatible grammars. These are the same grammars used by TextMate, Sublime Text, and Atom. (Documentation Link)

If still up to date, the easiest way to accomplish the syntax highlighting would be to repurpose the Sublime Syntax Highlighting (which only two people worked on). But then this current repo seems out of scope for the issue.

On the other hand, linguist requires "real world" usage examples - for which usable examples reside in the main repository with the same non-matching license.

What is the easiest way to make progress with this, is there a mailinglist i can contact or would you recommend opening another (linked) issue in the tamarin-prover/editor-sublime or tamarin-prover/tamarin-prover repo?

rkunnema commented 3 months ago

On the other hand, linguist requires "real world" usage examples - for which usable examples reside in the main repository with the same non-matching license.

That one is easy. examples/accountability/masters-thesis-morio/CentralizedMonitor.spthy was only edited by me and @kevinmorio, we can relicense this one (just tell us which one you prefer).

If the TextMate-grammar is incomplete, you might use the grammar we've just integrated for help. https://github.com/tamarin-prover/tamarin-prover/pull/669 There is an output to BNF which could be repurposed ... or maybe even generate the textmate-grammar, if you fancy.

What is the easiest way to make progress with this, is there a mailinglist i can contact or would you recommend opening another (linked) issue in the tamarin-prover/editor-sublime or tamarin-prover/tamarin-prover repo?

I think an issue works; tamarin-prover/tamarin-prover is the right address for that.

JeuJeus commented 2 months ago

That sounds like a good starting point so far.

I haven't shelved the project, but I have a lot to do at the moment, so I'll get to work as soon as I have time.