From b8faaffcf9e112a7728d0f579fc228727ceb6e2f Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 19 Nov 2023 01:04:22 -0500 Subject: [PATCH] chore: bump lean to `v4.3.0-rc2` --- .github/workflows/build.yml | 2 +- .gitignore | 5 ++-- ProofWidgets/Compat.lean | 2 +- ProofWidgets/Component/Basic.lean | 2 +- ProofWidgets/Component/HtmlDisplay.lean | 4 ++-- ProofWidgets/Component/MakeEditLink.lean | 2 +- ProofWidgets/Component/OfRpcMethod.lean | 2 +- .../Component/Panel/GoalTypePanel.lean | 2 +- .../Component/Panel/SelectionPanel.lean | 2 +- ProofWidgets/Component/PenroseDiagram.lean | 2 +- ProofWidgets/Component/Recharts.lean | 2 +- ProofWidgets/Demos/InteractiveSvg.lean | 2 +- ProofWidgets/Demos/Plot.lean | 2 +- ProofWidgets/Demos/RbTree.lean | 2 +- ProofWidgets/Demos/Rubiks.lean | 2 +- ProofWidgets/Presentation/Expr.lean | 2 +- README.md | 4 ++-- lake-manifest.json | 24 ++++++++++--------- lakefile.lean | 8 +++---- lean-toolchain | 2 +- widget/rollup.config.js | 2 +- widget/tsconfig.json | 2 +- 22 files changed, 39 insertions(+), 40 deletions(-) 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 :=
Init!!!
, diff --git a/ProofWidgets/Demos/Plot.lean b/ProofWidgets/Demos/Plot.lean index ae87a19..6cc13e9 100644 --- a/ProofWidgets/Demos/Plot.lean +++ b/ProofWidgets/Demos/Plot.lean @@ -39,7 +39,7 @@ structure AnimatedHtmlProps where @[widget_module] def AnimatedHtml : Component AnimatedHtmlProps where - javascript := include_str ".." / ".." / "build" / "js" / "animatedHtml.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "animatedHtml.js" open scoped ProofWidgets.Jsx in -- put your cursor on the below line to see an animated widget diff --git a/ProofWidgets/Demos/RbTree.lean b/ProofWidgets/Demos/RbTree.lean index 81a4d8b..ace306c 100644 --- a/ProofWidgets/Demos/RbTree.lean +++ b/ProofWidgets/Demos/RbTree.lean @@ -100,7 +100,7 @@ open ProofWidgets @[widget_module] def RBDisplay : Component RBDisplayProps where - javascript := include_str ".." / ".." / "build" / "js" / "rbTree.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "rbTree.js" open scoped Jsx in partial def drawTree? (e : Expr) : MetaM (Option Html) := do diff --git a/ProofWidgets/Demos/Rubiks.lean b/ProofWidgets/Demos/Rubiks.lean index 342aa52..817cff4 100644 --- a/ProofWidgets/Demos/Rubiks.lean +++ b/ProofWidgets/Demos/Rubiks.lean @@ -9,7 +9,7 @@ structure RubiksProps where @[widget_module] def Rubiks : Component RubiksProps where - javascript := include_str ".." / ".." / "build" / "js" / "rubiks.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "rubiks.js" def eg := #["L", "L", "D⁻¹", "U⁻¹", "L", "D", "D", "L", "U⁻¹", "R", "D", "F", "F", "D"] diff --git a/ProofWidgets/Presentation/Expr.lean b/ProofWidgets/Presentation/Expr.lean index 0eb8927..2ed0b7d 100644 --- a/ProofWidgets/Presentation/Expr.lean +++ b/ProofWidgets/Presentation/Expr.lean @@ -107,6 +107,6 @@ are used to render the expression when selected. The one with highest precedence default. -/ @[widget_module] def ExprPresentation : Component ExprPresentationProps where - javascript := include_str ".." / ".." / "build" / "js" / "exprPresentation.js" + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "exprPresentation.js" end ProofWidgets diff --git a/README.md b/README.md index 66c6d81..8a93462 100644 --- a/README.md +++ b/README.md @@ -74,9 +74,9 @@ Outputs of `npm` commands are not always shown by default: use `lake build -v [t If this happens, run `npm clean-install` in the `widget/` directory and then try `lake build` again. ⚠️ We use the `include_str` term elaborator to splice the JavaScript produced by `tsc` into our Lean -files. The JS is stored in `build/js/`. Note however that due to Lake issue [#86](https://github.com/leanprover/lake/issues/86), +files. The JS is stored in `.lake/build/js/`. Note however that due to Lake issue [#86](https://github.com/leanprover/lake/issues/86), rebuilding the `.js` will *not* rebuild the Lean file that includes it. To ensure freshness you may -have to resort to hacks such as removing `build/lib/` (this contains the `.olean`s) or adding a +have to resort to hacks such as removing `.lake/build/lib/` (this contains the `.olean`s) or adding a random comment in the Lean file that uses `include_str` in order to ensure it gets rebuilt. Alternatively, you can run `lake clean` to delete the entire build directory. diff --git a/lake-manifest.json b/lake-manifest.json index d546ca1..6cc7d27 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,12 +1,14 @@ -{"version": 6, - "packagesDir": "lake-packages", +{"version": 7, + "packagesDir": ".lake/packages", "packages": - [{"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "f91a64c789426debe48827ae6ef9efc8fa96bfcc", - "opts": {}, - "name": "std", - "inputRev?": "main", - "inherited": false}}], - "name": "proofwidgets"} + [{"url": "https://github.com/leanprover/std4", + "type": "git", + "subDir": null, + "rev": "d3049643f6dded69eb7ce8124796cb1ec8df8840", + "name": "std", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "proofwidgets", + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 9b590ae..411a0a3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,12 +1,10 @@ import Lake open Lake DSL System -package proofwidgets { +package proofwidgets where preferReleaseBuild := true - buildDir := "build" -} -lean_lib ProofWidgets {} +lean_lib ProofWidgets require std from git "https://github.com/leanprover/std4" @ "main" @@ -26,7 +24,7 @@ target widgetPackageLock : FilePath := do cwd := some widgetDir } -/-- Target to build `build/js/foo.js` from a `widget/src/foo.tsx` widget module. +/-- Target to build `.lake/build/js/foo.js` from a `widget/src/foo.tsx` widget module. Rebuilds whenever the `.tsx` source, or any part of the build configuration, has changed. -/ def widgetTsxTarget (pkg : NPackage _package.name) (nodeModulesMutex : IO.Mutex Bool) (tsxName : String) (deps : Array (BuildJob FilePath)) (isDev : Bool) : diff --git a/lean-toolchain b/lean-toolchain index 1e9ed23..24a3cdb 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-10-12 +leanprover/lean4:v4.3.0-rc2 diff --git a/widget/rollup.config.js b/widget/rollup.config.js index 07d4432..550eadb 100644 --- a/widget/rollup.config.js +++ b/widget/rollup.config.js @@ -19,7 +19,7 @@ export default cliArgs => { const configForInput = fname => ({ input: fname, output: { - dir: '../build/js', + dir: '../.lake/build/js', format: 'es', // Hax: apparently setting `global` makes some CommonJS modules work ¯\_(ツ)_/¯ intro: 'const global = window;', diff --git a/widget/tsconfig.json b/widget/tsconfig.json index b48d520..9cecb5f 100644 --- a/widget/tsconfig.json +++ b/widget/tsconfig.json @@ -5,7 +5,7 @@ "module": "esnext", "moduleResolution": "node", "sourceMap": false, - "outDir": "../build/js", + "outDir": "../.lake/build/js", "allowSyntheticDefaultImports": true, "esModuleInterop": true, "forceConsistentCasingInFileNames": true,