F* highlighting is broken (a fix is made in a fork because original repo is abandoned)

[hacklex]

Lines like

reveal_opaque (`%symbol) (symbol)

are being wrongly treated by F* highlighter.

To see the bug, look at this F* source file

I made a quick fix to the grammar, but since the referenced project that has the currently-in-use fstar grammar file seems to be abandoned, I don't know where to even put it :)

[lildude]

I'd suggest submitting a PR to the grammar as it may appear abandoned, but it is owned by the F* community so it might get a review and merge.

Failing that, the only other options are to fork and maintain the grammar yourself and update Linguist to use your fork, or find another grammar that doesn't have the problem and is actively maintained and update Linguist to use that… maybe there's an active grammar for VSCode or Textmate?

[hacklex]

I believe only fstar-mode for emacs is currently up-to-date with fstar. Will ask the guys in their chat how to best handle this...

[hacklex]

I forked that grammar and committed the fix. The original atom-fstar is abandoned after all :(

Can we just reference my fork?

[lildude]

Can we just reference my fork?

Sure… https://github.com/github/linguist/blob/master/CONTRIBUTING.md#changing-the-source-of-a-syntax-highlighting-grammar

[hacklex]

#5582

[hacklex]

Can we just reference my fork?

Sure… https://github.com/github/linguist/blob/master/CONTRIBUTING.md#changing-the-source-of-a-syntax-highlighting-grammar

Done! Can you review @ accept my PR?

[Alhadis]

The original atom-fstar is abandoned after all :(

Where/how exactly did you confirm this?

I have reservations about replacing an official grammar when its maintenance status is unclear at best. FStarLang/atom-fstar was last updated in July 2018, and you only submitted #8 a few days ago. Give it a bit more time.

[hacklex]

I confirmed it by asking in F* community slack chats. They only write in emacs, and fstar-mode for emacs is the only editor that is kept up-to-date. Support for other editors such as vscode, atom, etc, is effectively dead, as even the grammars are years behind the current language version, not to mention the interactive mode that is essential if you write anything more complex than hello world.

Is there an option to switch linguist to using my fork and immediately switch back if atom-fstar suddenly turns out to be alive?

[Alhadis]

That's a real pain. Perhaps ask one of the @FStarLang members to transfer maintenance of the repository to you? If it's officially abandoned, transferring ownership will at least continue to benefit those using the package in Atom.

Failing that, our last resort is to use a fork.

[hacklex]

Alright. I contacted the guys in charge, and they merged my PR to atom-fstar.

Still, it is indeed abandoned, so we'll soon copy the file directly to the FStar repository, and ask linguist team to reference that instead

My current PR to linguist only contains the submodule update within the original atom-fstar repo.

[Alhadis]

Still, it is indeed abandoned, so we'll soon copy the file directly to the FStar repository, and ask linguist team to reference that instead

This doesn't sit well with me. For a start, that'll require us to hardcode an exception to the logic usually employed to locate grammar files. Since upstream might change the grammar's location within the project in the future, we'll be forced to tamper with Go code every time its location changes. Ideally, this should be configurable, but it currently isn't; see #4990.

The other problem is size. Checking out the entire FStarLang/FStar project is, unsurprisingly, much slower than checking out a more dedicated submodule. Since most of the updates done upstream won't be highlighting related, there's also a lot of unnecessary churn when updating grammar files.

[hacklex]

Don't change anything then. Leave the reference to atom-fstar and its several years obsolete grammar. At least I fixed the most disturbing error there was, and my fix was merged there successfully.

You are right on all counts. I will propose them to make one small child project that will only host the actual fstar grammar in the future. But at least, if linguist updates to the current state of atom-fstar master, my eyes will stop bleeding every time I view some of my files in github.

So, in other words, what really doesn't sit well with me is, my fstar files (as well as many files of the fstar sources) look like this:

This hurted my eyes so much that I went through the trouble of finding out who's responsible for github syntax highlighting, where's the fstar grammar, what's wrong with it, and even taking time of several people (including you) to finally get my little fix accepted to an effectively dead repository. All for the sake of my pet CAS project sources highlighting properly on github...

I'm honestly sorry for all the fuss around this. I just hate wrong highlighting that badly.

I most certainly hope there'll be no situations with highlightinig being broken so spectacularily in the future :)

[lildude]

Your F* file referenced in the OP looks good now. Closing.

[hacklex]

Awesome! Thanks!