{"_id":"@bryangingechen/lean-client-js-browser","_rev":"4-73e0821b22ec9b255d2163bbf0b2c182","name":"@bryangingechen/lean-client-js-browser","dist-tags":{"latest":"1.4.0"},"versions":{"1.3.0":{"name":"@bryangingechen/lean-client-js-browser","version":"1.3.0","description":"Fork of lean-client-js-browser: Interface to the Lean server","main":"lib/index.js","types":"lib/index.d.ts","unpkg":"dist/leanBrowser.js","jsdelivr":"dist/leanBrowser.js","keywords":[],"author":{"name":"Bryan Gin-ge Chen","email":"bryangingechen@gmail.com"},"contributors":[{"name":"Gabriel Ebner","email":"gebner@gebner.org"}],"repository":{"type":"git","url":"git+https://github.com/bryangingechen/lean-client-js.git"},"scripts":{"compile":"tsc -w -p ./"},"license":"Apache-2.0","dependencies":{"@types/dropboxjs":"0.0.29","@types/filesystem":"0.0.28","@types/node":"=8.0.19","browserfs":"^1.4.3","lean-client-js-core":"^1.2.12"},"bugs":{"url":"https://github.com/bryangingechen/lean-client-js/issues"},"homepage":"https://github.com/bryangingechen/lean-client-js#readme","_id":"@bryangingechen/lean-client-js-browser@1.3.0","_nodeVersion":"10.16.0","_npmVersion":"6.10.1","dist":{"integrity":"sha512-i0p4OA1OrFzt2dVv5mi+L/t1dlQ60i0DUZaKknmkz47p3QRkWwWDC2NNCJBmvN57S2JKQDoLb7Ave5ghocH7Yg==","shasum":"a4db791c2f939ca3ec854193d67732a2c7a22eb5","tarball":"https://registry.npmjs.org/@bryangingechen/lean-client-js-browser/-/lean-client-js-browser-1.3.0.tgz","fileCount":23,"unpackedSize":169424,"npm-signature":"-----BEGIN PGP SIGNATURE-----\r\nVersion: OpenPGP.js v3.0.4\r\nComment: https://openpgpjs.org\r\n\r\nwsFcBAEBCAAQBQJdNiUeCRA9TVsSAnZWagAAg9MP/iyZiWfI/6baf1fviR+D\nWpeXlhJuickbjhzUxFXkqQZ3zjwK4a6Hk4XkQSbsOxZZ3LKZrGptWdTNOW+7\n4dLRXuPZ9LBhEdPWSUx6gCp89GiGNw48QpTtFihKFrcBV9GqKGU/RQ1Q6IM2\nlXYFwEYfAxt44nfEWTfMpEoUo6RWo1zFC2lV1ox2yU3oxgJ0GR0hOVf/0Fdl\nsUZ3k0WhGkoAmcIFrbWKdW58wx5KF1C8T7fgTAFqmsHD21BPu2jTD2dG6FzM\ni7CeMQPdYhl3BiokK0locdA11/GMZA9cffgnfgrgh+tNd/ns0YltWS1M8Jfu\nLtU1SnmUYrLRQr0GNuPpqmEcBreriN7KDu53ZDo1W9tDGP4v0sIc1KKNvz1l\nVCJsp6pXYuxVoB7UECQfNFbYnN0bKj8pmfIxiw5vKTkj/VxMYTgX8Rj6ZZO8\nd8bHedG4OwvSw8E+dpGC5L1QqoI4q06fwmZC/zWWwRe3SaH8+D3XEmhaFhlk\n1W/dPL9r5Deu/K4anhf8ea84EjgSwP1Nhk3OaQ+i4zXhT9omnwAQOqOhvVpz\nCM/OI1k8OZUYH3udElInfK9zdChkPGMWV3E09+sAy5c9ZIZB1KTMPNXnn2OF\n/N9FngmjVKencHvwg0mD1I+3bM76yli0vyPH//tb/l+PqndAWyk1WRm/2l0R\nN+jr\r\n=Ylq1\r\n-----END PGP SIGNATURE-----\r\n","signatures":[{"keyid":"SHA256:jl3bwswu80PjjokCgh0o2w5c2U4LhQAE57gj9cz1kzA","sig":"MEUCIQCHKVqzYKPj53iHK4gqF1IcTkaC5r/NJZ7W79CpeMwgzQIgR+N7YtO8TMQen83w6QQ2UD1Ubat7n0wdPL8j/7uxjG0="}]},"maintainers":[{"name":"bryangingechen","email":"bryangingechen@gmail.com"}],"_npmUser":{"name":"bryangingechen","email":"bryangingechen@gmail.com"},"directories":{},"_npmOperationalInternal":{"host":"s3://npm-registry-packages","tmp":"tmp/lean-client-js-browser_1.3.0_1563829533578_0.9618951968421632"},"_hasShrinkwrap":false},"1.3.1":{"name":"@bryangingechen/lean-client-js-browser","version":"1.3.1","description":"Fork of lean-client-js-browser: Interface to the Lean server","main":"lib/index.js","types":"lib/index.d.ts","unpkg":"dist/leanBrowser.js","jsdelivr":"dist/leanBrowser.js","keywords":[],"author":{"name":"Bryan Gin-ge Chen","email":"bryangingechen@gmail.com"},"contributors":[{"name":"Gabriel Ebner","email":"gebner@gebner.org"}],"repository":{"type":"git","url":"git+https://github.com/bryangingechen/lean-client-js.git"},"scripts":{"compile":"tsc -w -p ./"},"license":"Apache-2.0","dependencies":{"@types/dropboxjs":"0.0.29","@types/filesystem":"0.0.28","@types/node":"=8.0.19","browserfs":"^1.4.3","lean-client-js-core":"^1.2.12"},"bugs":{"url":"https://github.com/bryangingechen/lean-client-js/issues"},"homepage":"https://github.com/bryangingechen/lean-client-js#readme","_id":"@bryangingechen/lean-client-js-browser@1.3.1","_nodeVersion":"10.16.0","_npmVersion":"6.10.1","dist":{"integrity":"sha512-zLEHhMmbAl0pzQ281CKLY3LzkLB9M48escEaccyBi+dxRuNlHbsEaIaZ/WaDQOOOSvtQLC2kiCmTvas7bFTNGg==","shasum":"53f06ae4978c163646dc5f4dccb25d166799546a","tarball":"https://registry.npmjs.org/@bryangingechen/lean-client-js-browser/-/lean-client-js-browser-1.3.1.tgz","fileCount":25,"unpackedSize":169871,"npm-signature":"-----BEGIN PGP SIGNATURE-----\r\nVersion: OpenPGP.js v3.0.4\r\nComment: https://openpgpjs.org\r\n\r\nwsFcBAEBCAAQBQJdNighCRA9TVsSAnZWagAA+MgP/3oKRgqKA1CyrC2oH5iB\nKGDos06EdBaFOmoA6HkNLpJb2Dyovvghwn4t4jwdqwTuKYIPOHrre9vpuKAf\nqMK+OUHtVqOYuJW/xo6btgDujuK3jVtCV/77/IGooqAn6A2ceh+9u5rFTV1r\nprxh7t+SGGfo1BFEFeOk3+Fmqn8weR82cxvYFjLvk/9LOXWSgjUerOYV/L7l\n+5obOzaByx9ttIuRMxSxFoE6PKjW9rj528ZAen9nby3UB9xEFhNqhPM5NnwC\nPabvYzlZHdfJFUrI3BgshCJbFVQKu+T/9bK9tb480uPRV2sQjjL5ZReDDyUB\noGUbJO7pkXjs+pC+K7crpjS7kvmWiY6aiUMLctsLnjgIsX/wKH0z/BjHKq19\n3YqafOgWQuQB49IbQtCGk+PvYGbzkhkL+vVc7CRo3Fp3seU1RYMiE6YXGdpP\nn8kC1mKtJORWtCAdisS6T9smQ5fWdPt66C8zqbpM7ns5K12Sj2qH6XsZufeh\nfGjGPrm2FOL7cnQO/YpgR/EfR+dZnGZNE5Vl+jQEpgrVAPzjxu3k4b+hZO52\nvna9XawsLPqAg7Jk7ixfK0VwmXZOWERZh7rwGDvqyP5At9tUY9rHVhon4YeR\nFi3h06Fyx6E4X0cWUm00fr+JhGTXgXOUNEAVWmSKbwZBaSPkvDGlmkOpHc1p\n7dps\r\n=NCEn\r\n-----END PGP SIGNATURE-----\r\n","signatures":[{"keyid":"SHA256:jl3bwswu80PjjokCgh0o2w5c2U4LhQAE57gj9cz1kzA","sig":"MEUCIQDuDh3aIKN6xBQbyZMAvyKA+apGvwk4gmc7LsyWeb+cPgIgG2t3v72NLjKQonlWk9An6nnnzzoMOOQAXHwCYcjT+y4="}]},"maintainers":[{"name":"bryangingechen","email":"bryangingechen@gmail.com"}],"_npmUser":{"name":"bryangingechen","email":"bryangingechen@gmail.com"},"directories":{},"_npmOperationalInternal":{"host":"s3://npm-registry-packages","tmp":"tmp/lean-client-js-browser_1.3.1_1563830304624_0.6303061238809948"},"_hasShrinkwrap":false},"1.3.2":{"name":"@bryangingechen/lean-client-js-browser","version":"1.3.2","description":"Fork of lean-client-js-browser: Interface to the Lean server","main":"lib/index.js","types":"lib/index.d.ts","unpkg":"dist/leanBrowser.js","jsdelivr":"dist/leanBrowser.js","keywords":[],"author":{"name":"Bryan Gin-ge Chen","email":"bryangingechen@gmail.com"},"contributors":[{"name":"Gabriel Ebner","email":"gebner@gebner.org"}],"repository":{"type":"git","url":"git+https://github.com/bryangingechen/lean-client-js.git"},"scripts":{"compile":"tsc -w -p ./"},"license":"Apache-2.0","dependencies":{"@types/dropboxjs":"0.0.29","@types/filesystem":"0.0.28","@types/node":"=8.0.19","browserfs":"^1.4.3","lean-client-js-core":"^1.2.12"},"bugs":{"url":"https://github.com/bryangingechen/lean-client-js/issues"},"homepage":"https://github.com/bryangingechen/lean-client-js#readme","_id":"@bryangingechen/lean-client-js-browser@1.3.2","_nodeVersion":"10.16.3","_npmVersion":"6.11.3","dist":{"integrity":"sha512-xJb2f/fTCa5Efq7KGLItq1XctQUHJ8c4YZzlhoPEY+Cw9Vd+zCpjkrqjtiZnDkmipg5eJBtOZsZbiziPxEtXJQ==","shasum":"652fcf39be2484a21dfc79f888ba1be35a6ba2e7","tarball":"https://registry.npmjs.org/@bryangingechen/lean-client-js-browser/-/lean-client-js-browser-1.3.2.tgz","fileCount":25,"unpackedSize":168390,"npm-signature":"-----BEGIN PGP SIGNATURE-----\r\nVersion: OpenPGP.js v3.0.4\r\nComment: https://openpgpjs.org\r\n\r\nwsFcBAEBCAAQBQJdkkn5CRA9TVsSAnZWagAARv0P/RiTly29JurewufxN/dV\ny2XcYw3y6aY5FAApp8kL+DrlOiQmbO4oKNMI0BUoW8siNUrRg1zRpQgnF9iA\n2pdJY6F+BKN7yiJoNgHjG7sD0cUP7XIoOMT0iR7uaFrV+NXRQcriFsreHheH\nxLz2J85y6gsWd88D04MhcqsMh4MIKtg78biX6fMUBitnuE333ulBSg63itZ3\nReHZ1pn7DfOt7PLlpoymN2nGwA1q40l67qpqH/a5393hn7Dh1iR5vxLUOJID\n1jvOXGelymBw5F4t2434JGbOyXznlX3lM9GkXsAuqtHaGUE/GBOu/nHW38u2\nqXejz+Lob/6QV19DCnTfnjqsGXmgrIBC18SJUJ+3pRB7JNfAtqubcbpde+Uu\nlll+0wggVb/f3R9R/x4OePgZNTYDsT4cYvgGvBPG8oGoDiHGLIxO2QfIA0Jn\nW7K0o3FE4j/AcDHU5uIHnwvnFVpe6q+ChVbyNW8HZ+n7GcXW6pgsHzLLmhTd\nNUhehqUqF9W9Bb9pTDzkC522wQusD5NbhSvmXfAh9gyDjZRJSJdvLFpDepN+\ngR6UtOsQ+/QlYuFGTUmBoVaP27DEdhMN37vnfhARo5sVOuHvRPC5FrxaeZhr\n+NE5VxxQHMVmva9N6iiU2MHaBf9ia3GR2M0vlLtQXQCI8fMtsTd1H8hifsmB\nFJUf\r\n=zPqr\r\n-----END PGP SIGNATURE-----\r\n","signatures":[{"keyid":"SHA256:jl3bwswu80PjjokCgh0o2w5c2U4LhQAE57gj9cz1kzA","sig":"MEUCIBf2glx3qccbS8jMkGk9Oep1DbakSXtg7IxSraAUC4/QAiEAylEBKChiX7hzS5iNzN1N8MXkguvNLjPmfWquh6P0u+w="}]},"maintainers":[{"name":"bryangingechen","email":"bryangingechen@gmail.com"}],"_npmUser":{"name":"bryangingechen","email":"bryangingechen@gmail.com"},"directories":{},"_npmOperationalInternal":{"host":"s3://npm-registry-packages","tmp":"tmp/lean-client-js-browser_1.3.2_1569868280523_0.09857877443344143"},"_hasShrinkwrap":false},"1.4.0":{"name":"@bryangingechen/lean-client-js-browser","version":"1.4.0","description":"Fork of lean-client-js-browser: Interface to the Lean server","main":"lib/index.js","types":"lib/index.d.ts","unpkg":"dist/leanBrowser.js","jsdelivr":"dist/leanBrowser.js","keywords":[],"author":{"name":"Bryan Gin-ge Chen","email":"bryangingechen@gmail.com"},"contributors":[{"name":"Gabriel Ebner","email":"gebner@gebner.org"}],"repository":{"type":"git","url":"git+https://github.com/bryangingechen/lean-client-js.git"},"scripts":{"compile":"tsc -w -p ./"},"license":"Apache-2.0","dependencies":{"@types/dropboxjs":"0.0.29","@types/filesystem":"0.0.28","@types/node":"=8.0.19","browserfs":"^1.4.3","lean-client-js-core":"^1.2.12"},"bugs":{"url":"https://github.com/bryangingechen/lean-client-js/issues"},"homepage":"https://github.com/bryangingechen/lean-client-js#readme","_id":"@bryangingechen/lean-client-js-browser@1.4.0","_nodeVersion":"12.16.2","_npmVersion":"6.14.5","dist":{"integrity":"sha512-VMmUc/8nfpX0o8sSY8VntKNpLlLh8nCOAtS23U5KTyEUe3C/6l7vP8VzbACw4by/plhdzymM895ub3nzi7DfLQ==","shasum":"b78637855456c300d4fdca74a554c9d47e3787ea","tarball":"https://registry.npmjs.org/@bryangingechen/lean-client-js-browser/-/lean-client-js-browser-1.4.0.tgz","fileCount":25,"unpackedSize":173256,"npm-signature":"-----BEGIN PGP SIGNATURE-----\r\nVersion: OpenPGP.js v3.0.4\r\nComment: https://openpgpjs.org\r\n\r\nwsFcBAEBCAAQBQJex0xfCRA9TVsSAnZWagAAyxcP/jMOCyjgYoIS0FBlQYq7\n5ZgwUxjqFWWVnWpZamGii9ePjA/fL5FB3lZg5gTdUkIQeFSK+sanAplYxJ4Y\n1YX0YNjwMMLwgomTgk0Mja+ctOzPwvoQ6bDw1KFFdlW4M22XjKupogu5aeJx\nw6xQF5HO46UfgbdExsAumZQUVH872gdCCu+4vF8AKmplI9qU4M3dsB+PcRuv\nJyxXzVy7FoGoFZ/RMGHxVNtenC+qMzUN2PN4G5nDjamjByhby6+4a9qwPPez\nJtUOKZSBjsy6vXuH6HAhKJRkMJjWqJodu338u2Y1tM/ajMbmZU6RaLfJWPsj\niuXyCz7CYIC7aPVAS3IAx1e0rj2MOQZT2ilQ4sxaOWr7FMKWWfdSBpjivPwP\nutMlG87bs0EtLmMGIViITvZugIDNTPVk5q3s60H7JQ3vqpE1VN4RjcjcYubP\nDLT/FSfaW85CwnqSQiZTy9dfvyZyXm3/jbSgk7ZH5zgx7f7bjwtAZzSeGsju\ndG4FWhm7VPXYV/QSoBznMStKCeZi0EfQ8/UlGHTyXU/DyJLiUSt+Pu+NOKnQ\nCQmA3YAj6SDFh5QYg22KZ1Bcp5NgLMJejs5jS7LBLLZXOBLATxHj/8E6a+CC\n9qipNmknd4t7iZygagzuYGCLSTRvkuybk/Od1QepAE2h+iX1kkKqrkiJKI5O\nJzP0\r\n=kBng\r\n-----END PGP SIGNATURE-----\r\n","signatures":[{"keyid":"SHA256:jl3bwswu80PjjokCgh0o2w5c2U4LhQAE57gj9cz1kzA","sig":"MEYCIQDD6F9sAMFuxgjXBJXx5WBAacqx9lrpXnzmqiuWbAIHkgIhAKUJOuMIS/KkElUF+IFOgsW6hnY7lFn8orA+gcaQJ9EX"}]},"maintainers":[{"name":"bryangingechen","email":"bryangingechen@gmail.com"}],"_npmUser":{"name":"bryangingechen","email":"bryangingechen@gmail.com"},"directories":{},"_npmOperationalInternal":{"host":"s3://npm-registry-packages","tmp":"tmp/lean-client-js-browser_1.4.0_1590119518399_0.32807102730085447"},"_hasShrinkwrap":false}},"time":{"created":"2019-07-22T21:05:33.355Z","1.3.0":"2019-07-22T21:05:33.902Z","modified":"2022-04-04T20:49:44.086Z","1.3.1":"2019-07-22T21:18:24.776Z","1.3.2":"2019-09-30T18:31:20.679Z","1.4.0":"2020-05-22T03:51:58.558Z"},"maintainers":[{"name":"bryangingechen","email":"bryangingechen@gmail.com"}],"description":"Fork of lean-client-js-browser: Interface to the Lean server","homepage":"https://github.com/bryangingechen/lean-client-js#readme","keywords":[],"repository":{"type":"git","url":"git+https://github.com/bryangingechen/lean-client-js.git"},"contributors":[{"name":"Gabriel Ebner","email":"gebner@gebner.org"}],"author":{"name":"Bryan Gin-ge Chen","email":"bryangingechen@gmail.com"},"bugs":{"url":"https://github.com/bryangingechen/lean-client-js/issues"},"license":"Apache-2.0","readme":"# lean-client-js-browser\n\nThis is a JavaScript library to interface with the server mode of the [Lean theorem prover](https://leanprover.github.io/).\n\nThis package contains the web browser version. It communicates with an Emscripten build of Lean in a WebWorker, using WebAssembly if available.\n\nThe [original version](https://github.com/leanprover/lean-client-js/tree/master/lean-client-js-browser) was authored by Gabriel Ebner.\n\n## How to use\n\nYou will need to place the files from the Lean Emscripten build (downloadable from [here](https://github.com/leanprover-community/lean-nightly/releases), see the `lean-*-browser.zip` files) and a suitable `.zip` bundle of `.olean` files (see instructions [here](https://github.com/leanprover-community/lean-web-editor/#creating-a-customized-libraryzip)) 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.\n\nThe main class is `WebWorkerTransport`. The constructor takes [a `LeanJsOptions` object](src/inprocesstypes.ts) with the following fields:\n  - `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.\n  - `libraryMeta` (optional): URL to `library.info.json`, a JSON file whose keys are the Lean packages contained in `library.zip` and whose values are URL prefixes that point to the Lean source files. (default: the value of `libraryZip` with the final `.zip` replaced with `.info.json`)\n  - `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 `libraryZip` with the final `.zip` replaced with `.olean_map.json`)\n  - `libraryKey` (optional): name for the key used in the indexedDB cache (default: the filename of `libraryZip` with `.zip` removed)\n  - At least one of `javascript` or (`webassemblyWasm` + `webassemblyJs`) must be provided:\n    - `javascript`: URL to `lean_js_js.js`\n    - Both of the following fields should be provided to use the WebAssembly version of the Lean server:\n      - `webassemblyWasm`: URL to `lean_js_wasm.wasm`\n      - `webassemblyJs`: URL to `lean_js_wasm.js`\n  - `memoryMB` (optional): size of memory in MB provided (default: 256)\n  - `dbName` (optional): name of the IndexedDB database used to cache (default: `leanlibrary`)\n\nThe `WebWorkerTransport` object that is returned should be passed to the `Server` constructor. See the `lean-client-js` library for more information about the `Server` class.\n\nSee [`demo.ts`](./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.\n\nSee [`leanprover-community/lean-web-editor`](https://github.com/leanprover-community/lean-web-editor) and [`mpedramfar/Lean-game-maker`](https://github.com/mpedramfar/Lean-game-maker) for example TypeScript projects that use this library.\n\nSee [these Observable notebooks](https://observablehq.com/collection/@bryangingechen/lean) for example webpages that use the UMD module `leanBrowser.js`.\n\n## Building\n\nTo 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 `dist/demo.html`.\n\nRunning `../node_modules/.bin/webpack` 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.\n\nOnce the files are built, you can check them out by starting a local web server (from the `dist/` directory) and navigating to `/index.html` or `/lib_test.html`.\n\n## About this fork\n\nThis version of `lean-client-js-browser` has two main differences from the original:\n\n1. 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.\n\n2. 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 `meta`:\n  - `meta` is a key-value store, where the key used is given by `opts.libName` and the values are JSON objects which map the Lean package names in the ZIP file to source links\n  - `library` is another key-value store, where the keys are the same as in `meta` and the values are the ZIP files stored as binary blobs.\n","readmeFilename":"README.md"}