Jason Rute (Jan 29 2020 at 03:15):
I recently discovered that Lean can read from
stdin. So now I'm curious if it is possible to do the following in Lean:
- read in a string (representing a Lean term)
- parse that string into an expression
- evaluate (the term given by) that expression
- print the output
(1) and (4) are easy, but what about (2) and (3)? I assume (3) is possible with the meta stuff, but (2), I have no idea.
Jason Rute (Jan 29 2020 at 03:17):
I'm actually more interested in this scenario so feel free to comment on that one also:
- read in a string (representing a Lean Prop)
- parse that string into an expression
- set that expression as a goal
- apply a tactic to that goal
- print the result
Jason Rute (Jan 29 2020 at 03:21):
To be clear, I'm thinking about parsing Lean's syntax. (Of course, since expressions are algebraic data structures, one can could pass in say an s-expression for that expression and write a custom parser for those s-expressions.)
Jason Rute (Jan 29 2020 at 03:29):
Actually, as I think about it, even if there was no Lean syntax parser, I'd still be interested in the other steps (evaluating an expression and setting an expression as a goal).
Simon Hudon (Jan 29 2020 at 03:45):
For parsing an expression:
lean.parser.with_input interactive.types.texpr my_string
Simon Hudon (Jan 29 2020 at 03:46):
it will give you a
pexpr (plus a string) which you can feed into
to_expr to elaborate the term into something that you can evaluate or create a goal from
Simon Hudon (Jan 29 2020 at 03:50):
To evaluate it, you have to write a routine by hand creating a value of type you're interested in from an
expr. It can probably be automated with some meta programming
Simon Hudon (Jan 29 2020 at 03:51):
To set a goal with your expression:
v <- mk_meta_var e, gs <- get_goals, set_goals $ v :: gs
Jason Rute (Jan 29 2020 at 03:55):
Thanks! I will have to try this out.
Tim Daly (Jan 29 2020 at 04:22):
@Jason Rute I'm very interested in any code you write for this (obviously). Please make it available either publicly or email me.
Jason Rute (Jan 29 2020 at 04:32):
Sure, but I will warn you @Tim Daly that I am a hobbist, so I might not get around to it too quickly (or I might wake up tomorrow and want to give it a try :) ).
Jason Rute (Jan 29 2020 at 05:48):
@Simon Hudon I got this far, but I think I am mixing the
tactic monads. Do you know what I need to do here?
def experiment (s : string) : lean.parser unit := do pe <- lean.parser.with_input interactive.types.texpr s, -- parser monad e <- to_expr pe.1, -- tactic monad v <- mk_meta_var e, gs <- get_goals, set_goals $ v :: gs, t <- target, trace t, -- should output the goal given by the string s return ()
Jason Rute (Jan 29 2020 at 05:51):
Simon Hudon (Jan 29 2020 at 05:55):
Yes, that's a very annoying separation when you need to invoke the parser. You can invoke tactic from parser but not the other way around. Figuring out how to get the user to call your automation can be tricky. If you only want to call tactic from parser, you can use
Simon Hudon (Jan 29 2020 at 06:00):
For the other way around, it depends on how you want to invoke the script. If you want to call it from a normal proof script (in a
end block), then we use the
parse syntax. Otherwise, you can define a
user_command using the attribute
user_command and then you just write
my_command . at the top level and it will call your script
Mario Carneiro (Jan 29 2020 at 06:41):
I don't think it is possible to use
with_input when using
Jason Rute (Jan 29 2020 at 13:31):
meta def experiment (s : string) : lean.parser unit := do pe <- lean.parser.with_input interactive.types.texpr s, e <- lean.parser.of_tactic (tactic.to_expr pe.1), v <- lean.parser.of_tactic (tactic.mk_meta_var e), gs <- lean.parser.of_tactic (tactic.get_goals), lean.parser.of_tactic (tactic.set_goals $ v :: gs), t <- lean.parser.of_tactic tactic.target, lean.parser.of_tactic (tactic.trace t), return () run_cmd experiment "true"
is giving me an error at
run_cmd: "vm check failed: dynamic_cast<vm_State*>(to_external(o)) (possibly due to incorrect axioms, or sorry)". Maybe this is related to what Mario was talking about about not being able to use
Sebastian Ullrich (Jan 29 2020 at 13:38):
That's a bug,
run_cmd should only accept
lean.parser cannot be used outside of user-defined parser extensions (notations/commands/tactic params).
Jason Rute (Jan 29 2020 at 13:42):
@Simon Hudon Can you point me to examples of what you mean by "the
parse syntax" or using
user_command? (Or does Mario's comment mean what I want to do is ultimately doomed to fail?)
Simon Hudon (Jan 29 2020 at 16:59):
While it is fresh, can you file this
run_cmd issue? I'd like to make the error message better.
Simon Hudon (Jan 29 2020 at 17:01):
I wouldn't say your project is doomed. I would only say that you'll have to run your experiment while parsing / elaborating Lean files, not as a Lean program (with a main, etc)
Simon Hudon (Jan 29 2020 at 17:11):
Now about the
user_command idea (which I think is what you need):
setup_tactic_parser -- this is actually a user command too @[user_command] meta def my_command (meta_info : decl_meta_info) (_ : parse (tk "my_command")) : lean.parser unit := do parser.of_tactic $ trace "hello world" . my_command . -- prints "hello world"
Simon Hudon (Jan 29 2020 at 17:12):
Then if you want to user to write in an expression, you can do:
@[user_command] meta def my_command (meta_info : decl_meta_info) (_ : parse (tk "my_command")) : lean.parser unit := do e <- texpr, parser.of_tactic $ trace e . my_command 1 + 1 . -- prints "1 + 1"
(be sure not to forget the
Simon Hudon (Jan 29 2020 at 17:16):
Then you can skip the part where you parse from a string. If you read the string from a file, this is where I would use the
Jason Rute (Jan 29 2020 at 23:10):
While it is fresh, can you file this
run_cmdissue? I'd like to make the error message better.
Jason Rute (Jan 29 2020 at 23:11):
@Simon Hudon Thanks for all the help! I am wondering if I need to take a step back however. Maybe I don't want/need parsing of Lean code in the first place.
Simon Hudon (Jan 29 2020 at 23:13):
Can you explain a bit more how you'd like the user to call your program?
Bryan Gin-ge Chen (Jan 29 2020 at 23:13):
The issue should probably be on
leanprover-community/lean instead. I bet @Simon Hudon can transfer it over though.
Simon Hudon (Jan 29 2020 at 23:15):
Simon Hudon (Jan 29 2020 at 23:16):
Good call @Bryan Gin-ge Chen
Jason Rute (Jan 29 2020 at 23:22):
@Simon Hudon The user will be a machine and it will call
lean --run my_program and communicate via stdin and stdout. Specifically the user will send some string representing a theorem to be proved (more on that in a second) via stdin. The program will read that string in, convert it to an expression, make a goal of that type, apply a tactic (this may also be specified by the user, but for now I'm worried about the goal itself), and print (to stdout) whether the tactic succeeded and the resulting goal (in some serialization). This will be a loop. So the program waits for the next input. I'm starting to realize that it is better to directly serialize the expression than to directly parse Lean code. I was just about to ask on a new topic if there is a standard serialization of Lean expressions or if I should make my own?
Jason Rute (Jan 29 2020 at 23:23):
For motivation, I'm trying to make a better and more reliable version of what I made here.
Jason Rute (Jan 29 2020 at 23:25):
There I used the Lean server, but I think stdin and stdout of a running Lean program is better, faster, and more reliable.
Simon Hudon (Jan 29 2020 at 23:26):
I see. For serialization, have a look here: https://github.com/leanprover-community/lean/blob/ec1613aef1eee72e601f192b16740629c6d49690/library/system/io.lean
Rob Lewis (Jan 29 2020 at 23:34):
What imports will your lean program use? If it's a large environment, e.g. all of mathlib, you might still be better off with the server interface. There's overhead to building the environment even if the dependencies are precompiled. Keeping a single server instance going will avoid this.
Jason Rute (Jan 29 2020 at 23:41):
It would be nice to try both. To be clear, I intend to keep either instance "going". If I use stdin/stdout, it will be in a loop.
Jason Rute (Jan 29 2020 at 23:42):
@Simon Hudon That looks really promising! I need to upgrade Lean apparently to get that... Do you by chance know what the serialization looks like?
Simon Hudon (Jan 29 2020 at 23:50):
I don't remember what it looks like. I'll have a look
Simon Hudon (Jan 30 2020 at 01:49):
The serialization is not really legible. It's binary serialization format
Jason Rute (Jan 30 2020 at 13:20):
Jason Rute (Jan 30 2020 at 13:33):
Ignoring the details of serialization for now (which have and could be solved in a number of ways), here is what I have in mind. I tested it (with dummy serializations). This code works (and is very fast to call from say Python).
import system.io open io meta def serialize_expr (e : expr) : string := sorry meta def deserialize_expr(s : string) : expr := sorry meta def apply_tactic_to_goal (t : tactic unit) (goal : expr) : tactic (list expr) := do -- set expression as goal v <- tactic.mk_meta_var goal, tactic.set_goals $ [v], -- run tactic on goal t, -- return results gs <- tactic.get_goals, return gs meta def read_eval_print (_ : unit) : io_core error (option unit) := do do -- get serialized expression from stdin expr_str ← get_line, let e := deserialize_expr expr_str, -- run tactic (skip tactic in this case) on goal gs ← io.run_tactic (apply_tactic_to_goal tactic.skip e), -- print serialized goals to stdout let goal_strs := gs.map serialize_expr, put_str (to_string goal_strs), return () meta def main : io unit := -- loop forever do iterate () read_eval_print, return ()
Jason Rute (Jan 30 2020 at 13:34):
When I say fast, I mean that the first call is slow, but after that it is really fast compared to the lean server.
Jason Rute (Jan 30 2020 at 13:36):
Of course this is a prototype. A better version needs error handling (and more features around selecting which tactics to apply).
Jason Rute (Feb 09 2020 at 14:04):
@Rob Lewis I just discovered
expr.to_raw_fmt from your other post. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.3F.3F.3F/near/187757930 I don't suppose that hidden somewhere in Lean is a parser for this format (which takes a string of this format and converts it to an
Mario Carneiro (Feb 09 2020 at 14:05):
Mario Carneiro (Feb 09 2020 at 14:06):
It's almost good enough that you can use it as lean surface syntax for an object of type
expr though (i.e. using the constructors directly)
Mario Carneiro (Feb 09 2020 at 14:07):
expr.to_raw_fmt is defined in lean though and it's a relatively short definition so you can modify it to suit your needs
Jason Rute (Feb 09 2020 at 14:11):
Thanks Mario! I actually already have made my own
string function before I discovered this and made a parser too (although I haven't finished covering all the cases, like macros). I just thought it was better to use built-in tools when possible. Thanks!
Jason Rute (May 21 2020 at 23:09):
Mario Carneiro said:
I don't think it is possible to use
I'm reviving this thread. It is not possible to run the parser monad inside the tactic monad or the io monad.* I'm curious if this is by necessity (i.e. the parser monad requires information that shouldn't be available in the tactic monad or the io monad) or by omission (no one has bothered to implement
io.run_parser). I know the io monad in particular has access to the tactic environment (so one can run
io.run_tactic), but I don't know if it also has (or could have) access to the parser state. I'm getting by with the user command trick, but I'm curious nonetheless.
Jason Rute (May 21 2020 at 23:11):
*It isn't entirely true that you can't run a parser in a tactic monad. You could start in the parser monad, grab the parser state, run a tactic inside the parser, and in that tactic, invoke the parser_state, but I think we can agree I'm being pedantic now. :slight_smile:
Last updated: May 08 2021 at 10:12 UTC