Error after installing boogie-friends

[pys]

Perhaps I missed something obvious, since I'm a total newcomer.
I installed as described, and I get the message :

Eager macro-expansion failure: (error "Unknown dafny:compilation/progress pattern: (dafny:compilation/progres
s :uri :status :message)")

[ayanamists]

After some digging, I found this problem due to a breaking change in lsp-mode version 9.0.1.

At this time, I don't know how to make a polyfill work for both lsp-mode version 9.0.1 and below version 9.0.0. But if you just want to use Dafny right now, I provide a hotfix in the attached file. (How to use it depends on how you install this package; you can ask ChatGPT if you're not experienced with Emacs).

dafny.patch

[keyboardDrummer]

@ayanamists I think this repository is lacking proper maintainer resources, so finding the right polyfill might be too ambitious. Would it be an idea to apply the diff in your patch, even though it will break boogie-friends users that are on an older lsp-mode version, so that at least users can fix themselves by updating both boogie-friends and lsp-mode?

[ayanamists]

@keyboardDrummer This might be a solution, but (1) 9.0.1 is an unreleased version of `lsp-mode`, and most users are likely to encounter errors. (2) Your solution still seems to require approval from the maintainer, who hasn't been active for a long time.

…

On 29/11/2024 01:48, Remy Willems wrote: @ayanamists I think this repository is lacking proper maintainer resources. Would it be an idea to apply the diff in your patch, even though it will break boogie-friends users that are on an older lsp-mode version, so that at least users can fix themselves by updating both `boogie-friends` and `lsp-mode`?