Skip to content

Instantly share code, notes, and snippets.

@bryangingechen

bryangingechen/.block

Created July 20, 2020 15:13
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save bryangingechen/5dd3910365d477dc01fc5c3577d96278 to your computer and use it in GitHub Desktop.
Save bryangingechen/5dd3910365d477dc01fc5c3577d96278 to your computer and use it in GitHub Desktop.
Download ZIP
leanBrowser.js demo
Raw
.block
license: mit
Raw
index.html
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<title>leanBrowser.js bundle test</title>
</head>
<body>
<script src="https://cdn.jsdelivr.net/npm/d3-require@1"></script>
<script>
// must use absolute URL since worker script is inlined in leanBrowser.js
const prefix = "https://bryangingechen.github.io/lean/lean-web-editor/";
d3.require("https://cdn.jsdelivr.net/npm/@bryangingechen/lean-client-js-browser@1.4.0/dist/leanBrowser.js").then((lean) => {
window.lean = lean;
const opts = {
// javascript: 'https://leanprover.github.io/lean.js/lean3.js',
javascript: prefix+'/lean_js_js.js',
webassemblyJs: prefix+'/lean_js_wasm.js',
webassemblyWasm: prefix+'/lean_js_wasm.wasm',
libraryZip: prefix+'/library.zip',
// Uncomment to test optional fields
// libraryMeta: prefix + '/library.info.json',
// libraryOleanMap: prefix + '/library.olean_map.json',
// dbName: 'leanlib2',
// libraryKey: 'lib'
};
const transport = new lean.WebWorkerTransport(opts);
const server = new lean.Server(transport);
server.error.on((err) => console.log('error:', err));
server.allMessages.on((allMessages) => console.log('messages:', allMessages.msgs));
server.tasks.on((currentTasks) => console.log('tasks:', currentTasks.tasks));
window.server = server; // allow debugging from the console
server.connect();
const testfile = ''
+ 'variables p q r s : Prop\n'
+ 'theorem my_and_comm : p /\\ q <-> q /\\ p :=\n'
+ 'iff.intro\n'
+ ' (assume Hpq : p /\\ q,\n'
+ ' and.intro (and.elim_right Hpq) (and.elim_left Hpq))\n'
+ ' (assume Hqp : q /\\ p,\n'
+ ' and.intro (and.elim_right Hqp) (and.elim_left Hqp))\n'
+ '#check @nat.rec_on\n'
+ '#print "end of file!"\n';
server.sync('test.lean', testfile)
.catch((err) => console.log('error while syncing file:', err));
server.info('test.lean', 3, 0)
.then((res) => console.log(`got info: ${JSON.stringify(res)}`))
.catch((err) => console.log('error while getting info:', err));
});
</script>
Check the console output; you can also play with the <pre style='display: inline;'>lean</pre> and <pre style='display: inline;'>server</pre> objects.
</body>
</html>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment