Skip to content

Commit b528d36

Browse files
jackeownjackeown
committed
WASM runner: async readline, wasm32 build, interactive UI
1 parent 8c1cb30 commit b528d36

File tree

8 files changed

+667
-213
lines changed

8 files changed

+667
-213
lines changed

‎buildVampireWasm.sh‎

Lines changed: 96 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@ else
99
echo "Repo 'vampire' already exists, skipping clone."
1010
fi
1111

12+
BUILD_DIR=${BUILD_DIR:-build-ems}
13+
1214
# 2. Copy smallWasmBuild.sh into the repo
1315
echo "Copying smallWasmBuild.sh..."
1416
cp -f smallWasmBuild.sh vampire/
@@ -17,17 +19,109 @@ cp -f smallWasmBuild.sh vampire/
1719
echo "Editing CMakeLists.txt..."
1820
./editCMakeLists.sh vampire/CMakeLists.txt
1921

22+
# 3b. Apply interactive stdin/stdout hooks for the WASM build
23+
echo "Applying interactive WASM patch..."
24+
./patchVampireInteractive.sh vampire
25+
2026
# 4. cd into vampire
2127
cd vampire
2228

2329
# 5. Run build script
2430
echo "Running smallWasmBuild.sh..."
2531
chmod +x smallWasmBuild.sh
26-
./smallWasmBuild.sh
32+
BUILD_DIR="$BUILD_DIR" ./smallWasmBuild.sh
2733

2834
# 6. Copy build artifacts back to parent directory
2935
echo "Copying build artifacts..."
30-
cp build-ems64/vampire.js build-ems64/vampire.wasm ../docusaurus-site/static/vampire-runner/
36+
cp "$BUILD_DIR"/vampire.js "$BUILD_DIR"/vampire.wasm ../docusaurus-site/static/vampire-runner/
3137

3238
echo "Done! Built files are in docusaurus-site/static/vampire-runner."
3339

