Skip to content

Commit b513d86

Browse files
committed
feat: cancellation in trace display
1 parent 99f0a82 commit b513d86

File tree

2 files changed

+29
-3
lines changed

2 files changed

+29
-3
lines changed

ProofWidgets/Demos/TraceDisplay.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -586,3 +586,7 @@ def exampleAssertionFailure : Json := json% {"violation":
586586
"result": "found_violation"}
587587

588588
#displayTrace exampleAssertionFailure
589+
590+
def exampleCancelled : Json := json% {"result": "cancelled"}
591+
592+
#displayTrace exampleCancelled

widget/src/traceDisplay.tsx

Lines changed: 25 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,9 @@ type ModelCheckingResult =
7777
termination_reason: TerminationReason;
7878
trace?: TraceData | null;
7979
}
80+
| {
81+
result: "cancelled";
82+
}
8083
| {
8184
// Trace-only data without a result (for displaying execution traces)
8285
trace: TraceData;
@@ -288,11 +291,23 @@ const TheorySection: React.FC<{ theory: Record<string, unknown> }> = ({ theory }
288291

289292
/** Header showing the result status with appropriate icon */
290293
const ResultHeader: React.FC<{
291-
resultType: "found_violation" | "no_violation_found";
294+
resultType: "found_violation" | "no_violation_found" | "cancelled";
292295
violation?: Violation;
293296
exploredStates?: number;
294297
terminationReason?: TerminationReason;
295298
}> = ({ resultType, violation, exploredStates, terminationReason }) => {
299+
if (resultType === "cancelled") {
300+
return (
301+
<div className="result-header result-cancelled">
302+
<span className="result-icon"></span>
303+
<span className="result-label">Cancelled</span>
304+
<div className="result-details">
305+
Model checking was cancelled before completion
306+
</div>
307+
</div>
308+
);
309+
}
310+
296311
if (resultType === "found_violation" && violation) {
297312
let icon: string;
298313
let label: string;
@@ -388,7 +403,7 @@ const ModelCheckerView: React.FC<ModelCheckerViewProps> = ({
388403
const [showFilterPanel, setShowFilterPanel] = React.useState(false);
389404

390405
// Compute all unique field names from the trace
391-
const traceData = result.trace;
406+
const traceData = 'trace' in result ? result.trace : undefined;
392407
const allFieldNames = React.useMemo(() => {
393408
if (!traceData?.states) return [];
394409
const names = new Set<string>();
@@ -616,6 +631,11 @@ const ModelCheckerView: React.FC<ModelCheckerViewProps> = ({
616631
border: 1px solid var(--vscode-inputValidation-infoBorder);
617632
color: var(--vscode-inputValidation-infoForeground, var(--vscode-foreground));
618633
}
634+
.result-cancelled {
635+
background: var(--vscode-inputValidation-warningBackground);
636+
border: 1px solid var(--vscode-inputValidation-warningBorder);
637+
color: var(--vscode-inputValidation-warningForeground, var(--vscode-foreground));
638+
}
619639
.result-icon { font-size: 18px; }
620640
.result-label { font-size: 14px; }
621641
.result-details {
@@ -737,7 +757,9 @@ const ModelCheckerView: React.FC<ModelCheckerViewProps> = ({
737757
<>
738758
{'result' in result && (
739759
<>
740-
{result.result === "no_violation_found" ? (
760+
{result.result === "cancelled" ? (
761+
<ResultHeader resultType="cancelled" />
762+
) : result.result === "no_violation_found" ? (
741763
<ResultHeader
742764
resultType="no_violation_found"
743765
exploredStates={result.explored_states}

0 commit comments

Comments
 (0)