Zulip Chat Archive

Stream: general

Topic: Try this!


view this post on Zulip Scott Morrison (Apr 20 2020 at 10:52):

import tactic.suggest
open tactic

@[priority 2000]
meta instance : interactive.executor tactic :=
{ config_type := unit,
  inhabited := (),
  execute_with := λ _ t, t >> (done <|> lock_tactic_state (try ((target >>= is_prop >>= guardb) >> `[library_search]))) }

example : 0 < 1  1 < 2 :=
begin
  split,
end

and follow the prompts. :-)

view this post on Zulip Mario Carneiro (Apr 20 2020 at 10:55):

heh, next thing you know begin end is going to call obviously

view this post on Zulip Scott Morrison (Apr 20 2020 at 10:55):

I would really like to get the blue underline on the end, rather than on the example.

view this post on Zulip Scott Morrison (Apr 20 2020 at 10:56):

Is there some way to do this? I've never understood how error messages get located.

view this post on Zulip Mario Carneiro (Apr 20 2020 at 10:57):

I don't know the whole story, but I do know that when you write a tactic proof in begin end, this gets compiled down to a term of type tactic unit, where instead of the regular bind, tactic.istep is used, which is magically provided a location argument from the parser

view this post on Zulip Mario Carneiro (Apr 20 2020 at 10:59):

#check `[intro, simp]
-- has_bind.seq (tactic.save_info {line := 1, column := 9}) (tactic.step (tactic.interactive.intro none)) >>
--   has_bind.seq (tactic.save_info {line := 1, column := 16})
--     (tactic.step (tactic.interactive.simp none ff list.nil list.nil (interactive.loc.ns [none]))) :
--   tactic unit

view this post on Zulip Mario Carneiro (Apr 20 2020 at 11:03):

I'm not sure how to show the produced tactic in a begin end block but it uses istep instead of step, and you can see bits of this in error messages

#check by nat
-- type mismatch at application
--   tactic.istep 2 10 2 10 ℕ
-- term
--   ℕ
-- has type
--   Type : Type 1
-- but is expected to have type
--   tactic ?m_1 : Type ?

view this post on Zulip Mario Carneiro (Apr 20 2020 at 11:05):

istep calls the magic function scope_trace

/-- This function has a native implementation that displays in the given position all trace messages used in f.
   The arguments line and col are filled by the elaborator. -/
def scope_trace {α : Type u} {line col: nat} (f : thunk α) : α :=
f ()

which allows you to control where trace and tactic.trace print their output

view this post on Zulip Mario Carneiro (Apr 20 2020 at 11:11):

That said, this doesn't answer the question of how to locate the end. It's quite possible that this information is never exposed to lean, and I don't know if the tactic scripts that begin end blocks produce have a terminating pos argument

view this post on Zulip Johan Commelin (Apr 20 2020 at 11:11):

@Scott Morrison Wow, that's cool!
If you open the Problems tab in VScode (below the editor window), you can see the suggestions. (Independent of current cursor position.) That's nice. But the "Try this" functionality is broken, alas.

view this post on Zulip Scott Morrison (Apr 20 2020 at 11:44):

The "Try this" functionality would potentially be fixable: by emitting slightly different text we could trigger the VS Code extension to do the replacement somewhere different.

view this post on Zulip Scott Morrison (Apr 20 2020 at 12:42):

@Bryan Gin-ge Chen, did you write the code in the VSCode extension that does "Try this:" substitution?

view this post on Zulip Scott Morrison (Apr 20 2020 at 12:44):

I'm wondering how hard it would be to check if the location of the "Try this:" trace message was on the theorem or def keyword at the beginning of the declaration (rather than on a tactic invocation), and if so, insert the "Try this:" hint at the end of the first failing begin ... end block in that declaration.

view this post on Zulip Bryan Gin-ge Chen (Apr 20 2020 at 15:10):

@Scott Morrison @Alexander Bentkamp wrote that code actually.

view this post on Zulip Bryan Gin-ge Chen (Apr 20 2020 at 15:15):

What you describe sounds possible, but I think it'd be better to control the position that the message is emitted from within Lean. @Gabriel Ebner and @Simon Hudon mentioned a related needed change to Lean in #2267.

view this post on Zulip Scott Morrison (Apr 20 2020 at 23:29):

@Keeley Hoek, do you know how hard it would be for an executor to gain access to the locations (in the sense of pos) of the begin and end tokens, so that trace messages could be located on them?

view this post on Zulip Reid Barton (Apr 20 2020 at 23:41):

@Jason Rute hmm, is this stuff relevant to you? ^

view this post on Zulip Jason Rute (Apr 21 2020 at 00:05):

@Reid Barton I'm interested in the "Try this" stuff. If one ever gets AI for lean working, then "Try this" will be the way to have the found proof or tactics suggested to the user.

If you are asking about tracing, then I don't know the answer off hand, but I am interested in seeing the answer. I'm experimenting with various ways to get information out of lean, and and this is one of the ways.

view this post on Zulip Keeley Hoek (Apr 21 2020 at 02:54):

That's not hard I think, but I've never written code which does that
If I remember I'll take a look!

I really want my "interactive edit notification" thing to go in anyway, so I'll do it then


Last updated: May 09 2021 at 19:11 UTC