interactive save_widget

Stream: metaprogramming / tactics

[Johan Commelin]

Is there a way to make this work? I've been looking at the implementation of the #html command. The effect I'm trying to get is that some tactic takes a bunch of html and renders it below the goal state in the Info View.

example : true :=
begin
  let D : html empty := "hello world",
  let c₁ : component unit empty := component.stateless (λ _, [D]),
  let c₂ : component tactic_state empty := component.ignore_props c₁,
  tactic.save_widget ⟨0,0⟩ c₂, -- fails: unknown identifier 'c₂'
end

[Johan Commelin]

Basically, I would like a variant of trace that renders html.

[Gabriel Ebner]

I'd try trace_widget.

[Gabriel Ebner]

Oh, and you're mixing up two things here.

[Gabriel Ebner]

You're not writing tactic code, but instead calling the let-tactic (i.e. you try to prove true using the lemma html empty).

[Gabriel Ebner]

What you want is

example : true :=
begin
  (do let D : html := "hello world",
         ...
         tactic.trace_widget c₂)
end

[Johan Commelin]

@Gabriel Ebner Thanks! Now the code is compiling. But I don't actually see any result in the Info View.

[Gabriel Ebner]

I can reproduce the error, something's seriously going wrong:

{response: "error", message: "'unreachable' code was reached", seq_num: 750}

[Johan Commelin]

This is what I have atm:

example : true :=
begin
  -- let s : string := "test",
  (do
    let X : html empty := "hello world",
    let c₁ : component unit empty := component.stateless (λ _, ["joy"]),
    let c₂ : component tactic_state empty := component.ignore_props c₁,
    tactic.trace_widget c₂,
    tactic.trace "boo",
    tactic.skip),
  trivial
end

[Gabriel Ebner]

It's not you, it's an issue in Lean. Some widgets seem to fail to render. I've just pushed an update to the vscode extension to show the error message.

[Johan Commelin]

Aha, thanks for your help!

[Kevin Buzzard]

Johan gets a rare bonus point for reaching unreachable code. This has become much harder recently.

[Gabriel Ebner]

Mmmh, so for some unclear reason trace_widget does not work inside tactic proofs. This works just fine:

#eval tactic.trace_widget $ component.pure $ λ _, ["hello world"]

[Johan Commelin]

The error shows up as a regular message, in green font, instead of the usual red font. Is that because it's somehow too nested for the extension to recognize it as an error message?

[Gabriel Ebner]

The "'unreachable' code was reached" message? I didn't spend too much time styling it.

[Gabriel Ebner]

(The error message only refers to the body of the message. When it works, trace_widget generates a regular "green" message. The only thing failing here is rendering the message body.)

[Johan Commelin]

aha

[Johan Commelin]

@Gabriel Ebner I just learned from @Alex J. Best that the following works (and fails):

meta def trace_html (h : html empty) : tactic unit :=
tactic.trace_widget $ component.pure $ λ _, h

meta def foo (s : string) : html empty := h "em" [] [s]

example : true :=
begin
  let s : string := "test",
  trace_html (foo "joy!"), -- works
  trace_html (foo "more joy!"), -- works
  -- trace_html (foo s), -- fails
  trivial
end

[Gabriel Ebner]

I think you know why the last trace_html fails.

[Gabriel Ebner]

I'm relieved that trace_widget seems to work after all, although you have to put it behind a helper definition. Maybe it's because of the lambdas?

[Johan Commelin]

Gabriel Ebner said:

I think you know why the last trace_html fails.

No, actually I don't. I really hoped that it would work.

[Johan Commelin]

My mental model is that let is just an "inline" def. But apparently this is not the case.

[Alex J. Best]

My assumption was just that it uses the name of the tactic to hook the position, so when the tactic is anonymous it doesn't have anything to get the pos from

[Johan Commelin]

Oooh, I guess I need to do some sort of tactic parser dance to make the version with s work?

[Gabriel Ebner]

Johan Commelin said:

Gabriel Ebner said:

I think you know why the last trace_html fails.

No, actually I don't. I really hoped that it would work.

What happens is that you have two lists of variables. 1) The list of variables in the meta-world, where your tactic runs. and 2) The list of variables in the object-world, the proof of true. The two kinds of variables cannot refer to each other.

The let tactic creates a variable in 2), while your tactic wants one in 1).

[Gabriel Ebner]

Johan Commelin said:

Oooh, I guess I need to do some sort of tactic parser dance to make the version with s work?

(do let s : string := "test", trace_html (foo s)) should work.

[Johan Commelin]

Right, but usually you don't notice this distinction. rw [lemma_foo, hyp_foo] just works.

[Gabriel Ebner]

Johan Commelin said:

Right, but usually you don't notice this distinction. rw [lemma_foo, hyp_foo] just works.

hyp_foo is a variable in 2).

[Gabriel Ebner]

You probably don't notice the distinction because the list 1) is always empty in a tactic block.

[Johan Commelin]

Where does lemma_foo live? And where does my let s live? Don't they all live in (2)?

[Gabriel Ebner]

Yes, the let tactic modifies (2). lemma_foo is in the environment and accessible to both tactics and the proof.

[Johan Commelin]

So rw is grabbing things from (2). I want a version of trace_html that also grabs things from (2). That should be possible, right?

[Reid Barton]

example (s : string) : true :=
begin
  trace_html (foo s), -- ??
  trivial
end

[Johan Commelin]

But I guess I need to do ctx ← local_context, etc...

[Johan Commelin]

@Reid Barton Right... I understand that can't work. But somehow let s := ... records specific data.

[Gabriel Ebner]

Alex J. Best said:

My assumption was just that it uses the name of the tactic to hook the position, so when the tactic is anonymous it doesn't have anything to get the pos from

It's indeed the lambdas. https://github.com/leanprover-community/lean/pull/663

When Lean executes VM code, it compiles lambdas by adding aux definitions to the environment. These aux definitions are only available in the environment of the VM state, but not the environment of the tactic state.

[Johan Commelin]

So, could there in theory be some metalet that adds data to some (tactic?) state that is then made available to things like trace and trace_html?

[Johan Commelin]

Here is what I would like to be able to do:

meta def foobar (l : list name) : html empty := h "div" [] $ l.map (html.of_string ∘ to_string)

example (a b c d e : ℕ) : true :=
begin
  (do ctx ← tactic.local_context, trace_html ctx), -- works, and I understand why
  let s : string := "test",
  let what_I_care_about := [`a, `d, `s],
  trace_html (foobar what_I_care_about), -- fails, and I understand why
  let k : ℕ := 3,
  let x : ℤ := -1,
  let what_I_care_about := what_I_care_about ++ [x],
  trace_html (foobar what_I_care_about),
  trivial
end

[Johan Commelin]

So somehow, I want to record some metadata, during the proof, and I want to be able to refer to this later on.

[Johan Commelin]

I guess this can be done using new tactic state types. But it then all the old tactics aren't easily available.

[Johan Commelin]

I would love to have this "blend in" transparently in the usual tactic state.

[Trebor Huang]

I think that's called "quasiquote" in programming?