lean4

lean4 copied to clipboard

This PR contains a number of improvements to trace messages, most notably collapsible trace nodes can now have a message. Before (neovim screenshot):

[Meta.synthInstance] ▼
  [Meta.synthInstance] main goal R A D
  [Meta.synthInstance.newSubgoal] R A D
  [Meta.synthInstance.globalInstances] R A D, [@I4]
  [Meta.synthInstance.generate] instance @I4
  [Meta.synthInstance.tryResolve] ▶
  [Meta.synthInstance.newSubgoal] R A _tc.0
  [Meta.synthInstance.globalInstances] R A ?m.269, [@I4, I1, I2]
  [Meta.synthInstance.generate] instance I2
  [Meta.synthInstance.tryResolve] ▶
  [Meta.synthInstance.newAnswer] size: 0, R ?m.268 ?m.269
  [Meta.synthInstance.newAnswer] val: I2
  [Meta.synthInstance.resume] size: 1, R A D <== R ?m.268 ?m.269
  [Meta.synthInstance.newSubgoal] R C D
  [Meta.synthInstance.globalInstances] R C D, [@I4, I3]
  [Meta.synthInstance.generate] instance I3
  [Meta.synthInstance.tryResolve] ▶
  [Meta.synthInstance.newAnswer] size: 0, R ?m.269 ?m.270
  [Meta.synthInstance.newAnswer] val: I3
  [Meta.synthInstance.resume] size: 2, R A D <== R ?m.269 ?m.270
  [Meta.synthInstance.newAnswer] size: 2, R A D
  [Meta.synthInstance.newAnswer] val: I4

After:

[Meta.synthInstance] ✅ R A D ▼
  [] new goal R A D ▶
  [] ✅ apply @I4 to R A D ▶
  [] ✅ apply I2 to R A C ▶
  [resume] propagating R A C to subgoal R A ?m.269 of R A D ▶
  [] ✅ apply I3 to R C D ▶
  [resume] propagating R C D to subgoal R C D of R A D ▶
  [] result I4

Rough overview of changes:

• MessageData now has a .trace constructor. Nested traces are represented as .trace _ _ #[.trace .., .trace ..]. And there's a new RPC call lazyTraceChildrenToInteractive. I avoided mutually inductive types because that's painful with the derive handlers.
• The new API to produce traces is withTraceNode `trace.class msg do ... where msg : Except ε α → m MessageData is a function that can produce different messages depending on the return value.
• traceCtx and withNestedTraces is removed, including the feature where traceCtx would drop all trace messages in its body if its trace option was not enabled.
• Trace class inheritance is now opt-in. set_option trace.foo true no longer automatically implies set_option trace.foo.bar true. Inheritance can be enabled---after careful consideration---on a case-by-case basis by calling registerTraceClass `foo.bar (inherited := true).
• Multiple trace messages for the same range are grouped into a single diagnostic.
• Due to the structured transmission of the trace messages, the editor plugins now omit common prefixes of trace classes (with the full name as popup), gray out the trace class, etc.
• I've edited a few trace messages.

To try out this PR, you need a compatible editor plugin:

• neovim: https://github.com/Julian/lean.nvim/pull/267
• vscode: https://github.com/leanprover/vscode-lean4/pull/237

When editing the trace messages, I've tried to follow some key principles:

