Skip to content

refactor: replace dependency gitpkg.vercel.app dependencies#431

Merged
joneugster merged 3 commits intomainfrom
remove-vercel
Jan 8, 2026
Merged

refactor: replace dependency gitpkg.vercel.app dependencies#431
joneugster merged 3 commits intomainfrom
remove-vercel

Conversation

@abentkamp
Copy link
Collaborator

Fixes #416

@abentkamp abentkamp marked this pull request as draft December 28, 2025 14:20
@RichardKelley
Copy link
Contributor

Not sure what the status of this PR is, but I was able (with Codex) to get a fork of the remove-vercel branch working on a few games and passing all of the Cypress tests here:

https://github.com/RichardKelley/lean4game/tree/remove-vercel

I don't want to propose a competing PR if this one is moving forward; if the above is useful I'm happy to help integrate or do additional testing.

@abentkamp
Copy link
Collaborator Author

Thats great. I didnt have the time to finish this.

@abentkamp
Copy link
Collaborator Author

Your branch looks okay, although I don't fully understand all the changes, but that's okay, I think.

Can you open a PR and maybe comment on why the duplicated definitions in client/src/components/infoview/notification_util.ts are necesssary?

@RichardKelley
Copy link
Contributor

Let me see if I can get rid of notification_utils.ts - I think it's just a holdover from my first attempted workaround for the dependencies. I'll create a PR with some explanation later today.

// Find an ancestor that contains the lean4game directory.
let current = this.dir
for (let i = 0; i < 10; i++) {
if (fs.existsSync(path.join(current, 'lean4game'))) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This isn't really stable. User might have multiple instances of the repo on the computer and the clone might have a different name

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

reverted this

@joneugster
Copy link
Collaborator

Screenshot 2026-01-08 at 12 55 13

Max recursion when a game does not exist or isn't built.

@joneugster
Copy link
Collaborator

Screenshot 2026-01-08 at 12 55 13 Max recursion when a game does not exist or isn't built.

Might be unrelated to this PR.

@joneugster joneugster marked this pull request as ready for review January 8, 2026 12:11
@joneugster
Copy link
Collaborator

Thank you @abentkamp and @RichardKelley ! I verified it working locally

@joneugster joneugster merged commit 3acefd8 into main Jan 8, 2026
1 check passed
joneugster added a commit that referenced this pull request Jan 8, 2026
Co-authored-by: Richard Kelley <richard.kelley@gmail.com>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
@ovo-Tim
Copy link

ovo-Tim commented Feb 10, 2026

Could you port this to older branches like bump-v4.23.0? RealAnalysisGame is not compiling now. My workaround is also not working.

@joneugster
Copy link
Collaborator

I think the simplest solution is to bump RealAnalysisGame... I'll try to see if I can assist the author

@ovo-Tim
Copy link

ovo-Tim commented Feb 13, 2026

I think the simplest solution is to bump RealAnalysisGame... I'll try to see if I can assist the author

I've tried to do so.
AlexKontorovich/RealAnalysisGame#106

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Error during npm install

4 participants

Comments