feat: Track game activity metadata#536
Conversation
micuele
changed the title
| } | ||
| }) | ||
| }) | ||
| .get('/api/game-activity', async (_req, res) => { |
There was a problem hiding this comment.
This endpoint now provides an easy way to query all hidden games. Previously, I think, that was only possible by brute-forcing the URL.
I'm not saying this is necessarily bad, but I think this should be communicated clearly (as it's relaxing the security on one feature) and/or be explicitly mentioned in the docs.
| const defaultActivityPath = path.join(process.cwd(), 'games', '.lean4game', 'activity.json') | ||
|
|
||
| export const gameActivityStore = new GameActivityStore( | ||
| process.env.GAME_ACTIVITY_FILE || defaultActivityPath |
There was a problem hiding this comment.
In lean4web there is a list of all env variables: https://github.com/leanprover-community/lean4web/blob/main/doc/Installation.md#environment-variables
Maybe you could add something similar to the documentation?
There was a problem hiding this comment.
Sounds good! I’ll also update the documentation for the new environment variable and the /api/game-activity endpoint
| return this.update(owner, repo, 'seen', now) | ||
| } | ||
|
|
||
| private update(owner: string, repo: string, event: 'import' | 'play' | 'seen', now: Date): Promise<void> { |
2 participants
Adds activity metadata for inactive-game detection.
Lean4Game can now record first-seen, import, and play timestamps in
games/.lean4game/activity.jsonand exposes them via/api/game-activity.