diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 106271a..e52ef01 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -65,7 +65,7 @@ jobs: # All our runners are 64-bit ¯\_(ツ)_/¯ run: | export COPYFILE_DISABLE=true - tar -c -z -f ./${LEAN_OS}-64.tar.gz -C ./build . + tar -c -z -f ./${LEAN_OS}-64.tar.gz -C ./.lake/build . gh release upload ${RELEASE_TAG} ./${LEAN_OS}-64.tar.gz env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.gitignore b/.gitignore index e632605..1ca50cc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,5 @@ -/build -/lake-packages/* +/.lake # JavaScript build artefacts. /widget/dist /widget/node_modules -lakefile.olean +/widget/*.hash diff --git a/ProofWidgets/Compat.lean b/ProofWidgets/Compat.lean index b8da154..78f59c1 100644 --- a/ProofWidgets/Compat.lean +++ b/ProofWidgets/Compat.lean @@ -171,7 +171,7 @@ def getPanelWidgets (args : GetPanelWidgetsParams) : RequestM (RequestTask GetPa def metaWidget : Lean.Widget.UserWidgetDefinition where -- The header is sometimes briefly visible before compat.tsx loads and hides it name := "Loading ProofWidgets.." - javascript := include_str ".." / "build" / "js" / "compat.js" + javascript := include_str ".." / ".lake" / "build" / "js" / "compat.js" open scoped Json in /-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`. diff --git a/ProofWidgets/Component/Basic.lean b/ProofWidgets/Component/Basic.lean index 320e730..5aa30ed 100644 --- a/ProofWidgets/Component/Basic.lean +++ b/ProofWidgets/Component/Basic.lean @@ -65,6 +65,6 @@ preferrable to use the eager `InteractiveCode` in order to avoid the extra clien needed for the pretty-printing RPC call. -/ @[widget_module] def InteractiveExpr : Component InteractiveExprProps where - javascript := include_str ".." / ".." / "build" / "js" / "interactiveExpr.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "interactiveExpr.js" end ProofWidgets diff --git a/ProofWidgets/Component/HtmlDisplay.lean b/ProofWidgets/Component/HtmlDisplay.lean index 4842481..595eece 100644 --- a/ProofWidgets/Component/HtmlDisplay.lean +++ b/ProofWidgets/Component/HtmlDisplay.lean @@ -12,11 +12,11 @@ structure HtmlDisplayProps where @[widget_module] def HtmlDisplay : Component HtmlDisplayProps where - javascript := include_str ".." / ".." / "build" / "js" / "htmlDisplay.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "htmlDisplay.js" @[widget_module] def HtmlDisplayPanel : Component HtmlDisplayProps where - javascript := include_str ".." / ".." / "build" / "js" / "htmlDisplayPanel.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "htmlDisplayPanel.js" open Elab in unsafe def evalHtmlUnsafe (stx : Term) : TermElabM Html := do diff --git a/ProofWidgets/Component/MakeEditLink.lean b/ProofWidgets/Component/MakeEditLink.lean index 349190a..6170bef 100644 --- a/ProofWidgets/Component/MakeEditLink.lean +++ b/ProofWidgets/Component/MakeEditLink.lean @@ -59,6 +59,6 @@ and potentially moves the cursor or makes a selection. -/ @[widget_module] def MakeEditLink : Component MakeEditLinkProps where - javascript := include_str ".." / ".." / "build" / "js" / "makeEditLink.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "makeEditLink.js" end ProofWidgets diff --git a/ProofWidgets/Component/OfRpcMethod.lean b/ProofWidgets/Component/OfRpcMethod.lean index a5b087c..ca34501 100644 --- a/ProofWidgets/Component/OfRpcMethod.lean +++ b/ProofWidgets/Component/OfRpcMethod.lean @@ -5,7 +5,7 @@ import ProofWidgets.Data.Html namespace ProofWidgets open Lean Server Meta Elab Term -def ofRpcMethodTemplate := include_str ".." / ".." / "build" / "js" / "ofRpcMethod.js" +def ofRpcMethodTemplate := include_str ".." / ".." / ".lake" / "build" / "js" / "ofRpcMethod.js" /-- The elaborator `mk_rpc_widget%` allows writing certain widgets in Lean instead of JavaScript. Specifically, it translates an RPC method of type `MyProps → RequestM (RequestTask Html)` diff --git a/ProofWidgets/Component/Panel/GoalTypePanel.lean b/ProofWidgets/Component/Panel/GoalTypePanel.lean index 4a760a4..d23a16e 100644 --- a/ProofWidgets/Component/Panel/GoalTypePanel.lean +++ b/ProofWidgets/Component/Panel/GoalTypePanel.lean @@ -5,6 +5,6 @@ namespace ProofWidgets /-- Display the goal type using known `Expr` presenters. -/ @[widget_module] def GoalTypePanel : Component PanelWidgetProps where - javascript := include_str ".." / ".." / ".." / "build" / "js" / "goalTypePanel.js" + javascript := include_str ".." / ".." / ".." / ".lake" / "build" / "js" / "goalTypePanel.js" end ProofWidgets diff --git a/ProofWidgets/Component/Panel/SelectionPanel.lean b/ProofWidgets/Component/Panel/SelectionPanel.lean index 3c611f4..fff0314 100644 --- a/ProofWidgets/Component/Panel/SelectionPanel.lean +++ b/ProofWidgets/Component/Panel/SelectionPanel.lean @@ -50,6 +50,6 @@ presenter should be used to display each of those expressions. Expressions can be selected using shift-click. -/ @[widget_module] def SelectionPanel : Component PanelWidgetProps where - javascript := include_str ".." / ".." / ".." / "build" / "js" / "presentSelection.js" + javascript := include_str ".." / ".." / ".." / ".lake" / "build" / "js" / "presentSelection.js" end ProofWidgets diff --git a/ProofWidgets/Component/PenroseDiagram.lean b/ProofWidgets/Component/PenroseDiagram.lean index 2091c48..f7083f6 100644 --- a/ProofWidgets/Component/PenroseDiagram.lean +++ b/ProofWidgets/Component/PenroseDiagram.lean @@ -35,6 +35,6 @@ and can be accessed as, for example, `theme.foreground` in the provided `sty` in the editor theme. -/ @[widget_module] def PenroseDiagram : Component PenroseDiagramProps where - javascript := include_str ".." / ".." / "build" / "js" / "penroseDisplay.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "penroseDisplay.js" end ProofWidgets diff --git a/ProofWidgets/Component/Recharts.lean b/ProofWidgets/Component/Recharts.lean index 8dd78ab..00494b0 100644 --- a/ProofWidgets/Component/Recharts.lean +++ b/ProofWidgets/Component/Recharts.lean @@ -5,7 +5,7 @@ open Lean @[widget_module] def Recharts : Module where - javascript := include_str "../../build/js/recharts.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "recharts.js" inductive LineChartLayout where | horizontal diff --git a/ProofWidgets/Demos/InteractiveSvg.lean b/ProofWidgets/Demos/InteractiveSvg.lean index da76d17..00426c9 100644 --- a/ProofWidgets/Demos/InteractiveSvg.lean +++ b/ProofWidgets/Demos/InteractiveSvg.lean @@ -46,7 +46,7 @@ def updateSvg (params : UpdateParams State) : RequestM (RequestTask (UpdateResul -- TODO: the tsx file is pretty broken @[widget_module] def SvgWidget : Component (UpdateResult State) where - javascript := include_str ".." / ".." / "build" / "js" / "interactiveSvg.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "interactiveSvg.js" def init : UpdateResult State := { html :=