feat: customizable error message on build (#105)

* feat; customizable error message on build * doc: add errorOnBuild to README --------- Co-authored-by: Wojciech Nawrocki <[email protected]>
leanprover-community · Feb 12, 2025 · 322a050 · 322a050
1 parent 8fff3f0
commit 322a050
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 4 deletions.
diff --git a/README.md b/README.md
@@ -41,18 +41,27 @@ to keep a widget in view. You can then live code your widgets.
 
 Put this in your `lakefile.lean`, making sure to reference a **release tag**
 rather than the `main` branch:
+
 ```lean
 -- You should replace v0.0.3 with the latest version published under Releases
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4"@"v0.0.3"
 ```
 
-Note that [developing ProofWidgets](#developing-proofwidgets) involves building TypeScript code with NPM.
+[Developing ProofWidgets](#developing-proofwidgets) involves building TypeScript code with NPM.
 When depending on `ProofWidgets` but not writing any custom TypeScript yourself,
-you likely want to spare yourself and your users from having to run NPM.
+you likely want to spare yourself and your users from having to install and run NPM.
 ProofWidgets is configured to use Lake's [cloud releases](https://github.com/leanprover/lake/#cloud-releases) feature
 which will automatically fetch pre-built JavaScript files *as long as* you require a release tag
 rather than the `main` branch.
-In this mode, you don't need to have NPM installed.
+In this mode, you and your users should not need to have NPM installed.
+However, fetching cloud release may sometimes fail,
+in which case ProofWidgets may still revert to a full build.
+You can force ProofWidgets to fail with a custom error in this case by importing it like so:
+
+```lean
+-- You should replace v0.0.3 with the latest version published under Releases
+require proofwidgets with NameMap.empty.insert `errorOnBuild "<my message>" from git "https://github.com/leanprover-community/ProofWidgets4"@"v0.0.3"
+```
 
 ⚠️ [EXPERIMENTAL] To use ProofWidgets4 JS components in widgets defined in other Lean packages,
 you can import [@leanprover-community/proofwidgets4](https://www.npmjs.com/package/@leanprover-community/proofwidgets4) from NPM.

diff --git a/lakefile.lean b/lakefile.lean
@@ -46,7 +46,9 @@ def widgetJsAllTarget (pkg : Package) (isDev : Bool) : FetchM (Job (Array FilePa
   pkg.afterBuildCacheAsync $ deps.mapM fun depInfo => do
     let traceFile := pkg.buildDir / "js" / "lake.trace"
     let _ ← buildUnlessUpToDate? traceFile (← getTrace) traceFile do
-       /- HACK: Ensure that NPM modules are installed before building TypeScript,
+      if let some msg := get_config? errorOnBuild then
+        error msg
+      /- HACK: Ensure that NPM modules are installed before building TypeScript,
        *if* we are building Typescript.
        It would probably be better to have a proper target for `node_modules`
        that all the JS/TS modules depend on.