leanprover-community · kim-em · Oct 21, 2025 · Sep 18, 2025 · Sep 18, 2025 · Sep 18, 2025
diff --git a/ProofWidgets/Cancellable.lean b/ProofWidgets/Cancellable.lean
@@ -1,7 +1,11 @@
-import Lean.Data.Json.FromToJson
-import Lean.Server.Rpc.RequestHandling
-import Std.Data.HashMap
-import ProofWidgets.Compat
+module
+
+public meta import Lean.Data.Json.FromToJson
+public meta import Lean.Server.Rpc.RequestHandling
+public meta import Std.Data.HashMap
+public meta import ProofWidgets.Compat
+
+public meta section
 
 /-! Experimental support for cancellable RPC requests.
 

diff --git a/ProofWidgets/Compat.lean b/ProofWidgets/Compat.lean
@@ -1,4 +1,8 @@
-import Lean.Elab.InfoTree.Main
+module
+
+public meta import Lean.Elab.InfoTree.Main
+
+public meta section
 
 namespace ProofWidgets
 open Lean Server Elab

diff --git a/ProofWidgets/Component/Basic.lean b/ProofWidgets/Component/Basic.lean
@@ -1,6 +1,10 @@
-import Lean.Widget.InteractiveCode
-import Lean.Widget.UserWidget
-import ProofWidgets.Compat
+module
+
+public meta import Lean.Widget.InteractiveCode
+public meta import Lean.Widget.UserWidget
+public meta import ProofWidgets.Compat
+
+public meta section
 
 namespace ProofWidgets
 open Lean

diff --git a/ProofWidgets/Component/FilterDetails.lean b/ProofWidgets/Component/FilterDetails.lean
@@ -1,4 +1,8 @@
-import ProofWidgets.Data.Html
+module
+
+public meta import ProofWidgets.Data.Html
+
+public meta section
 
 namespace ProofWidgets
 open Lean

diff --git a/ProofWidgets/Component/GraphDisplay.lean b/ProofWidgets/Component/GraphDisplay.lean
@@ -1,5 +1,9 @@
-import ProofWidgets.Component.Basic
-import ProofWidgets.Data.Html
+module
+
+public meta import ProofWidgets.Component.Basic
+public meta import ProofWidgets.Data.Html
+
+public meta section
 
 namespace ProofWidgets.GraphDisplay
 open Lean Server Jsx

diff --git a/ProofWidgets/Component/HtmlDisplay.lean b/ProofWidgets/Component/HtmlDisplay.lean
@@ -1,7 +1,11 @@
-import Lean.Server.Rpc.Basic
-import Lean.Elab.Command
+module
 
-import ProofWidgets.Data.Html
+public meta import Lean.Server.Rpc.Basic
+public meta import Lean.Elab.Command
+
+public meta import ProofWidgets.Data.Html
+
+public meta section
 
 namespace ProofWidgets
 open Lean Server

diff --git a/ProofWidgets/Component/InteractiveSvg.lean b/ProofWidgets/Component/InteractiveSvg.lean
@@ -1,4 +1,8 @@
-import ProofWidgets.Data.Svg
+module
+
+public meta import ProofWidgets.Data.Svg
+
+public meta section
 
 namespace ProofWidgets
 open Lean Std

diff --git a/ProofWidgets/Component/MakeEditLink.lean b/ProofWidgets/Component/MakeEditLink.lean
@@ -1,5 +1,9 @@
-import Lean.Server.Utils
-import ProofWidgets.Component.Basic
+module
+
+public meta import Lean.Server.Utils
+public meta import ProofWidgets.Component.Basic
+
+public meta section
 
 /-- Assuming that `s` is the content of a file starting at position `p`,
 advance `p` to the end of `s`. -/

