chore: bump lean to v4.3.0-rc2

leanprover-community · Nov 19, 2023 · b8faaff · b8faaff
1 parent c3b9f0d
commit b8faaff
Show file tree

Hide file tree

Showing 22 changed files with 39 additions and 40 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 := <div>Init!!!</div>,

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -5,7 +5,7 @@
     "module": "esnext",
     "moduleResolution": "node",
     "sourceMap": false,
-    "outDir": "../build/js",
+    "outDir": "../.lake/build/js",
     "allowSyntheticDefaultImports": true,
     "esModuleInterop": true,
     "forceConsistentCasingInFileNames": true,