Remove visualize since it has been removed in Kani

Author: celinval

docs/dev-documentation.md

@@ -1,6 +1,6 @@
 ### Build from Source
 
-The Kani extension is built using NPM and nodejs. Here is the [NPM install guide](https://nodejs.dev/en/learn/how-to-install-nodejs/)
+The Kani extension is built using NPM and nodejs. Here is the [NPM install guide](https://nodejs.org/en/download)
 for steps on installing it on your operating system.
 
 You will also need to install `make` on your machine using `apt-get install build-essential` or `brew install make`.

docs/user-guide.md

@@ -11,9 +11,6 @@ This guide provides the various workflows that you can use to verify and debug y
   - [Generate a counterexample unit test](#generate-a-counterexample-unit-test)
   - [Run Kani-generated unit test](#run-kani-generated-unit-test)
   - [Debug a Kani-generated unit test](#debug-kani-generated-unit-test)
-- [View trace report](#view-trace-report)
-  - [Generate trace report](#generate-trace-report)
-  - [View trace report in window](#view-trace-report-in-window)
 - [Kani output logging](#kani-output-logging)
   - [View full Kani output](#view-full-kani-output)
 - [Coverage information](#coverage-information)
@@ -32,11 +29,9 @@ This is how the VSCode window looks like when you click on the panel:
 
 You can then run your harnesses using the harness tree view by clicking the play button beside the harness that was automatically picked up by the Kani VSCode Extension.
 Once you run the harness using the extension, you are shown an error message if the verification fails.
-You are then presented with two options:
- 1. [Generate the report for the harness](#view-trace-report)
- 2. [Run concrete playback to generate unit tests](#use-concrete-playback-to-debug-a-kani-harness).
+You are then presented with the option to
+[run concrete playback to generate unit tests](#use-concrete-playback-to-debug-a-kani-harness).
 
-We are going to describe the flows in detail in their respective sections, but explain the concrete playback feature first.
 
 ![Image: run harness.gif](../resources/screenshots/run-proof.gif)
 
@@ -70,22 +65,6 @@ By setting breakpoints and clicking the `Debug Test (Kani)` button, you are take
 You can then use the debugger controller to step through, into, out of, replay and also change values on the trace panel on the left for interactive debugging.
 
 
-### View trace report
-
-#### Generate trace report
-
-By clicking the `Generate report for (your harness)` option in the error banner, you can view the trace for the harness in an HTML report.
-
-![Generate Report](../resources/screenshots/generate-report.png)
-
-#### View trace report in window
-
-You can click on the `Preview in Editor` button to view the HTML trace within VSCode.
-It should look like this:
-
-![View Report](../resources/screenshots/view-report.png)
-
-
 ### Kani output logging
 
 #### View full Kani output

resources/screenshots/generate-report.png

@@ -21,7 +21,6 @@ import { callConcretePlayback } from './ui/concrete-playback/concretePlayback';
 import { runKaniPlayback } from './ui/concrete-playback/kaniPlayback';
 import CoverageConfig from './ui/coverage/config';
 import { CoverageRenderer, runCodeCoverageAction } from './ui/coverage/coverageInfo';
-import { callViewerReport } from './ui/reportView/callReport';
 import { showInformationMessage } from './ui/showMessage';
 import { SourceCodeParser } from './ui/sourceCodeParser';
 import { startWatchingWorkspace } from './ui/watchWorkspace';
@@ -181,15 +180,7 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
 		showInformationMessage('Kani.runcargoKani');
 	});
 
-	// Register the run viewer report command
-	const runningViewerReport = vscode.commands.registerCommand(
-		'Kani.runViewerReport',
-		async (harnessArgs) => {
-			callViewerReport('Kani.runViewerReport', harnessArgs);
-		},
-	);
-
-	// Register the run viewer report command
+	// Register the concrete playback command
 	const runningConcretePlayback = vscode.commands.registerCommand(
 		'Kani.runConcretePlayback',
 		async (harnessArgs) => {
@@ -277,7 +268,6 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
 
 	context.subscriptions.push(runKani);
 	context.subscriptions.push(runcargoKani);
-	context.subscriptions.push(runningViewerReport);
 	context.subscriptions.push(runningConcretePlayback);
 	context.subscriptions.push(providerDisposable);
 	context.subscriptions.push(

resources/screenshots/view-report.png

@@ -443,34 +443,14 @@ class FailedCase extends TestCase {
 	}
 
 	handleFailure(): TestMessage {
-		const failureMessage: MarkdownString = this.appendLink(this.failed_checks);
-		const finalFailureMessage: MarkdownString = this.appendConcretePlaybackLink(failureMessage);
+		const finalFailureMessage: MarkdownString = this.appendConcretePlaybackLink(this.failed_checks);
 		const messageWithLink = new TestMessage(finalFailureMessage);
 		return messageWithLink;
 	}
 
 	// Add link and present to the user as the diff message
-	appendLink(failedChecks: string): MarkdownString {
+	appendConcretePlaybackLink(failedChecks: string): MarkdownString {
 		const sample: MarkdownString = this.makeMarkdown(failedChecks);
-		// vscode.commands.executeCommand('Kani.runViewerReport', this.harness_name);
-		const args = [
-			{
-				harnessName: this.harness_name,
-				harnessFile: this.file_name,
-				harnessType: this.proof_boolean,
-			},
-		];
-		const stageCommandUri = Uri.parse(
-			`command:Kani.runViewerReport?${encodeURIComponent(JSON.stringify(args))}`,
-		);
-		sample.appendMarkdown(`[Generate report for ${this.harness_name}](${stageCommandUri})`);
-
-		return sample;
-	}
-
-	// Add link and present to the user as the diff message
-	appendConcretePlaybackLink(sample: MarkdownString): MarkdownString {
-		sample.appendMarkdown('<br>');
 		const args = [
 			{
 				harnessName: this.harness_name,

src/extension.ts

@@ -11,7 +11,7 @@ import GlobalConfig from '../../globalConfig';
 import { CommandArgs, getPackageName, getRootDir, splitCommand } from '../../utils';
 
 /**
- * Call the visualize flag on the harness and render the html page
+ * Call the concrete playback feature in Kani.
  *
  * @param commandURI - vscode command that is being executed
  * @param harnessObj - metadata about the harness
@@ -37,7 +37,7 @@ export async function callConcretePlayback(harnessObj: {
 		finalCommand = `${responseObject}`;
 	}
 
-	// Wait for the the visualize command to finish generating the report
+	// Wait for the the playback command to finish
 	executePlaybackCommand(finalCommand);
 }