Skip to content

Commit 909febc

Browse files
kim-emkim-em
authored
Merge pull request #34 from leanprover-community/bump_rc2
chore: bump lean to `v4.3.0-rc2`
2 parents c3b9f0d + b8faaff commit 909febc

22 files changed

+39
-40
lines changed

‎.github/workflows/build.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ jobs:
6565
# All our runners are 64-bit ¯\_(ツ)_/¯
6666
run: |
6767
export COPYFILE_DISABLE=true
68-
tar -c -z -f ./${LEAN_OS}-64.tar.gz -C ./build .
68+
tar -c -z -f ./${LEAN_OS}-64.tar.gz -C ./.lake/build .
6969
gh release upload ${RELEASE_TAG} ./${LEAN_OS}-64.tar.gz
7070
env:
7171
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

‎.gitignore

+2-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
1-
/build
2-
/lake-packages/*
1+
/.lake
32
# JavaScript build artefacts.
43
/widget/dist
54
/widget/node_modules
6-
lakefile.olean
5+
/widget/*.hash

‎ProofWidgets/Compat.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ def getPanelWidgets (args : GetPanelWidgetsParams) : RequestM (RequestTask GetPa
171171
def metaWidget : Lean.Widget.UserWidgetDefinition where
172172
-- The header is sometimes briefly visible before compat.tsx loads and hides it
173173
name := "Loading ProofWidgets.."
174-
javascript := include_str ".." / "build" / "js" / "compat.js"
174+
javascript := include_str ".." / ".lake" / "build" / "js" / "compat.js"
175175

176176
open scoped Json in
177177
/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.

‎ProofWidgets/Component/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,6 @@ preferrable to use the eager `InteractiveCode` in order to avoid the extra clien
6565
needed for the pretty-printing RPC call. -/
6666
@[widget_module]
6767
def InteractiveExpr : Component InteractiveExprProps where
68-
javascript := include_str ".." / ".." / "build" / "js" / "interactiveExpr.js"
68+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "interactiveExpr.js"
6969

7070
end ProofWidgets

‎ProofWidgets/Component/HtmlDisplay.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,11 @@ structure HtmlDisplayProps where
1212

1313
@[widget_module]
1414
def HtmlDisplay : Component HtmlDisplayProps where
15-
javascript := include_str ".." / ".." / "build" / "js" / "htmlDisplay.js"
15+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "htmlDisplay.js"
1616

1717
@[widget_module]
1818
def HtmlDisplayPanel : Component HtmlDisplayProps where
19-
javascript := include_str ".." / ".." / "build" / "js" / "htmlDisplayPanel.js"
19+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "htmlDisplayPanel.js"
2020

2121
open Elab in
2222
unsafe def evalHtmlUnsafe (stx : Term) : TermElabM Html := do

‎ProofWidgets/Component/MakeEditLink.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,6 @@ and potentially moves the cursor
5959
or makes a selection. -/
6060
@[widget_module]
6161
def MakeEditLink : Component MakeEditLinkProps where
62-
javascript := include_str ".." / ".." / "build" / "js" / "makeEditLink.js"
62+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "makeEditLink.js"
6363

6464
end ProofWidgets

‎ProofWidgets/Component/OfRpcMethod.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ import ProofWidgets.Data.Html
55
namespace ProofWidgets
66
open Lean Server Meta Elab Term
77

8-
def ofRpcMethodTemplate := include_str ".." / ".." / "build" / "js" / "ofRpcMethod.js"
8+
def ofRpcMethodTemplate := include_str ".." / ".." / ".lake" / "build" / "js" / "ofRpcMethod.js"
99

1010
/-- The elaborator `mk_rpc_widget%` allows writing certain widgets in Lean instead of JavaScript.
1111
Specifically, it translates an RPC method of type `MyProps → RequestM (RequestTask Html)`

‎ProofWidgets/Component/Panel/GoalTypePanel.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ namespace ProofWidgets
55
/-- Display the goal type using known `Expr` presenters. -/
66
@[widget_module]
77
def GoalTypePanel : Component PanelWidgetProps where
8-
javascript := include_str ".." / ".." / ".." / "build" / "js" / "goalTypePanel.js"
8+
javascript := include_str ".." / ".." / ".." / ".lake" / "build" / "js" / "goalTypePanel.js"
99

1010
end ProofWidgets

‎ProofWidgets/Component/Panel/SelectionPanel.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,6 @@ presenter should be used to display each of those expressions.
5050
Expressions can be selected using shift-click. -/
5151
@[widget_module]
5252
def SelectionPanel : Component PanelWidgetProps where
53-
javascript := include_str ".." / ".." / ".." / "build" / "js" / "presentSelection.js"
53+
javascript := include_str ".." / ".." / ".." / ".lake" / "build" / "js" / "presentSelection.js"
5454

5555
end ProofWidgets

‎ProofWidgets/Component/PenroseDiagram.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,6 @@ and can be accessed as, for example, `theme.foreground` in the provided `sty` in
3535
the editor theme. -/
3636
@[widget_module]
3737
def PenroseDiagram : Component PenroseDiagramProps where
38-
javascript := include_str ".." / ".." / "build" / "js" / "penroseDisplay.js"
38+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "penroseDisplay.js"
3939

4040
end ProofWidgets

‎ProofWidgets/Component/Recharts.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ open Lean
55

66
@[widget_module]
77
def Recharts : Module where
8-
javascript := include_str "../../build/js/recharts.js"
8+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "recharts.js"
99

1010
inductive LineChartLayout where
1111
| horizontal

‎ProofWidgets/Demos/InteractiveSvg.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ def updateSvg (params : UpdateParams State) : RequestM (RequestTask (UpdateResul
4646
-- TODO: the tsx file is pretty broken
4747
@[widget_module]
4848
def SvgWidget : Component (UpdateResult State) where
49-
javascript := include_str ".." / ".." / "build" / "js" / "interactiveSvg.js"
49+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "interactiveSvg.js"
5050

5151
def init : UpdateResult State := {
5252
html := <div>Init!!!</div>,

‎ProofWidgets/Demos/Plot.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ structure AnimatedHtmlProps where
3939

4040
@[widget_module]
4141
def AnimatedHtml : Component AnimatedHtmlProps where
42-
javascript := include_str ".." / ".." / "build" / "js" / "animatedHtml.js"
42+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "animatedHtml.js"
4343

4444
open scoped ProofWidgets.Jsx in
4545
-- put your cursor on the below line to see an animated widget

‎ProofWidgets/Demos/RbTree.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ open ProofWidgets
100100

101101
@[widget_module]
102102
def RBDisplay : Component RBDisplayProps where
103-
javascript := include_str ".." / ".." / "build" / "js" / "rbTree.js"
103+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "rbTree.js"
104104

105105
open scoped Jsx in
106106
partial def drawTree? (e : Expr) : MetaM (Option Html) := do

‎ProofWidgets/Demos/Rubiks.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ structure RubiksProps where
99

1010
@[widget_module]
1111
def Rubiks : Component RubiksProps where
12-
javascript := include_str ".." / ".." / "build" / "js" / "rubiks.js"
12+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "rubiks.js"
1313

1414
def eg := #["L", "L", "D⁻¹", "U⁻¹", "L", "D", "D", "L", "U⁻¹", "R", "D", "F", "F", "D"]
1515

‎ProofWidgets/Presentation/Expr.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,6 @@ are used to render the expression when selected. The one with highest precedence
107107
default. -/
108108
@[widget_module]
109109
def ExprPresentation : Component ExprPresentationProps where
110-
javascript := include_str ".." / ".." / "build" / "js" / "exprPresentation.js"
110+
javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "exprPresentation.js"
111111

112112
end ProofWidgets

‎README.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -74,9 +74,9 @@ Outputs of `npm` commands are not always shown by default: use `lake build -v [t
7474
If this happens, run `npm clean-install` in the `widget/` directory and then try `lake build` again.
7575

7676
⚠️ We use the `include_str` term elaborator to splice the JavaScript produced by `tsc` into our Lean
77-
files. The JS is stored in `build/js/`. Note however that due to Lake issue [#86](https://github.com/leanprover/lake/issues/86),
77+
files. The JS is stored in `.lake/build/js/`. Note however that due to Lake issue [#86](https://github.com/leanprover/lake/issues/86),
7878
rebuilding the `.js` will *not* rebuild the Lean file that includes it. To ensure freshness you may
79-
have to resort to hacks such as removing `build/lib/` (this contains the `.olean`s) or adding a
79+
have to resort to hacks such as removing `.lake/build/lib/` (this contains the `.olean`s) or adding a
8080
random comment in the Lean file that uses `include_str` in order to ensure it gets rebuilt.
8181
Alternatively, you can run `lake clean` to delete the entire build directory.
8282

‎lake-manifest.json

+13-11
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,14 @@
1-
{"version": 6,
2-
"packagesDir": "lake-packages",
1+
{"version": 7,
2+
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"git":
5-
{"url": "https://github.com/leanprover/std4",
6-
"subDir?": null,
7-
"rev": "f91a64c789426debe48827ae6ef9efc8fa96bfcc",
8-
"opts": {},
9-
"name": "std",
10-
"inputRev?": "main",
11-
"inherited": false}}],
12-
"name": "proofwidgets"}
4+
[{"url": "https://github.com/leanprover/std4",
5+
"type": "git",
6+
"subDir": null,
7+
"rev": "d3049643f6dded69eb7ce8124796cb1ec8df8840",
8+
"name": "std",
9+
"manifestFile": "lake-manifest.json",
10+
"inputRev": "main",
11+
"inherited": false,
12+
"configFile": "lakefile.lean"}],
13+
"name": "proofwidgets",
14+
"lakeDir": ".lake"}

‎lakefile.lean

+3-5
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,10 @@
11
import Lake
22
open Lake DSL System
33

4-
package proofwidgets {
4+
package proofwidgets where
55
preferReleaseBuild := true
6-
buildDir := "build"
7-
}
86

9-
lean_lib ProofWidgets {}
7+
lean_lib ProofWidgets
108

119
require std from git "https://github.com/leanprover/std4" @ "main"
1210

@@ -26,7 +24,7 @@ target widgetPackageLock : FilePath := do
2624
cwd := some widgetDir
2725
}
2826

29-
/-- Target to build `build/js/foo.js` from a `widget/src/foo.tsx` widget module.
27+
/-- Target to build `.lake/build/js/foo.js` from a `widget/src/foo.tsx` widget module.
3028
Rebuilds whenever the `.tsx` source, or any part of the build configuration, has changed. -/
3129
def widgetTsxTarget (pkg : NPackage _package.name) (nodeModulesMutex : IO.Mutex Bool)
3230
(tsxName : String) (deps : Array (BuildJob FilePath)) (isDev : Bool) :

‎lean-toolchain

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:nightly-2023-10-12
1+
leanprover/lean4:v4.3.0-rc2

‎widget/rollup.config.js

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ export default cliArgs => {
1919
const configForInput = fname => ({
2020
input: fname,
2121
output: {
22-
dir: '../build/js',
22+
dir: '../.lake/build/js',
2323
format: 'es',
2424
// Hax: apparently setting `global` makes some CommonJS modules work ¯\_(ツ)_/¯
2525
intro: 'const global = window;',

‎widget/tsconfig.json

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"module": "esnext",
66
"moduleResolution": "node",
77
"sourceMap": false,
8-
"outDir": "../build/js",
8+
"outDir": "../.lake/build/js",
99
"allowSyntheticDefaultImports": true,
1010
"esModuleInterop": true,
1111
"forceConsistentCasingInFileNames": true,

0 commit comments

Comments
 (0)