31:T899,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). A 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/). These three online books are also good sources for introductory material about Lean: - ["Theorem Proving in Lean"](https://leanprover.github.io/theorem_proving_in_lean/) by Jeremy Avigad, Leonardo de Moura and Soonho Kong - ["Logic and Proof"](https://avigad.github.io/logic_and_proof/) by Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn. - 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. The 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. ⚠️ 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! Here'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)): `32:T5d9,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.

👉 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.

For 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): \`\`\`js import {leanEditor, leanEditorFrom, InfoView, LeanFile, leanControl, leanHL, parseLeanMsgs} from '@bryangingechen/hello-lean-prover' \`\`\` ⚡️ 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)! Feel 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! `33:T803,md`### Related work: The 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. Patrick 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. The [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. Wylie 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)).`34:T9b9,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). This 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). ⚠️ \`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. Currently, 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. The 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/).`35:T419,md`

Click here to see the server's main properties

- 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.) - 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). - The \`sentRequests\` map consists of requests sent to the server which are still being processed (or which have gotten stuck in some other way). - The \`conn\` property is the connection to the \`WebWorkerTransport\` object. `36:Td1f,ServerCommands = md`### Server commands

Click here to see a list of the primary Lean server commands:

The main method for communicating with the Lean server is [\`server.send(req)\`](https://github.com/leanprover/lean-client-js/blob/83f190d044502d1cd39f320ef15da5357547d539/lean-client-js-core/src/server.ts#L48). Here's its type from that source file: \`\`\`js send(req: Request): Promise \`\`\` This sends the given request object [(see the interfaces which extend \`Request\` here)](https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/commands.ts) to the server and returns a promise that resolves when the server sends a response message (see the interfaces extending \`Response\` in that link). This class doesn't use the Language Service Protocol, unfortunately, (though there is [a LSP implementation in the \`lean-client-js\` repository](https://github.com/leanprover/lean-client-js/tree/master/lean-language-server)). It's easier to use the command-specific wrappers for \`send\`, which look like this: - \`\`\`js info(file: string, line: number, column: number): Promise \`\`\` returns type info, docstrings, tactic state at a position in the file, called in [\`leanEditor()\`](#leanEditor) to display information about the file at the cursor and when hovering ⚠️ The Lean server works with positions where the line numbers are 1-indexed and column numbers are 0-indexed! - \`\`\`js sync(file: string, contents: string): Promise \`\`\` sync a Lean file with the server, called in [\`leanEditor()\`](#leanEditor) when a file is edited - \`\`\`js complete(file: string, line: number, column: number, skipCompletions?: boolean): Promise \`\`\` return completion suggestions at a position in the file, used in [\`leanEditor()\`](#leanEditor) via CodeMirror's ["hint" addon](https://codemirror.net/doc/manual.html#addon_show-hint) - \`\`\`js search(query: string): Promise \`\`\` search the current Lean environment for declarations matching the given string - \`\`\`js allHoleCommands(file: string): Promise \`\`\` return hole commands for the entire document (Hole commands are info or edit operations that the Lean editor can perform on the source. They are like "code actions" in VS Code. [Here's](https://github.com/leanprover-community/mathlib/blob/64431ae841f14108f0d1c4a6c3f519c23e95fb80/docs/holes.md) a very incomplete doc on hole commands provided by mathlib.) - \`\`\`js holeCommands(file: string, line: number, column: number): Promise \`\`\` return hole commands for a position in the file, used in [\`leanEditor()\`](#leanEditor) via CodeMirror's ["hint" addon](https://codemirror.net/doc/manual.html#addon_show-hint) - \`\`\`js hole(file: string, line: number, column: number, action: string): Promise \`\`\` perform a hole command; returns a message or a replacement (edit) to be applied to the file, used in [\`leanEditor()\`](#leanEditor) via CodeMirror's ["hint" addon](https://codemirror.net/doc/manual.html#addon_show-hint) - \`\`\`js roi(mode: CheckingMode, files: FileRoi[]): Promise \`\`\` change the "range of interest" of the server, see [below](#RangeOfInterest) `37:T61a,RangeOfInterest = md`### Range of interest syncing The Lean server can sync with multiple files at once, which means we can "open" several different files on a page without having to open new instances of the server. By default, the Lean server responds with messages for every file that has been opened since it was started. Currently, there doesn't seem to be a way to actually "close" a file in the Lean server. However, we can get it to stop processing and reporting messages on a file by removing the file from the server's "range of interest" using [the \`server.roi()\` method](https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/server.ts#L103). The \`vscode-lean\` extension [uses this feature](https://github.com/leanprover/vscode-lean/blob/master/src/roi.ts) to allow users to specify that Lean processes only "visible" lines or "visible and above" lines, among several more standard options. In this notebook we use only the \`'open-files'\` ROI mode. The functions below are used to keep track of the files that are in the server's ROI in a Map object; this is used to ensure that (parts of) Lean files are not being modified by more than one editor or \`LeanFile\` object at a time. ⚠️ If \`openLeanFiles\` falls out of sync with the editor instances / \`LeanFile\` objects on the page, this will result in errors stating that some file is already open when it isn't. Clicking the \`roiReset\` button in the [\`LeanControls\` form](#LeanControls) above (or calling \`resetOpenLeanFiles\') should fix things. `38:Tecf,class LeanFile { constructor(opts, invPromise) { __OPEN_LEAN_FILES_RESETS; // re-run when open lean files are reset if (opts.value !== undefined && typeof opts.value !== 'string') throw new Error(`LeanFile: value must be string (currently: ${opts.value}`); if (opts.fileName !== undefined && typeof opts.fileName !== 'string') throw new Error(`LeanFile: fileName must be string (currently: ${opts.fileName}`); if (!(invPromise instanceof Promise)) throw new Error(`LeanFile: second argument must be an invalidation promise (currently: ${invPromise})`); const fileName = opts.fileName || DOM.uid('lean').id; if (openLeanFiles.has(fileName)) { throw new Error(`LeanFile: ${fileName} already opened`); } openLeanFiles.set(fileName, true); invPromise.then(() => { openLeanFiles.delete(fileName); roiSync(); }); Object.defineProperties(this, { opts: { value: opts, enumerable: true, }, fileName: { value: fileName, enumerable: true, }, _firstSync: { value: false, writable: true, }, _hasSynced: { value: () => { if (!this._firstSync) throw new Error(`call the async method '.sync()' to sync the value with the server before working with this object`); if (!server.alive()) { server.error.fire('LeanFile: server is not alive (_hasSynced)'); throw new Error(`Server is not alive!`); } }, }, _updateMsgs: { value: (msgArr) => { this._msgs = msgArr.filter(msg => msg.file_name === this.fileName); }, }, _value: { writable: true, }, _msgs: { writable: true, }, }); const msgsTimer = new CoalescedTimer(); const msgsHandler = server.allMessages.on(({msgs}) => { msgsTimer.do(config.debounceAllMessages, () => { this._updateMsgs(msgs); }); }); invPromise.then(() => { msgsHandler.dispose(); }); } get value() { this._hasSynced(); return this._value; } set value(v) { throw new Error(`to set the value, use the async method 'sync(value)'`); } sync(v) { addToRunning(this.fileName); return server.sync(this.fileName, v || (this.opts.value || config.defaultValue)).then( () => { removeFromRunning(this.fileName); this._value = v || (this.opts.value || config.defaultValue); if (!this._firstSync) { // add to 'open-files' ROI return roiSync().then(() => { this._firstSync = true; this._updateMsgs(server.currentMessages); return this; }); } return this; }, (e) => { console.log(`LeanFile ${this.fileName} sync failed: ${e}`); if (!server.alive()) { server.error.fire('LeanFile: server is not alive (sync)'); throw new Error(`Server is not alive!`); } return this; } ); } get msgs() { this._hasSynced(); return this._msgs; } set msgs(m) { throw new Error(`msgs is read-only!`); } info(line, column) { this._hasSynced(); return server.info(this.fileName, line, column); } complete(line, column, skipCompletions) { this._hasSynced(); return server.complete(this.fileName, line, column, skipCompletions); } allHoleCommands() { this._hasSynced(); return server.allHoleCommands(this.fileName); } holeCommands(line, column) { this._hasSynced(); return server.holeCommands(this.fileName, line, column); } hole(line, column, action) { this._hasSynced(); return server.hole(this.fileName, line, column, action); } }39:T1fd4,initCodeMirrorLeanMode = CodeMirror => { CodeMirror.defineMode(LEAN_MODE, function(_config, modeConfig) { function switchState(source, setState, state, f) { setState(f); return f(source, setState, state); } const digitRE = /\d/; const hexitRE = /[0-9A-Fa-f]/; const whiteCharRE = /[ \t\v\f]/; // newlines are handled in tokenizer const defBeginRE = /^(inductive|coinductive|structure|theorem|axiom|axioms|abbreviation|lemma|definition|def|instance|class|constant)/; const escapedSingleCharRE = /^'(\\\\(x[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'/; const keywordOtherRE = /^(import|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd|restate_axiom|calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from|λ *|∀ *|Π *|∃ *|Σ *|if|then|else)(?!\.)\b/; // const operatorsRE = /^==?|>{0,3}=|>{1,3}|<[\|$]>|<[\*=<]?|<<=|≥|≤|!|~|\?|:=?|←|→|\$|\+|\*|&[&=]?|\|[\|=]?/; function normal(source, setState, state) { if (source.sol()) state.lastChar = null; // must reset lastChar at start of new line if (source.eatWhile(whiteCharRE)) { state.lastChar = source.peek() && ' '; return null; } if (source.match(/^--/)) { source.skipToEnd(); state.lastChar = null; return 'comment'; } if (source.match('/-')) { if (source.peek() === '-' || source.peek() === '!') { // doc or module comment source.next(); setState(docComment); return 'comment'; } return switchState( source, setState, state, ncomment("comment", 1, state) ); } if (!state.lastChar || !state.lastChar.match(/\w/)) { // \b if (source.match(/^(Prop|Type|Sort)\b/)) { state.lastChar = source.peek() && 'a'; return "builtin"; } // \b if (source.match(/^attribute\b\s*\[[^\]]*\]/)) { state.lastChar = source.peek() && ']'; return "attribute"; } // \b if (source.match(/^@\[[^\]]*\]/)) { state.lastChar = source.peek() && ']'; return "attribute"; } // \b if (source.match(/^sorry\b/)) { state.lastChar = source.peek() && 'y'; return "error"; } if (state.lastChar !== '.') { // \b no '.' if ( source.match(/^(private|meta|mutual|protected|noncomputable)\b/) ) { state.lastChar = source.peek() && 'a'; return "keyword"; } // \b no '.' if (source.match(defBeginRE)) { setState(defCommand); return "keyword"; } // \b no '.' if (source.match(keywordOtherRE)) { state.lastChar = source.peek() && 'a'; return 'keyword'; } } } // if (source.match(operatorsRE)) { // state.lastChar = null; // return "operator"; // } if ( source.match( /^#print\s+(def|definition|inductive|instance|structure|axiom|axioms|class)\b/ ) ) { state.lastChar = source.peek() && 'a'; return 'meta'; } if (source.match(/^#(print|eval|reduce|check|help|exit|find|where)\b/)) { state.lastChar = source.peek() && 'a'; return 'meta'; } if (source.eat('"')) { state.lastChar = source.peek() && '"'; return switchState(source, setState, state, stringLiteral); } if (source.match(/^'[^\\\\']'/) || source.match(escapedSingleCharRE)) { state.lastChar = source.peek() && '\''; return "string-2"; } if (source.match(/^([0-9]+|0([xX][0-9a-fA-F]+))\b/)) { state.lastChar = source.peek() && '0'; return "number"; } const ch = source.next(); state.lastChar = ch; return null; } function defCommand(source, setState, state) { if (source.eatWhile(whiteCharRE)) return null; if (source.sol()) state.lastChar = null; if (source.match(/^--/)) { source.skipToEnd(); state.lastChar = null; return 'comment'; } if (source.match('/-')) { return switchState( source, setState, state, ncomment("comment", 1, state, defCommand) ); } if (source.match(/^with\b|^extends\b|^[:\|$\[\{⦃<>]/, false)) { setState(normal); state.lastChar = source.peek() && 'a'; return null; } if (!state.lastChar || !state.lastChar.match(/\w/)) { // \b if (source.match(/^[^:«»\($\{\} \t\v\f=→λ∀?][^:«»\{\} \t\v\f]*/)) { setState(normal); state.lastChar = source.peek() && 'a'; return 'def'; } } if (source.eat("«")) { state.lastChar = source.peek() && "»"; return switchState(source, setState, state, defInDoubleAngle); } return null; } function defInDoubleAngle(source, setState, state) { if (source.eat("»")) { setState(defCommand); return null; } source.next(); return 'def'; } function docComment(source, setState, state) { if (source.match('-/')) { setState(normal); state.lastChar = source.peek() && '/'; return 'comment'; } source.next(); return 'comment'; } function ncomment(type, nest, state, returnState = normal) { if (nest == 0) { state.lastChar = '/'; return returnState; } return function(source, setState, state) { let currNest = nest; while (!source.eol()) { const ch = source.next(); if (ch == '/' && source.eat('-')) { ++currNest; } else if (ch == '-' && source.eat('/')) { --currNest; if (currNest == 0) { setState(returnState); state.lastChar = source.peek() && '/'; return type; } } } setState(ncomment(type, currNest, state, returnState)); return type; }; } function stringLiteral(source, setState, state) { while (!source.eol()) { const ch = source.next(); if (ch == '"') { setState(normal); return "string"; } if (ch == '\\') { if ( source.eat('\\') || source.eat('\"') || source.eat('n') || source.eat('t') || source.eat('\'') ) return "string"; else if (source.eat('x')) { source.next(); // should really match only 0-9a-fA-F here and below... source.next(); return "string"; } else if (source.eat('u')) { source.next(); source.next(); source.next(); source.next(); return "string"; } } } setState(normal); return "string error"; } return { startState: function() { return { f: normal, lastChar: null }; }, copyState: function(s) { return { f: s.f, lastChar: s.lastChar }; }, token: function(stream, state) { // second argument below is "setState"; it changes the state function (but not lastChar) return state.f( stream, function(s) { state.f = s; }, state ); }, blockCommentStart: "/-", blockCommentEnd: "-/", lineComment: "--" }; }); CodeMirror.defineMIME("text/lean", "lean"); }3a:T2e0d,initCodeMirrorLeanLint = CodeMirror => { var GUTTER_ID = "CodeMirror-lint-markers"; function showTooltip(e, content) { var tt = document.createElement("div"); tt.className = CSS_CLASSES.CODE_MIRROR_LINT_TOOLTIP; tt.appendChild(content.cloneNode(true)); document.body.appendChild(tt); function position(e) { if (!tt.parentNode) return CodeMirror.off(document, "mousemove", position); tt.style.top = Math.max(0, e.clientY - tt.offsetHeight - 5) + "px"; tt.style.left = e.clientX + 5 + "px"; } CodeMirror.on(document, "mousemove", position); position(e); if (tt.style.opacity != null) tt.style.opacity = 1; return tt; } function rm(elt) { if (elt.parentNode) elt.parentNode.removeChild(elt); } function hideTooltip(tt) { if (!tt.parentNode) return; if (tt.style.opacity == null) rm(tt); tt.style.opacity = 0; setTimeout(function() { rm(tt); }, 600); } // for gutter: function showTooltipFor(e, content, node) { var tooltip = showTooltip(e, content); function hide() { CodeMirror.off(node, "mouseout", hide); if (tooltip) { hideTooltip(tooltip); tooltip = null; } } var poll = setInterval(function() { if (tooltip) for (var n = node; ; n = n.parentNode) { if (n && n.nodeType == 11) n = n.host; if (n == document.body) return; if (!n) { hide(); break; } } if (!tooltip) return clearInterval(poll); }, 400); CodeMirror.on(node, "mouseout", hide); } // for onMouseMove: function showTooltipForMove(e, content, node) { var tt = document.createElement("div"); tt.className = CSS_CLASSES.CODE_MIRROR_LINT_TOOLTIP; tt.appendChild(content.cloneNode(true)); document.body.appendChild(tt); // TODO: don't let tooltip go outside of editor div tt.style.top = Math.max(0, e.clientY - tt.offsetHeight - 5) + "px"; tt.style.left = e.clientX + 5 + "px"; if (tt.style.opacity != null) tt.style.opacity = 1; function hide() { CodeMirror.off(document, "mousemove", hide); rm(tt); } CodeMirror.on(document, "mousemove", hide); } function LintState(cm, options, hasGutter) { this.marked = []; this.options = options; this.timeout = null; this.hoverTimeout = null; this.hasGutter = hasGutter; if (options.delay) { this.onMouseMove = function(e) { onMouseMoveWithDelay(cm, e); }; } else { this.onMouseMove = function(e) { onMouseMove(cm, e); }; } this.waitingFor = 0; } function parseOptions(_cm, options) { if (options instanceof Function) return { getAnnotations: options }; if (!options || options === true) options = {}; return options; } function clearMarks(cm) { var state = cm.state.lint; if (state.hasGutter) cm.clearGutter(GUTTER_ID); for (var i = 0; i < state.marked.length; ++i) state.marked[i].clear(); state.marked.length = 0; } function makeMarker(labels, severity, multiple, tooltips) { var marker = document.createElement("div"), inner = marker; marker.className = "CodeMirror-lint-marker CodeMirror-lint-marker-" + severity; if (multiple) { inner = marker.appendChild(document.createElement("div")); inner.className = "CodeMirror-lint-marker CodeMirror-lint-marker-multiple"; } if (tooltips != false) CodeMirror.on(inner, "mouseover", function(e) { showTooltipFor(e, labels, inner); }); return marker; } function getMaxSeverity(a, b) { if (a == "error") return a; else return b; } function groupByLine(annotations) { var lines = []; for (var i = 0; i < annotations.length; ++i) { var ann = annotations[i], line = ann.from.line; (lines[line] || (lines[line] = [])).push(ann); } return lines; } function annotationTooltip(ann) { var severity = ann.severity; if (!severity) severity = "error"; var tip = document.createElement("div"); tip.className = "CodeMirror-lint-message CodeMirror-lint-message-" + severity; if (typeof ann.messageHTML != 'undefined') { tip.innerHTML = ann.messageHTML; } else if (typeof ann.messageNode != 'undefined') { tip.appendChild(ann.messageNode.cloneNode(true)); // cloneNode added to fix gutter tooltip disappearing after hovering on underlined text (possible bug in CodeMirror?) } else { tip.appendChild(document.createTextNode(ann.message)); } return tip; } function lintAsync(cm, getAnnotations, passOptions) { var state = cm.state.lint; var id = ++state.waitingFor; function abort() { id = -1; cm.off("change", abort); } cm.on("change", abort); getAnnotations( cm.getValue(), function(annotations, arg2) { cm.off("change", abort); if (state.waitingFor != id) return; if (arg2 && annotations instanceof CodeMirror) annotations = arg2; cm.operation(function() { updateLinting(cm, annotations); }); }, passOptions, cm ); } function startLinting(cm) { var state = cm.state.lint, options = state.options; /* * Passing rules in `options` property prevents JSHint (and other linters) from complaining * about unrecognized rules like `onUpdateLinting`, `delay`, `lintOnChange`, etc. */ var passOptions = options.options || options; var getAnnotations = options.getAnnotations || cm.getHelper(CodeMirror.Pos(0, 0), "lint"); if (!getAnnotations) return; if (options.async || getAnnotations.async) { lintAsync(cm, getAnnotations, passOptions); } else { var annotations = getAnnotations(cm.getValue(), passOptions, cm); if (!annotations) return; if (annotations.then) annotations.then(function(issues) { cm.operation(function() { updateLinting(cm, issues); }); }); else cm.operation(function() { updateLinting(cm, annotations); }); } } function updateLinting(cm, annotationsNotSorted) { clearMarks(cm); var state = cm.state.lint, options = state.options; var annotations = groupByLine(annotationsNotSorted); for (var line = 0; line < annotations.length; ++line) { var anns = annotations[line]; if (!anns) continue; var maxSeverity = null; var tipLabel = state.hasGutter && document.createDocumentFragment(); // cf. popupTooltips for (var i = 0; i < anns.length; ++i) { var ann = anns[i]; var severity = ann.severity; if (!severity) severity = "error"; maxSeverity = getMaxSeverity(maxSeverity, severity); if (options.formatAnnotation) ann = options.formatAnnotation(ann); if (state.hasGutter) tipLabel.appendChild(annotationTooltip(ann)); if (ann.to) state.marked.push( cm.markText(ann.from, ann.to, { className: "CodeMirror-lint-mark CodeMirror-lint-mark-" + severity, __annotation: ann }) ); } if (state.hasGutter) cm.setGutterMarker( line, GUTTER_ID, makeMarker( tipLabel, maxSeverity, anns.length > 1, state.options.tooltips ) ); } if (options.onUpdateLinting) options.onUpdateLinting(annotationsNotSorted, annotations, cm); } function popupTooltips(annotations, e) { var target = e.target || e.srcElement; var tooltip = document.createDocumentFragment(); for (var i = 0; i < annotations.length; i++) { var ann = annotations[i]; tooltip.appendChild(annotationTooltip(ann)); } showTooltipForMove(e, tooltip, target); } function onMouseMoveWithDelay(cm, e) { var state = cm.state.lint, delay = state.options.delay; clearTimeout(state.hoverTimeout); // if (e.srcElement) { // // hack for IE, because e.srcElement failed when it is used in the tiemout function // var newE = {srcElement: e.srcElement, clientX : e.clientX, clientY: e.clientY}; // e = newE; // } state.hoverTimeout = setTimeout(function() { onMouseMove(cm, e); }, delay); } function onMouseMove(cm, e) { var state = cm.state.lint; var target = e.target || e.srcElement; var annotations = []; if (/\bCodeMirror-lint-mark-/.test(target.className)) { var box = target.getBoundingClientRect(), x = (box.left + box.right) / 2, y = (box.top + box.bottom) / 2; var spans = cm.findMarksAt(cm.coordsChar({ left: x, top: y }, "client")); for (var i = 0; i < spans.length; ++i) { // grab annotation object from gutter marks, created in updateLinting var ann = spans[i].__annotation; if (ann) annotations.push(ann); } } const pos = cm.coordsChar({ left: e.clientX, top: e.clientY }); if (!pos.outside && Math.abs(pos.xRel) < 10) // see 'hover' function in leanEditor state.options.hoverProvider(cm, pos, e).then(ann => { // prepends the formatted goal object to the annotations if it exists if (ann) annotations.unshift(ann); // unicode symbol input info const symbol = cm.getRange(pos, { line: pos.line, ch: pos.ch + 1 }); if (symbol) { const symbolAnn = getAbbreviations(symbol); if (symbolAnn) annotations.unshift(symbolAnn); } if (annotations.length) popupTooltips(annotations, e); }); // TODO: allow non-async? // if (annotations.length) popupTooltips(annotations, e); } // see https://github.com/leanprover/vscode-lean/blob/6678cd653d64dc2c775a72b96900c46baba0829b/src/input.ts#L38 function getAbbreviations(symbol) { const abbrevs = []; for (const k in translations) { if (translations[k] === symbol) { abbrevs.push(k); } } return ( abbrevs.length > 0 && { severity: 'warning', message: `Input "${symbol}" by typing ${abbrevs .sort((a, b) => a.length - b.length) .map(a => '"\\' + a + '"') .join(' or ')} and then pressing tab.` } ); } function onChange(cm) { var state = cm.state.lint; if (!state) return; clearTimeout(state.timeout); state.timeout = setTimeout(function() { startLinting(cm); }, state.options.delay || 500); } CodeMirror.defineOption("lint", false, function(cm, val, old) { if (old && old != CodeMirror.Init) { clearMarks(cm); if (cm.state.lint.options.lintOnChange !== false) cm.off("change", onChange); CodeMirror.off( cm.getWrapperElement(), "mouseover", cm.state.lint.onMouseMove ); clearTimeout(cm.state.lint.timeout); delete cm.state.lint; } if (val) { var gutters = cm.getOption("gutters"), hasLintGutter = false; for (var i = 0; i < gutters.length; ++i) if (gutters[i] == GUTTER_ID) hasLintGutter = true; var state = (cm.state.lint = new LintState( cm, parseOptions(cm, val), hasLintGutter )); if (state.options.lintOnChange !== false) cm.on("change", onChange); if (state.options.tooltips != false && state.options.tooltips != "gutter") CodeMirror.on(cm.getWrapperElement(), "mousemove", state.onMouseMove); startLinting(cm); } }); CodeMirror.defineExtension("performLint", function() { if (this.state.lint) startLinting(this); }); }3b:T1039,CMLeanEditor = md`### Lean editor Here are the main features of the Lean editor: - Hovering over text in the editor will display a popup with the following info: - (if hovering over a Unicode character) the relevant [translation strings](#translations), - the type of the term under the mouse pointer and any documentation, - any error, warning or info messages applicable, and - the tactic state at that point (if in tactic mode). - Error, warning, and info messages are marked by icons in the gutter on the left and underlined with squiggly lines. - By default, the Lean editor shows an infoview panel that has two modes: - "Display Goal"

mode: the type / documentation / tactic state at the editor cursor location is displayed. - "Display Messages"

mode: error, warning, and info messages from the Lean server are displayed. - On narrow screens (below ${config.stackWidth}, set by [\`config.stackWidth\`](#ConfigDoc)), the built-in infoview panel will be displayed below the editor, rather than on the right. - Clicking the Save button opens a browser dialog to save the current Lean file to disk. The suggested filename can be changed by changing \`saveFileName\` in the editor value object. - If the editor is not read-only, a Reset button appears. Single-clicking performs a "soft" reset, where the value of the editor is replaced with its original value. This value be changed by changing \`resetValue\` in the editor value object. Double-clicking performs a "hard" reset, which disposes and reinitializes the editor and any [custom header / footer values](#headerFooterDoc). The [Codemirror default keybinds](https://github.com/codemirror/CodeMirror/blob/master/src/input/keymap.js) should work in these editors, with a few additions listed here. For non-read-only editors, the "Toggle toolbar" button will show a toolbar containing the buttons below (the toolbar is shown by default if a mobile browser is detected). - You can input Unicode characters from [this list](#translations) by typing '\`\\\`' before its translation string and then pressing Tab or clicking . For instance, typing '\`\\N\`' and hitting Tab will result in '\`ℕ\`'. Many of the translation strings are LaTeX-inspired, so try those first. You can also hover over a Unicode character to see its translation strings. - Completion suggestions pop up automatically after the server syncs, roughly ${config.delayMs}ms after typing stops (this delay is set by [\`config.delayMs\`](#ConfigDoc)). They can also be requested manually by typing Ctrl+Space or clicking . - Type Ctrl+' or click to insert the \`{!!}\` hole indicator; you can select some text before hitting that key combo and the selection will be placed "inside" the hole. Hole commands will be included in the completions if the cursor is by a hole indicator. - Type Ctrl+/ or click to toggle line comments on a selection. - Type Ctrl+m to toggle the display mode of the infoview panel between showing the goal under the cursor (

) and showing all messages (

). - Type Esc to enable changing focus off the editor by pressing Tab / Shift+Tab (useful for keyboard navigation). Pressing Esc again before changing focus will restore the usual behavior of Tab / Shift+Tab, as does unfocusing and then refocusing the editor.`3c:T4ee3,function leanEditor(opts0, invPromise) { __OPEN_LEAN_FILES_RESETS; // re-run when open lean files are reset const opts = { showToolbar, ...opts0 }; // ----------------- // DOCARRAY CHECKING // ----------------- if ( opts.docArray && (!Array.isArray(opts.docArray) || opts.docArray.length === 0) ) throw new Error( `leanEditor: docArray must be a non-empty array (currently: ${JSON.stringify( opts.docArray )})` ); if ( opts.docArray && (opts.docIndex !== Math.round(opts.docIndex) || opts.docIndex >= opts.docArray.length || opts.docIndex < 0) ) throw new Error( `leanEditor: docIndex must be an integer between 0 and ${opts.docArray .length - 1} (inclusive) (currently: ${opts.docIndex})` ); // Assign opts.value from docArray if (opts.value === undefined) opts.value = (opts.docArray && opts.docArray[opts.docIndex]) || config.defaultValue; // -------------------- // OTHER INPUT CHECKING // -------------------- if (!(invPromise instanceof Promise)) throw new Error( `leanEditor: second argument must be an invalidation promise (currently: ${invPromise})` ); if (opts.infoView && !(opts.infoView instanceof InfoView)) throw new Error( `leanEditor: infoView must be an instance of the InfoView class` ); // ----------------- // FILENAME CHECKING // ----------------- const fileName = opts.fileName || DOM.uid('lean').id.replace(/-/g, '_') + '.lean'; if (openLeanFiles.has(fileName)) { const val = openLeanFiles.get(fileName); if (val === true || !opts.docArray) throw new Error(`leanEditor: ${fileName} already opened`); if (val.has(opts.docIndex)) throw new Error( `leanEditor: index ${opts.docIndex} of ${fileName} already opened` ); } // set openLeanFiles here to prevent race condition if (opts.docArray) { const val = openLeanFiles.get(fileName) || new Set([opts.docIndex]); openLeanFiles.set(fileName, val.add(opts.docIndex)); } else { openLeanFiles.set(fileName, true); } // ensure roi disposal invPromise.then(() => { if (opts.docArray) { const val = openLeanFiles.get(fileName); if (val) { val.delete(opts.docIndex); if (val.size === 0) { openLeanFiles.delete(fileName); } } } else { openLeanFiles.delete(fileName); } roiSync(); }); // -------------------- // EDITOR INSTANCE VARS // -------------------- let editInst; // exposed as div.value.editor let filteredMsgs = []; // contains messages in server.currentMessages which apply to this editor instance, set and updated in msgWidget(), exposed as div.value.msgs // the next 3 variables are used in syncIn() const syncTimer = new CoalescedTimer(); let thisVersion = 0; let firstSync = false; // The following 3 variables are used to set up a promise which resolves on sync responses: // first used to delay server requests until after first sync (in init()) // then used to buffer completion requests (in hint()) let syncPromise; // exposed as div.value.syncPromise let syncTrigger; let syncFired = true; // disposal function let dispose; // set to true when server is not alive let dead = false; // ------------- // HTML ELEMENTS // ------------- // the reset and tool buttons are only displayed if not readOnly const saveButton = html``; saveButton.onclick = () => { const file = new Blob( [ opts.docArray ? opts.docArray.join( opts.splitString !== undefined ? opts.splitString : '\n---\n' ) : editInst.getValue() ], { type: 'text/plain' } ); const a = document.createElement('a'); const url = URL.createObjectURL(file); a.href = url; a.download = div.value.saveFileName; document.body.appendChild(a); a.click(); setTimeout(() => { document.body.removeChild(a); window.URL.revokeObjectURL(url); }, 0); }; const resetButton = html``; // Editing toolbar: const disableReadonly = opts.readOnly ? 'disabled' : ''; const commentButton = html` `; commentButton.onclick = () => { if (!opts.readOnly) { editInst.execCommand('toggleComment'); } editInst.focus(); }; const unicodeButton = html` `; unicodeButton.onclick = () => { if (!opts.readOnly) { unicodeHandler(editInst); } editInst.focus(); }; const completeButton = html` `; completeButton.onclick = () => { if (!opts.readOnly) { editInst.execCommand('autocomplete'); } editInst.focus(); }; const holeButton = html` `; holeButton.onclick = () => { if (!opts.readOnly) { insertHole(editInst); } editInst.focus(); }; const undoButton = html` `; undoButton.onclick = () => { if (!opts.readOnly) { editInst.execCommand('undo'); } editInst.focus(); }; const redoButton = html` `; redoButton.onclick = () => { if (!opts.readOnly) { editInst.execCommand('redo'); } editInst.focus(); }; const toolbar = html` ${commentButton}${unicodeButton}${completeButton}${holeButton}${undoButton}${redoButton} `; const toolButton = html` `; toolButton.onclick = () => { toolbar.style.display = toolbar.style.display === 'none' ? 'inline' : 'none'; opts.showToolbar = !opts.showToolbar; }; // Outer buttons wrapper: const buttonsWrapper = html` ${opts.readOnly ? `` : toolbar} ${opts.readOnly ? `` : toolButton}${ // only show toolbar if not read-only // only show reset button if not read-only or if there's a header or footer opts.readOnly && !opts.header && !opts.footer ? `` : resetButton } ${saveButton} `; const height = opts.height || config.editorHeight; const cmDiv = html`

`; // CodeMirror is appended to this one! const infoView = opts.infoView || new InfoView( { displayMode: opts.displayMode, filterMode: opts.filterMode, className: opts.infoViewClassName, node: opts.infoViewNode }, invPromise ); const containerDiv = html`

${cmDiv}${opts.infoView ? `` : infoView.node}

`; const header = (typeof opts.header === 'function' ? html`` : opts.header) || ` ${fileName} ${ opts.docArray ? ` (${opts.docIndex + 1}/${opts.docArray.length})` : `` }: `; const footer = (typeof opts.footer === 'function' ? html`

` : opts.footer) || ``; const div = html`

${header}${buttonsWrapper}${containerDiv}${footer}

`; div.value = {}; Object.defineProperties(div.value, { opts: { value: opts, enumerable: true }, infoView: { value: infoView, enumerable: true }, node: { value: div, enumerable: true }, editor: { get: () => editInst, enumerable: true }, value: { get: () => editInst.getValue(), enumerable: true }, resetValue: { value: opts.resetValue || opts.value, enumerable: true, writable: true }, syncPromise: { get: () => syncPromise, enumerable: true }, fileName: { value: fileName, enumerable: true }, saveFileName: { value: fileName, enumerable: true, writable: true }, msgs: { get: () => filteredMsgs, enumerable: true }, updateInfoView: { value: updateInfoView, enumerable: true } }); // ------------------------------- // SET BACKGROUND WHEN SERVER DIES // ------------------------------- const errorHandler = server.error.on(() => { if (!server.alive()) die('errorHandler'); }); invPromise.then(() => errorHandler.dispose()); function die(from) { // only called if !server.alive(); if (dead) return; errorHandler.dispose(); dead = true; containerDiv.className = `${CSS_CLASSES.LEAN_EDITOR_CONTAINER} ${CSS_CLASSES.STOPPED}`; if (from !== 'errorHandler') server.error.fire(`Server is dead (${from}): ${fileName}`); } if (!server.alive()) die('init'); // ------------------- // FILE SYNC BUFFERING // ------------------- function syncIn(ms) { if (syncFired) { syncFired = false; syncPromise = new Promise(resolve => (syncTrigger = resolve)); // 'input' event will be dispatched by change() } if (dead) return; addToRunning(fileName); // cf. currentlyRunning cell and runningHandler in init() const version = (thisVersion += 1); syncTimer.do(ms, () => { server.sync(fileName, getDoc(editInst.getValue())).then( () => { if (thisVersion === version) { removeFromRunning(fileName); // cf. currentlyRunning cell and runningHandler in init() syncFired = true; syncTrigger(); } if (!firstSync) { // add to 'open-files' ROI roiSync().then(() => (firstSync = true)); } }, e => { console.log(`error syncing ${fileName} (sync): ${e}`); if (!server.alive()) die('sync'); } ); }); } // function syncNow() { syncIn(0); } // ---------------- // DOCARRAY HELPERS // ---------------- function min_line() { // get first line number of this file (in Lean server) return opts.docArray ? opts.docArray.reduce( (a, d, i) => (i < opts.docIndex ? a + d.split('\n').length : a), 1 ) : 1; } // CodeMirror's position objects start at line 0 but the displayed line numbers start from line 1 // the Lean server's line numbers start at 1 opts.lineNumberFormatter = line => min_line() - 1 + line; // getDoc(val) updates and returns the full document if editing part of a docArray, // otherwise it just returns val const getDoc = opts.docArray ? val => opts.docArray .map((d, i, a) => (i === opts.docIndex ? (a[i] = val) : d)) .join('\n') : d => d; // -------------- // LINT AND HOVER // -------------- // controls gutter messages and underlining function lint(value, options, cm) { if (!filteredMsgs) return null; const lintMsgs = filteredMsgs.map( ({ caption, end_pos_col, end_pos_line, pos_col, pos_line, severity, text }) => { const from = { line: pos_line - min_line(), ch: pos_col }; return { // replace with commented code when styles / icon for 'information' severity are added severity: severity !== 'error' ? 'warning' : 'error', // severity || 'warning', from, to: end_pos_line !== undefined ? { line: end_pos_line - min_line(), ch: end_pos_col } : from, // default to = from // message: (caption ? caption + ':\n' : '') + text, messageNode: formatMsg({ severity, pos_line, pos_col, caption, text }) }; } ); return lintMsgs; } function hover(cm, data, event) { if (dead) return; const { line, ch } = data; const origLine = line + min_line(); return syncPromise .then(() => server.info(fileName, origLine, ch)) .then( ({ record }) => record && { messageNode: formatGoal(record, line, ch), // replace with commented code when styles / icon for 'information' severity are added severity: 'warning' // 'information', }, e => { console.log(`error getting info (hover): ${e}`); if (!server.alive()) die('hover'); } ); } opts.lint = { lintOnChange: true, getAnnotations: lint, hoverProvider: hover, delay: config.hoverDelay }; // ------------------------- // HINT: COMPLETION AND HOLE // ------------------------- const hintTimer = new CoalescedTimer(); function hint(cm, cb) { if (dead) return; return syncPromise.then(() => hintTimer.do( 0, // only make one completion request when typing ends () => { const { line, ch } = cm.getCursor(); const origLine = line + min_line(); Promise.all([ server.complete(fileName, origLine, ch), server.holeCommands(fileName, origLine, ch) ]).then( ([{ completions, prefix }, { results }]) => { if (!completions && !results) return null; const to = { line, ch }; const from = { line: line, ch: ch - ((prefix && prefix.length) || 0) }; let list = []; // hole command: apply using hole() if (results) list = list.concat( results.map(({ name, description }) => ({ displayText: `${name} : ${description}`, name, line, ch, origLine, hint: hole })) ); // ordinary completion: display with renderCompletion() if (completions) list = list.concat( completions.map(({ doc, text, type, tactic_params }) => ({ doc, text, type, tactic_params, render: renderCompletion })) ); cb({ to, from, list }); }, e => { console.log(`error getting completions (hint): ${e}`); if (!server.alive()) die('hint'); } ); } ) ); } hint.async = true; function hole(cm, self, data) { const { name, line, ch, origLine } = data; if (dead) return; server.hole(fileName, origLine, ch, name).then( ({ message, replacements }) => { if (message) { infoView.hole({ origLine, ch, name, message }); } if (replacements && replacements.alternatives) { const { start, end, alternatives: [{ code }] } = replacements; // TODO: ask user if more than one alternative? const from = { line: start.line - min_line(), ch: start.column }; const to = { line: end.line - min_line(), ch: end.column }; cm.replaceRange(code, from, to, "complete"); CodeMirror.signal(data, "pick", code); } }, e => { console.log(`error performing hole command (hole): ${e}`); if (!server.alive()) die('hole'); } ); } opts.hintOptions = { hint // closeOnUnfocus: false, }; // ---------------------------- // SENDING MESSAGES TO INFOVIEW // ---------------------------- const msgFilter = msg => msg.file_name === fileName && msg.pos_line >= min_line() && msg.pos_line < min_line() + editInst.lineCount(); function updateMsgs(msgArr) { const msgs = msgArr.filter(msgFilter); const msgsChanged = JSON.stringify(msgs) !== JSON.stringify(filteredMsgs); if (msgsChanged) { filteredMsgs = msgs; div.dispatchEvent(new CustomEvent('input')); editInst.performLint(); } } function updateInfoView() { const { line, ch } = editInst.getCursor(); const origLine = line + min_line(); infoView.update({ fileName, origLine, ch, filteredMsgs, msgFilter }); } // ----------------- // INITIALIZE EDITOR // ----------------- function init() { editInst = editor(cmDiv, infoView, opts); editInst.getWrapperElement().style.height = height; if (opts.readOnly) { cmDiv.querySelector('.CodeMirror').classList.add(CSS_CLASSES.READONLY); cmDiv .querySelector('.CodeMirror-scroll') .classList.add(CSS_CLASSES.READONLY); cmDiv .querySelector('.CodeMirror-gutters') .classList.add(CSS_CLASSES.READONLY); } // set up event handlers function change() { syncIn(config.delayMs); div.dispatchEvent(new CustomEvent('input')); } editInst.on('change', change); const msgsTimer = new CoalescedTimer(); const msgsHandler = server.allMessages.on(({ msgs }) => { msgsTimer.do(config.debounceAllMessages, () => { editInst.refresh(); // mainly to update displayed line numbers if another part of the docArray is edited updateMsgs(msgs); }); }); editInst.on('cursorActivity', updateInfoView); editInst.on('focus', updateInfoView); const runningHandlers = attachRunningHandlers(div.value); // ensure event handler disposal dispose = () => { msgsHandler.dispose(); runningHandlers.forEach(h => h.dispose()); }; invPromise.then(dispose); // call handlers for the first time change(); syncPromise.then(() => { updateMsgs(server.currentMessages); editInst.refresh(); updateInfoView(); }); } let headerNode = null; let footerNode = null; function afterInit() { if (typeof opts.header === 'function') { if (headerNode) header.removeChild(headerNode); headerNode = header.appendChild(opts.header(div.value)); } if (typeof opts.footer === 'function') { if (footerNode) footer.removeChild(footerNode); footerNode = footer.appendChild(opts.footer(div.value)); } editInst.refresh(); } // CALL INIT & APPEND HEADER / FOOTER: init(); setTimeout(afterInit, 0); // RESET BUTTON if (!opts.readOnly) { // different functionality for single click vs double click: https://stackoverflow.com/a/1546183 let buttonTimer = null; resetButton.onclick = () => { // double: dispose and rerun init if (buttonTimer) { clearTimeout(buttonTimer); dispose(); opts.value = div.value.resetValue; init(); setTimeout(afterInit, 0); buttonTimer = null; return; } buttonTimer = setTimeout(() => { // single: set editor value to initial value editInst.setValue(div.value.resetValue); buttonTimer = null; }, config.dblClickDelay); }; } return div; }3d:T8cc,function editor(container, infoView, opts0) { while (container.firstChild) { container.removeChild(container.firstChild); } const opts = { // defaults: might get overridden by opts0 mode: "lean", lineWrapping: true, lineNumbers: true, // value should already be set in leanEditor gutters: ["CodeMirror-lint-markers"], // required for linting tabIndex: 0, // non-CodeMirror options: // fileName, docArray, and docIndex (used in leanEditor function) // showToolbar // infoView, displayMode, filterMode, infoViewClass, infoViewNode // header, footer (HTML elements placed before / after container in leanEditor) // splitString ...opts0 }; const editor = CodeMirror(container, opts); // ------------ // KEY BINDINGS // ------------ function escHandler(cm) { if (!editor.state.completionActive) cm.setOption("extraKeys", navKeyMap); } function navEscHandler(cm) { if (!editor.state.completionActive) cm.setOption("extraKeys", keyMap); } function toggleInfoViewDisplayMode() { infoView.toggleDisplayMode(); } const keyMap = { Tab: tabHandler, Esc: escHandler, "Ctrl-/": "toggleComment", "Ctrl-'": insertHole, "Ctrl-M": toggleInfoViewDisplayMode, }; const navKeyMap = { Tab: false, "Shift-Tab": false, Esc: navEscHandler, "Ctrl-/": "toggleComment", "Ctrl-'": insertHole, "Ctrl-M": toggleInfoViewDisplayMode, } if (!opts.readOnly) { // enable completion for non-read-only editors navKeyMap["Ctrl-Space"] = keyMap["Ctrl-Space"] = "autocomplete"; // completion on keyup except for certain characters: https://stackoverflow.com/a/33908969/ const keys = {}; editor.on("keyup", function(editor, event) { keys[event.key] = false; if (!keys["Control"] && !editor.state.completionActive && !ExcludedIntelliSenseTriggerKeys[(event.keyCode || event.which).toString()]) { CodeMirror.commands.autocomplete(editor, null, { completeSingle: false }); } }); editor.on("keydown", function(editor, event) { keys[event.key] = true; }); } editor.setOption("extraKeys", keyMap); editor.on("focus", navEscHandler); return editor; }3e:T1d82,class InfoView { constructor(opts, invPromise) { if (!(invPromise instanceof Promise)) throw new Error(`InfoView: second argument must be an invalidation promise (currently: ${invPromise})`); Object.defineProperties(this, { opts: { value: opts, enumerable: true, }, _displayMode: { value: opts.displayMode || config.displayMode, // 0: goal, 1: all messages writable: true, }, _filterMode: { value: opts.filterMode || config.filterMode, // 0: per-editor, 1: per-file writable: true, }, _lastGoal: { value: null, // cache data from the last editor that sent info to this infoview writable: true, }, _msgFilter: { value: null, // message filtering function either directly provided by the last editor (opts.filterMode === 0) or derived from the filename given by the last editor (opts.filterMode === 1) writable: true, }, _filteredMsgs: { value: [], writable: true, }, _updateMsgs: { value: (msgArr) => { let msgs = this._msgFilter ? msgArr.filter(this._msgFilter) : []; this._msgsChanged = JSON.stringify(msgs) !== JSON.stringify(this._filteredMsgs); if (this._msgsChanged) { this._filteredMsgs = msgs; } }, }, _updateTimer: { value: new CoalescedTimer() }, _goal: { value: (fileName, origLine, ch) => { if (this._displayMode === 1) { while (this._goalDiv.firstChild) { this._goalDiv.removeChild(this._goalDiv.firstChild); } return; } server.info(fileName, origLine, ch).then( (res) => { while (this._goalDiv.firstChild) { this._goalDiv.removeChild(this._goalDiv.firstChild); } if (res.record) { this._goalDiv.appendChild(formatGoal(res.record, origLine, ch)); } }, (e) => console.log(`error getting info (InfoView.goal, ${fileName} at ${origLine}:${ch}): ${e}`) ); }, }, _msgs: { value: (fileName, origLine, ch, msgs) => { while (this._msgsDiv.firstChild) { this._msgsDiv.removeChild(this._msgsDiv.firstChild); } if (this._displayMode === 0) { msgs = msgs.filter( ({pos_col, pos_line, end_pos_col, end_pos_line}) => { return pos_line <= origLine && ((!end_pos_line && origLine === pos_line) || origLine <= end_pos_line) && (origLine !== pos_line || pos_col <= ch) && (origLine !== end_pos_line || end_pos_col >= ch); } ); } for (const msg of msgs) { this._msgsDiv.appendChild(formatMsg(msg)); } }, }, _updateIcons: { value: () => { const createClass = (defaultClass, selectedCode) => `${defaultClass} ${this._displayMode === selectedCode ? CSS_CLASSES.ACTIVE : CSS_CLASSES.INACTIVE}`; this._displayGoalImg.className = createClass(CSS_CLASSES.INFO_VIEW_GOAL_ICON, 0); this._displayMsgsImg.className = createClass(CSS_CLASSES.INFO_VIEW_MSGS_ICON, 1); }, }, }); // ------------- // HTML ELEMENTS // ------------- if (!opts.node) { Object.defineProperties(this, { _displayGoalImg: { value: html``, }, _displayMsgsImg: { value: html``, }, _goalDiv: { value: html`

`, }, _msgsDiv: { value: html`

`, }, }); this._updateIcons(); Object.defineProperty(this, 'node', { value: html`

${this._displayGoalImg}${this._displayMsgsImg}

${this._goalDiv}${this._msgsDiv}

`, enumerable: true, }); } else { const {node} = opts; if (!(node instanceof Element)) throw new Error(`InfoView: opts.node should be an Element (currently: ${node})`); Object.defineProperties(this, { node: { value: node, enumerable: true, }, _goalDiv: { value: node.querySelector(`.${CSS_CLASSES.INFO_VIEW_GOAL_WIDGET}`), }, _msgsDiv: { value: node.querySelector(`.${CSS_CLASSES.INFO_VIEW_MSGS_WIDGET}`), }, _displayGoalImg: { value: node.querySelector(`.${CSS_CLASSES.INFO_VIEW_GOAL_ICON}`), }, _displayMsgsImg: { value: node.querySelector(`.${CSS_CLASSES.INFO_VIEW_MSGS_ICON}`), }, }); } this.node.value = this; this._displayGoalImg.addEventListener('click', () => this.displayModeClick(0)); this._displayMsgsImg.addEventListener('click', () => this.displayModeClick(1)); // -------------- // EVENT HANDLERS // -------------- Object.defineProperty(this, '_msgsChanged', { value: true, // set and updated in _updateMsgs(), true if filteredMsgs has changed since the last allMessages event writable: true, }); const msgsTimer = new CoalescedTimer(); const msgsHandler = server.allMessages.on(({msgs}) => { msgsTimer.do(config.debounceAllMessages, () => { this._updateMsgs(msgs); if (this._lastGoal && this._msgsChanged) { const {fileName, origLine, ch} = this._lastGoal; this._goal(fileName, origLine, ch); this._msgs(fileName, origLine, ch, this._filteredMsgs); } }); }); invPromise.then(() => { msgsHandler.dispose(); }); } displayModeClick(m) { this._displayMode = m; this._updateIcons(); if (this._lastGoal) { const {fileName, origLine, ch} = this._lastGoal; this._goal(fileName, origLine, ch); this._updateMsgs(server.currentMessages); this._msgs(fileName, origLine, ch, this._filteredMsgs); } } toggleDisplayMode() { this.displayModeClick(1 - this._displayMode); } // Given filename + cursor position, set filter & last editor info and update infoview update({fileName, origLine, ch, filteredMsgs, msgFilter}) { this._updateTimer.do(config.debounceInfoViewUpdate, () => { this._goal(fileName, origLine, ch); this._lastGoal = {fileName, origLine, ch}; if (this._filterMode) { this._msgFilter = (msg) => msg.file_name === fileName; this._updateMsgs(server.currentMessages); this._msgs(fileName, origLine, ch, this._filteredMsgs); } else { this._msgFilter = msgFilter; this._msgs(fileName, origLine, ch, filteredMsgs); } }); } hole({origLine, ch, name, message}) { const msg = html`

${origLine}:${ch} hole command: ${name}

${message}

`; this._goalDiv.insertBefore(msg, this._goalDiv.firstChild); } }3f:T91c,md`

Click here to see a list of the Lean editor-specific options that can be used in \`opts0\`:

- \`className\`: *string*, CSS class name that will be applied to the container div, - \`fileName\`: *string*, the filename to assign to this editor in the Lean server, - \`height\`: *dimension*, the height of the editor (e.g. in px or %) (this differs from the way that CodeMirror treats the \`height\` option!), - \`showToolbar\`: *boolean*, show the button toolbar above the editor (by default, is only shown if a mobile browser is detected [below](#showToolbar)), - \`header\`, \`footer\`: *Element* | *function*, Used to add custom DOM elements before / after the editor. Should be either an HTML element or a function of the [CodeMirror editor object](https://codemirror.net/doc/manual.html#api) that returns an HTML element. [Below](#headerFooterDoc), I show how to use this option to display a form which can manipulate the editor. - \`infoView\`: *InfoView*, if present, the editor will use this [\`InfoView\`](#InfoView) object for the info panel. This can be used to share an infoview panel between editors. See an example [below](#infoDivDoc).
If \`infoView\` is not set, then the following fields of \`opts0\` are passed to the \`InfoView\` constructor (discussed before the example [below](#infoViewDoc)): - \`displayMode\`: *0* or *1*, (default ${config.displayMode}, controlled by [\`config.displayMode\`](#ConfigDoc)) - \`filterMode\`: *0* or *1*, (default ${config.filterMode}, controlled by [\`config.filterMode\`](#ConfigDoc)) - \`infoViewClassName\`: *string*, placed in the \`class\` field of the \`InfoView\` options object - \`infoViewNode\`: *Element*, placed in the \`node\` field of the \`InfoView\` options object - the \`value\` (*string*) and \`docArray\` (*Array* of *string*s) options are used to specify the initial text in the editor and are demonstrated in more detail [below](#CMLeanEditorExamples). If \`docArray\` is set, the following options may be used: - \`docIndex\`: *number* between 0 and \`docArray.length - 1\` (inclusive), (required), sets the initial value of the editor to the string at this index in \`docArray\`, - \`splitString\`: *string* (default "\`\\n---\\n\`"). When saving, this string is used to join the parts of the \`docArray\`. `40:T530,leanEditorValueDoc = md`As pointed out in the intro, Lean editor instances are [views](https://observablehq.com/@observablehq/introduction-to-views). Their values are objects with several fields:

- \`opts\`*: the options object passed to \`leanEditor\`, - \`infoView\`*: the \`InfoView\` object associated to this editor, - \`node\`*: the DOM node containing the editor and infoview that is returned by \`leanEditor\`, - \`editor\`*: the CodeMirror instance associated to this editor, - \`value\`*: the string being edited / displayed in the editor (to change the value, use \`editor.setValue()\`), - \`resetValue\`: the string that the editor was initialized with; if the editor is not read-only, the content of the editor will be replaced with this string when the Reset button is clicked, - \`syncPromise\`*: a promise which will resolve the next time the editor finishes syncing with the Lean server, - \`fileName\`*: the filename given to the Lean server, - \`saveFileName\`: the filename that is suggested when the Save button is clicked, - \`msgs\`*: an array containing the error, warning, and info message objects that apply to this editor. The fields marked with an asterisk (*) are getters and cannot be modified. `41:T818,infoViewDoc = md`#### Share an infoview panel between editors You can use the \`infoView\` option to specify a custom HTML element to use for the infoview. If this option is used, the Lean editor will send its messages to the given [\`InfoView\` object](#infoViewDoc). To create such an object, call the constructor with an options object and the \`invalidation\` promise.

Click to see a list of the options:

- \`displayMode\`: *0* or *1*, (default ${config.displayMode}, controlled by [\`config.displayMode\`](#ConfigDoc)). If set to 0, this infoview panel displays the goal under the cursor when it starts (

). If set to 1, it displays all messages when it starts (

). - \`filterMode\`: *0* or *1*, (default ${config.filterMode}, controlled by [\`config.filterMode\`](#ConfigDoc)). Changes the messages shown when this infoview panel is set to display messages (i.e. when \`displayMode\` is 1

). An infoview panel will always display messages from the last editor that sent it data. If set to 0, only messages associated to the range of lines displayed in that editor are shown. If set to 1, all messages associated to the file opened in that editor are shown. - \`className\`: *string*, a custom CSS class name applied to the infoview panel. By default, the class is \`infoview\`. See [\`infoViewCSS\`](#infoViewCSS) for the relevant style rules. - \`node\`: *Element*, an HTML element to use in place of the default one. To function properly, the element should have children with classes \`${CSS_CLASSES.INFO_VIEW_GOAL_ICON}\`, \`${CSS_CLASSES.INFO_VIEW_MSGS_ICON}\`, \`${CSS_CLASSES.INFO_VIEW_GOAL_WIDGET}\`, and \`${CSS_CLASSES.INFO_VIEW_MSGS_WIDGET}\`. `42:T4d3,md`\`InfoView\` objects have two public methods: - \`displayModeClick(i)\`: changes the infoview display mode to \`i\` (as above, 0 means display goal

, 1 means display messages

.) - \`toggleDisplayMode()\`: toggles the infoview display mode between 0 and 1. And two public properties: - \`node\`: the HTML element for the infoview panel - \`opts\`: the options that were used to create this object There are also two methods used by \`leanEditor\` to send data to the \`InfoView\` object which probably should not be called otherwise:

- \`update({fileName, origLine, ch, filterMsgs, msgFilter})\`: used to pass data about the cursor location (\`origLine\` (line number in the Lean file), \`ch\`) and the messages associated to the lines in the editor (\`filteredMsgs\`). When \`filterMode\` is 0, \`msgFilter\` is used as the filter for selecting from the server's messages. - \`hole({origLine, ch, name, message})\`: used to display a hole message in the infoview. `43:T7f4,config = ({ // default editor value; CAN OVERRIDE with 'value' in leanEditor options defaultValue: `-- Live ${ WebAssembly ? 'WebAssembly' : 'JavaScript' } version of Lean (default Lean file): #eval let v := lean.version in let s := lean.special_version_desc in string.join ["Lean (version ", v.1.repr, ".", v.2.1.repr, ".", v.2.2.repr, ", ", if s ≠ "" then s ++ ", " else s, "commit ", (lean.githash.to_list.take 12).as_string, ")"] example (m n : ℕ) : m + n = n + m := by simp [nat.add_comm]`, // default InfoView display mode; CAN OVERRIDE with 'displayMode' in leanEditor options displayMode: 0, // 0: goal, 1: messages // default InfoView message filter mode; CAN OVERRIDE with 'filterMode' in leanEditor options // in "display messages" mode, show all messages associated with: filterMode: 0, // 0: the lines in the currently active editor, 1: the fileName in the currently active editor // STYLING editorHeight: '250px', // default height; CAN OVERRIDE with 'height' in leanEditor options editorPercentage: 0.65, // percentage of width / height of editor vs InfoView (also changes CSS) stackWidth: '720px', // min width of window before changing from vertical to horizontal panel arrangement (changes leanCSS also) runningColor: '#fa5', // editor outline while server is running: orange-ish doneColor: '#bfb', // editor outline when server is done: green-ish initColor: '#aff', // editor outline before it finishes initializing: blue-ish stoppedColor: '#faa', // editor outline if server has stopped: pink-ish // TIMING (in milliseconds) delayMs: 750, // delay after last typed character before syncing editor contents with server hoverDelay: 400, // delay before popping up a hover element debounceAllMessages: 150, // delay after last "allMessages" event before updating InfoView debounceInfoViewUpdate: 100, // delay after last request to update goal before making a server.info() request and updating InfoView dblClickDelay: 250 // speed of double-click on reset button })44:T408,function formatGoal(goal, line, ch) { const {text, doc, type, state} = goal; const goalDiv = html`

`; if (state) { goalDiv.appendChild(html`

${line}:${ch}: goal

`); goalDiv.appendChild(html`

${leanHLSpan`${state}`}

`); } if (text) { goalDiv.appendChild(html`

tactic ${leanHLSpan`${text}`}

`); } else if (type) { goalDiv.appendChild(html`

${line}:${ch}: type ${goal['full-id'] ? `of ${goal['full-id']}` : ``}

`); goalDiv.appendChild(html`

${leanHLSpan`${type}`}

`); } if (doc) { goalDiv.appendChild(formatDoc(doc)); } return goalDiv; }45:T852,// http://detectmobilebrowser.com/mobile (UNLICENSE) showToolbar = { const a = (navigator.userAgent||navigator.vendor||window.opera); return (/(android|bb\d+|meego|android|ipad|playbook|silk).+mobile|avantgo|bada\/|blackberry|blazer|compal|elaine|fennec|hiptop|iemobile|ip(hone|od)|iris|kindle|lge |maemo|midp|mmp|mobile.+firefox|netfront|opera m(ob|in)i|palm( os)?|phone|p(ixi|re)\/|plucker|pocket|psp|series(4|6)0|symbian|treo|up\.(browser|link)|vodafone|wap|windows ce|xda|xiino/i.test(a)||/1207|6310|6590|3gso|4thp|50[1-6]i|770s|802s|a wa|abac|ac(er|oo|s\-)|ai(ko|rn)|al(av|ca|co)|amoi|an(ex|ny|yw)|aptu|ar(ch|go)|as(te|us)|attw|au(di|\-m|r |s )|avan|be(ck|ll|nq)|bi(lb|rd)|bl(ac|az)|br(e|v)w|bumb|bw\-(n|u)|c55\/|capi|ccwa|cdm\-|cell|chtm|cldc|cmd\-|co(mp|nd)|craw|da(it|ll|ng)|dbte|dc\-s|devi|dica|dmob|do(c|p)o|ds(12|\-d)|el(49|ai)|em(l2|ul)|er(ic|k0)|esl8|ez([4-7]0|os|wa|ze)|fetc|fly(\-|_)|g1 u|g560|gene|gf\-5|g\-mo|go(\.w|od)|gr(ad|un)|haie|hcit|hd\-(m|p|t)|hei\-|hi(pt|ta)|hp( i|ip)|hs\-c|ht(c(\-| |_|a|g|p|s|t)|tp)|hu(aw|tc)|i\-(20|go|ma)|i230|iac( |\-|\/)|ibro|idea|ig01|ikom|im1k|inno|ipaq|iris|ja(t|v)a|jbro|jemu|jigs|kddi|keji|kgt( |\/)|klon|kpt |kwc\-|kyo(c|k)|le(no|xi)|lg( g|\/(k|l|u)|50|54|\-[a-w])|libw|lynx|m1\-w|m3ga|m50\/|ma(te|ui|xo)|mc(01|21|ca)|m\-cr|me(rc|ri)|mi(o8|oa|ts)|mmef|mo(01|02|bi|de|do|t(\-| |o|v)|zz)|mt(50|p1|v )|mwbp|mywa|n10[0-2]|n20[2-3]|n30(0|2)|n50(0|2|5)|n7(0(0|1)|10)|ne((c|m)\-|on|tf|wf|wg|wt)|nok(6|i)|nzph|o2im|op(ti|wv)|oran|owg1|p800|pan(a|d|t)|pdxg|pg(13|\-([1-8]|c))|phil|pire|pl(ay|uc)|pn\-2|po(ck|rt|se)|prox|psio|pt\-g|qa\-a|qc(07|12|21|32|60|\-[2-7]|i\-)|qtek|r380|r600|raks|rim9|ro(ve|zo)|s55\/|sa(ge|ma|mm|ms|ny|va)|sc(01|h\-|oo|p\-)|sdk\/|se(c(\-|0|1)|47|mc|nd|ri)|sgh\-|shar|sie(\-|m)|sk\-0|sl(45|id)|sm(al|ar|b3|it|t5)|so(ft|ny)|sp(01|h\-|v\-|v )|sy(01|mb)|t2(18|50)|t6(00|10|18)|ta(gt|lk)|tcl\-|tdg\-|tel(i|m)|tim\-|t\-mo|to(pl|sh)|ts(70|m\-|m3|m5)|tx\-9|up(\.b|g1|si)|utst|v400|v750|veri|vi(rg|te)|vk(40|5[0-3]|\-v)|vm40|voda|vulc|vx(52|53|60|61|70|80|81|83|85|98)|w3c(\-| )|webc|whit|wi(g |nc|nw)|wmlb|wonu|x700|yas\-|your|zeto|zte\-/i.test(a.substr(0,4))); }46:T5c8,editorWrapperCSS = html``47:T6b0,customCodeMirrorCSS = html``48:T54b,infoViewCSS = html``49:T6ff,CSS_CLASSES = ({ READONLY: "readonly", ACTIVE: "active", INACTIVE: "inactive", RUNNING: "running", DONE: "done", STOPPED: "stopped", CODE_MIRROR: "CodeMirror", CODE_MIRROR_GUTTERS: "CodeMirror-gutters", CODE_MIRROR_GUTTER_BUSY: "CodeMirror-gutter-busy", CODE_MIRROR_HINT: "CodeMirror-hint", CODE_MIRROR_HINT_ACTIVE: "CodeMirror-hint-active", CODE_MIRROR_LINT_TOOLTIP: "CodeMirror-lint-tooltip", LEAN_COMPLETION_DESC: "lean-completion-desc", LEAN_COMPLETION_HIGHLIGHT: "lean-completion-highlight", LEAN_EDITOR_WRAPPER: "lean-editor-wrapper", LEAN_EDITOR_CONTAINER: "lean-editor-container", LEAN_EDITOR_HEADER: "lean-editor-header", LEAN_EDITOR_SAVE_BUTTON: "lean-editor-save-button", LEAN_EDITOR_UNDO_BUTTON: "lean-editor-undo-button", LEAN_EDITOR_REDO_BUTTON: "lean-editor-redo-button", LEAN_EDITOR_HOLE_BUTTON: "lean-editor-hole-button", LEAN_EDITOR_UNICODE_BUTTON: "lean-editor-unicode-button", LEAN_EDITOR_COMPLETE_BUTTON: "lean-editor-complete-button", LEAN_EDITOR_RESET_BUTTON: "lean-editor-reset-button", LEAN_EDITOR_COMMENT_BUTTON: "lean-editor-comment-button", LEAN_EDITOR_TOOLBAR: "lean-editor-toolbar", LEAN_EDITOR_TOGGLE_TOOLBAR_BUTTON: "lean-editor-toggle-toolbar-button", LEAN_EDITOR_BUTTON_WRAPPER: "lean-editor-button-wrapper", CODE_MIRROR_CONTAINER: "cm-container", INFO_VIEW: "info-view", INFO_VIEW_GOAL_ICON: "info-view-goal-icon", INFO_VIEW_MSGS_ICON: "info-view-msgs-icon", INFO_VIEW_BUTTONS: "info-view-buttons", INFO_VIEW_GOAL_WIDGET: "info-view-goal-widget", INFO_VIEW_MSGS_WIDGET: "info-view-msgs-widget", HOLE_MSG_CONTAINER: "hole-msg-container", INFO_VIEW_INFO_HEADER: "info-view-info-header", INFO_VIEW_CODE_BLOCK: "info-view-code-block", INFO_VIEW_TOGGLE_DOC: "info-view-toggle-doc" })4a:T7d3,TODO = md`## 4. TODO: - Refactor \`leanEditor\` into smaller components! - Start moving code to separate repos: - CodeMirror Lean mode / linting - Consider using \`Generators.disposable\` instead of passing \`invalidation\` promises around? - \`InfoView\` / \`LeanFile\` are classes and should have some indication of when to dispose their message handlers - If \`leanEditor\` returns a generator, then using it within a cell or other code becomes a lot harder - Think harder about caching. It seems that "hard-refreshing" Firefox doesn't always replace the cached version of the WASM files (maybe because it's downloaded via a \`fetch\` call?). - Use BroadcastChannel to coordinate locking IndexedDB? (Not supported in Safari...) - \`vscode-lean\` features: - Truncate messages longer than X / show only first X messages - Syntax highlighting for tactic state / messages - "goals accomplished" instead of "no goals" (like in \`vscode-lean\`)? - Links or hover in message headers - Scroll infoview when cursor moves in editor - Fix up the CSS in general: - Editor seems to expand to height of InfoView regardless of \`height\` option? - Draggable boundary between editor and infoview / adjustable height - Add styles / icons for \`'information'\` severity (see [this CSS file for CodeMirror's linting](https://github.com/codemirror/CodeMirror/blob/master/addon/lint/lint.css)) - Restyle editor? - Consider using CodeMirror's [\`linkedDoc\` feature](https://codemirror.net/doc/manual.html#linkedDoc) - Consider using CodeMirror's \`firstLineNumber\` option to replace \`min_line()\` stuff - Do something about the shared code between \`LeanFile\` and \`leanEditor\`. (Should \`leanEditor\` be a class?) - Do more with the "source" properties of server responses (containing links to github) - Is there any good interface for the Server's \`search\` command? - Add cache-clearing buttons to toolbar and a message about them if "\`file '/library/init/default.lean' not found\`" `4b:T1004,md`### Version history: - [2019/07/28](https://observablehq.com/@bryangingechen/hello-lean-prover@4946): first release - [2019/07/31](https://observablehq.com/@bryangingechen/hello-lean-prover@5055): support [locally-running Lean via websocketd](https://observablehq.com/@bryangingechen/lean-websocketd), editor background turns red when server is dead, clean up object properties - [2019/08/01](https://observablehq.com/@bryangingechen/hello-lean-prover@5065): improve and clarify text (thanks [@kappelmann](https://observablehq.com/@kappelmann)!) - [2019/08/08](https://observablehq.com/@bryangingechen/hello-lean-prover@5081): Merged suggestion from @kappelmann: "Fix CSS (right outline was invisible) of cm-container-full for small screens by using \`flex-grow: 1;\` instead of \`width: 100%\`" and also remove workaround for [this Firefox issue](https://talk.observablehq.com/t/misalignment-of-source-cells-in-firefox-when-divs-have-non-integer-px-heights/2029). - [2019/08/12](https://observablehq.com/@bryangingechen/hello-lean-prover@5118): Fixed cursor positioning after Unicode translation for paired brackets and added French quotes "\`‹›\`" to [\`hackyReplacements\`](#hackyReplacements). - [2019/08/15](https://observablehq.com/@bryangingechen/hello-lean-prover@5203): Many, many improvements from a suggestion by @kappelmann: "replaced hard-coded CSS classes, fixed some styling (e.g. resizing with CSS), [...], add highlighting in goal state, etc." Breaking changes: - \`refresh()\` method removed from \`value\` object of \`leanEditor()\` - \`height\` option to \`leanEditor()\` must now be a CSS length string, not a number. - many CSS class names changed. Refer to [\`CSS_CLASSES\`](#CSS_CLASSES). - [2019/08/18](https://observablehq.com/@bryangingechen/hello-lean-prover@5205): Merged suggestion from @kappelmann: “fix right margin CSS if there is no info view”. - [2019/08/20](https://observablehq.com/@bryangingechen/hello-lean-prover@5217): expose \`updateInfoview()\` as a method of the \`leanEditor\`'s' \`value\` object. - [2019/08/21](https://observablehq.com/@bryangingechen/hello-lean-prover@5236): Breaking change: rename \`updateInfoview()\` to \`updateInfoView()\`, and merged suggestion from @kappelmann: “Add debouncing for info view update and change download URL”. - [2019/08/27](https://observablehq.com/@bryangingechen/hello-lean-prover@5238): Merged suggestion from @kappelmann: “When passing a function to header, it should be displayed in a \`\` (just like the default header does).” - [2019/09/13](https://observablehq.com/@bryangingechen/hello-lean-prover@5245): Add workaround from [this issue](https://github.com/codemirror/CodeMirror/issues/4895) so that scrollbars appear in Safari (thanks @kappelmann!). **Warning: This workaround broke the editor on narrow screens. (Fixed in 2019/09/16 update.) ** - [2019/09/16](https://observablehq.com/@bryangingechen/hello-lean-prover@5272): Simplified height handling; editor should now scroll properly in Firefox, Chrome and Safari on both wide and narrow screens. - [2019/12/15](https://observablehq.com/@bryangingechen/hello-lean-prover@5307): Several additions: - changed CDN to https://gitcdn.link/ - added message about WASM being broken in Safari - added doc and module comment handling to syntax highlighting - [2020/03/06](https://observablehq.com/@bryangingechen/hello-lean-prover@5313): change host and update default file for new version of Lean - [2020/05/19](https://observablehq.com/@bryangingechen/hello-lean-prover@5319): update default file for new version of Lean - [2020/05/21](https://observablehq.com/@bryangingechen/hello-lean-prover@5327): Switch to \`@bryangingechen/lean-client-js-browser\` v1.4.0. - [2020/11/03](https://observablehq.com/@bryangingechen/hello-lean-prover@5346): Switch to \`lean-client-js-browser\` v2.0.1 and update linting code for [changes in CodeMirror 5.58.0](https://github.com/codemirror/CodeMirror/commit/18aa69e17cc7703f106fbe03992456b8e59e8cdc). - 2021/01/26: update link to \`translations.json\` (thanks @kappelmann!). `4c:[] 2f:{"title":"Hello, Lean prover!","cells":[{"id":0,"value":"md`# Hello, Lean prover!\n\n

`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1227,"value":"$31","pinned":false,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":1535,"value":"test0.msgs","pinned":true,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":1391,"value":"$32","pinned":false,"hidden":false,"mode":"ojs"},{"id":3829,"value":"$33","pinned":false,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":2,"value":"lean = require('lean-client-js-browser@2.0.1')","pinned":false,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":5193,"value":"transport = new lean.WebWorkerTransport(transportOpts)","pinned":false,"hidden":false,"mode":"ojs"},{"id":1275,"value":"$34","pinned":false,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":5192,"value":"transportOptsURL = \"https://bryangingechen.github.io/lean/lean-web-editor/\" //'https://gitcdn.link/repo/bryangingechen/lean-web-editor-dist/master/'","pinned":false,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":3919,"value":"md`We can now create a cell for the server object`","pinned":false,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":5188,"value":"md`and some cells to reset the server. Use \\`resetServer()\\` to re-initialise the Lean server.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":5187,"value":"mutable __LEAN_SERVER_RESTARTS = 0","pinned":false,"hidden":false,"mode":"ojs"},{"id":5186,"value":"resetServer = () => { mutable __LEAN_SERVER_RESTARTS += 1; }","pinned":false,"hidden":false,"mode":"ojs"},{"id":1288,"value":"$35","pinned":false,"hidden":false,"mode":"ojs"},{"id":3727,"value":"md`The server object's [main methods](#ServerCommands) will be discussed in the next section.`","pinned":false,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":1133,"value":"logByDefault = false","pinned":false,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":1456,"value":"resolveLeanURL = (file) => `${libmeta.info[libmeta.oleanmap[file]]}${file}.lean`","pinned":false,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"id":3067,"value":"setLeanURL = resolveLeanURL('init/data/set')","pinned":true,"hidden":false,"mode":"ojs"},{"id":1462,"value":"md`We can then fetch the Lean file into an Observable cell:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1465,"value":"setLean = fetch(setLeanURL).then(res => res.text())","pinned":true,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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,"hidden":false,"mode":"ojs"},{"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} Log messages to (=>) / from (<=) server in console`;\n check.onchange = () => {\n server.logMessagesToConsole = check.checked;\n console.log(`Logging ${check.checked ? 'on' : 'off'}!`);\n };\n server.logMessagesToConsole = check.checked;\n return form;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":643,"value":"serverReset = {\n const button = html`