Skip to content

fix: importer - #575

Open
micuele wants to merge 3 commits into
leanprover-community:mainfrom
micuele:fix/importer
Open

micuele wants to merge 3 commits into
leanprover-community:mainfrom
micuele:fix/importer

Conversation

@micuele

@micuele micuele commented Oct 17, 2026

Copy link
Copy Markdown
Contributor

This fixes several issues in the game importer:

  • Failed imports now show the actual error and allow another attempt.
  • Downloads finish writing before extraction, and stalled transfers time out.
  • Artifacts are extracted and checked before replacing the installed game, so extraction or quota failures preserve the existing version.
  • Disk quota checks account for the extracted game size and the version being replaced.
  • Temporary files are cleaned up after failed imports.
  • Existing Lean toolchains are reused.

This still needs to be tested on the dev instance of lean4game.

…ow the actual error, allow retries, and preserve the installed game if extraction or quota checks fail.
@micuele micuele changed the title Fix/importer fix: importer Oct 17, 2026
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.

1 participant