here to learn
Published
Edited
Feb 3, 2020
Importers
5 stars
mathjax-editing.jshighlightjs for LeanCindyJS import exampleTOCD3 ScatterplotD3 Log-Scaled HistogramLean exercise boxStepping through currying in LeanHello, Lean prover!MathJaxPolygon inputHello, cubic-spline!Brython in observableHello, Bokeh.js!commentOnLabeling connected componentsDrag to re-arrange (vertical edition)Dynamic import polyfillHello, R on OpenCPU!Hello, noUiSlider!Hello, CindyJS!Hello, chess!Grid inputs
Connect Observable notebooks to Lean on your computer with websocketd
Also listed in…
Lean
leanEditor({}, invalidation)
leanEditor({
value: `-- import .src.scratch`,
}, invalidation)
import {leanEditor, leanEditorFrom, InfoView, LeanFile, leanControl, leanHL, parseLeanMsgs,
lean, serverReset, currentlyRunning, config, CoalescedTimer, CSS_CLASSES,
__LEAN_SERVER_RESTARTS, resetOpenLeanFiles,logByDefault }
with {transport, deleteIdb, deleteJSWasm, attachRunningHandlers, server}
from '@bryangingechen/hello-lean-prover'
wsUrl = 'ws://localhost:43263'
transport = {
// https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/transport.ts
/* export declare type TransportError = StderrError | ConnectError;
export interface Transport {
connect(): Connection;
}
export interface Connection {
error: Event<TransportError>;
jsonMessage: Event<any>;
alive: boolean;
send(jsonMsg: any): any;
dispose(): any;
} */
const { Event } = lean;
function connect() {
const error = new Event();
const jsonMessage = new Event();
const ws = new WebSocket(wsUrl);
const conn = { error, jsonMessage, alive: true, send, dispose, ws };
let opened = false;
let openResolve = null;
const openedPromise = new Promise(resolve => (openResolve = resolve));
ws.onopen = () => {
openResolve();
opened = true;
console.log(`Lean websocket connected at ${wsUrl}`);
};
ws.onmessage = ({ data }) => {
try {
jsonMessage.fire(JSON.parse(data));
} catch (e) {
error.fire({
error: 'connect',
message: `cannot parse: ${data}, error: ${e}`
});
}
};
ws.onerror = e => {
error.fire({ error: 'websocketError' }); // websocket errors don't give much info: https://www.w3.org/TR/websockets/#concept-websocket-close-fail
};
ws.onclose = () => {
conn.alive = false;
};
function send(msg) {
if (!opened) openedPromise.then(() => ws.send(JSON.stringify(msg)));
else ws.send(JSON.stringify(msg));
}
function dispose() {
ws.close();
}
return conn;
}
return { connect };
}
server = {
__LEAN_SERVER_RESTARTS; // create dependency to be able to restart the server (this is a bit hacky)
resetOpenLeanFiles();
const server = new lean.Server(transport);
server.logMessagesToConsole = logByDefault;
server.error.on(err => console.log('error:', err));
// window.server = server; // uncomment this to allow running commands from the dev console
try {
server.connect();
} catch (e) {
console.log('Lean server: WebSocket connection failed!');
return fakeServer;
}
server.conn.ws.addEventListener('close', () => {
server.error.fire('Lean websocket closed');
});
return Generators.disposable(server, server => {
console.log('disposing lean server...');
server.dispose(); // dispose server when cell is invalidated
});
}
function attachRunningHandlers({editor, node, fileName, opts}) {
const containerDiv = node.querySelector(`.${CSS_CLASSES.LEAN_EDITOR_CONTAINER}`);
const decoTimer = new CoalescedTimer();
return [
currentlyRunning.updated.on((files) => {
containerDiv.className = `${CSS_CLASSES.LEAN_EDITOR_CONTAINER} ${files.length ? CSS_CLASSES.RUNNING : CSS_CLASSES.DONE}`;
}),
// tasks as orange lines in the gutter
server.tasks.on(({tasks, is_running}) => {
decoTimer.do(0 && config.debounceAllMessages, () => {
const min_line = opts.lineNumberFormatter(1);
const filteredTasks = tasks.filter(({file_name}) => file_name === fileName);
if (filteredTasks.length) {
filteredTasks.map(({pos_line, end_pos_line}) => {
for (let j=0; j<editor.lineCount(); j++) {
if (j+min_line >= pos_line || j+min_line < end_pos_line) {
editor.addLineClass(j, "gutter", `${CSS_CLASSES.CODE_MIRROR_GUTTER_BUSY}`);
} else {
editor.removeLineClass(j, "gutter", `${CSS_CLASSES.CODE_MIRROR_GUTTER_BUSY}`);
}
}
});
} else {
for (let j=0; j<editor.lineCount(); j++) {
editor.removeLineClass(j, "gutter", `${CSS_CLASSES.CODE_MIRROR_GUTTER_BUSY}`);
}
}
containerDiv.className = `${CSS_CLASSES.LEAN_EDITOR_CONTAINER} ${is_running ? CSS_CLASSES.RUNNING : CSS_CLASSES.DONE}`;
});
})
];
}
fakeServer = ({
conn: { alive: false },
allMessages: new lean.Event(),
error: new lean.Event(),
tasks: new lean.Event(),
alive: () => false,
roi: () => {},
fake: true
})
One platform to build and deploy the best data apps
Experiment and prototype by building visualizations in live JavaScript notebooks. Collaborate with your team and decide which concepts to build out.
Use Observable Framework to build data apps locally. Use data loaders to build in any language or library, including Python, SQL, and R.
Seamlessly deploy to Observable. Test before you ship, use automatic deploy-on-commit, and ensure your projects are always up-to-date.