by interactive!

Stream: lean4

[Joachim Breitner]

by_interactive.gif

[Joachim Breitner]

It works! Very sluggish as it loses focus, so probalby due to the missing cache that @Edward Ayers mentioned. But hey, we are getting somewhere

[Joachim Breitner]

And just 9 minutes to create a new dynamic input widget for a new type (Int), including reading how to convert Int to String in Lean and TypeScript.
All new code is on the screen!
by_interactive_int.gif

[Eric Wieser]

Great, you can now implement a selection of everyone's favorite telephone number entry fields!

[Joachim Breitner]

This is the core of the idea:

/-- The public interface: -/
class Interactive (a : Type) where
  /--
  JS source of a React module/component. Its props argument will contain
   * data : string : A String representing the current state
   * onDataChange : string -> (): A callback called when the state changes
  -/
  component : String
  /--
  A lean function converting a string representation to a lean value.
  TODO: How should errors be reported here?
  -/
  fromInteractiveString : String -> a

The current implementation is very shoddy. My secret plan is that someone finds the idea great but the implementation disgusting and will do it nicely again :-)

[Kyle Miller]

It would be cool if you could use this sort of thing to configure a tactic, where when you click on a tactic it shows a list of configuration options, then when you change one it reflects that back into the code.

[Kyle Miller]

Floris and I were just talking about something like tactic#squeeze_simp, where after squeezing it could replace itself. I know this isn't what you're going for with interactive, but this does seem to suggest a number of interesting UI directions.

[Joachim Breitner]

Yes, definitely related, and could use the same infrastructure. (Even simpler, as no JS is involved)

[Sebastian Ullrich]

If you don't need a visualization in the info view, you should use code actions instead

[Joachim Breitner]

@Edward Ayers I am now caching the Component (I believe), and the input field keeps the focus, but it does not keep, for example, the cursor position in the input.

[Adam Topaz]

One thing I think would be extremely useful is something similar to the "extract lemma" functionality of idris (I don't know what it's actually called). IIRC, the general consensus is that this was not possible with Lean3, but this demo and the comments suggest that it might be possible in Lean4?

[Edward Ayers]

Joachim Breitner said:

Edward Ayers I am now caching the Component (I believe), and the input field keeps the focus, but it does not keep, for example, the cursor position in the input.

I think this means that when react is diffing the new DOM with the old DOM it's not identifying the two components. Which suggests to me they might not be being cached. Could you share your code?

[Joachim Breitner]

https://github.com/nomeata/lean4-interactive-tactic/blob/master/widget/src/widget.tsx

[Sebastian Ullrich]

@Adam Topaz If that is sensitive to the current selection, I don't think that is covered by code actions. It would have to be yet another custom request.

[Joachim Breitner]

20 loc!
by_interactive_color.png

[Joachim Breitner]

Ed, with this widget the cursor stays in the right position. Maybe this component is smarter about being rebuilt with the same data as a plain <input>, but it works nice.

[Joachim Breitner]

I’ll add some debounce to the general widget

[Edward Ayers]

Joachim Breitner said:

https://github.com/nomeata/lean4-interactive-tactic/blob/master/widget/src/widget.tsx

Can you try this:

instance : Interactive String := {
  component := "
      import * as React from 'react';
      const e = React.createElement;
      export default function(props) {
        const [str, setStr] = React.useState(props.data)
        React.useEffect(() => setStr(props.data), [props.data])
        return e('div', null,
          'You can edit the String here!',
          e('input', {
             value: str,
             onChange : (event) => {
              const value =event.target.value
              setStr(value)
              props.onDataChange(value);
              },
          })
        )
      }",
  fromInteractiveString := id
  }

[Edward Ayers]

I think the problem is just that there is a delay between changing <input> and the props.data changing, and during this delay React gets itself in to a funny state, so the solution is to have a local state too.

[Joachim Breitner]

Spot on! I accidentially solved this when adding debouncing, as there I also have a local state. But in the wrapper widget, so that authors of the small snippets don’t have to deal with this.

[Joachim Breitner]

It's coming along pretty nicely :-)

[Reid Barton]

How can I build the widget.js file?

[Joachim Breitner]

Run

npm install
npm run build

in the widget directory (and also the color directory)

[Reid Barton]

I think my node/npm is perhaps several years too old

[Reid Barton]

e.g.

$ /home/rwbarton/math/lean4/lean4-interactive-tactic/widget/node_modules/rollup/dist/bin/rollup --help
/home/rwbarton/math/lean4/lean4-interactive-tactic/widget/node_modules/rollup/dist/bin/rollup:1270
const SECOND_ROUNDING_EPSILON = 0.000_000_1;
                                ^^^^^

SyntaxError: Invalid or unexpected token
    at Module._compile (internal/modules/cjs/loader.js:723:23)
    at Object.Module._extensions..js (internal/modules/cjs/loader.js:789:10)
    at Module.load (internal/modules/cjs/loader.js:653:32)
    at tryModuleLoad (internal/modules/cjs/loader.js:593:12)
    at Function.Module._load (internal/modules/cjs/loader.js:585:3)
    at Function.Module.runMain (internal/modules/cjs/loader.js:831:12)
    at startup (internal/bootstrap/node.js:283:19)
    at bootstrapNodeJSCore (internal/bootstrap/node.js:623:3)

[Reid Barton]

Aha, I found a successful path: blow away my node_modules directory from previous attempts and then run in turn npm install node, npm install npm, add "type": "module" to packages.json (IDK what this means, but something suggested it), and then npm run build.

[Joachim Breitner]

As a prototype to make nice gifs to show off this is “done”. But where should we take it now? Should by interactive be a feature that comes with lean proper, like #widget itself (after plenty of cleanup, error handling, unifying the dynamic module loading with the existing infrastructure)? Or only a separately installable library?

[Johan Commelin]

I imagine that it could be a self-contained library (that maybe depends on std). And then mathlib can depend on your lib.

[Johan Commelin]

But I'm not an expert on Lean 4 library infrastructure.

[Reid Barton]

Have you thought about supporting parameterized instances (e.g. instance {n : Nat} : Interactive (Fin n → Int) )? Or providing access to the proof state?

[Reid Barton]

I hacked up something ugly for parameterized instances using eval, though I think it could also be done without

[Joachim Breitner]

It’s just using instance resolution as is, so parametrized instances could “just work”, could they? Or maybe I am misunderstanding what you want to achieve.

[Joachim Breitner]

I did think about generic instances like Interactive t -> Interactive (List t) that wrap an arbitrary interactive widgets for t in a generic list editing widget… doable, but not sure how useful it is.

[Reid Barton]

e.g. for Interactive (Fin n → Int), the widget should already know the value of n somehow.

[Joachim Breitner]

Ah, I see: You want to allow the class to pass the values of the instance parameters to the widget somehow?

[Reid Barton]

I tried just splicing it into the component field, but then whnf doesn't reduce it to a string literal any more.

[Joachim Breitner]

I get it now. Yes, the whnf is a crutch anyways, and “proper evaluation” makes more sense, if possible.

[Wojciech Nawrocki]

By the way, this work on Graphite does something very similar for Eclipse except the widgets show up inline. VS Code has an editor inset API but it looks very experimental and possibly not working.