"Download" emits `undefined`

[TonalidadeHidrica]

I presume that the "Download" feature allows me to export the current progress of the game (including all the proofs I've ever written) as a JSON file. However, when I click it, the downloaded file solely contains a string undefined. (As far as I search on this repo, there is no other such complaints, which surprises me. I'm hoping it's not just because of my environment, and reproducible by others.)

[TentativeConvert]

I can confirm this bug. (And I can also confirm it used to work …)

[yzqzss]

As a workaround, if anyone needs it, you can execute this ugly script in your browser console to export the progress.

(()=>{const h=location.hash.replace(/^#\/*/,'').split('/').filter(Boolean),p=location.pathname.split('/').filter(Boolean),gid=(p.length>=2?`g/${p[0]}/${p[1]}`:(h[0]==='g'&&h.length>=3?h.slice(0,3).join('/'):null));if(!gid)return alert('No game route detected (run this on a game page).');const gp=JSON.parse(localStorage.getItem('game_progress')||'{"games":{}}'),data=gp?.games?.[gid];if(!data)return alert(`No saved progress found for: ${gid}`);const a=document.createElement('a');a.href=URL.createObjectURL(new Blob([JSON.stringify(data,null,2)],{type:'application/json'}));a.download=`lean4game-${gid}-${new Date().toLocaleDateString()}.json`;a.click();URL.revokeObjectURL(a.href);})();

[Osalotioman]

I've seen this issue too, but just worked-around it on my end by by going into local storage to get the data directly.

I can work on figuring out what went wrong and try to fix it if no one else is working on this already @TentativeConvert ?

[TentativeConvert]

@Osalotioman Thanks for the offer! I don't think anyone is working on this specifically, but better check with @joneugster whether it makes sense to try and fix this at the moment, and which branch to start from – there are many moving parts right now.

[joneugster]

That would be welcome, thanks!

the game progress should be available in the atoms in "progress-atoms.ts" and you can probably inspect the downloadProgress function in the erase popup

[joneugster]

but note that the version live is quite far off from main, might be that this issue isn't present in both versions

[Osalotioman]

Alright, thanks. I'll get to work on it.

[Osalotioman]

The download emitting undefined has been fixed on the current version in the main branch, but there is a new issue. When you reload the the page all the data gets wiped, I'm looking into this now.