no lean messages output in hacked mode

Stream: general

[Kevin Buzzard]

@Rob Lewis made me a new "mode", it looks a bit like this:

-- lots of stuff omitted
meta def kevin.interactive.induction :
  interactive.parse interactive.cases_arg_p →
  interactive.parse interactive.types.using_ident →
  interactive.parse interactive.types.with_ident_list →
  interactive.parse (optional (lean.parser.tk "generalizing" *> lean.parser.many lean.parser.ident)) → tactic unit
:= tactic.interactive.induction

run_cmd copy_decls

example (n : ℕ) : true :=
begin [kevin]
  induction n,
    sorry, sorry
end

so I can have my hacked version of induction just by writing induction, as long as the user writes begin [kevin]. But there is no output on the Lean Messages screen in VS Code! I think this is because Rob didn't know how to turn this on. @Sebastian Ullrich do you know how to turn this on?

[Kevin Buzzard]

https://gist.github.com/kbuzzard/a91012b1ab7a255990a1ec9045820f4b

[Simon Hudon]

You can look at https://github.com/unitb/temporal-logic/blob/master/src/temporal_logic/tactic.lean to see how to make that work. I copied a comment by Leo in the file

[Simon Hudon]

Actually, here is the comment:

/-
   The auto quotation currently supports two classes of tactics: tactic and smt_tactic.
   To add a new class Tac, we have to
   1) Make sure it is a monad. That is, we have an instance for (monad Tac)
   2) There is a namespace Tac.interactive
   3) There is a definition: Tac.step {α : Type} (t : Tac α) : Tac unit
   4) (Optional) Tac.istep {α : Type} (line0 col0 : nat) (line col : nat) (tac : Tac α) : Tac unit
      Similar to step but it should scope trace messages at the given line/col,
      and ensure that the exception position is after (line0, col0)
   6) There is a definition Tac.save_info (line col : nat) : Tac unit
   7) There is a definition Tac.execute (tac : Tac unit) : tactic unit
   8) There is a definition Tac.execute_with (cfg : config) (tac : Tac unit) : tactic unit
      where config is an arbitrary type.
   TODO(Leo): improve the "recipe" above. It is too ad hoc.
-/

[Kevin Buzzard]

I want to rewrite the defintions of tactics which are already there

[Rob Lewis]

Oh, I thought I fixed this while you were here. Change the definition of save_info: meta def save_info := tactic.save_info

[Kevin Buzzard]

Doesn't work for me

[Kevin Buzzard]

open tactic

meta def copy_decl (d : declaration) : tactic unit :=
add_decl $ d.update_name $ d.to_name.update_prefix `kevin.interactive

@[reducible] meta def filter (d : declaration) : bool :=
d.to_name ∉ [`tactic.interactive.induction]

meta def copy_decls : tactic unit :=
do env ← get_env,
  let ls := env.fold [] list.cons,
  ls.mmap' $ λ dec, when (dec.to_name.get_prefix = `tactic.interactive ∧ filter dec) (copy_decl dec)

@[reducible] meta def kevin := tactic

namespace kevin

--meta instance : monad kevin := by delta kevin; apply_instance

--meta instance : alternative kevin := by delta kevin; apply_instance

meta def step {α} (c : kevin α) : kevin unit :=
c >> return ()

meta def save_info := tactic.save_info

meta def execute (c : kevin unit) : kevin unit :=
c

--meta def trace_state {α : Type}

end kevin

--#check tactic.interactive.induction

meta def kevin.interactive.induction :
  interactive.parse interactive.cases_arg_p →
  interactive.parse interactive.types.using_ident →
  interactive.parse interactive.types.with_ident_list →
  interactive.parse (optional (lean.parser.tk "generalizing" *> lean.parser.many lean.parser.ident)) → tactic unit
:= tactic.interactive.induction

run_cmd copy_decls

example (n : ℕ) : n = n :=
begin [kevin]
  induction n,
  -- no output in Lean window
    sorry, sorry
end

[Kevin Buzzard]

trace_state indicates that the goals are fine, I just can't see them.

[Kevin Buzzard]

 4) (Optional) Tac.istep {α : Type} (line0 col0 : nat) (line col : nat) (tac : Tac α) : Tac unit
      Similar to step but it should scope trace messages at the given line/col,

That's what Sebastian is referring to perhaps.

[Rob Lewis]

Oh, that's weird, changing save_info fixes it in the "display goal" view but not in "display messages."

[Kevin Buzzard]

meta def istep : Π {α : Type*}, ℕ → ℕ → ℕ → ℕ → tactic α → tactic unit := tactic.istep

[Kevin Buzzard]

This does it.

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

aargh no it doesn't; my trace_state was still left in

[Simon Hudon]

If the only benefit is having induction behave in a specific way, this solution is overkill. You're going to need to explicitly bring every tactic that you want available in your proof language. You're much better off calling your tactic my_induction or induction' or kevin_induction and staying in tactic.interactive

[Kevin Buzzard]

I've finally got it working :-) Thanks.

[Rob Lewis]

Wait, there are sorrys there, there shouldn't be anything displaying in "display messages." It works perfectly fine for me with save_info changed.

[Kevin Buzzard]

I was in the other mode :-/ I wish they won't both called "Lean messages" in VS Code.

[Kevin Buzzard]

In CoCalc it's "all messages" and "info at cursor"

[Kevin Buzzard]

This is brilliant, thanks Rob and Sebastian.

[Kevin Buzzard]

@Sebastian Ullrich this is for some standalone project where the user won't see the [kevin] nonsense but will want to be using familiar Lean tactics.

[Koundinya Vajjha]

When a tactic class like this is defined, are all the interactive tactics available by default or should they be manually lifted to the [kevin] tactic class?

[Koundinya Vajjha]

Oh sorry Simon already answered this

[Rob Lewis]

In Kevin's file, there's a command that copies everything in tactic.interactive to kevin.interactive.

[Sebastian Ullrich]

This is brilliant, thanks Rob and Sebastian.

Uh, you're welcome...?

[Simon Hudon]

@Sebastian Ullrich I'm starting to think @Kevin Buzzard does not know that you and I are two separate people

[Kevin Buzzard]

I am very vague at the best of times

[Kevin Buzzard]

I see my mistake now. Thanks @Simon Hudon . My silly mode is now fully compliant with the comment and I've had a much more pleasant experience with it since. Thanks!

[Marc Huisinga]

this "canonically isomorphic"-business is going too far, now he's applying it to people!!

[Kevin Buzzard]

all computer scientists are equivalent

[Kevin Buzzard]

gaargh sorry doesn't work in my monad (now called less_leaky)

invalid tactic class 'less_leaky', 'less_leaky.solve1' has not been defined

[Kevin Buzzard]

I'll get back to Simon's list

[Kevin Buzzard]

Oh I've fixed it myself.

[Kevin Buzzard]

Whatever I don't have, I just take from the tactic namespace. Duh.

[Kevin Buzzard]

@Simon Hudon it seems to me that tactic does not follow rule 8?

   8) There is a definition Tac.execute_with (cfg : config) (tac : Tac unit) : tactic unit
      where config is an arbitrary type.

[Kevin Buzzard]

(deleted)

[Keeley Hoek]

Sure, it's hardcoded not to look for such when you're in tactic

[Kevin Buzzard]

That doesn't tell me how to write my own one then :-)

[Simon Hudon]

You can look at the smt example or my own temporal example

[Kevin Buzzard]

I just stole the smt one