Skip to content

fix: Progress Tracking#494

Open
Osalotioman wants to merge 5 commits intoleanprover-community:mainfrom
Osalotioman:fix/progress-export
Open

fix: Progress Tracking#494
Osalotioman wants to merge 5 commits intoleanprover-community:mainfrom
Osalotioman:fix/progress-export

Conversation

@Osalotioman
Copy link
Copy Markdown
Contributor

@Osalotioman Osalotioman commented Apr 8, 2026

  • Verified that exporting game data currently works.
  • Fixed typo reading to => writing to.
  • Create default values when json field does not exist for level or world.
  • Add a use effect to set code field for levels so they persist in storage.

closes: #489

Copy link
Copy Markdown
Collaborator

@joneugster joneugster left a comment

Choose a reason for hiding this comment

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

Thanks for the PR! I'll have a closer look later

const worldProgress = get(worldProgressAtom)
if (!levelId || !worldProgress) return
const copied = { ...worldProgress }
if (levelId == null) return
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

this is likely correct for when levelId is 0 but I need to check this later

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

It's not the same behaviour since 0 is falsy, I've updated it so worldProgressAtom does not get updated when we are in level 0.

@@ -0,0 +1,12 @@
import { LevelProgress, WorldProgress } from "./progress-types"

export const createDefaultWorldProgress = (): WorldProgress => ({
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Id prefer to use the style export function ... project wide, could you change to that, please? Also, is the as necessary?

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

or even better,
this doesn't need to be a create-function does it? This can simply be a constant

const defaultLevelProgress: LevelProgress = {
  ...
}

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

I've updated it to be a constant, and put it under defaultProgress in progress-atoms.ts.

(get, set, val: boolean) => {
const levelProgress = get(levelProgressAtom)
if (!levelProgress) return
const levelProgress = get(levelProgressAtom) ?? createDefaultLevelProgress()
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Have you consodered if it would make sense that levelProgressAtom directly returns a default, so thos doesn't need to be added in multiple places?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

I made levelProgressAtom and worldProgressAtom directly return the defaults, but still ended up adding those defaults in multiple places cause levelProgressAtom is allowed to return null when there is no worldId/progress/levelId/levelProgress. I'm looking through to see if I can take out checks like that so it returns the default value or actual value all the time, then I can remove the default values from other places.

@Osalotioman
Copy link
Copy Markdown
Contributor Author

I just noticed a new issue, one that was being blocked earlier cause progress was not being properly updated.
The useEffect in main.tsx which sets the current level as completed when the proof is complete does so pre-maturely when a user takes the following action:

  1. User finishes level A, so proof.completed becomes true.
  2. User navigates to level B.
  3. Before proof state is fully refreshed/reset for level B, that effect can still see the old proof.completed === true.
  4. Now the completedAtom auto-creates missing progress, it writes { completed: true } for level B immediately, instead of waiting for proof.completed to get updated when the current proof state finishes loading.

I don't know if I should address it here or leave it for another PR so this one does not go out of scope too much.

@Osalotioman Osalotioman requested a review from joneugster April 11, 2026 03:56
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.

"Download" emits undefined

2 participants