81 lines
2.5 KiB
HTML
81 lines
2.5 KiB
HTML
<html>
|
|
<head>
|
|
<title>lean.js minimal working example</title>
|
|
<meta charset="utf-8">
|
|
</head>
|
|
<body>
|
|
|
|
<p>Small example of using lean.js</p>
|
|
|
|
<pre id="output"></pre>
|
|
|
|
<script type="text/javascript">
|
|
var myTimer = null;
|
|
function now () { return (new Date()).getTime(); }
|
|
function startTimer () { myTimer = now(); }
|
|
function checkTimer () { return '(took ' + (now() - myTimer) + 'ms)'; }
|
|
|
|
var outputElement = document.getElementById("output");
|
|
function outputLog(msg) {
|
|
console.log(msg);
|
|
outputElement.appendChild(document.createTextNode(String(msg) + "\n"));
|
|
}
|
|
|
|
/*
|
|
* "Module" must be initialized before the <script> tag for lean.js.
|
|
* The lean.js script populates Module with compiled Lean code,
|
|
* but it needs to know about the parameters below or it will throw errors.
|
|
*/
|
|
outputLog('--- Loading Lean VM...'); startTimer();
|
|
Module = { };
|
|
Module.TOTAL_MEMORY = 64 * 1024 * 1024;
|
|
Module.noExitRuntime = true;
|
|
Module.print = function(text) { outputLog(text); };
|
|
Module.preRun = [
|
|
function () {
|
|
outputLog('--- Lean VM loaded. ' + checkTimer());
|
|
outputLog('--- Running Lean VM...'); startTimer();
|
|
}
|
|
];
|
|
Module.postRun = function () {
|
|
outputLog('--- Lean VM has been run. ' + checkTimer());
|
|
}
|
|
</script>
|
|
|
|
<!-- Import the Lean javascript module generated by emscripten. -->
|
|
<script src="lean_js.js" type="text/javascript" charset="utf-8"></script>
|
|
|
|
<script type="text/javascript" charset="utf-8">
|
|
|
|
outputLog('--- Calling lean_init()...'); startTimer();
|
|
Module.lean_init();
|
|
outputLog('--- lean_init() complete. ' + checkTimer());
|
|
|
|
outputLog('--- Importing standard library...'); startTimer();
|
|
Module.lean_import_module('standard');
|
|
outputLog('--- Import complete. ' + checkTimer());
|
|
|
|
outputLog('--- Writing test.lean to virtual FS...'); startTimer();
|
|
testfile = ''
|
|
+ 'variables p q r s : Prop\n'
|
|
+ 'theorem 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';
|
|
outputLog( testfile );
|
|
FS.writeFile('test.lean', testfile, { encoding: 'utf8' });
|
|
outputLog('--- test.lean written. ' + checkTimer());
|
|
|
|
outputLog('--- Running Lean on test.lean...'); startTimer();
|
|
Module.lean_process_file('test.lean');
|
|
outputLog('--- Lean has been run on test.lean. ' + checkTimer());
|
|
|
|
outputLog("--- Finished.");
|
|
|
|
</script>
|
|
</body>
|
|
</html>
|