Skip to content

Commit 011f303

Browse files
jackeownjackeown
committed
latest. hopefully good and interactive?
1 parent f390931 commit 011f303

6 files changed

Lines changed: 513 additions & 32 deletions

File tree

‎buildVampireWasm.sh‎

Lines changed: 28 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,50 @@
11
#!/usr/bin/env bash
22
set -euo pipefail
33

4+
VAMPIRE_DIR=${VAMPIRE_DIR:-vampire}
5+
# Pin to a known-good commit for reproducible builds; override via env if needed.
6+
VAMPIRE_REF=${VAMPIRE_REF:-5a7e9a5e82bc89aa8303ae5033d1d22b555c6fd7}
7+
VAMPIRE_RECLONE=${VAMPIRE_RECLONE:-0}
8+
49
# 1. Clone the Vampire repo if not already present
5-
if [[ ! -d vampire ]]; then
6-
echo "Cloning Vampire..."
7-
git clone https://github.com/vprover/vampire.git
10+
if [[ "$VAMPIRE_RECLONE" == "1" && -d "$VAMPIRE_DIR" ]]; then
11+
echo "Removing existing '$VAMPIRE_DIR' for a clean clone..."
12+
rm -rf "$VAMPIRE_DIR"
13+
fi
14+
15+
if [[ ! -d "$VAMPIRE_DIR" ]]; then
16+
echo "Cloning Vampire ($VAMPIRE_REF)..."
17+
git clone https://github.com/vprover/vampire.git "$VAMPIRE_DIR"
18+
if [[ -n "$VAMPIRE_REF" ]]; then
19+
git -C "$VAMPIRE_DIR" checkout "$VAMPIRE_REF"
20+
fi
821
else
9-
echo "Repo 'vampire' already exists, skipping clone."
22+
echo "Repo '$VAMPIRE_DIR' already exists, using it as-is."
23+
if [[ -n "$VAMPIRE_REF" ]]; then
24+
current_ref=$(git -C "$VAMPIRE_DIR" rev-parse HEAD)
25+
if [[ "$current_ref" != "$VAMPIRE_REF" ]]; then
26+
echo "Warning: '$VAMPIRE_DIR' is at $current_ref, expected $VAMPIRE_REF."
27+
echo "Set VAMPIRE_RECLONE=1 to reclone a clean copy at the pinned ref."
28+
fi
29+
fi
1030
fi
1131

1232
BUILD_DIR=${BUILD_DIR:-build-ems}
1333

1434
# 2. Copy smallWasmBuild.sh into the repo
1535
echo "Copying smallWasmBuild.sh..."
16-
cp -f smallWasmBuild.sh vampire/
36+
cp -f smallWasmBuild.sh "$VAMPIRE_DIR"/
1737

1838
# 3. Apply patch/edit script to CMakeLists.txt
1939
echo "Editing CMakeLists.txt..."
20-
./editCMakeLists.sh vampire/CMakeLists.txt
40+
./editCMakeLists.sh "$VAMPIRE_DIR"/CMakeLists.txt
2141

2242
# 3b. Apply interactive stdin/stdout hooks for the WASM build
2343
echo "Applying interactive WASM patch..."
24-
./patchVampireInteractive.sh vampire
44+
./patchVampireInteractive.sh "$VAMPIRE_DIR"
2545

2646
# 4. cd into vampire
27-
cd vampire
47+
cd "$VAMPIRE_DIR"
2848

2949
# 5. Run build script
3050
echo "Running smallWasmBuild.sh..."

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

Lines changed: 73 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -112,9 +112,14 @@ fof(b, conjecture, p).`,
112112
const pendingResolveRef = useRef(null);
113113
const pendingPromiseRef = useRef(null);
114114
const [running, setRunning] = useState(false);
115+
const [hasOutput, setHasOutput] = useState(false);
116+
const hasOutputRef = useRef(false);
117+
const [runningDots, setRunningDots] = useState(0);
115118
const outWrapRef = useRef(null);
116119
const outCodeRef = useRef(null);
117120
const latestOutRef = useRef('Ready.');
121+
const flushTimerRef = useRef(null);
122+
const cancelRunRef = useRef(null);
118123
const runIdRef = useRef(0);
119124

120125
useEffect(() => {
@@ -125,7 +130,7 @@ fof(b, conjecture, p).`,
125130
useEffect(() => {
126131
if (typeof window === 'undefined') return;
127132
highlightNowOrWhenReady(outCodeRef.current);
128-
}, [out, outputLanguage, pendingPrompt, pendingInput, pendingInline]);
133+
}, [out, outputLanguage]);
129134