1. Trace messages explain to the user what problem Lean solved and what steps it took. This is not the place for debugging output or todos. Think of trace messages like a figure in a paper.
2. Expansion progressively increases detail. Each level of expansion (of the trace node in the editor) should reveal more details. For example, the unexpanded node should show the top-level goal. Expanding it should show a list of steps. Expanding one of the steps then shows what happens during that step.
3. One trace message per step. The [trace.class] marker functions as a visual bullet point, making it easy to identify the different steps at a glance.
4. Outcome first. The top-level trace message already shows whether the action failed or succeeded, as opposed to a "success" trace message that comes pages later.
5. Be concise. Keep messages short. Avoid repetitive text. (This is also why the editor plugins abbreviate the common prefixes.)
6. Emoji are concisest. Several helper functions in Lean.Util.Trace help with a consistent emoji language.
7. Good defaults. Setting set_option trace.Meta.synthInstance true (etc.) should produce great trace messages out-of-the-box, without needing extra options to tweak it. (That's the motivation for making inheritance opt-in.)

Addresses #591.

@gebner This is great. Thanks for working on this. I didn't have time to review it yet. BTW, the PR is currently marked as a draft, is something missing? Could you please copy some of the comments above as docstrigs? For example, the inherited text could be copied as a docstring for registerTraceClass.

!bench

Here are the benchmark results for commit f722465dc8d5028a4c67da7ee975edc6647f3d74. There were significant changes against commit 860d726d726ebd30a95ff95d192bb8a2fe55e30c:

  Benchmark     Metric    Change
  ==============================
+ stdlib size   lines C      -1%

This is awesome! Could you comment on whether there is a clear path to implementing Daniel's proposal later as well?

This is awesome! Could you comment on whether there is a clear path to implementing Daniel's proposal later as well?

Is it possible to implement something like Daniel suggested (if I understand it correctly, a set_option trace.inside.Meta.isDefEq true that enables all trace messages inside a Meta.isDefEq node)? Certainly. But that would also enable a lot of junk trace messages as well, so I'm not sure how useful such a blanket setting would be.

Is it possible to implement something like Daniel suggested (if I understand it correctly, a set_option trace.inside.Meta.isDefEq true that enables all trace messages inside a Meta.isDefEq node)? Certainly. But that would also enable a lot of junk trace messages as well, so I'm not sure how useful such a blanket setting would be

Probably not much, but the suggestion of composable filters would be extremely useful:

One might want the Meta.synthInstance.newSubgoal calls that occur inside isDefEq calls.

With the trace explorer, the ideal UI might be something like a fuzzy search input box where we can type in isDefEq Meta.synthInstance.newSubgoal (think CSS selectors) and have the trace tree auto-expand to show those. It would either need server support so that we don't have to eagerly toInteractive the entire trace, or we could send just a "trace outline" containing only the classes but not the messages and have the client filter that.

It would either need server support so that we don't have to eagerly toInteractive the entire trace, or we could send just a "trace outline" containing only the classes but not the messages and have the client filter that.

Any thoughts on what the ideal RPC API for that would be? With this PR there's only a LazyTraceChildren type, so even if we add an RPC call like searchTraceChildren{ children: LazyTraceChildren, query: String }: SearchResult we'd still need to do half of the search on the client (since we only have an RPC reference for the kids, but not the root node). On the other hand, I didn't want to hide the root node behind an RPC ref, because that would require additional round-trips.

Specifying the filters on the Lean side is much easier of course, and requires less API work. Something like enable_trace isDefEq>synthInstance in def ... would be fairly straightforward to implement.

BTW, the PR is currently marked as a draft, is something missing?

I wanted some discussion on the RPC API first (see exchange with Wojciech). There's also plenty of trace messages to change so that they fit better into the new concept. The only module I've really touched is the TC synthesizer, the rest is just the minimum to get rid of traceCtx and withNestedTraces. But I can also do that in follow-up PRs.

It looks like this could also serve as the basis for a metaprogram that essentially tests a trace against a spec, right? The idea here is that I'd like to step through some instance searches in Functional Programming in Lean to help readers get an idea of how outParam and defaultInstance affect the process, but this is only tenable to keep up to date if I can test the resulting text against what Lean is actually doing. It seems that enabling the right traces, capturing them, and then validating them could be doable with this new .trace constructor, right?

Any thoughts on what the ideal RPC API for that would be?

Sadly no, you probably have a better idea of it by now.

Specifying the filters on the Lean side is much easier of course, and requires less API work. Something like enable_trace isDefEq>synthInstance in def ... would be fairly straightforward to implement.

The tradeoff seems to be:

• If we send a trace outline, we could have a nice quickly-responsive UI with a fuzzy search box. But implementation effort is duplicated across infoview/NVim.
• If we use an enable_trace command, the server does everything and no changes to clients may be required thanks to the collapseByDefault flag which we can just toggle appropriately. If done the obvious way though, there will be a pretty bad interaction with long-running commands which produce huge traces in that changing the enable_trace will re-elaborate the entire snapshot of the command below. So quick searching of the trace would not really work.

Thinking about the search API issue a bit more, I believe that all searching should happen server-side. This is great because:

• It also works on the command-line.
• Filters can be shared in snippets on Zulip.
• It reduces code duplication in editors.
• The content of the traces can be searched as well. For example, we can show all type-class traces with metavariables in them, etc.

We can implement this without breaking backwards compatibility by adding an additional field to the MsgEmbed for traces, namely WithRpcRef MessageData for the .trace object itself (maybe with indentation and naming contexts etc.). Then we only need to add an RPC call searchTrace{trace: MessageData, query: String}: MessageData and hook it up in the editors.

It looks like this could also serve as the basis for a metaprogram that essentially tests a trace against a spec, right? The idea here is that I'd like to step through some instance searches in Functional Programming in Lean to help readers get an idea of how outParam and defaultInstance affect the process, but this is only tenable to keep up to date if I can test the resulting text against what Lean is actually doing. It seems that enabling the right traces, capturing them, and then validating them could be doable with this new .trace constructor, right?

@david-christiansen Indeed, what you describe is a bit easier now since there is a structured trace representation so you don't need to search for the regex \[([^]+)\] (.*) in the diagnostic to find traces. The trace messages are however completely free-form, you still need string processing to check if ✅ apply I2 to R A C is the expected output or not.

The trace messages are also not stable, and will be improved over time.

I've changed the serialization of trace to an object to make easier to extend in the future. See comment above about server-side search.

Being unstable and improved over time seems to be a common feature of Lean 4 :-) Thanks!