diff --git a/ProofWidgets/Component/OfRpcMethod.lean b/ProofWidgets/Component/OfRpcMethod.lean
@@ -1,7 +1,11 @@
-import Lean.Elab.ElabRules
-import ProofWidgets.Component.Basic
-import ProofWidgets.Data.Html
-import ProofWidgets.Cancellable
+module
+
+public meta import Lean.Elab.ElabRules
+public meta import ProofWidgets.Component.Basic
+public meta import ProofWidgets.Data.Html
+public meta import ProofWidgets.Cancellable
+
+public meta section
 
 namespace ProofWidgets
 open Lean Server Meta Elab Term

diff --git a/ProofWidgets/Component/Panel/Basic.lean b/ProofWidgets/Component/Panel/Basic.lean
@@ -1,7 +1,11 @@
-import ProofWidgets.Compat
-import ProofWidgets.Component.Basic
-import Lean.Elab.Tactic
-import Lean.Widget.Commands
+module
+
+public meta import ProofWidgets.Compat
+public meta import ProofWidgets.Component.Basic
+public meta import Lean.Elab.Tactic
+public meta import Lean.Widget.Commands
+
+public meta section
 
 namespace ProofWidgets
 open Lean Elab Tactic

diff --git a/ProofWidgets/Component/Panel/GoalTypePanel.lean b/ProofWidgets/Component/Panel/GoalTypePanel.lean
@@ -1,4 +1,8 @@
-import ProofWidgets.Component.Panel.Basic
+module
+
+public meta import ProofWidgets.Component.Panel.Basic
+
+public meta section
 
 namespace ProofWidgets
 

diff --git a/ProofWidgets/Component/Panel/SelectionPanel.lean b/ProofWidgets/Component/Panel/SelectionPanel.lean
@@ -1,6 +1,10 @@
-import Lean.Meta.ExprLens
-import ProofWidgets.Component.Panel.Basic
-import ProofWidgets.Presentation.Expr -- Needed for RPC calls in SelectionPanel
+module
+
+public meta import Lean.Meta.ExprLens
+public meta import ProofWidgets.Component.Panel.Basic
+public meta import ProofWidgets.Presentation.Expr
+
+public meta section -- Needed for RPC calls in SelectionPanel
 
 open ProofWidgets in
 /-- Save the expression corresponding to a goals location. -/

diff --git a/ProofWidgets/Component/PenroseDiagram.lean b/ProofWidgets/Component/PenroseDiagram.lean
@@ -1,6 +1,10 @@
-import ProofWidgets.Component.Basic
-import ProofWidgets.Data.Html
-import Std.Data.HashMap
+module
+
+public meta import ProofWidgets.Component.Basic
+public meta import ProofWidgets.Data.Html
+public meta import Std.Data.HashMap
+
+public meta section
 
 namespace ProofWidgets.Penrose
 open Lean Server Std

diff --git a/ProofWidgets/Component/Recharts.lean b/ProofWidgets/Component/Recharts.lean
@@ -1,4 +1,8 @@
-import ProofWidgets.Component.Basic
+module
+
+public meta import ProofWidgets.Component.Basic
+
+public meta section
 
 namespace ProofWidgets.Recharts
 open Lean

diff --git a/ProofWidgets/Data/Html.lean b/ProofWidgets/Data/Html.lean
@@ -3,13 +3,17 @@
  Released under Apache 2.0 license as described in the file LICENSE.
  Authors: Wojciech Nawrocki, Sebastian Ullrich, Eric Wieser
  -/
-import Lean.Data.Json.FromToJson
-import Lean.Parser
-import Lean.PrettyPrinter.Delaborator.Basic
-import Lean.Server.Rpc.Basic
+module
 
-import ProofWidgets.Component.Basic
-import ProofWidgets.Util
+public meta import Lean.Data.Json.FromToJson
+public meta import Lean.Parser
+public meta import Lean.PrettyPrinter.Delaborator.Basic
+public meta import Lean.Server.Rpc.Basic
+
+public meta import ProofWidgets.Component.Basic
+public meta import ProofWidgets.Util
+
+public meta section
 
 /-! We define a representation of HTML trees together with a JSX-like DSL for writing them. -/
 