130135
useEffect(() => {
131136
if (!outWrapRef.current) return;
@@ -137,8 +142,24 @@ fof(b, conjecture, p).`,
137142
outWrapRef.current?.focus({ preventScroll: true });
138143
}, [pendingPrompt]);
139144

145+
useEffect(() => {
146+
if (!running) {
147+
setRunningDots(0);
148+
return;
149+
}
150+
const id = setInterval(() => {
151+
setRunningDots(prev => (prev + 1) % 3);
152+
}, 500);
153+
return () => clearInterval(id);
154+
}, [running]);
155+
140156
const visibleOut = (() => {
141-
if (pendingPrompt === null) return out;
157+
if (pendingPrompt === null) {
158+
if (!running || hasOutput) return out;
159+
const dots = '.'.repeat((runningDots % 3) + 1);
160+
const sep = out ? '\n' : '';
161+
return out + sep + `Running${dots}`;
162+
}
142163
const lastLineRaw = out.split('\n').slice(-1)[0] || '';
143164
const lastLine = lastLineRaw.replace(/\s+$/, '');
144165
const forceInline = pendingMatchText && lastLine.endsWith(pendingMatchText);
@@ -149,27 +170,40 @@ fof(b, conjecture, p).`,
149170
return out + sep + (pendingPrompt ?? '> ') + pendingInput;
150171
})();
151172

173+
const scheduleFlush = () => {
174+
if (flushTimerRef.current) return;
175+
flushTimerRef.current = setTimeout(() => {
176+
flushTimerRef.current = null;
177+
setOut(latestOutRef.current || '');
178+
}, 50);
179+
};
180+
181+
useEffect(() => () => {
182+
if (flushTimerRef.current) {
183+
clearTimeout(flushTimerRef.current);
184+
}
185+
}, []);
186+
152187
// Append a line to the transcript (one big string for highlighting)
153188
const appendLine = (text) => {
154-
setOut(prev => {
155-
const next = prev ? `${prev}\n${text}` : text;
156-
latestOutRef.current = next;
157-
return next;
158-
});
189+
const prev = latestOutRef.current || '';
190+
latestOutRef.current = prev ? `${prev}\n${text}` : text;
191+
scheduleFlush();
159192
};
160193

161194
const appendInline = (text) => {
162-
setOut(prev => {
163-
const next = (prev || '') + text;
164-
latestOutRef.current = next;
165-
return next;
166-
});
195+
latestOutRef.current = (latestOutRef.current || '') + text;
196+
scheduleFlush();
167197
};
168198

