Skip to content

RELEASES.md

Latest commit

 

History

History
122 lines (85 loc) · 4.8 KB

RELEASES.md

File metadata and controls

122 lines (85 loc) · 4.8 KB

ProofWidgets4 releases

This file contains work-in-progress notes for the upcoming release, as well as previous releases. Please check the releases page for the build artifacts.

v0.0.95

  • Add pre-built JS files to the repository. This removes our reliance on the Lake cloud release fetching these.

v0.0.93

  • Added RefreshComponent. It supports widget implementations that continue updating the UI while new information is being computed in the background.

  • Deprecated @[server_rpc_method_cancellable]. All @[server_rpc_method]s are now cancellable. To migrate, replace @[server_rpc_method_cancellable] with @[server_rpc_method], and replace calls to IO.checkCanceled with RequestM.checkCancelled.

    If the RPC method spawns CoreM computations, it is also encouraged to pass cancelTk.cancelledByCancelRequest from RequestContext into Core.Context (note that this needs lean4#12948).

v0.0.92

  • Renamed syntax categories for JSX to be unique to ProofWidgets4. They used to clash with doc-gen4.

v0.0.83

  • Added #checkh and #checkh' commands that are similar to #check but dim implicit arguments.

v0.0.77

  • Ported to the new module system.

v0.0.56

  • Added path/ellipse/rect/text primitives to Data.Svg.

v0.0.52

  • Added the errorOnBuild Lake configuration option.

v0.0.49

v0.0.47

  • Generalized GraphDisplay.Vertex.radius to GraphDisplay.Vertex.boundingShape.
  • Added demo of metavariable graph display in tactic proofs.

v0.0.46

  • Renamed DigraphDisplay to GraphDisplay. Undirected graphs can be rendered by turning off arrowheads.
  • Added support for edge labels and more customization to GraphDisplay.

v0.0.45

  • Updated Lean to v4.14.0-rc1.

v0.0.44

  • Added DigraphDisplay component. It uses d3-force for layout and can accommodate a variety of display styles. See Demos/Digraph.lean for more.
  • Added MarkdownDisplay component to display Markdown (including LaTeX).
  • Fixed cloud release issue (see Zulip).

v0.0.30

  • Moved the toolchain to leanprover/lean4:v4.7.0-rc1.
  • Performance improvements for widgets using mk_rpc_widget%. Redundant, duplicate calls were previously made to the underlying RPC method; this has been fixed. Furthermore, serverside execution of the RPC method gets cancelled by the infoview as long as its results are no longer needed (for example because the user moved the cursor elsewhere). To opt into this mechanism, use @[server_rpc_method_cancellable] instead of @[server_rpc_method]. RPC methods using that attribute can check whether they have been cancelled using IO.checkCanceled, and immediately return with an error or a partial result.

v0.0.29

  • Moved the toolchain to leanprover/lean4:v4.6.0.
  • Exposed theme.background to Penrose style programs.

v0.0.26 - v0.0.28

  • Toolchain bumps and associated tweaks.

v0.0.25

  • Build the demos in CI.

v0.0.24

  • Moved the toolchain to leanprover/lean4:v4.5.0-rc1. This brings changes to the user widget API described here.
  • Removed ProofWidgets.savePanelWidgetInfo. For now you should use Lean.Widget.savePanelWidgetInfo instead. An example migration can be found here.
  • The with_panel_widgets tactic now optionally accepts props for each listed widget.
  • Several components now use mk_rpc_widget% instead of JavaScript string literals.
  • Fixes and improvements in the PenroseDiagram component and the Euclidean demo.