search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
198 stars 35 forks source link

Make local commands in the game source file apply to the game #31

Closed abentkamp closed 1 year ago

abentkamp commented 1 year ago

Currently, any local commands in the source file of a game do not have an effect in the game because technically the game file is only imported by the server. It would be much more intuitive for authors if the server would literally take the source file and replace the proof.

This refactoring is not super-urgent. For now we can probably live with a custom command that allows us to open namespaces.

Technical implementation: We probably cannot use the olean files for this. We'll have to read in the original .lean source file and parse the contained commands. We search for the "Statement" command and substitute the player's proof.

abentkamp commented 1 year ago

Or maybe the Statement command could read out its own file and save it into the environment extension?

joneugster commented 1 year ago

Alongside this, it would also be more intuitive if there was a way to set global options that apply for all files, i.e. set_option autoImplicit false. Currently we set these options when loading a level which has the potential that levels which load fine in VS-Code crash later when building/running the game.