169199
const handleRequestInput = (promptText) => {
170200
if (pendingResolveRef.current) {
171201
return pendingPromiseRef.current || new Promise(() => {});
172202
}
203+
if (!hasOutputRef.current) {
204+
hasOutputRef.current = true;
205+
setHasOutput(true);
206+
}
173207
const raw = String(promptText ?? '');
174208
const trimmed = raw.replace(/\s+$/, '');
175209
const lastLineRaw = (latestOutRef.current || '').split('\n').slice(-1)[0] || '';
@@ -240,12 +274,19 @@ fof(b, conjecture, p).`,
240274
async function onRun() {
241275
const newRunId = runIdRef.current + 1;
242276
runIdRef.current = newRunId;
277+
if (cancelRunRef.current) {
278+
cancelRunRef.current();
279+
cancelRunRef.current = null;
280+
}
243281
if (pendingResolveRef.current) {
244282
pendingResolveRef.current = null;
245283
pendingPromiseRef.current = null;
246284
}
247285
setRunning(true);
248-
setOut('Running…');
286+
setHasOutput(false);
287+
hasOutputRef.current = false;
288+
latestOutRef.current = '';
289+
setOut('');
249290
setPendingPrompt(null);
250291
setPendingInput('');
251292
setPendingInline(false);
@@ -266,16 +307,31 @@ fof(b, conjecture, p).`,
266307
args,
267308
onStdout: (msg) => {
268309
if (runIdRef.current !== newRunId) return;
269-
String(msg ?? '').split('\n').forEach(appendLine);
310+
const text = String(msg ?? '');
311+
if (text && !hasOutputRef.current) {
312+
hasOutputRef.current = true;
313+
setHasOutput(true);
314+
}
315+
text.split('\n').forEach(appendLine);
270316
},
271317
onStderr: (msg) => {
272318
if (runIdRef.current !== newRunId) return;
273-
String(msg ?? '').split('\n').forEach(line => appendLine(`[err] ${line}`));
319+
const text = String(msg ?? '');
320+
if (text && !hasOutputRef.current) {
321+
hasOutputRef.current = true;
322+
setHasOutput(true);
323+
}
324+
text.split('\n').forEach(line => appendLine(`[err] ${line}`));
274325
},
275326
requestInput: (promptText) => {
276327
if (runIdRef.current !== newRunId) return new Promise(() => {});
277328
return handleRequestInput(promptText);
278329
},
330+
onReady: (ready) => {
331+
if (ready && typeof ready.cancel === 'function') {
332+
cancelRunRef.current = ready.cancel;
333+
}
334+
},
279335
});
280336
if (runIdRef.current === newRunId) {
281337
const exitCode = typeof code === 'number' ? code : 0;
@@ -300,6 +356,8 @@ fof(b, conjecture, p).`,
300356
setPendingSpacer('');
301357
setPendingMatchText('');
302358
setRunning(false);
359+
cancelRunRef.current = null;
360+
scheduleFlush();
303361
}
304362
}
305363
}

‎docusaurus-site/static/vampire-runner/script.js‎

Lines changed: 105 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,108 @@ export function shellQuote(argv) {
6767
}
6868

6969
// ---------- Runner APIs ----------
70+
function buildArgv(tptp, args) {
71+
const argv = parseArgs(String(args ?? ''));
72+
if (!argv.some(x => x.endsWith('.p') || x.startsWith('/'))) {
73+
argv.push('/work/input.p');
74+
}
75+
return argv;
76+
}
77+
78+
async function runVampireInWorker({ tptp, args, onStdout, onStderr, requestInput, onReady }) {
79+
const base = getBaseUrl();
80+
const workerUrl = base + 'vampire-runner/worker.js';
81+
const worker = new Worker(workerUrl, { type: 'module' });
82+
83+
const stdoutBuf = [];
84+
const stderrBuf = [];
85+
let resolveRun;
86+
let resolved = false;
87+
const done = new Promise((resolve) => (resolveRun = resolve));
88+
const finish = (code) => {
89+
if (resolved) return;
90+
resolved = true;
91+
resolveRun({
92+
stdout: stdoutBuf.join('\n'),
93+
stderr: stderrBuf.join('\n'),
94+
code
95+
});
96+
};
97+
98+
worker.onmessage = async (ev) => {
99+
const msg = ev.data || {};
100+
if (msg.type === 'stdout') {
101+
const line = String(msg.data ?? '');
102+
stdoutBuf.push(line);
103+
onStdout?.(line);
104+
return;
105+
}
106+
if (msg.type === 'stderr') {
107+
const line = String(msg.data ?? '');
108+
stderrBuf.push(line);
109+
onStderr?.(line);
110+
return;
111+
}
112+
if (msg.type === 'requestInput') {
113+
if (typeof requestInput !== 'function') {
114+
worker.postMessage({ type: 'input', value: '' });
115+
return;
116+
}
117+
try {
118+
const answer = await requestInput(String(msg.prompt ?? ''));
119+
worker.postMessage({ type: 'input', value: answer ?? '' });
120+
} catch {
121+
worker.postMessage({ type: 'input', value: '' });
122+
}
123+
return;
124+
}
125+
if (msg.type === 'done') {
126+
finish(typeof msg.code === 'number' ? msg.code : 0);
127+
worker.terminate();
128+
return;
129+
}
130+
if (msg.type === 'fatal') {
131+
const line = String(msg.message ?? 'FATAL');
132+
stderrBuf.push(line);
133+
onStderr?.(line);
134+
finish(-1);
135+
worker.terminate();
136+
}
137+
};
138+
139+
worker.onerror = (err) => {
140+
const line = String(err?.message || err);
141+
stderrBuf.push(line);
142+
onStderr?.(line);
143+
finish(-1);
144+
worker.terminate();
145+
};
146+
147+
const argv = buildArgv(tptp, args);
148+
worker.postMessage({
149+
type: 'run',
150+
tptp: String(tptp ?? ''),
151+
argv
152+
});
153+
154+
if (typeof onReady === 'function') {
155+
onReady({
156+
cancel: () => {
157+
if (!resolved) {
158+
finish(-1);
159+
}
160+
worker.terminate();
161+
}
162+
});
163+
}
164+
165+
return done;
166+
}
167+
70168
export async function runVampireRaw({ tptp, args, onStdout, onStderr, requestInput, onReady }) {
169+
if (typeof Worker !== 'undefined') {
170+
return runVampireInWorker({ tptp, args, onStdout, onStderr, requestInput, onReady });
171+
}
71172
const base = getBaseUrl();
72173

73174
const glueUrl = base + 'vampire-runner/vampire.js';
@@ -89,6 +190,7 @@ export async function runVampireRaw({ tptp, args, onStdout, onStderr, requestInp
89190
};
90191

91192
const isInteractive = typeof requestInput === 'function';
193+
const stdin = () => null;
92194
const Module = {
93195
noInitialRun: true,
94196
// Keep the runtime alive during interactive runs; allow exit otherwise
@@ -107,6 +209,8 @@ export async function runVampireRaw({ tptp, args, onStdout, onStderr, requestInp
107209
vampireReadline: requestInput
108210
? (prompt) => Promise.resolve(requestInput(String(prompt ?? '')))
109211
: undefined,
212+
stdin,
213+
input: stdin,
110214
onExit: (code) => finish(code),
111215
onAbort: (what) => {
112216
const msg = String(what ?? 'abort');
@@ -125,10 +229,7 @@ export async function runVampireRaw({ tptp, args, onStdout, onStderr, requestInp
125229
try { mod.FS.mkdir('/work'); } catch {}
126230
mod.FS.writeFile('/work/input.p', new TextEncoder().encode(String(tptp ?? '')));
127231

128-
const argv = parseArgs(String(args ?? ''));
129-
if (!argv.some(x => x.endsWith('.p') || x.startsWith('/'))) {
130-
argv.push('/work/input.p');
131-
}
232+
const argv = buildArgv(tptp, args);
132233

133234
const ret = mod.callMain(argv);
134235
try {

0 commit comments

Comments
 (0)