Skip to content

Commit

Permalink
Merge pull request #34 from leanprover-community/bump_rc2
Browse files Browse the repository at this point in the history
chore: bump lean to `v4.3.0-rc2`
  • Loading branch information
kim-em authored Nov 20, 2023
2 parents c3b9f0d + b8faaff commit 909febc
Show file tree
Hide file tree
Showing 22 changed files with 39 additions and 40 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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 }}
Expand Down
5 changes: 2 additions & 3 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
/build
/lake-packages/*
/.lake
# JavaScript build artefacts.
/widget/dist
/widget/node_modules
lakefile.olean
/widget/*.hash
2 changes: 1 addition & 1 deletion ProofWidgets/Compat.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
2 changes: 1 addition & 1 deletion ProofWidgets/Component/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions ProofWidgets/Component/HtmlDisplay.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ProofWidgets/Component/MakeEditLink.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion ProofWidgets/Component/OfRpcMethod.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)`
Expand Down
2 changes: 1 addition & 1 deletion ProofWidgets/Component/Panel/GoalTypePanel.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion ProofWidgets/Component/Panel/SelectionPanel.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion ProofWidgets/Component/PenroseDiagram.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion ProofWidgets/Component/Recharts.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ProofWidgets/Demos/InteractiveSvg.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
Expand Down
2 changes: 1 addition & 1 deletion ProofWidgets/Demos/Plot.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ProofWidgets/Demos/RbTree.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ProofWidgets/Demos/Rubiks.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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"]

Expand Down
2 changes: 1 addition & 1 deletion ProofWidgets/Presentation/Expr.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
24 changes: 13 additions & 11 deletions lake-manifest.json
Original file line number Diff line number Diff line change
@@ -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"}
8 changes: 3 additions & 5 deletions lakefile.lean
Original file line number Diff line number Diff line change
@@ -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"

Expand All @@ -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) :
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:nightly-2023-10-12
leanprover/lean4:v4.3.0-rc2
2 changes: 1 addition & 1 deletion widget/rollup.config.js
Original file line number Diff line number Diff line change
Expand Up @@ -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;',
Expand Down
2 changes: 1 addition & 1 deletion widget/tsconfig.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
"module": "esnext",
"moduleResolution": "node",
"sourceMap": false,
"outDir": "../build/js",
"outDir": "../.lake/build/js",
"allowSyntheticDefaultImports": true,
"esModuleInterop": true,
"forceConsistentCasingInFileNames": true,
Expand Down

0 comments on commit 909febc

Please sign in to comment.