40+
echo "Patching generated vampire.js for memory64 BigInt interop..."
41+
python - <<'PY'
42+
from pathlib import Path
43+
44+
def patch_file(path: Path):
45+
if not path.exists():
46+
return
47+
text = path.read_text()
48+
49+
utf_old = 'var UTF8ToString=(ptr,maxBytesToRead,ignoreNul)=>{assert(typeof ptr=="number",`UTF8ToString expects a number (got ${typeof ptr})`);return ptr?UTF8ArrayToString(HEAPU8,ptr,maxBytesToRead,ignoreNul):""};'
50+
utf_new = "var UTF8ToString=(ptr,maxBytesToRead,ignoreNul)=>{if(typeof ptr==='bigint'){ptr=Number(ptr);}else if(typeof ptr!=='number'){assert(false,`UTF8ToString expects a number (got ${typeof ptr})`);}return ptr?UTF8ArrayToString(HEAPU8,ptr,maxBytesToRead,ignoreNul):\"\"};"
51+
if utf_old in text:
52+
text = text.replace(utf_old, utf_new, 1)
53+
54+
ptr_old = 'var ptrToString=ptr=>{assert(typeof ptr==="number");if(ptr<0)ptr=2n**64n+BigInt(ptr);return"0x"+ptr.toString(16).padStart(16,"0")};'
55+
ptr_new = 'var ptrToString=ptr=>{if(typeof ptr==="bigint"){if(ptr<0)ptr+=2n**64n;}else if(typeof ptr==="number"){ptr=ptr<0?2n**64n+BigInt(ptr):BigInt(ptr);}else{assert(false,`ptrToString expects a number/bigint (got ${typeof ptr})`);}return"0x"+ptr.toString(16).padStart(16,"0")};'
56+
if ptr_old in text:
57+
text = text.replace(ptr_old, ptr_new, 1)
58+
59+
# Wrap invoke_* indices to avoid BigInt table lookups exploding in JS.
60+
if "__ensureSafeWasmInvokes" not in text:
61+
snippet = """
62+
// Injected: sanitize invoke_* indices for memory64/BigInt
63+
let __wasmTableLenSnapshot = 0;
64+
function __sanitizeWasmInvokeIndex(value){
65+
const len = (typeof wasmTable!=='undefined' && typeof wasmTable.length==='number') ? wasmTable.length : (__wasmTableLenSnapshot||0);
66+
if(len<=0){
67+
try{return Number(value);}catch(_ignore){return 0;}
68+
}
69+
__wasmTableLenSnapshot = len;
70+
let num;
71+
if(typeof value==='bigint'){
72+
const mod = value % BigInt(len);
73+
num = Number(mod < 0n ? mod + BigInt(len) : mod);
74+
}else{
75+
try{num=Number(value);}catch(_ignore){num=0;}
76+
}
77+
num = num % len;
78+
if(num<0) num += len;
79+
if(!Number.isFinite(num)){num=0;}
80+
return Math.trunc(num);
81+
}
82+
function __wrapWasmInvoke(imports,name){
83+
const original = imports[name];
84+
if(typeof original!=='function' || original.__wasmInvokeSanitized){
85+
return;
86+
}
87+
const wrapper = function(index,...rest){
88+
const sanitized = __sanitizeWasmInvokeIndex(index);
89+
return original.call(this,sanitized,...rest);
90+
};
91+
wrapper.__wasmInvokeSanitized = true;
92+
wrapper.isAsync = original.isAsync;
93+
imports[name] = wrapper;
94+
}
95+
function __ensureSafeWasmInvokes(imports){
96+
Object.keys(imports).forEach(name=>{
97+
if(name.startsWith('invoke_')){
98+
__wrapWasmInvoke(imports,name);
99+
}
100+
});
101+
}
102+
"""
103+
idx = text.find("function invoke_")
104+
if idx != -1:
105+
text = text[:idx] + snippet + text[idx:]
106+
107+
get_imports = "function getWasmImports(){Asyncify.instrumentWasmImports(wasmImports);return{env:wasmImports,wasi_snapshot_preview1:wasmImports}}"
108+
get_with_ensure = "function getWasmImports(){Asyncify.instrumentWasmImports(wasmImports);__ensureSafeWasmInvokes(wasmImports);return{env:wasmImports,wasi_snapshot_preview1:wasmImports}}"
109+
if get_imports in text:
110+
text = text.replace(get_imports, get_with_ensure, 1)
111+
elif "function getWasmImports()" in text and "__ensureSafeWasmInvokes" in text:
112+
# best-effort regex swap
113+
import re
114+
text = re.sub(r"function getWasmImports\\(\\)\\{[^}]*Asyncify\\.instrumentWasmImports\\(wasmImports\\);return\\{env:wasmImports,wasi_snapshot_preview1:wasmImports}}",
115+
get_with_ensure, text, count=1)
116+
117+
ri_old = 'wasmTable=wasmExports["__indirect_function_table"];assert(wasmTable,"table not found in wasm exports");assignWasmExports(wasmExports);return wasmExports}'
118+
ri_new = 'wasmTable=wasmExports["__indirect_function_table"];assert(wasmTable,"table not found in wasm exports");__wasmTableLenSnapshot=wasmTable.length||__wasmTableLenSnapshot;__ensureSafeWasmInvokes(wasmImports);assignWasmExports(wasmExports);return wasmExports}'
119+
if ri_old in text and "__ensureSafeWasmInvokes" in text:
120+
text = text.replace(ri_old, ri_new, 1)
121+
122+
path.write_text(text)
123+
print(f"Patched {path}")
124+
125+
for rel in ["vampire.js", "../docusaurus-site/static/vampire-runner/vampire.js"]:
126+
patch_file(Path(rel))
127+
PY

‎docusaurus-site/src/components/VampireRunner.jsx‎

Lines changed: 118 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -16,51 +16,35 @@ function highlightNowOrWhenReady(el) {
1616
window.addEventListener('load', tryHl, { once: true });
1717
}
1818

