- Cover the command end-to-end via shell integration
- Test the files, logging and terminal dependencies
- Re-create the log output channel after deactivate

@@ -14,3 +14,4 @@
+	proofClause: RocqDefinitionLink | null;
 }
 
 export interface RocqDefinitionLink {

@@ -20,3 +21,4 @@
+	targetName: string;
 }
 
 export interface LoopAnnotation {

@@ -46,3 +60,3 @@
 	clause: Node,
 	existing: ClauseNode | null,
-	keyword: 'PRE' | 'POST',
+	clauseName: 'PRE' | 'POST',

@@ -59,2 +75,4 @@
+async function parseLinkClause(
 	clause: Node,
 	existing: RocqDefinitionLink | null,
+	clauseName: 'SPEC' | 'PROOF',

@@ -155,3 +187,3 @@
 		}
-	});
+	}
 	const [firstInvClause] = invClauses;

@@ -0,0 +16,4 @@
+		?.activate();
+}
+
+// proofDocumentUri:proofName

@@ -0,0 +21,4 @@
+	vsRocqApi: VsRocqApi,
+	proofDocumentUri: vscode.Uri,
+	proofName: string,
+	retries = 0,

@@ -0,0 +37,4 @@
+	if (!proofs) {
+		return null;
+	}
+	const escapedProofName = proofName.replace(/[.*+?^${}()|[\]\\]/g, '\\$&');

@@ -0,0 +24,4 @@
+	retries = 0,
+): Promise<ProofBlock | null> {
+	let proofs: DocumentProofsResponse | undefined;
+	for (let attempt = 0; attempt < 1 + retries; attempt++) {

@@ -0,0 +30,4 @@
+			break;
+		} catch {
+			if (attempt < retries) {
+				await new Promise((resolve) => setTimeout(resolve, 100));

@@ -0,0 +48,4 @@
+	return proof ?? null;
+}
+
+// proofDocumentUri:definitionName

@@ -0,0 +88,4 @@
+	return null;
+}
+
+function removeComments(

@@ -0,0 +1,178 @@
+// copied from https://github.com/rocq-prover/vsrocq/blob/main/client/src/protocol/types.ts

@@ -85,1 +85,4 @@
 
+	const vsRocqApi = await getVsRocqApi();
+	if (vsRocqApi === undefined) {
+		vscode.window.showErrorMessage('failed to load vsrocq extension!');

@@ -86,0 +87,4 @@
+	if (vsRocqApi === undefined) {
+		vscode.window.showErrorMessage('failed to load vsrocq extension!');
+	} else {
+		vscode.window.showInformationMessage('loaded vsrocq extension');

@@ -86,0 +88,4 @@
+		vscode.window.showErrorMessage('failed to load vsrocq extension!');
+	} else {
+		vscode.window.showInformationMessage('loaded vsrocq extension');
+		// vsRocqApi.onProofStateChanged((p) => {

@@ -123,2 +136,4 @@
 		),
 	);
+
+	// TODO: code completions suggesting proofs/definitions to link to when writing a PROOF or SPEC clause

@@ -14,1 +23,4 @@
+): (doc: vscode.TextDocument) => Promise<void> {
+	return async (doc) => {
 		if (doc.languageId === 'c') {
+			if (!vsRocqApi) {

@@ -14,1 +25,4 @@
 		if (doc.languageId === 'c') {
+			if (!vsRocqApi) {
+				vscode.window.showErrorMessage(
+					'failing to connect to VsRocq extension!!',

@@ -28,0 +87,4 @@
+							}
+						}
+					} catch {
+						diagnostics.push(

@@ -28,0 +58,4 @@
+									vsRocqApi,
+									fileUri,
+									linkClause.targetName,
+									3, // these are retries if the vsRocqApi might not be initialized should NOT be as many in onChangeDocument

@@ -28,0 +85,4 @@
+								);
+								break;
+							}
+						}

@@ -198,11 +198,6 @@ suite('commands/createRocqModel (integration)', () => {
 			);
 
 			if (execution === undefined) {
-				// A host advertised shell integration via

@@ -0,0 +1,384 @@
+From Coq Require Import String List ZArith.

@@ -0,0 +29,4 @@
+		);
+		await vscode.window.showTextDocument(document);
+		assert.ok(vsRocqApi);
+		await delay(1_000); // letting vsrocq load the rocq document

@@ -0,0 +33,4 @@
+		return document;
+	}
+
+	test('vsrocq interpret to end', async () => {

@@ -0,0 +43,4 @@
+	});
+
+	test('vsrocqApi get proof block', async () => {
+		const document = await openAndShowTestRocqDoc('verif_sumarray.v');

@@ -0,0 +74,4 @@
+	});
+
+	test('gets blocks for minimal completed proofs', async () => {
+		const document = await openAndShowTestRocqDoc('simple_proofs.v');

@@ -0,0 +94,4 @@
+	});
+
+	test('handles exact proof names and non-proofs', async () => {
+		const document = await openAndShowTestRocqDoc('edge_case_proofs.v');

@@ -0,0 +134,4 @@
+	});
+
+	test('returns blocks for admitted and incomplete proofs', async () => {
+		const document = await openAndShowTestRocqDoc('broken_proofs.v');

@@ -0,0 +158,4 @@
+	});
+
+	test('gets ranges for single-line and multiline definitions', async () => {
+		const document = await openAndShowTestRocqDoc('definitions.v');

@@ -0,0 +193,4 @@
+	});
+
+	test('matches definition names exactly and ignores comments', async () => {
+		const document = await openAndShowTestRocqDoc('definitions.v');

@@ -0,0 +221,4 @@
+	});
+
+	test('gets definition ranges from verif_sumarray.v', async () => {
+		const document = await openAndShowTestRocqDoc('verif_sumarray.v');