<commit_before><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.");<commit_msg>fix(shell/lean_js): the and_comm name is taken now<commit_after><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 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';
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.");
{'fraction_non_alphanumeric': 0.18946144905075551, 'fraction_numerical': 0.005424254165052305, 'mean_word_length': 3.3828522920203734, 'pattern_counts': {'":': 0, '<': 39, '<?xml version=': 0, '>': 39, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5794881', 'n_tokens_mistral': 1726, 'n_tokens_neox': 1678, 'n_words': 461}