This package contains the web browser version. It communicates with an Emscripten build of Lean in a WebWorker, using WebAssembly if available.
You will need to place the files from the Lean Emscripten build (downloadable from here, see the
lean-*-browser.zip files) and a suitable
.zip bundle of
.olean files (see instructions here) into a subdirectory of this directory called
dist/ for the demo files to work. The
library.zip file is cached in IndexedDB to save on downloading, provided that its associated
library.info.json is present at the same path.
The main class is
WebWorkerTransport. The constructor takes a
LeanJsOptions object with the following fields:
libraryZip: URL to
library.zip. Must end in
.zip. This field is used to generate the default values for some of the optional fields below.
libraryMeta(optional): URL to
library.info.json, a JSON file whose keys are the Lean packages contained in
library.zipand whose values are URL prefixes that point to the Lean source files. (default: the value of
libraryZipwith the final
libraryOleanMap(optional): URL to
library.olean_map.json, a JSON file whose keys are the filenames of the oleans in
library.zip(with .olean removed) and whose values are the name of the Lean package that they originate from (default: the value of
libraryZipwith the final
libraryKey(optional): name for the key used in the indexedDB cache (default: the filename of
webassemblyJs) must be provided:
webassemblyWasm: URL to
webassemblyJs: URL to
memoryMB(optional): size of memory in MB provided (default: 256)
dbName(optional): name of the IndexedDB database used to cache (default:
WebWorkerTransport object that is returned should be passed to the
Server constructor. See the
lean-client-js library for more information about the
demo.ts for an example on how to use this package in a TypeScript project. After building, see
dist/lib_test.html for how to use this package in a webpage.
See these Observable notebooks for example webpages that use the UMD module
To build the demo file, follow the directions in the README file in the parent package
lean-client-js. The demo file will be written to
npm run build from this directory will build and output the test file
dist/lib_test.html as well as a UMD module
dist/leanBrowser.js for use in webpages.
Once the files are built, you can check them out by starting a local web server (from the
dist/ directory) and navigating to
This version of
lean-client-js-browser has two main differences from versions before v2.0.0:
First, it removes the
BrowserInProcessTransport class which allowed running the Lean Emscripten server in the browser's main thread. You must use
WebWorkerTransport, which runs the server in a WebWorker.
Second, it caches the
library.zip file in the browser's IndexedDB store. The database name is determined by
opts.dbName. This DB contains two "Object stores", one named
library and one named
metais a key-value store, where the key used is given by
opts.libNameand the values are JSON objects which map the Lean package names in the ZIP file to source links
libraryis another key-value store, where the keys are the same as in
metaand the values are the ZIP files stored as binary blobs.