diff --git a/ProofWidgets/Data/Svg.lean b/ProofWidgets/Data/Svg.lean
@@ -1,5 +1,9 @@
-import ProofWidgets.Data.Html
-import Std.Data.HashMap
+module
+
+public meta import ProofWidgets.Data.Html
+public meta import Std.Data.HashMap
+
+public meta section
 
 namespace ProofWidgets
 open Lean Std

diff --git a/ProofWidgets/Demos/Dynkin.lean b/ProofWidgets/Demos/Dynkin.lean
@@ -1,4 +1,8 @@
-import ProofWidgets.Component.HtmlDisplay
+module
+
+public meta import ProofWidgets.Component.HtmlDisplay
+
+public meta section
 
 /-! Ported from Lean 3 code by Oliver Nash:
 https://gist.github.com/ocfnash/fb61a17d0f1598edcc752999f17b70c6 -/
@@ -7,7 +11,7 @@ def List.product : List α → List β → List (α × β)
   | [], _     => []
   | a::as, bs => bs.map ((a, ·)) ++ as.product bs
 
-def Matrix (n m α : Type) := n → m → α
+@[expose] def Matrix (n m α : Type) := n → m → α
 
 namespace Matrix
 

diff --git a/ProofWidgets/Demos/Euclidean.lean b/ProofWidgets/Demos/Euclidean.lean
@@ -3,13 +3,16 @@
  Released under Apache 2.0 license as described in the file LICENSE.
  Authors: Vladimir Sedlacek, Wojciech Nawrocki
  -/
+module
 
-import Lean.Elab.Tactic
-import ProofWidgets.Component.PenroseDiagram
-import ProofWidgets.Component.HtmlDisplay
-import ProofWidgets.Component.Panel.Basic
-import ProofWidgets.Component.OfRpcMethod
-import ProofWidgets.Component.MakeEditLink
+public meta import Lean.Elab.Tactic
+public meta import ProofWidgets.Component.PenroseDiagram
+public meta import ProofWidgets.Component.HtmlDisplay
+public meta import ProofWidgets.Component.Panel.Basic
+public meta import ProofWidgets.Component.OfRpcMethod
+public meta import ProofWidgets.Component.MakeEditLink
+
+public meta section
 
 /-! A widget to display Euclidean geometry diagrams,
 and another one to make geometric constructions in the UI. -/

diff --git a/ProofWidgets/Demos/ExprPresentation.lean b/ProofWidgets/Demos/ExprPresentation.lean
@@ -1,5 +1,9 @@
-import ProofWidgets.Component.Panel.SelectionPanel
-import ProofWidgets.Component.Panel.GoalTypePanel
+module
+
+public meta import ProofWidgets.Component.Panel.SelectionPanel
+public meta import ProofWidgets.Component.Panel.GoalTypePanel
+
+public meta section
 
 open ProofWidgets Jsx
 

diff --git a/ProofWidgets/Demos/Graph/Basic.lean b/ProofWidgets/Demos/Graph/Basic.lean
@@ -1,5 +1,9 @@
-import ProofWidgets.Component.GraphDisplay
-import ProofWidgets.Component.HtmlDisplay
+module
+
+public meta import ProofWidgets.Component.GraphDisplay
+public meta import ProofWidgets.Component.HtmlDisplay
+
+public meta section
 
 /-! ## Directed graphs with `GraphDisplay` -/
 

diff --git a/ProofWidgets/Demos/Graph/ExprGraph.lean b/ProofWidgets/Demos/Graph/ExprGraph.lean
@@ -1,6 +1,10 @@
-import ProofWidgets.Component.GraphDisplay
-import ProofWidgets.Component.HtmlDisplay
-import Lean.Util.FoldConsts
+module
+
+public meta import ProofWidgets.Component.GraphDisplay
+public meta import ProofWidgets.Component.HtmlDisplay
+public meta import Lean.Util.FoldConsts
+
+public meta section
 
 open ProofWidgets Jsx
 

