{"id":"2c3cf8464aed9c1f","slug":"hello-lean-prover","trashed":false,"description":"","likes":38,"publish_level":"public","forks":2,"fork_of":null,"has_importers":true,"update_time":"2021-01-26T17:37:23.351Z","first_public_version":null,"paused_version":null,"publish_time":"2019-07-28T19:34:54.661Z","publish_version":5348,"latest_version":5348,"thumbnail":"90ec3d3750f7d06c21ecc29f59b558cfe3ad9f18501b1ede75c7d05d0bd66774","default_thumbnail":"8dc01e380330c9de53d8fd3ef75224fa4d3d39448c897c806b48c01efc5b4bd8","roles":[],"sharing":null,"owner":{"id":"d2fd23101beb2a61","avatar_url":"https://avatars.observableusercontent.com/avatar/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","login":"bryangingechen","name":"Bryan Gin-ge Chen","bio":"here to learn","home_url":"https://twitter.com/blockspins","type":"team","tier":"starter_2024"},"creator":{"id":"5c13a1a27cf52564","avatar_url":"https://avatars.observableusercontent.com/avatar/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","login":"bryangingechen","name":"Bryan Gin-ge Chen","bio":"here to learn","home_url":"https://twitter.com/blockspins","tier":"public"},"authors":[{"id":"5c13a1a27cf52564","avatar_url":"https://avatars.observableusercontent.com/avatar/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","name":"Bryan Gin-ge Chen","login":"bryangingechen","bio":"here to learn","home_url":"https://twitter.com/blockspins","tier":"public","approved":true,"description":""}],"collections":[{"id":"68b035771823d0b5","type":"public","slug":"lean","title":"Lean","description":"Notebooks related to the Lean theorem prover https://leanprover.github.io","update_time":"2019-12-14T08:32:41.501Z","pinned":false,"ordered":true,"custom_thumbnail":"e31ecdc4b6bd07378620dcddfaefecb887a104cb84645085ff32760cf4f3d2a4","default_thumbnail":"90ec3d3750f7d06c21ecc29f59b558cfe3ad9f18501b1ede75c7d05d0bd66774","thumbnail":"e31ecdc4b6bd07378620dcddfaefecb887a104cb84645085ff32760cf4f3d2a4","listing_count":10,"parent_collection_count":0,"owner":{"id":"d2fd23101beb2a61","avatar_url":"https://avatars.observableusercontent.com/avatar/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","login":"bryangingechen","name":"Bryan Gin-ge Chen","bio":"here to learn","home_url":"https://twitter.com/blockspins","type":"team","tier":"starter_2024"}},{"id":"80583d7c09f19038","type":"public","slug":"inputs","title":"Ingredients","description":"duty-free imports of inputs, tools, and libraries!","update_time":"2019-03-04T21:23:36.451Z","pinned":false,"ordered":false,"custom_thumbnail":"deca5a470fcbf5a75aa2e7c987fba0f36983be403c13315876f6cc150be0c7cb","default_thumbnail":"fcde2368f35e13a9ab2dd16547487c94be80963caefde9b3a926d575b729d411","thumbnail":"deca5a470fcbf5a75aa2e7c987fba0f36983be403c13315876f6cc150be0c7cb","listing_count":24,"parent_collection_count":0,"owner":{"id":"d2fd23101beb2a61","avatar_url":"https://avatars.observableusercontent.com/avatar/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","login":"bryangingechen","name":"Bryan Gin-ge Chen","bio":"here to learn","home_url":"https://twitter.com/blockspins","type":"team","tier":"starter_2024"}}],"files":[],"comments":[],"commenting_lock":null,"suggestion_from":null,"suggestions_to":[],"version":5348,"title":"Hello, Lean prover!","license":null,"copyright":"","nodes":[{"id":0,"value":"md`# Hello, Lean prover!\n\n
\n\n
`","pinned":false,"mode":"js","data":null,"name":null},{"id":1227,"value":"md`The [Lean theorem prover](https://leanprover.github.io/) is an open source [interactive theorem prover](https://en.wikipedia.org/wiki/Proof_assistant) developed at Microsoft Research. The Lean project was launched in 2013 by [Leonardo de Moura](http://leodemoura.github.io/) (of [Z3](https://github.com/Z3Prover/z3) fame) and so it is a relatively new entrant to the field ([Coq](https://coq.inria.fr/), [Isabelle](https://isabelle.in.tum.de/), [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) are a few others). \n\nA fun way to start playing around in Lean is Kevin Buzzard's [Natural Number Game](http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/).\n\nThese three online books are also good sources for introductory material about Lean:\n- [\"Theorem Proving in Lean\"](https://leanprover.github.io/theorem_proving_in_lean/) by Jeremy Avigad, Leonardo de Moura and Soonho Kong\n- [\"Logic and Proof\"](https://avigad.github.io/logic_and_proof/) by Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn.\n- Lecture notes to [the course \"Logical Verification in Lean\"](https://lean-forward.github.io/logical-verification/2019/) by Tim Baanen, Alexander Bentkamp, Jasmin Blanchette and Johannes Hölzl.\n\nThe Lean developers have put in quite a bit of effort to make Lean usable in the browser. For instance, the Natural Number Game runs in the browser and the first two books above have snippets of Lean code which link to the [\\`lean-web-editor\\`](https://leanprover.github.io/live/latest), a web app that runs an Emscripten build of Lean. In light of my positive experiences writing interactive documents in Observable, I thought that it might be fun to explore whether Observable notebooks + Lean could become a viable option for explaining and sharing formalized math on the web.\n\n⚠️ The WASM version of Lean does not work in Safari 13.0 (see [this WebKit bug](https://bugs.webkit.org/show_bug.cgi?id=201028)). Please upgrade to Safari 13.1 or try Firefox or Chrome instead!\n\nHere's an instance of the [Lean CodeMirror editor](#leanEditor) from this notebook. Try hovering and moving the cursor around, and then try editing (the full features are described [below](#CMLeanEditor)):\n`","pinned":false,"mode":"js","data":null,"name":null},{"id":809,"value":"viewof test0 = leanEditor({\n fileName: 'test0.lean',\n value: String.raw`variables p q r s : Prop\ntheorem my_and_comm : p /\\ q <-> q /\\ p :=\niff.intro\n(assume Hpq : p /\\ q,\nand.intro (and.elim_right Hpq) (and.elim_left Hpq))\n(assume Hqp : q /\\ p,\nand.intro (and.elim_right Hqp) (and.elim_left Hqp))\n#check @nat.rec_on\n#print \"end of file!\"\n`,\n height: '200px',\n}, invalidation)","pinned":false,"mode":"js","data":null,"name":null},{"id":1400,"value":"md`The border changes color depending on the server status:\n- the editor is initializing\n- Lean is busy\n- Lean is ready\n- the Lean server has stopped and needs to be reset.\n\nThe Lean editor cells are [views](https://observablehq.com/@observablehq/introduction-to-views), and their values are objects which contain (among other things) the responses from the Lean server, allowing data to be passed from Lean to Observable:\n`","pinned":false,"mode":"js","data":null,"name":null},{"id":1535,"value":"test0.msgs","pinned":true,"mode":"js","data":null,"name":null},{"id":1532,"value":"md`This notebook also provides [a tag function](#leanHL) for syntax-highlighting (but not actually processing) Lean code like this:\n\n${leanHL`def collatz_fn (n : ℕ) : ℕ :=\nif (2 ∣ n) then n / 2 else 3 * n + 1\n\n#eval collatz_fn 0\n\ntheorem collatz_conjecture (n : ℕ) : n > 0 → ∃ m,\n nat.iterate collatz_fn m n = 4 := sorry\n\n#eval nat.iterate collatz_fn 10 7`}`","pinned":false,"mode":"js","data":null,"name":null},{"id":1391,"value":"md`This notebook primarily consists of the code gluing everything together along with some notes documenting how it works (it assumes [basic knowledge about Observable](https://observablehq.com/@observablehq/observable-user-manual)). It's meant more for reference / hacking than for education or entertainment.\n\n
👉 Check out the companion notebooks [\"Fibonacci formalized\"](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums) to see some formalized mathematics written using the functions here.
\n\nFor convenience, here's an import command that you can copy and paste (you can delete any items in the list that you don't use directly):\n\n\\`\\`\\`js\nimport {leanEditor, leanEditorFrom, InfoView, LeanFile, leanControl, leanHL, parseLeanMsgs}\n from '@bryangingechen/hello-lean-prover'\n\\`\\`\\`\n\n⚡️ If you already have Lean installed on your computer, you can try using that as a backend for the Lean editor (instead of relying on the much slower Emscripten build) by following the directions [here](https://observablehq.com/@bryangingechen/lean-websocketd)!\n\nFeel free to make suggestions on the notebook using Observable's \"suggest\" feature or by messaging me [on twitter](https://twitter.com/blockspins). For questions about Lean, check out [the Lean zulip chat](https://leanprover.zulipchat.com/)! Questions at all levels are welcomed; I certainly learned tons from the folks there!\n`","pinned":false,"mode":"js","data":null,"name":null},{"id":3829,"value":"md`### Related work:\n\nThe functions and cells below integrate the Emscripten-compiled JS and WebAssembly versions of Lean with the [CodeMirror editor](https://codemirror.net/index.html). This notebook builds heavily on (lifts code from) the [\\`lean-client-js\\`](https://github.com/leanprover/lean-client-js), [\\`lean-web-editor\\`](https://github.com/leanprover/lean-web-editor) and [\\`vscode-lean\\`](https://github.com/leanprover/vscode-lean) projects by Gabriel Ebner, Jared Roesch, Sebastian Ulrich and other contributors.\n\nPatrick Massot's [\\`format-lean\\`](https://github.com/leanprover-community/format_lean) project also aims to make Lean code presentable on the web (see [this beautiful example](https://www.math.u-psud.fr/~pmassot/lean/) and [these course notes (in French)](https://www.math.u-psud.fr/~pmassot/enseignement/math114/)). The approach there is to generate HTML & JS documents from commented Lean files.\n\nThe [CoCalc](https://cocalc.com) project also has code that integrates [Lean with Codemirror](https://github.com/sagemathinc/cocalc/tree/67c3f43a812e88d2a3f761c90e63897a81fe96a7/src/smc-webapp/frame-editors/lean-editor), including a [\"Lean mode\"](https://github.com/sagemathinc/cocalc/blob/d0124719b36621bc03d8becb256b300f255c05ac/src/smc-webapp/codemirror/mode/lean.ts). The focus of that project is on collaboratively editing and saving files hosted on their servers. The CoCalc Lean editor communicates with [Lean running on their servers](https://github.com/sagemathinc/cocalc/tree/67c3f43a812e88d2a3f761c90e63897a81fe96a7/src/smc-project/lean) rather than with Emscripten Lean running in the browser.\n\nWylie Conlon's [\\`lsp-editor-adapter\\`](https://github.com/wylieconlon/lsp-editor-adapter) is an interesting project which aims to let CodeMirror editors communicate with servers that speak the \"language server protocol\". Sadly, the Lean server doesn't use the LSP directly (though there is an implementation of a [Lean language server](https://github.com/leanprover/lean-client-js/tree/master/lean-language-server)).`","pinned":false,"mode":"js","data":null,"name":null},{"id":1864,"value":"Contents = md`## Contents\n\n1. [Starting the Lean server](#Starting)\n2. [Controlling the Lean server](#Controlling)\n - [Server control form](#ServerForm)\n - [Server commands](#ServerCommands)\n - [Range of interest syncing](#RangeOfInterest)\n - [Lean file objects](#LeanFileDoc)\n3. [CodeMirror editor](#CodeMirrorEditor)\n - [Lean mode](#CMLeanMode)\n - [Lean editor](#CMLeanEditor)\n - [Usage](#CMLeanEditorUsage)\n - [Examples](#CMLeanEditorExamples)\n - [Global config object](#ConfigDoc)\n - [Auxiliary functions](#AuxFunctions)\n - [CSS](#CodeMirrorCSS)\n4. [TODO / Version history](#TODO)\n5. [LICENSE](#LICENSE)\n`","pinned":false,"mode":"js","data":null,"name":null},{"id":1235,"value":"Starting = md`## 1. Starting the Lean server\n\nThe [\\`lean-client-js\\`](https://github.com/leanprover/lean-client-js) package provides a convenient interface for the Lean server; in [a fork](https://github.com/bryangingechen/lean-client-js), I managed to coax webpack to output a UMD module that can be imported with \\`require\\`:\n`","pinned":false,"mode":"js","data":null,"name":null},{"id":2,"value":"lean = require('lean-client-js-browser@2.0.1')","pinned":false,"mode":"js","data":null,"name":null},{"id":1268,"value":"md`The constructor of \\`lean-client-js\\`'s [\\`Server\\` class](https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/server.ts) takes a \"transport\" object as input. We use a \\`WebWorkerTransport\\` object (which runs the JS/WASM in a WebWorker) (see [code here](https://github.com/bryangingechen/lean-client-js/blob/cache/lean-client-js-browser/src/inprocess.ts)).`","pinned":false,"mode":"js","data":null,"name":null},{"id":5193,"value":"transport = new lean.WebWorkerTransport(transportOpts)","pinned":false,"mode":"js","data":null,"name":null},{"id":1275,"value":"md`The options object passed to the \\`WebWorkerTransport\\` constructor contains URLs to the Lean server's JS/WASM as well as the library ZIP bundle which contains the \\`.olean\\` files (binaries which cache parsed Lean code) for Lean libraries that can then be imported into sessions with the Lean server. For more details, see the [\\`lean-client-js-browser\\` README](https://github.com/leanprover/lean-client-js/tree/master/lean-client-js-browser).\n\nThis notebook uses the core library bundle (~2 MB). It's also possible to load a ZIP bundle containing the main math library for Lean ([\\`mathlib\\`](https://github.com/leanprover-community/mathlib)) by overriding \\`leanLibName\\` with \\`\"library\"\\` when you import from this notebook, but note that it's ~19MB and growing! You can also make ZIP bundles out of your own Lean packages by using the [Python script in the community fork of the \\`lean-web-editor\\`](https://github.com/leanprover-community/lean-web-editor/blob/ui/mk_library.py).\n\n⚠️ \\`lean-client-js\\` caches all ZIP bundles in a IndexedDB store named \"\\`leanlibrary\\`\". This feature is a bit rough and can fail to work if Lean is being initialized in multiple notebooks at the same time (e.g. you may see errors like \"\\`TypeError: First argument must be a string, Buffer, ArrayBuffer, Array, or array-like object.\\`\"). Fortunately, reloading seems to fix things. You can avoid this issue by waiting for the Lean editors to appear before opening another notebook. There's also a [button](#deleteIdb) in the [Lean control form](#ServerForm) below which resets this IndexedDB store, in case this cache gets corrupted.\n\nCurrently, the necessary files are hosted by [Scott Morrison](https://tqft.net/) on his webserver (thanks Scott!), though from time to time I may change the host while things update. The JS/WASM files can also be downloaded from the [\\`leanprover-community/lean\\` releases page](https://github.com/leanprover-community/lean-nightly/releases); see [the community fork of the \\`lean-web-editor\\`](https://github.com/leanprover-community/lean-web-editor) for the Python script (\\`mk_library.py\\`) which bundles Lean library packages into a ZIP file.\n\nThe Lean developers are currently hard at work on a new, not-ready-for-public-use, version of Lean ([Lean 4](https://github.com/leanprover/lean4)). Because of this, the Lean server used in this notebook is built from the unofficial [\"community fork\" of Lean 3](https://github.com/leanprover-community/lean/).`","pinned":false,"mode":"js","data":null,"name":null},{"id":3642,"value":"// if you want to use the big bundle of libraries (~19MB rather than ~2MB), change the following to 'library'\nleanLibName = 'libcore'","pinned":false,"mode":"js","data":null,"name":null},{"id":5192,"value":"transportOptsURL = \"https://bryangingechen.github.io/lean/lean-web-editor/\" //'https://gitcdn.link/repo/bryangingechen/lean-web-editor-dist/master/'","pinned":false,"mode":"js","data":null,"name":null},{"id":1049,"value":"transportOpts = {\n return {\n javascript: `${transportOptsURL}lean_js_js.js`, // Lean server compiled to asm.js with Emscripten (won't be downloaded or used unless your browser doesn't support WASM)\n webassemblyJs: `${transportOptsURL}lean_js_wasm.js`, // JS code generated by Emscripten to call...\n webassemblyWasm: `${transportOptsURL}lean_js_wasm.wasm`, // Lean server compiled to WASM by Emscripten\n libraryZip: `${transportOptsURL}${leanLibName}.zip`, // bundle of .olean files\n }\n}","pinned":false,"mode":"js","data":null,"name":null},{"id":3919,"value":"md`We can now create a cell for the server object`","pinned":false,"mode":"js","data":null,"name":null},{"id":6,"value":"server = {\n __LEAN_SERVER_RESTARTS; // create dependency to be able to restart the server (this is a bit hacky)\n resetOpenLeanFiles();\n const server = new lean.Server(transport);\n server.logMessagesToConsole = logByDefault;\n server.error.on((err) => console.log('error:', err));\n // window.server = server; // uncomment this to allow running commands from the dev console\n server.connect();\n // return server when it begins to respond to messages\n return server.search('').then(() => Generators.disposable(server, server => {\n console.log('disposing lean server...');\n server.dispose(); // dispose server when cell is invalidated\n }));\n}","pinned":false,"mode":"js","data":null,"name":null},{"id":5188,"value":"md`and some cells to reset the server. Use \\`resetServer()\\` to re-initialise the Lean server.`","pinned":false,"mode":"js","data":null,"name":null},{"id":5187,"value":"mutable __LEAN_SERVER_RESTARTS = 0","pinned":false,"mode":"js","data":null,"name":null},{"id":5186,"value":"resetServer = () => { mutable __LEAN_SERVER_RESTARTS += 1; }","pinned":false,"mode":"js","data":null,"name":null},{"id":1288,"value":"md`
Click here to see the server's main properties\n\n- The server object has several [\\`Event\\`](https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/event.ts) channels (\\`error\\`, \\`allMessages\\`, \\`tasks\\`) to which you can attach listener callbacks using \\`event.on()\\`. Each \\`event.on()\\` method returns a \\`handler\\` object with a \\`.dispose()\\` method which can be used to remove the listener from the event. (Note that the \\`tasks\\` event never fires for Lean compiled with Emscripten.)\n- The \\`currentSeqNum\\` property is the ID of the last response received from the Lean server and \\`currentMessages\\` is an array of the error, warning, and informational messages that apply to the files in the server's current [\"range of interest\"](#RangeOfInterest). \n- The \\`sentRequests\\` map consists of requests sent to the server which are still being processed (or which have gotten stuck in some other way). \n- The \\`conn\\` property is the connection to the \\`WebWorkerTransport\\` object. \n`","pinned":false,"mode":"js","data":null,"name":null},{"id":3727,"value":"md`The server object's [main methods](#ServerCommands) will be discussed in the next section.`","pinned":false,"mode":"js","data":null,"name":null},{"id":1291,"value":"md`The following cell controls whether messages to and from the server will be logged to the browser dev console by default. The [\\`leanControl\\` form](#ServerForm) below allows you to change this without restarting the server, so \\`logByDefault\\` is here mainly for use with Observable's [\\`import...with\\` syntax](https://observablehq.com/@observablehq/introduction-to-imports) to make importing the \\`server\\` cell from this notebook a little more configurable.`","pinned":false,"mode":"js","data":null,"name":null},{"id":1133,"value":"logByDefault = false","pinned":false,"mode":"js","data":null,"name":null},{"id":1489,"value":"md`Here's a cell using Observable's [\\`Generators.observe\\`](https://github.com/observablehq/stdlib/#Generators_observe) function that reactively updates whenever the server fires its \\`allMessages\\` event:`","pinned":false,"mode":"js","data":null,"name":null},{"id":205,"value":"leanCurrentMessages = Generators.observe(notify => {\n const {dispose} = server.allMessages.on(m => notify(m.msgs));\n notify(server.currentMessages);\n return dispose;\n}) ","pinned":false,"mode":"js","data":null,"name":null},{"id":1494,"value":"md`The following object, \\`libmeta\\`, contains meta information about the \\`.olean\\` files contained in the \\`.zip\\` file loaded by the server. Its keys are:\n- \\`info\\`: URL prefixes to github repos for the Lean packages (includes the precise commits used)\n- \\`oleanmap\\`: an object whose keys correspond to the olean files and whose values are their corresponding Lean package keys in \\`libmeta.info\\`\n\nThis info is contained in two JSON files generated alongside the library bundle which are used to assist with caching in IndexedDB. They are expected to be in the same directory as the library ZIP file.`","pinned":false,"mode":"js","data":null,"name":null},{"id":1154,"value":"libmeta = {\n const url = transportOpts.libraryZip.slice(0,-3);\n return {\n info: await fetch(`${url}info.json`).then(res => res.json()),\n oleanmap: await fetch(`${url}olean_map.json`).then(res => res.json()),\n };\n}","pinned":false,"mode":"js","data":null,"name":null},{"id":3059,"value":"md`You can inspect the imports below; the \\`list\\` field contains an array of names and the \\`tree\\` field contains an object reflecting the directory structure:`","pinned":false,"mode":"js","data":null,"name":null},{"id":3062,"value":"libraryFiles = {\n const keys = Object.keys(libmeta.oleanmap).map(s => s.replace(/\\//g,'.'));\n const dir = {};\n for (let j = 0; j < keys.length; j++) { \n const file = keys[j].split('.');\n let obj = dir;\n while (file.length > 1) {\n const part = file.shift();\n if (typeof obj[part] !== 'object') {\n obj[part] = (obj[part] !== undefined) ? {'.': obj[part]} : {};\n }\n obj = obj[part];\n }\n obj[file[0]] = keys[j];\n }\n return {list:keys, tree:dir};\n}","pinned":false,"mode":"js","data":null,"name":null},{"id":3070,"value":"md`The following function uses the meta files to get a link to the source file on github corresponding to a given import.`","pinned":false,"mode":"js","data":null,"name":null},{"id":1456,"value":"resolveLeanURL = (file) => `${libmeta.info[libmeta.oleanmap[file]]}${file}.lean`","pinned":false,"mode":"js","data":null,"name":null},{"id":1431,"value":"md`For example, the source \\`.lean\\` file for \\`library/init/data/set.olean\\` in the ZIP file can be found at:`","pinned":false,"mode":"js","data":null,"name":null},{"id":3067,"value":"setLeanURL = resolveLeanURL('init/data/set')","pinned":true,"mode":"js","data":null,"name":null},{"id":1462,"value":"md`We can then fetch the Lean file into an Observable cell:`","pinned":false,"mode":"js","data":null,"name":null},{"id":1465,"value":"setLean = fetch(setLeanURL).then(res => res.text())","pinned":true,"mode":"js","data":null,"name":null},{"id":1459,"value":"md`The Lean server also returns Github links in the \\`source\\` property when responding to \\`server.search\\` and \\`server.info\\` queries.`","pinned":false,"mode":"js","data":null,"name":null},{"id":1245,"value":"Controlling = md`## 2. Controlling the Lean server\n\nIn this section, I'll demonstrate how to interact with the Lean server in Observable.`","pinned":false,"mode":"js","data":null,"name":null},{"id":2611,"value":"ServerForm = md`### Server control form\n\nThe \\`leanControl\\` gadget has several elements that are helpful in debugging and troubleshooting:\n- A checkbox that toggles logging of Lean server messages.\n- A button to Reset \"opened files\", which will be discussed [later in this section](#RangeOfInterest).\n- A button that resets the Lean server.\n- A button to delete the ZIP file cache in your browser's IndexedDB store. (Using this will trigger a redownload of the library bundle; this is only necessary if the cache somehow gets out of sync or becomes corrupted.)\n- A button to delete the cached JS/WASM files. It may be necessary to click this if the version of Emscripten Lean has recently been updated but your browser is still using an old cached version.\n\nThe cells which implement these controls follow. They appear blank because their output HTML elements are referenced in the \\`leanControl\\` form beneath them.\n`","pinned":false,"mode":"js","data":null,"name":null},{"id":621,"value":"serverLogging = {\n const id = DOM.uid('leanLog').id;\n // state persists after server reset\n const check = html``;\n const form = html`${check}