Building issue

[kant2002]

I have very strange issue,

https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c

Is inaccessible in my provider for some reasons. I would like to build project in some form, but some dependencies looks questionable.
"lean4-infoview" is same as "@leanprover/infoview": "^0.4.3" but older version 0.4.2.
"lean4web" also depends on "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985" which is older version of lean4 package.

Is there any appetite for updating dependencies and normalize them to use from published packages?

[joneugster]

There are plans to update all dependencies shortly, using some less hacky dependencies inside the Lean ecosystem. I already got around to do that for lean4web, but not finished yet for lean4game. :)

I'd hope to get around to do that eventually

[kant2002]

If you need help, or just testing, I willing to help. I would like translate NNG4 to Ukrainian, but I need working setup in order to even think realistically about it 😄

[joneugster]

at this stage, helping would be a bit a commitment (i.e. would need some effort to get familiar with the code) The "editor logic" works, but what's left is getting the typescript frontend working for this complete overhaul.

If you are keen to contribute, you could DM me on zulip and I'll explain the details, but I expect it to take a few days worth of work. :)