Multi-expression selection

[Vtec234]

There are many cases where we want to tell Lean which parts of the goal state are relevant to a particular action. For example, simp [h₁, h₂] marks these two hypotheses as the rewrite rules to use. This PR adds a mechanism to select one or more locations within the goal state. Below h₁, h₂, and the RHS of the goal type are selected.

Use cases

1. Tactic support and suggestions

This enables writing user widgets which use the current selection as a context/relevance filter for which parts of the goal to process. For example, the following widget (source code) becomes quite easily implementable:

recording.mp4

I believe that this also makes contextual suggestions (leanprover/lean4#1223) implementable in "user space", i.e. without touching core, as a user widget, and thus supersedes the locations part of that RFC.

2. Diagram contexts

In any production-sized local context it is difficult to algorithmically determine which hypotheses and values are relevant to drawing a diagram. Thus we defer the job of selecting what should be drawn, e.g. which relations between sets to include in a Venn diagram, to the user.

Implementation

This is based on the contextual suggestions prototype by @EdAyers but diverges from it in that locations are more strongly typed as follows.

/**
 * A location within a goal. It is either:
 * - one of the hypotheses; or
 * - (a subexpression of) the type of one of the hypotheses; or
 * - (a subexpression of) the value of one of the let-bound hypotheses; or
 * - (a subexpression of) the goal type. */
export type GoalLocation =
  { hyp: FVarId }
  | { hypType: [FVarId, SubexprPos] }
  | { hypValue: [FVarId, SubexprPos] }
  | { target: SubexprPos }

/**
 * A location within a goal state. It identifies a specific goal together with a {@link GoalLocation}
 * within it.  */
export interface GoalsLocation {
    /** Which goal the location is in. */
    mvarId: MVarId;
    loc: GoalLocation;
}

Moreover we elect not to show extra information such as suggestions in popups because they are already too cramped by docstrings. Instead, extra info should be shown as an extra panel below the tactic state, i.e. as a user widget. The infoview popups will probably not become extensible.

We extend the data passed to user widgets by the current goal state as well as the selection.

/** Props that every user widget receives as input to its `default` export. */
export interface UserWidgetProps {
    /** Cursor position in the file at which the widget is being displayed. */
    pos: DocumentPosition
    /** The current tactic-mode goals. */
    goals: InteractiveGoal[]
    /** The current term-mode goal, if any. */
    termGoal?: InteractiveTermGoal
    /** Locations currently selected in the goal state. */
    selectedLocations: GoalsLocation[]
}

We extend the InteractiveGoal type with a reference to the metavariable context. This eliminates the need discussed here for RPC handlers invoked by user widgets to search the server state for Snapshots and retrieve the goal state from those, effectively duplicating the work that getInteractiveGoals had already done. This used to result in unnecessarily brutal-looking server-side code, and could lead to potential inconsistencies if the goal state retrieval is not exactly the same. This relies on the companion PR to lean4.

Other changes

• I also made case blocks collapsible which helps read huge tactic states and moved the 'copy to comment' button down into <Goal> so that term goals are also copyable. If these are controversial changes I can revert.

• Some extra facilities for dynamic importing of modules and React components are now provided in @leanprover/infoview/

[Vtec234]

The API is sufficient to expose work by @KaseQuark on conv as a user widget.

recording.mp4

[gebner]

Is there a reason we can't just use T | null in the interface types instead?

[Vtec234]

We could, but this is the least invasive change which doesn't require all downstream code to check for !== null (or use truthish checks). IMO this is justified because null vs undefined is one of the many bizarre parts of JS with unclear semantics and it is easier to stick to always using undefined.

[gebner]

One concrete case where this pops up is with getInteractiveGoals.

{ goals: await getInteractiveGoals(...) }
-- where { goals?: InteractiveGoals }

If we keep null, then the easy fix would be to add a ?? undefined to the use site. But converting null to undefined seems convenient as well.

Note that we run into exactly the same issue with Option Foo, where the ToJson instance produces null. For consistency it might be better to avoid any special case hacks here (since it gives the incorrect impression that T | undefined is the correct RPC API for Option T).

[Vtec234]

Ahhh, you correctly point out that our entire RPC API is wrong. We serialize structure fields marked with the magic ? as missing similarly to Serde's skip_serializing_if. In JS accessing those fields gives undefined. But we cannot do this for top-level values as there is only a null but no undefined in JSON. For example

structure Foo where
  a? : Option String
  b  : Option String
  deriving ToJson

/- {"b": null} -/
#eval toJson { a? := none, b := none : Foo }

so all the top-level Option SomeResponse calls really return T | null. In this case I guess we should go through the whole API and adjust it, and make a breaking release. Let's do this in another PR however, and temporarily keep the hack.

[gebner]

Sounds good to me.