search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
198 stars 35 forks source link

Building issue #263

Open kant2002 opened 1 month ago

kant2002 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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. :)