{"id":"a91d5a34a2b26424","slug":"lean-websocketd","trashed":false,"description":"","likes":6,"publish_level":"public","forks":0,"fork_of":null,"has_importers":true,"update_time":"2020-02-03T02:01:30.124Z","first_public_version":null,"paused_version":null,"publish_time":"2019-07-31T17:53:30.737Z","publish_version":362,"latest_version":362,"thumbnail":"add9fd6545dcd3087ff28e21120d45c21be09ff2adeed3b0c26ac9e8e8be3973","default_thumbnail":"add9fd6545dcd3087ff28e21120d45c21be09ff2adeed3b0c26ac9e8e8be3973","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":362,"title":"Connect Observable notebooks to Lean on your computer with websocketd","license":null,"copyright":"","nodes":[{"id":0,"value":"md`# Connect Observable notebooks to Lean on your computer with websocketd\n\nThis notebook allows you to connect the Observable [Lean editor](https://observablehq.com/@bryangingechen/hello-lean-prover) to Lean running locally.\n\nTo use this, you'll of course need to have [installed Lean](https://github.com/leanprover-community/mathlib#installation) on your computer. You'll also need to download and install [websocketd](http://websocketd.com/) and put it in your terminal's PATH (on Macs with [Homebrew](https://brew.sh/) you can type \\`brew install websocketd\\`).\n\nAssuming you've done all that, here are the instructions. If you're using Chrome, this should be fairly easy:\n\nIn your terminal, navigate to the directory containing the Lean package you want to use (e.g. one with all the imports that the notebook you're using relies on) and enter:\n\\`\\`\\`bash\n> websocketd --port=43263 lean --server -M4096\n\\`\\`\\`\n(If for some reason you want to use a different port, be sure to override [\\`wsUrl\\`](#wsUrl) as well. Additional command-line options for \\`websocketd\\` can be found [here](https://github.com/joewalnes/websocketd/wiki/Command-line-options).)\n\nNow you're ready to use your computer's copy of Lean in place of Emscripten-Lean in any Observable notebook using the Lean editor! (See below if you're using Firefox or Safari.) Simply replace:\n\n\\`'@bryangingechen/hello-lean-prover'\\` \n\nwith \n\n\\`'@bryangingechen/lean-websocketd'\\` \n\nin the import cell. For convenience, here's an import statement with the main \"exports\":\n\\`\\`\\`js\nimport {leanEditor, leanEditorFrom, InfoView, LeanFile, leanControl, leanHL, parseLeanMsgs} \n from '@bryangingechen/lean-websocketd'\n\\`\\`\\`\n\nAs far as I know, it's not possible to restart the Lean server from the browser. If something goes wrong, you'll have to hit Ctrl+C in the terminal to kill the \\`websocketd\\` command and then run it again. Then you'll have to restart the server connection in the browser. I thus recommend placing the \\`leanControl\\` form somewhere in the notebook so that you can reconnect to Lean with the click of a button.\n\n⚠️ [Firefox](https://stackoverflow.com/questions/11768221/firefox-websocket-security-issue) and [Safari](https://bugs.webkit.org/show_bug.cgi?id=89068#c13) do not allow unsecured WebSocket connections to \\`localhost\\` from HTTPS-secured origins.\n\nIn Firefox, an easy solution is to navigate to [about:config](about:config) and set \\`network.websocket.allowInsecureFromHTTPS\\` to \\`true\\`; you may want to set this back after you're done unless you really know what you're doing though.\n\nAnother solution (which you'll have to use if you're using Safari) is to follow the instructions [here](https://letsencrypt.org/docs/certificates-for-localhost/) to create and self-sign a certificate for \\`localhost\\`. Then change \\`wsUrl\\` to \\`'wss://localhost:43263'\\` and run the following command instead of the one above:\n\\`\\`\\`bash\n> websocketd --port=43263 --devconsole -ssl -sslcert /path/to/localhost.crt -sslkey /path/to/localhost.key \n lean --server -M4096\n\\`\\`\\`\n`","pinned":false,"mode":"js","data":null,"name":null},{"id":222,"value":"md`## Testing`","pinned":false,"mode":"js","data":null,"name":null},{"id":86,"value":"leanControl","pinned":false,"mode":"js","data":null,"name":null},{"id":149,"value":"leanEditor({}, invalidation)","pinned":true,"mode":"js","data":null,"name":null},{"id":41,"value":"leanEditor({\n value: `-- import .src.scratch`,\n}, invalidation)","pinned":true,"mode":"js","data":null,"name":null},{"id":209,"value":"md`## Implementation`","pinned":false,"mode":"js","data":null,"name":null},{"id":34,"value":"import {leanEditor, leanEditorFrom, InfoView, LeanFile, leanControl, leanHL, parseLeanMsgs,\n lean, serverReset, currentlyRunning, config, CoalescedTimer, CSS_CLASSES, \n __LEAN_SERVER_RESTARTS, resetOpenLeanFiles,logByDefault } \n with {transport, deleteIdb, deleteJSWasm, attachRunningHandlers, server} \n from '@bryangingechen/hello-lean-prover'","pinned":true,"mode":"js","data":null,"name":null},{"id":261,"value":"md`These two cells override some buttons which aren't relevant when not using the Emscripten build of Lean.`","pinned":false,"mode":"js","data":null,"name":null},{"id":89,"value":"deleteIdb = ''","pinned":false,"mode":"js","data":null,"name":null},{"id":92,"value":"deleteJSWasm = ''","pinned":false,"mode":"js","data":null,"name":null},{"id":264,"value":"md`The following cell holds the URL to the local websocket server that's created by the above \\`websocketd\\` command: \n\n[Note that if you need to change this URL from localhost to some other for whatever reason, you will need to use a \\`wss:\\` URL (even if you're using Chrome). See the instructions above to acquire a self-signed certificate if necessary.]`","pinned":false,"mode":"js","data":null,"name":null},{"id":30,"value":"wsUrl = 'ws://localhost:43263'","pinned":true,"mode":"js","data":null,"name":null},{"id":269,"value":"md`This cell implements a \\`Transport\\` object for the \\`lean-client-js\\` \\`Server\\` class using the browser's WebSocket API. One caveat is that \\`websocketd\\` only reads from \\`stdout\\` and not \\`stderr\\`. This is probably OK since I don't think Lean's server mode makes any use of it.\n`","pinned":false,"mode":"js","data":null,"name":null},{"id":9,"value":"transport = {\n // https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/transport.ts\n /* export declare type TransportError = StderrError | ConnectError;\nexport interface Transport {\n connect(): Connection;\n}\nexport interface Connection {\n error: Event;\n jsonMessage: Event;\n alive: boolean;\n send(jsonMsg: any): any;\n dispose(): any;\n} */\n const { Event } = lean;\n\n function connect() {\n const error = new Event();\n const jsonMessage = new Event();\n const ws = new WebSocket(wsUrl);\n const conn = { error, jsonMessage, alive: true, send, dispose, ws };\n let opened = false;\n let openResolve = null;\n const openedPromise = new Promise(resolve => (openResolve = resolve));\n ws.onopen = () => {\n openResolve();\n opened = true;\n console.log(`Lean websocket connected at ${wsUrl}`);\n };\n ws.onmessage = ({ data }) => {\n try {\n jsonMessage.fire(JSON.parse(data));\n } catch (e) {\n error.fire({\n error: 'connect',\n message: `cannot parse: ${data}, error: ${e}`\n });\n }\n };\n ws.onerror = e => {\n error.fire({ error: 'websocketError' }); // websocket errors don't give much info: https://www.w3.org/TR/websockets/#concept-websocket-close-fail\n };\n ws.onclose = () => {\n conn.alive = false;\n };\n function send(msg) {\n if (!opened) openedPromise.then(() => ws.send(JSON.stringify(msg)));\n else ws.send(JSON.stringify(msg));\n }\n function dispose() {\n ws.close();\n }\n return conn;\n }\n return { connect };\n}","pinned":true,"mode":"js","data":null,"name":null},{"id":274,"value":"md`We override the \\`server\\` object with a few changes. The server object fires an error message when the websocket connection closes. These messages trigger the Lean editor to check if its server is alive and to change its background color if it's dead. Also, the server object is no longer wrapped in a promise as in the parent notebook to allow the notebook to \"fail fast\" if a websocket connection cannot be made.`","pinned":false,"mode":"js","data":null,"name":null},{"id":197,"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 try {\n server.connect();\n } catch (e) {\n console.log('Lean server: WebSocket connection failed!');\n return fakeServer;\n }\n\n server.conn.ws.addEventListener('close', () => {\n server.error.fire('Lean websocket closed');\n });\n return Generators.disposable(server, server => {\n console.log('disposing lean server...');\n server.dispose(); // dispose server when cell is invalidated\n });\n}","pinned":true,"mode":"js","data":null,"name":null},{"id":278,"value":"md`This function sets the background to orange when the Lean server is busy and also draws orange lines next to lines that are reported by the Lean server's \\`tasks\\` channel.`","pinned":false,"mode":"js","data":null,"name":null},{"id":158,"value":"function attachRunningHandlers({editor, node, fileName, opts}) {\n const containerDiv = node.querySelector(`.${CSS_CLASSES.LEAN_EDITOR_CONTAINER}`);\n const decoTimer = new CoalescedTimer();\n return [\n currentlyRunning.updated.on((files) => {\n containerDiv.className = `${CSS_CLASSES.LEAN_EDITOR_CONTAINER} ${files.length ? CSS_CLASSES.RUNNING : CSS_CLASSES.DONE}`;\n }),\n // tasks as orange lines in the gutter\n server.tasks.on(({tasks, is_running}) => {\n decoTimer.do(0 && config.debounceAllMessages, () => {\n const min_line = opts.lineNumberFormatter(1);\n const filteredTasks = tasks.filter(({file_name}) => file_name === fileName);\n if (filteredTasks.length) {\n filteredTasks.map(({pos_line, end_pos_line}) => {\n for (let j=0; j= pos_line || j+min_line < end_pos_line) {\n editor.addLineClass(j, \"gutter\", `${CSS_CLASSES.CODE_MIRROR_GUTTER_BUSY}`);\n } else {\n editor.removeLineClass(j, \"gutter\", `${CSS_CLASSES.CODE_MIRROR_GUTTER_BUSY}`);\n }\n }\n });\n } else {\n for (let j=0; j false,\n roi: () => {},\n fake: true\n})","pinned":true,"mode":"js","data":null,"name":null},{"id":237,"value":"// https://observablehq.com/@observablehq/how-to-embed-a-notebook-in-a-react-app#styles\nhtml`