idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
267 stars 70 forks source link

Update semantic highlighting code in line with the update IDE protocol #547

Closed ohad closed 2 years ago

ohad commented 2 years ago

Adds minor protocol version support

See idris2 PR#2171's new spec for Bounds

(wait until we merge #2171 before merging.)

jfdm commented 2 years ago

@Ohad Thanks for these updates. They are very much appreciated. Looking at the error, it is something I have seen before, and my fix was to drop the older versions of Emacs tested...I am, however, concerned about dropping more versions. In the past there was a soft rule that we tested against the earliest known Emacs released in Debian Stable/Ubuntu LTS. I have seen this issue discussed elsewhere which may require us to look at how we setup the emacs for testing.

jfdm commented 2 years ago

@ohad I have had a look at the issue with emacs, batching, and CIs in the mentioned issue. I think the issue is that, in Emacs, we need to call initialise before we refresh the package contents. I have drafted #548 which might help your issue. If not we can investigate further.

jfdm commented 2 years ago

So far so good... the Idris2 tests have completed on time, just waiting for Idris1 one's to complete. Hopefully, this will work. Once the tests have passed we can merge.

jfdm commented 2 years ago

Well that was a simple fix. Apologies that this too soo long to address, for something so simple.

I have merge this.

Thanks, as always, for the contributions.

ohad commented 2 years ago

Thanks! Don't worry about it, I don't think it was blocking anyone (since they could have used the PR in the meanwhile).

Thanks for the fix!!

gallais commented 2 years ago

Ah nice. I was getting really puzzling CI errors on the idris(2)-mode merges so hopefully that may fix that too.