These dump the entire function representation at major compilation boundaries:
set_option trace.Compiler.init trueset_option trace.Compiler.saveBase true
| (async () => { | |
| const sleep = (ms) => new Promise((r) => setTimeout(r, ms)); | |
| // 1. Locate the true feed scroll container | |
| let container = document.querySelector('[data-scrollable]'); | |
| if (!container) { | |
| const feed = document.querySelector('[data-feed-group]'); | |
| if (feed) { | |
| let p = feed.parentElement; | |
| while (p && p !== document.body) { |
| ✘ ~/projects/mm0 learn ±✚ ./examples/test_pub_theorem.sh | |
| === Setting up test files === | |
| === First Verification (Base case) === | |
| elab test_thm.mm1 | |
| elabbed test_thm.mm1 | |
| 1 sorts, 1 term/def, 3 ax/thm | |
| Verification succeeded! | |
| === Experiment 1: Adding a new PUB theorem not declared in MM0 === | |
| elab test_thm.mm1 | |
| elabbed test_thm.mm1 |
| // ==UserScript== | |
| // @name Djinni Quick Apply Pro | |
| // @namespace http://tampermonkey.net/ | |
| // @version 2.2.0 | |
| // @description Automate job applications on Djinni.co directly via Tampermonkey | |
| // @author You | |
| // @match https://djinni.co/* | |
| // @grant none | |
| // ==/UserScript== |
| -- config | |
| def colorize := false | |
| def cyan (s : String) := if colorize then s!"\x1b[36m{s}\x1b[0m" else s | |
| def yellow (s : String) := if colorize then s!"\x1b[33m{s}\x1b[0m" else s | |
| def green (s : String) := if colorize then s!"\x1b[32m{s}\x1b[0m" else s | |
| def red (s : String) := if colorize then s!"\x1b[31m{s}\x1b[0m" else s | |
| -- 1. Helper to find integer powers of 2 (returns e ≥ 0) |
| Notebook[{Cell[ | |
| BoxData[RowBox[{}]],"Input",CellLabel -> "In[5]:= ",ExpressionUUID -> "a5eda00a-dbbb-408b-ae55-06412828302d"],Cell[ | |
| CellGroupData[ | |
| {Cell[ | |
| BoxData[RowBox[{RowBox[{"Manipulate","[",RowBox[{RowBox[{"Plot3D","[",RowBox[ | |
| {RowBox[{"{",RowBox[{RowBox[{RowBox[{"x","^","2"}]," ","+"," ",RowBox[{"y","^","2"}]}],","," ",RowBox[ | |
| {RowBox[{"-",RowBox[{"x","^","2"}]}]," ","-"," ",RowBox[{"y","^","2"}]}]}],"}"}],","," ",RowBox[ | |
| {"{",RowBox[{"x",","," ",RowBox[{"-","2"}],","," ","2"}],"}"}],","," ",RowBox[{"{",RowBox[ | |
| {"y",","," ",RowBox[{"-","2"}],","," ","2"}],"}"}],","," ","\n"," ",RowBox[{"RegionFunction"," ","\[Rule]"," ",RowBox[ | |
| {"Function","[",RowBox[{RowBox[{"{",RowBox[{"x",","," ","y",","," ","z"}],"}"}],","," ",RowBox[ |
| -- 1. The raw data structure | |
| inductive BinderImplementation (e : Type) where | |
| | Op : BinderImplementation e → Array (BinderImplementation e) → BinderImplementation e | |
| -- 2. The validation predicate | |
| def BinderImplementation.isWF {e : Type} : BinderImplementation e → Prop | |
| | .Op what whatElse => | |
| what.isWF ∧ whatElse.size > 0 ∧ (∀ x ∈ whatElse, x.isWF) | |
| -- 3. The actual Type |
| ~/projects/mm0/mm0-hs master for i in ../examples/*.mm[01]; do | |
| ./.stack-work/dist/x86_64-linux-nix/ghc-9.10.3/build/mm0-hs/mm0-hs compile "$i" \ | |
| && echo "=================== OK ==================== $i" \ | |
| || echo "=================== ERR =================== $i" | |
| done | |
| depth limit exceeded | |
| =================== ERR =================== ../examples/assembler-new.mm1 | |
| ../examples/assembler-old.mm1:7:24: | |
| | | |
| 7 | local def _x00: char = 0; |
| import Lean | |
| open Lean Elab Command Meta | |
| -- Macro to create a structure by omitting specified fields | |
| syntax "elab_omit" ident "[" term,* "]" : term | |
| -- Macro to create a structure by picking specified fields | |
| syntax "elab_pick" ident "[" term,* "]" : term |
sudo virsh net-start default sudo EDITOR=nvim virsh dumpxml win11-2 > /tmp/win11-2.xml sudo EDITOR=nvim virsh edit win11-2