PrettyPrinter (and lean4game)

Stream: general

[Hypatia du Bois-Marie]

Is there a way by which I can hook into the "styling" and control of the central panel to pretty print the environment and messages (as well as printing stuff at will, for example important definitions, etc, basically making it more similar to a Lean 4 text adventure game)? For example to make some literate LaTeX from the code, as well as perhaps generating a proof tree on the fly?
image.png

[Hypatia du Bois-Marie]

and also on a side note, in terms of the implementation of the server and the typescript codes, how entangled is it with lean itself? for example is it possible that i just put Software Foundations (in Coq) or some Agda/Prolog code on linguistics into it with a non-ridiculous amount of hacking?

[Hypatia du Bois-Marie]

PS. I think lean4game is a better alternative to e.g. https://logiclx.humnet.ucla.edu/.

[Hypatia du Bois-Marie]

PPS. my (horribly written) code is at https://github.com/analytic-bias/agora; the categorial grammar NL part is based on https://gist.github.com/wenkokke/cc12b92a8a60696b712c.

[Hypatia du Bois-Marie]

PPPS. how does reflection work in lean 4?

[Jon Eugster]

Hypatia du Bois-Marie said:

how entangled is it with lean itself? [...] is it possible [...] with a non-ridiculous amount of hacking?

The server itself is purely written in lean, so I would think the answer is no. You could look at the files here: server/GameServer. @Alexander Bentkamp might have more insight.

[Jon Eugster]

Hypatia du Bois-Marie said:

Is there a way by which I can hook into the "styling" and control of the central panel to pretty print the environment and messages (as well as printing stuff at will, for example important definitions, etc, basically making it more similar to a Lean 4 text adventure game)? For example to make some literate LaTeX from the code, as well as perhaps generating a proof tree on the fly?
image.png

I'm afraid I'm not 100% sure what you'd like to do, but I'm most certain the answer is "no / not yet". Might be useful to split your question into small, isolated feature requests and place them here on github

generating a proof tree on the fly

Not sure I understand this at all. The displayed messages are only dependent on the current goal and you can use Branch in the game to prepare different routes, so you could present the player with alternative paths. Is that what you are looking for?

[Jon Eugster]

Besides that, since it's written in Lean, you can do custom stuff like custom pretty-printers, etc. exactly how you would do them in lean itself.

[Alexander Bentkamp]

I dont know much about Coq and Agda, but I imagine it would be a lot of work to integrate them.

[Hypatia du Bois-Marie]

Jon Eugster said:

I'm afraid I'm not 100% sure what you'd like to do, but I'm most certain the answer is "no / not yet". Might be useful to split your question into small, isolated feature requests and place them here on github

Will do once I get to know the implementation of lean4game better and put aside enough time to start hacking! Thanks a lot!

[Hypatia du Bois-Marie]

And (forgot to ask...) is it possible to hook into the PrettyPrinter to structurally generate LaTeX?