Modified from https://github.com/bryangingechen/lean-client-js/blob/cache/lean-client-js-browser/lib_test.html
Built with blockbuilder.org
Created
July 20, 2020 15:13
-
-
Save bryangingechen/5dd3910365d477dc01fc5c3577d96278 to your computer and use it in GitHub Desktop.
leanBrowser.js demo
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| license: mit |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!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/[email protected]/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