You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A pickled widget is a widget module together with its Props serialized for the purpose of archival, for example on a static webpage via LeanInk.
We should provide a mechanism to pickle widgets, and a stub of the @leanprover/infoview module which pickled widgets would import. Some things obviously cannot work when there is no Lean server present, for example attempting an RPC call in the stub environment will fail, but as long as the widget Props contain sufficient data to display something informative, they can be archived.
The text was updated successfully, but these errors were encountered:
A pickled widget is a widget module together with its
Props
serialized for the purpose of archival, for example on a static webpage via LeanInk.We should provide a mechanism to pickle widgets, and a stub of the
@leanprover/infoview
module which pickled widgets would import. Some things obviously cannot work when there is no Lean server present, for example attempting an RPC call in the stub environment will fail, but as long as the widgetProps
contain sufficient data to display something informative, they can be archived.The text was updated successfully, but these errors were encountered: