I'm sorry I don't have time to make this comment more precise right now (so maybe its just a useless comment), but part of me can't help feeling some of this approach is a bit low-tech somehow? e.g. there is a lot of manual matching on and joining of strings. Although I don't know precisely how to do it immediately I would quite like to see a version of this PR that targets Syntax rather than strings/format, and uses the built in delaborators more somehow.
Of course if it gets good results as is then maybe we shouldn't worry too much right now, and maybe merge this and discuss whether a shorter/cleaner implementation is possible later, but if you were interested I think it would be good to play with a more Syntaxey version (I'd also like to try more seriously, but unfortunately can't this week)

Alex, I see what you are saying, although I do not really know how to actually put it in practice. I'm all for learning how to work with Syntax, but I am not really sure where to start.

When you have the time, I'd be happy to hear some suggestions! In the meantime, I'll see that I can find!

I will add a test that the extracted goal proves the given goal and emit a warning otherwise. However, I do not have time to do it right now!

I tried and failed. I am unable to get my hands on the output of logInfo msg, in order to parse it again. If I had that, then I would

• make sure that it parses with no issues, other than the sorry;
• check that the new declaration actually closes the initial goal.

I have added a couple of examples to the docs-module containing examples that would form good tests, if the above were implemented.

Still, I think that the tactic already works very well as is and these improvements could come later on.

An option would be to add something like extract_goal [...] pp.all to specify that you want the full, round-tripping expression.

@kmill, CI failed to build the tests, since #guard_msgs complained for the pp.all output. Does CI remove pp-options and hence the test will check against the non-pp.all message?

I am running CI again to test this, but maybe you already know what the issue it!

I'm not sure this is a CI issue per se, since it could be a difference between Lean in an editor and Lean on the command line. Maybe the options aren't actually guaranteed to be propagated into the pretty printer at line 135? I can take a look later.

I looked closer at the diff: the current hypothesis is that

• my computer displays funs as fun ... ↦ ...,
• CI displays funs as fun ... => ....

Yes, it seems to be this: on my local version, #guard_msgs complains that the outputs do not match, because of the fun arrow. On GitHub, though, the PR has passed the tests, so that #guard_msgs liked what it received.

Ok, that's a known issue then. Add set_option pp.unicode.fun true to the top of the tests file.

Thanks!

bors r+

In a followup PR, feel free to add this to Mathlib.Tactic.Common so that it's readily available.

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style