Here are some examples I'd like to add to the trio server:
A version of our current example, but with all the lines annotated so the user understands what it is doing.
A simple example of using InfoCommand, maybe just an example of running info on each token and printing the results (and maybe also printing messages after the sync).
An example or running eval and check programmatically to do some calculation and using messages to find the results.
An example of BFS in tactic state with a very simple tactic API.
A tool to refactor all references to a particular definition name with a new name (e.g. replacing all group.subgroup with group.sub) or something like that. (I made a tool like this once already and I think this is one of the most useful applications of the Lean server.)
An example combining the lean server and simple meta-programming, like making a tactic or user command to print some custom information to messages.
Also, I'd like to make better instructions on how to set up and run the Trio server on your own Lean project or for mathlib development.
Here are some examples I'd like to add to the trio server:
group.subgroupwithgroup.sub) or something like that. (I made a tool like this once already and I think this is one of the most useful applications of the Lean server.)Also, I'd like to make better instructions on how to set up and run the Trio server on your own Lean project or for mathlib development.