19-
// Find a base URL that serves your runner assets (coi-serviceworker + script.js).
20-
// If you already solved this elsewhere, you can swap this out.
19+
// Find a base URL that serves the runner assets.
2120
const BASE_CACHE_KEY = 'vampireRunner.baseUrl';
22-
async function headIsJs(url){
23-
try {
24-
const r = await fetch(url, { method: 'HEAD' });
25-
if (!r.ok) return false;
26-
const ct = (r.headers.get('content-type') || '').toLowerCase();
27-
return /javascript|ecmascript/.test(ct);
28-
} catch { return false; }
29-
}
21+
const ensureSlash = (p) => p.endsWith('/') ? p : (p + '/');
3022
async function findWorkingBaseUrl(){
3123
const cached = sessionStorage.getItem(BASE_CACHE_KEY);
32-
if (cached) return cached.endsWith('/') ? cached : cached + '/';
24+
if (cached) return ensureSlash(cached);
3325

34-
const candidates = new Set();
26+
const candidates = [];
3527
const docusaurusBase = typeof window!=='undefined' && window.__docusaurus && window.__docusaurus.baseUrl;
36-
if (docusaurusBase) candidates.add(docusaurusBase);
28+
if (docusaurusBase) candidates.push(docusaurusBase);
3729

38-
const baseTag = typeof document!=='undefined' && document.querySelector('base')?.getAttribute('href');
39-
if (baseTag) candidates.add(baseTag);
30+
const baseTag = typeof document!=='undefined' ? document.querySelector('base')?.getAttribute('href') : null;
31+
if (baseTag) candidates.push(baseTag);
4032

41-
const parts = typeof location!=='undefined' ? location.pathname.split('/').filter(Boolean) : [];
42-
for (let i=parts.length; i>=0; i--) {
43-
const prefix = '/' + parts.slice(0, i).join('/') + (i ? '/' : '');
44-
candidates.add(prefix || '/');
45-
}
46-
// common guesses
47-
candidates.add('/vampireGuide/');
48-
candidates.add('/');
49-
50-
for (const base0 of candidates) {
51-
const base = base0.endsWith('/') ? base0 : base0 + '/';
52-
const swOk = await headIsJs(base + 'coi-serviceworker.min.js');
53-
const glueOk = await headIsJs(base + 'vampire-runner/script.js');
54-
if (swOk && glueOk) {
55-
sessionStorage.setItem(BASE_CACHE_KEY, base);
56-
return base;
57-
}
33+
if (typeof location !== 'undefined') {
34+
candidates.push(new URL('./', location.href).pathname);
5835
}
59-
throw new Error('Could not locate baseUrl that serves Vampire Runner assets.');
36+
37+
candidates.push('/vampireGuide/');
38+
candidates.push('/');
39+
40+
const seen = new Set();
41+
const base = (candidates.map(ensureSlash).find(b => (seen.has(b) ? false : (seen.add(b), true))) || '/');
42+
sessionStorage.setItem(BASE_CACHE_KEY, base);
43+
return base;
6044
}
6145
async function getWorkingBaseUrl(){
6246
const base = await findWorkingBaseUrl();
63-
return base.endsWith('/') ? base : base + '/';
47+
return ensureSlash(base);
6448
}
6549

6650
/** ---------------------- LiveCode (Prism-Live editor) ---------------------- **/
@@ -112,31 +96,106 @@ fof(b, conjecture, p).`,
11296
outputLanguage = 'tptp',
11397
}) {
11498
const [tptp, setTptp] = useState(defaultProblem);
115-
const [args, setArgs] = useState('--proof on --time_limit 1');
99+
const [args, setArgs] = useState('--manual_cs on --show_new on --proof on');
116100
const [out, setOut] = useState('Ready.');
101+
const [pendingPrompt, setPendingPrompt] = useState(null);
102+
const [pendingInput, setPendingInput] = useState('');
103+
const pendingResolveRef = useRef(null);
104+
const [running, setRunning] = useState(false);
117105
const outCodeRef = useRef(null);
106+
const latestOutRef = useRef('Ready.');
118107

119108
// Re-highlight output whenever it changes (or when Prism arrives)
120109
useEffect(() => {
121110
if (typeof window === 'undefined') return;
122111
highlightNowOrWhenReady(outCodeRef.current);
123112
}, [out, outputLanguage]);
124113

114+
useEffect(() => {
115+
latestOutRef.current = out;
116+
}, [out]);
117+
118+
// Append a line to the transcript (one big string for highlighting)
119+
const appendLine = (text) => {
120+
setOut(prev => {
121+
const next = prev ? `${prev}\n${text}` : text;
122+
latestOutRef.current = next;
123+
return next;
124+
});
125+
};
126+
127+
const handleRequestInput = (promptText) => {
128+
const promptLine = promptText || '>';
129+
appendLine(promptLine);
130+
setPendingPrompt(promptLine);
131+
setPendingInput('');
132+
return new Promise((resolve) => {
133+
pendingResolveRef.current = resolve;
134+
});
135+
};
136+
137+
const submitPromptResponse = () => {
138+
if (!pendingResolveRef.current) return;
139+
const answer = pendingInput;
140+
appendLine(`> ${answer}`);
141+
pendingResolveRef.current(answer);
142+
pendingResolveRef.current = null;
143+
setPendingPrompt(null);
144+
setPendingInput('');
145+
};
146+
147+
const handleKeyDown = (ev) => {
148+
if (ev.key === 'Enter') {
149+
ev.preventDefault();
150+
submitPromptResponse();
151+
}
152+
};
153+
125154
async function onRun() {
155+
setRunning(true);
126156
setOut('Running…');
157+
setPendingPrompt(null);
158+
setPendingInput('');
159+
if (pendingResolveRef.current) {
160+
pendingResolveRef.current('');
161+
pendingResolveRef.current = null;
162+
}
127163
try {
128164
const base = await getWorkingBaseUrl();
129165
// Use webpackIgnore so the URL can be absolute at runtime
130166
const mod = await import(/* webpackIgnore: true */ (base + 'vampire-runner/script.js'));
131-
const run = mod.runVampire || mod.default;
132-
if (typeof run !== 'function') {
133-
setOut('Error: runVampire() not found in script.js');
167+
const runRaw = mod.runVampireRaw || mod.runVampire || mod.default;
168+
if (typeof runRaw !== 'function') {
169+
setOut('Error: runVampireRaw() not found in script.js');
170+
setRunning(false);
134171
return;
135172
}
136-
const result = await run({ tptp, args });
137-
setOut(String(result ?? ''));
173+
const { code } = await runRaw({
174+
tptp,
175+
args,
176+
onStdout: (msg) => String(msg ?? '').split('\n').forEach(appendLine),
177+
onStderr: (msg) => String(msg ?? '').split('\n').forEach(line => appendLine(`[err] ${line}`)),
178+
requestInput: handleRequestInput,
179+
});
180+
const exitCode = typeof code === 'number' ? code : 0;
181+
appendLine(`(exit ${exitCode})`);
182+
183+
// Best-effort clipboard copy to speed up sharing logs
184+
if (navigator?.clipboard?.writeText) {
185+
setTimeout(() => {
186+
navigator.clipboard.writeText(latestOutRef.current).catch(() => {});
187+
}, 0);
188+
}
138189
} catch (e) {
139190
setOut(`Error: ${e?.message || e}`);
191+
} finally {
192+
if (pendingResolveRef.current) {
193+
pendingResolveRef.current('');
194+
pendingResolveRef.current = null;
195+
}
196+
setPendingPrompt(null);
197+
setPendingInput('');
198+
setRunning(false);
140199
}
141200
}
142201

@@ -163,13 +222,30 @@ fof(b, conjecture, p).`,
163222
<textarea
164223
value={args}
165224
onChange={e => setArgs(e.target.value)}
166-
placeholder={`Example:\n --proof on --time_limit 1`}
225+
placeholder={`Example:\n --manual_cs on --show_new on --proof on`}
167226
/>
168227
</div>
169228
)}
170229
</div>
171230

172-
<p><button className="vr-run" onClick={onRun}>Run Vampire</button></p>
231+
<p><button className="vr-run" onClick={onRun} disabled={running}>Run Vampire</button></p>
232+
233+
{pendingPrompt && (
234+
<div style={{ marginBottom: '0.75rem' }}>
235+
<label>Input required (prompt: {pendingPrompt})</label>
236+
<input
237+
type="text"
238+
value={pendingInput}
239+
onChange={e => setPendingInput(e.target.value)}
240+
onKeyDown={handleKeyDown}
241+
style={{ width: '100%', padding: '0.4rem', fontFamily: 'monospace' }}
242+
autoFocus
243+
/>
244+
<button className="vr-run" onClick={submitPromptResponse} style={{ marginTop: '0.35rem' }}>
245+
Send
246+
</button>
247+
</div>
248+
)}
173249

174250
<label>Output</label>
175251
<pre style={{ maxHeight: outputMaxHeight, overflow: 'auto', marginTop: 0 }}>

0 commit comments

Comments
 (0)