feat: user widgets by EdAyers · Pull Request #1238 · leanprover/lean4

EdAyers · 2022-06-22T16:23:23Z

See also

RFC: RFC: User widgets #1225
vscode PR feat: user widgets vscode-lean4#194
https://github.com/Vtec234/npm-widget

Todo:

keep adding to documentation, including a full example of setting up npm etc with Lake
e2e interactive test for a simple widget
ToJson Syntax? Means that we can pass UserWidgetInfo directly to infoview. → removed
publish @lean4/infoview on npm Publish @lean4/infoview to npm vscode-lean4#203
vscode pr feat: user widgets vscode-lean4#194
content addressing of getWidgetSource
add rubiks cube, comm-diagrams, etc demos to lean-samples repository feat: rubiks cube sample leanprover-community/lean4-samples#3
fix hyperlink to lean4-samples (will fix when feat: rubiks cube sample leanprover-community/lean4-samples#3 is done)

src/Lean/Widget/UserWidget.lean

doc/widgets.md

src/Lean/Widget/UserWidget.lean

To satisfy leanprover#1238 (comment)

To satisfy leanprover/lean4#1238 (comment)

To satisfy leanprover#1238 (comment)

tests/lean/interactive/userWidget.lean

Vtec234

🌈🌈🌈

tests/lean/interactive/run.lean

src/Lean/Widget/UserWidget.lean

tests/lean/interactive/run.lean

src/Lean/Widget/UserWidget.lean

To satisfy leanprover#1238 (comment)

tests/common.sh

Vtec234 · 2022-07-19T17:20:54Z

Ok, I think this is good to go!

PatrickMassot · 2022-07-20T01:00:10Z

The PR description still has several TODOs. Should it be updated? Or are they meant as future work?

EdAyers · 2022-07-20T08:21:27Z

Yeah the remaining todos are cyclic dependencies, I'll make issues for them.

doc/widgets.md

src/Lean/Widget/UserWidget.lean

doc/widgets.md

See leanprover#1225

also rm hash field from UserWidgetInfo because it can be computed in handler instead.

To satisfy leanprover#1238 (comment)

[skip ci]

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

To satisfy leanprover/lean4#1238 (comment)

…tion name instead of WidgetSource This means that the environment extension is not storing a big text object and instead the text is retrieved from the declaration itself.

leodemoura · 2022-07-21T12:42:58Z

@EdAyers Is it ready to be merged? @Vtec234 and @Kha have already approved the changes. They also look good to me.

EdAyers · 2022-07-25T13:22:56Z

Happy to merge

To satisfy #1238 (comment)

Vtec234 reviewed Jun 22, 2022

View reviewed changes

src/Lean/Widget/UserWidget.lean Outdated Show resolved Hide resolved

Vtec234 reviewed Jun 22, 2022

View reviewed changes

src/Lean/Widget/UserWidget.lean Outdated Show resolved Hide resolved

Vtec234 reviewed Jun 22, 2022

View reviewed changes

src/Lean/Widget/UserWidget.lean Show resolved Hide resolved

EdAyers commented Jun 23, 2022

View reviewed changes

src/Lean/Widget/UserWidget.lean Show resolved Hide resolved

EdAyers mentioned this pull request Jun 23, 2022

feat: user widgets leanprover/vscode-lean4#194

Merged

3 tasks

hargoniX mentioned this pull request Jun 23, 2022

LeanInk: Pretty rendering leanprover/doc-gen4#61

Closed

This was referenced Jun 24, 2022

feat: rubiks cube sample leanprover-community/lean4-samples#3

Merged

Publish @lean4/infoview to npm leanprover/vscode-lean4#203

Closed

gebner reviewed Jun 27, 2022

View reviewed changes

EdAyers mentioned this pull request Oct 25, 2023

Support directory dependencies #2761

Closed

Vtec234 force-pushed the widget-pr branch from 80b7c63 to 680f66a Compare July 11, 2022 01:47

EdAyers added a commit to Vtec234/lean4 that referenced this pull request Jul 12, 2022

fix: widgets are now defined using a UserWidgetDefinition

ba50787

To satisfy leanprover#1238 (comment)

EdAyers added a commit to Vtec234/vscode-lean4 that referenced this pull request Jul 12, 2022

fix: refactor userwidget api

95c59a7

To satisfy leanprover/lean4#1238 (comment)

EdAyers added a commit to Vtec234/lean4 that referenced this pull request Jul 12, 2022

fix: widgets are now defined using a UserWidgetDefinition

d049498

To satisfy leanprover#1238 (comment)

EdAyers force-pushed the widget-pr branch from ba50787 to d049498 Compare July 12, 2022 10:16

EdAyers marked this pull request as ready for review July 12, 2022 10:33

Vtec234 reviewed Jul 14, 2022

View reviewed changes

tests/lean/interactive/userWidget.lean Show resolved Hide resolved

Vtec234 approved these changes Jul 14, 2022

View reviewed changes

Vtec234 reviewed Jul 15, 2022

View reviewed changes

tests/lean/interactive/run.lean Outdated Show resolved Hide resolved

gebner reviewed Jul 15, 2022

View reviewed changes

src/Lean/Widget/UserWidget.lean Show resolved Hide resolved

src/Lean/Widget/UserWidget.lean Outdated Show resolved Hide resolved

tests/lean/interactive/run.lean Outdated Show resolved Hide resolved

gebner reviewed Jul 18, 2022

View reviewed changes

src/Lean/Widget/UserWidget.lean Outdated Show resolved Hide resolved

src/Lean/Widget/UserWidget.lean Outdated Show resolved Hide resolved

Vtec234 pushed a commit to Vtec234/lean4 that referenced this pull request Jul 19, 2022

fix: widgets are now defined using a UserWidgetDefinition

2fd31b6

To satisfy leanprover#1238 (comment)

Vtec234 force-pushed the widget-pr branch from 60752f9 to 3168683 Compare July 19, 2022 15:38

Vtec234 reviewed Jul 19, 2022

View reviewed changes

tests/common.sh Show resolved Hide resolved

Kha reviewed Jul 20, 2022

View reviewed changes

doc/widgets.md Show resolved Hide resolved

Kha reviewed Jul 20, 2022

View reviewed changes

src/Lean/Widget/UserWidget.lean Outdated Show resolved Hide resolved

Kha approved these changes Jul 20, 2022

View reviewed changes

doc/widgets.md Outdated Show resolved Hide resolved

EdAyers and others added 15 commits July 20, 2022 14:38

feat: user widgets

04d481d

See leanprover#1225

chore: remove Json.syntax docstring

3e39daa

refactor: getWidgetInfos → getWidgets

23ea1ee

also rm hash field from UserWidgetInfo because it can be computed in handler instead.

chore: use invalidParams error code

537637f

chore: rebase on 2022-07-10

b213bbf

fix: widgets are now defined using a UserWidgetDefinition

8dfe661

To satisfy leanprover#1238 (comment)

doc: update widget docs

8da3f8d

[skip ci]

style: userwidget

1b53fcc

test: remove unused rpc case from runner

6f02917

style: tests/lean/interactive/run.lean

6b12c97

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

fix: local instances

0f3b5c4

fix: add Inhabited Std.RBMap

08b2a39

test: fix infoTree.lean

28f71f1

test: strip some more indices

cd669f0

doc: fix @Kha issues

e2fd65a

EdAyers force-pushed the widget-pr branch from b81ad00 to e2fd65a Compare July 20, 2022 13:38

EdAyers added a commit to Vtec234/vscode-lean4 that referenced this pull request Jul 20, 2022

fix: refactor userwidget api

d1eef2d

To satisfy leanprover/lean4#1238 (comment)

fix: widgetSourceRegistry now stores the UserWidgetDefinition declara…

2f05fb0

…tion name instead of WidgetSource This means that the environment extension is not storing a big text object and instead the text is retrieved from the declaration itself.

Vtec234 added 2 commits July 23, 2022 18:08

refactor: simplify position type

09de6cc

fix: tests

60ae60e

Kha added the awaiting-author Waiting for PR author to address issues label Jul 25, 2022

leodemoura merged commit 12b3573 into leanprover:master Jul 25, 2022

leodemoura pushed a commit that referenced this pull request Jul 25, 2022

fix: widgets are now defined using a UserWidgetDefinition

18a3d1a

To satisfy #1238 (comment)

Vtec234 deleted the widget-pr branch July 25, 2022 15:29

leodemoura removed the awaiting-author Waiting for PR author to address issues label Jul 27, 2022

Conversation

EdAyers commented Jun 22, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Vtec234 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Vtec234 commented Jul 19, 2022

Uh oh!

PatrickMassot commented Jul 20, 2022

Uh oh!

EdAyers commented Jul 20, 2022

Uh oh!

Uh oh!

Uh oh!

Uh oh!

leodemoura commented Jul 21, 2022

Uh oh!

EdAyers commented Jul 25, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

EdAyers commented Jun 22, 2022 •

edited

Loading