Try this!

Stream: general

[Scott Morrison]

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. :-)

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

#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

[Mario Carneiro]

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 ?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

@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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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.

[Bryan Gin-ge Chen]

@Scott Morrison @Alexander Bentkamp wrote that code actually.

[Bryan Gin-ge Chen]

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.

[Scott Morrison]

@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?

[Reid Barton]

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

[Jason Rute]

@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.

[Keeley Hoek]

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