diff --git a/ProofWidgets/Demos/Graph/MVarGraph.lean b/ProofWidgets/Demos/Graph/MVarGraph.lean
@@ -1,6 +1,10 @@
-import ProofWidgets.Component.GraphDisplay
-import ProofWidgets.Component.Panel.Basic
-import ProofWidgets.Component.OfRpcMethod
+module
+
+public meta import ProofWidgets.Component.GraphDisplay
+public meta import ProofWidgets.Component.Panel.Basic
+public meta import ProofWidgets.Component.OfRpcMethod
+
+public meta section
 
 /-! This demo visualizes the graph of metavariable assignments in tactic proofs. -/
 

diff --git a/ProofWidgets/Demos/InteractiveSvg.lean b/ProofWidgets/Demos/InteractiveSvg.lean
@@ -1,5 +1,9 @@
-import ProofWidgets.Component.InteractiveSvg
-import ProofWidgets.Component.HtmlDisplay
+module
+
+public meta import ProofWidgets.Component.InteractiveSvg
+public meta import ProofWidgets.Component.HtmlDisplay
+
+public meta section
 
 open Lean
 open ProofWidgets Svg Jsx

diff --git a/ProofWidgets/Demos/Jsx.lean b/ProofWidgets/Demos/Jsx.lean
@@ -1,4 +1,8 @@
-import ProofWidgets.Component.HtmlDisplay
+module
+
+public meta import ProofWidgets.Component.HtmlDisplay
+
+public meta section
 
 -- The `ProofWidgets.Jsx` namespace provides JSX-like notation for HTML
 open scoped ProofWidgets.Jsx

diff --git a/ProofWidgets/Demos/LazyComputation.lean b/ProofWidgets/Demos/LazyComputation.lean
@@ -1,4 +1,8 @@
-import ProofWidgets.Component.Basic
+module
+
+public meta import ProofWidgets.Component.Basic
+
+public meta section
 
 open ProofWidgets
 open Lean Meta Server Elab Tactic

diff --git a/ProofWidgets/Demos/Macro.lean b/ProofWidgets/Demos/Macro.lean
@@ -1,4 +1,8 @@
-import ProofWidgets.Component.HtmlDisplay
+module
+
+public meta import ProofWidgets.Component.HtmlDisplay
+
+public meta section
 
 -- See the `Jsx.lean` demo for more about JSX.
 open scoped ProofWidgets.Jsx

diff --git a/ProofWidgets/Demos/Plot.lean b/ProofWidgets/Demos/Plot.lean
@@ -1,5 +1,9 @@
-import ProofWidgets.Component.HtmlDisplay
-import ProofWidgets.Component.Recharts
+module
+
+public meta import ProofWidgets.Component.HtmlDisplay
+public meta import ProofWidgets.Component.Recharts
+
+public meta section
 
 open Lean ProofWidgets Recharts
 

diff --git a/ProofWidgets/Demos/RbTree.lean b/ProofWidgets/Demos/RbTree.lean
@@ -1,5 +1,9 @@
-import ProofWidgets.Presentation.Expr
-import ProofWidgets.Component.Panel.SelectionPanel
+module
+
+public meta import ProofWidgets.Presentation.Expr
+public meta import ProofWidgets.Component.Panel.SelectionPanel
+
+public meta section
 
 /-! ## References:
 - Chris Okasaki. "Functional Pearls: Red-Black Trees in a Functional Setting". 1993 -/

diff --git a/ProofWidgets/Demos/Rubiks.lean b/ProofWidgets/Demos/Rubiks.lean
@@ -1,4 +1,8 @@
-import ProofWidgets.Component.HtmlDisplay
+module
+
+public meta import ProofWidgets.Component.HtmlDisplay
+
+public meta section
 
 open Lean ProofWidgets
 open scoped ProofWidgets.Jsx