diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml index 78da7a97..18fee300 100644 --- a/.github/workflows/build-and-test.yml +++ b/.github/workflows/build-and-test.yml @@ -20,7 +20,7 @@ on: env: coqlsp-path: "coq-lsp" - coqlsp-version: "0.1.9+8.19" + coqlsp-version: "0.2.2+8.19" artifact-name: ubuntu-latest-build jobs: @@ -60,7 +60,7 @@ jobs: env: OPAMYES: true run: | - opam install coq-lsp.0.1.9+8.19 + opam install coq-lsp.0.2.2+8.19 eval $(opam env) - name: Install Node.js diff --git a/.prettierrc.json b/.prettierrc.json index d9954e13..a2ed5e7b 100644 --- a/.prettierrc.json +++ b/.prettierrc.json @@ -7,5 +7,6 @@ "printWidth": 80, "importOrder": ["^[./]*llm/(.*)$", "^[./]*coqLsp/(.*)$", "^[./]*core/(.*)$", "^../", "^./"], "importOrderSeparation": true, - "importOrderSortSpecifiers": true + "importOrderSortSpecifiers": true, + "importOrderParserPlugins": ["typescript", "@trivago/prettier-plugin-sort-imports", "decorators-legacy"] } \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json index 954f11e8..69726f9b 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,23 +1,26 @@ // Place your settings in this file to overwrite default and user settings. { "files.exclude": { + "**/*.vo": true, + "**/*.vok": true, + "**/*.vos": true, + "**/*.aux": true, + "**/*.glob": true, "**/.git": true, "**/.svn": true, "**/.hg": true, "**/CVS": true, "**/.DS_Store": true, "**/Thumbs.db": true, - "**/*.vo": true, - "**/*.vok": true, - "**/*.vos": true, - "**/*.aux": true, - "**/*.glob": true, - "out": false, - "**/*_cp_aux.v": true + "out": false }, "search.exclude": { "out": true // set this to false to include "out" folder in search results }, // Turn off tsc task auto detection since we have the necessary tasks as npm scripts - "typescript.tsc.autoDetect": "off" + "typescript.tsc.autoDetect": "off", + "coq-lsp.check_only_on_request": false, + "eslint.options": { + "experimentalDecorators": true + } } \ No newline at end of file diff --git a/CHANGELOG.md b/CHANGELOG.md index 6ff17b15..7ea7d76f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,19 @@ # Changelog +## 2.3.1 + +The version increment is minor, yet the changes are significant. The main focus of this release was to improve interaction with the `coq-lsp` server. We now completely got rid of temporary files in the `extension` part of `CoqPilot`. This was done thanks to [ejgallego](https://github.com/ejgallego) and his improvements in `coq-lsp`. Now checking of proofs is done via the `proof/goals` request via `command` parameter, which is much more reliable and faster. Now a single `lsp` server is created for the plugin until being explicitly closed, and it tracks changes in the file. If you are using `coq-lsp` plugin itself, it will help you to always keep track of whether file is checked or not. When `CoqPilot` is ran on a completely checked file, it will not bring any significant overhead apart from requests to the Completion Services. + +### Public changes +- Added a toggle button to enable/disable the extension +- Using the toggle switch, user can now abort the proof generation process +- Significant performance improvements in proof checking that are especially easy to see for large files + +### Internal changes +- Get rid of temporary files in the `extension` part of `CoqPilot` +- Refactor `CoqLspClient` +- Make computation of `initialGoal` for premises optional to avoid unnecessary requests to `coq-lsp` + ## 2.3.0 **A major upgrade of the benchmarking system**: At the moment, only a little **new** functionality is provided; moreover, the ability to run benchmarks on Tactician/CoqHammer is temporarily unavailable. However, it will soon be restored and improved. Excessive work has been done to make the benchmarking system more flexible, secure, robust, self-contained, and easy to use. Experiments via our benchmarking framework have been made more accessible than ever. The configurability and reliability of the pipeline have been improved drastically. In a nutshell, the main features of the improved benchmarking system include: diff --git a/README.md b/README.md index d5afe037..f8eb3ce8 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,4 @@ -# CoqPilot - -![Version](https://img.shields.io/badge/version-v2.3.0-blue?style=flat-square) +# CoqPilot ![Version](https://img.shields.io/badge/version-v2.3.1-blue?style=flat-square) *Authors:* Andrei Kozyrev, Gleb Solovev, Nikita Khramov, and Anton Podkopaev, [Programming Languages and Tools Lab](https://lp.jetbrains.com/research/plt_lab/) at JetBrains Research. @@ -30,7 +28,7 @@ ## Requirements -* `coq-lsp` version `0.1.9+8.19` is currently required to run the extension. +* `coq-lsp` version `0.2.2+8.19` is currently required to run the extension. ## Brief technical overview @@ -68,7 +66,7 @@ As soon as at least one valid proof is found, it is substituted in the editor an To run the extension, you must install a `coq-lsp` server. Depending on the system used in your project, you should install it using `opam` or `nix`. A well-configured `nix` project should have the `coq-lsp` server installed as a dependency. To install `coq-lsp` using `opam`, you can use the following commands: ```bash -opam pin add coq-lsp 0.1.9+8.19 +opam pin add coq-lsp 0.2.2+8.19 opam install coq-lsp ``` For more information on how to install `coq-lsp` please refer to [coq-lsp](https://github.com/ejgallego/coq-lsp). diff --git a/dataset/imm b/dataset/imm index 16637a92..14025d11 160000 --- a/dataset/imm +++ b/dataset/imm @@ -1 +1 @@ -Subproject commit 16637a922a817230ca03e0d2f6b0f961cc7d410a +Subproject commit 14025d11ee217b5397c544917c5623a80abbd28e diff --git a/package-lock.json b/package-lock.json index 2a0a8cee..1a236c72 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,12 +1,12 @@ { "name": "coqpilot", - "version": "2.3.0", + "version": "2.3.1", "lockfileVersion": 2, "requires": true, "packages": { "": { "name": "coqpilot", - "version": "2.3.0", + "version": "2.3.1", "dependencies": { "@codemirror/autocomplete": "^6.9.1", "ajv": "^8.12.0", @@ -17,7 +17,7 @@ "event-source-polyfill": "^1.0.31", "i": "^0.3.7", "mocha-param": "^2.0.1", - "node-ipc": "^11.1.0", + "node-ipc": "^12.0.0", "npm": "^10.4.0", "openai": "^4.6.0", "path": "^0.12.7", @@ -26,6 +26,7 @@ "tiktoken": "^1.0.17", "tmp": "^0.2.3", "toml": "^3.0.0", + "ts-results": "^3.3.0", "vscode-languageclient": "^9.0.1", "yargs": "^17.7.2" }, @@ -1242,9 +1243,9 @@ } }, "node_modules/axios": { - "version": "1.7.5", - "resolved": "https://registry.npmjs.org/axios/-/axios-1.7.5.tgz", - "integrity": "sha512-fZu86yCo+svH3uqJ/yTdQ0QHpQu5oL+/QE+QPSv6BZSkDAoky9vytxp7u5qk83OJFS3kEBcesWni9WTZAv3tSw==", + "version": "1.7.7", + "resolved": "https://registry.npmjs.org/axios/-/axios-1.7.7.tgz", + "integrity": "sha512-S4kL7XrjgBmvdGut0sN3yJxqYzrDOnivkBiN0OFs6hLiUam3UPvswUo0kqGyhqUZGEOytHyumEdXsAkgCOUf3Q==", "dependencies": { "follow-redirects": "^1.15.6", "form-data": "^4.0.0", @@ -3092,15 +3093,13 @@ } }, "node_modules/node-ipc": { - "version": "11.1.0", - "resolved": "https://registry.npmjs.org/node-ipc/-/node-ipc-11.1.0.tgz", - "integrity": "sha512-BfE098Uyx06O//uatDNbSNxa5HLejwd2gV33yU0VfYv5wm4e22Um3VnNTOacqSxcl02v4fx6ZNUqJG9ZK+0Ufg==", - "license": "MIT", + "version": "12.0.0", + "resolved": "https://registry.npmjs.org/node-ipc/-/node-ipc-12.0.0.tgz", + "integrity": "sha512-QHJ2gAJiqA3cM7cQiRjLsfCOBRB0TwQ6axYD4FSllQWipEbP6i7Se1dP8EzPKk5J1nCe27W69eqPmCoKyQ61Vg==", "dependencies": { "event-pubsub": "5.0.3", "js-message": "1.0.7", "js-queue": "2.0.2", - "peacenotwar": "^9.1.5", "strong-type": "^1.0.1" }, "engines": { @@ -5689,15 +5688,6 @@ "node": ">=8" } }, - "node_modules/peacenotwar": { - "version": "9.1.7", - "resolved": "https://registry.npmjs.org/peacenotwar/-/peacenotwar-9.1.7.tgz", - "integrity": "sha512-tMTCcK/MFZQXg6cJPYv1rYAU5V4G1jw7vyJ6cxX35BZ+Jb58of7TTTwktK6LCGouPlyEkIDFLT0KYq/hE1Lstg==", - "license": "GPL-3.0-or-later", - "engines": { - "node": ">=4.0.0" - } - }, "node_modules/picomatch": { "version": "2.3.1", "resolved": "https://registry.npmjs.org/picomatch/-/picomatch-2.3.1.tgz", @@ -6359,6 +6349,11 @@ "resolved": "https://registry.npmjs.org/tr46/-/tr46-0.0.3.tgz", "integrity": "sha512-N3WMsuqV66lT30CrXNbEjx4GEwlow3v6rr4mCcv6prnfwhS01rkgyFdjPNBYd9br7LpXV1+Emh01fHnq2Gdgrw==" }, + "node_modules/ts-results": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/ts-results/-/ts-results-3.3.0.tgz", + "integrity": "sha512-FWqxGX2NHp5oCyaMd96o2y2uMQmSu8Dey6kvyuFdRJ2AzfmWo3kWa4UsPlCGlfQ/qu03m09ZZtppMoY8EMHuiA==" + }, "node_modules/tslib": { "version": "1.14.1", "resolved": "https://registry.npmjs.org/tslib/-/tslib-1.14.1.tgz", @@ -7557,9 +7552,9 @@ "integrity": "sha512-kNOjDqAh7px0XWNI+4QbzoiR/nTkHAWNud2uvnJquD1/x5a7EQZMJT0AczqK0Qn67oY/TTQ1LbUKajZpp3I9tQ==" }, "axios": { - "version": "1.7.5", - "resolved": "https://registry.npmjs.org/axios/-/axios-1.7.5.tgz", - "integrity": "sha512-fZu86yCo+svH3uqJ/yTdQ0QHpQu5oL+/QE+QPSv6BZSkDAoky9vytxp7u5qk83OJFS3kEBcesWni9WTZAv3tSw==", + "version": "1.7.7", + "resolved": "https://registry.npmjs.org/axios/-/axios-1.7.7.tgz", + "integrity": "sha512-S4kL7XrjgBmvdGut0sN3yJxqYzrDOnivkBiN0OFs6hLiUam3UPvswUo0kqGyhqUZGEOytHyumEdXsAkgCOUf3Q==", "requires": { "follow-redirects": "^1.15.6", "form-data": "^4.0.0", @@ -8905,14 +8900,13 @@ } }, "node-ipc": { - "version": "11.1.0", - "resolved": "https://registry.npmjs.org/node-ipc/-/node-ipc-11.1.0.tgz", - "integrity": "sha512-BfE098Uyx06O//uatDNbSNxa5HLejwd2gV33yU0VfYv5wm4e22Um3VnNTOacqSxcl02v4fx6ZNUqJG9ZK+0Ufg==", + "version": "12.0.0", + "resolved": "https://registry.npmjs.org/node-ipc/-/node-ipc-12.0.0.tgz", + "integrity": "sha512-QHJ2gAJiqA3cM7cQiRjLsfCOBRB0TwQ6axYD4FSllQWipEbP6i7Se1dP8EzPKk5J1nCe27W69eqPmCoKyQ61Vg==", "requires": { "event-pubsub": "5.0.3", "js-message": "1.0.7", "js-queue": "2.0.2", - "peacenotwar": "^9.1.5", "strong-type": "^1.0.1" } }, @@ -10601,11 +10595,6 @@ "integrity": "sha512-gDKb8aZMDeD/tZWs9P6+q0J9Mwkdl6xMV8TjnGP3qJVJ06bdMgkbBlLU8IdfOsIsFz2BW1rNVT3XuNEl8zPAvw==", "dev": true }, - "peacenotwar": { - "version": "9.1.7", - "resolved": "https://registry.npmjs.org/peacenotwar/-/peacenotwar-9.1.7.tgz", - "integrity": "sha512-tMTCcK/MFZQXg6cJPYv1rYAU5V4G1jw7vyJ6cxX35BZ+Jb58of7TTTwktK6LCGouPlyEkIDFLT0KYq/hE1Lstg==" - }, "picomatch": { "version": "2.3.1", "resolved": "https://registry.npmjs.org/picomatch/-/picomatch-2.3.1.tgz", @@ -11088,6 +11077,11 @@ "resolved": "https://registry.npmjs.org/tr46/-/tr46-0.0.3.tgz", "integrity": "sha512-N3WMsuqV66lT30CrXNbEjx4GEwlow3v6rr4mCcv6prnfwhS01rkgyFdjPNBYd9br7LpXV1+Emh01fHnq2Gdgrw==" }, + "ts-results": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/ts-results/-/ts-results-3.3.0.tgz", + "integrity": "sha512-FWqxGX2NHp5oCyaMd96o2y2uMQmSu8Dey6kvyuFdRJ2AzfmWo3kWa4UsPlCGlfQ/qu03m09ZZtppMoY8EMHuiA==" + }, "tslib": { "version": "1.14.1", "resolved": "https://registry.npmjs.org/tslib/-/tslib-1.14.1.tgz", diff --git a/package.json b/package.json index a5b9fb42..1c93e85a 100644 --- a/package.json +++ b/package.json @@ -8,7 +8,7 @@ "url": "https://github.com/JetBrains-Research/coqpilot" }, "publisher": "JetBrains-Research", - "version": "2.3.0", + "version": "2.3.1", "engines": { "vscode": "^1.82.0" }, @@ -392,6 +392,7 @@ "pretest": "npm run compile && npm run lint", "test": "npm run test-only", "clean": "rm -rf out", + "rebuild": "npm run clean && npm run compile && npm run format", "rebuild-test-resources": "cd ./src/test/resources/coqProj && make clean && make", "preclean-test": "npm run clean && npm run rebuild-test-resources && npm run compile && npm run lint", "clean-test": "npm run test-only", @@ -441,7 +442,7 @@ "event-source-polyfill": "^1.0.31", "i": "^0.3.7", "mocha-param": "^2.0.1", - "node-ipc": "^11.1.0", + "node-ipc": "^12.0.0", "npm": "^10.4.0", "openai": "^4.6.0", "path": "^0.12.7", @@ -450,6 +451,7 @@ "tiktoken": "^1.0.17", "tmp": "^0.2.3", "toml": "^3.0.0", + "ts-results": "^3.3.0", "vscode-languageclient": "^9.0.1", "yargs": "^17.7.2" } diff --git a/set_gitignore.sh b/set_gitignore.sh deleted file mode 100755 index 26d8d06d..00000000 --- a/set_gitignore.sh +++ /dev/null @@ -1,33 +0,0 @@ -#!/bin/bash - -# Git config directory -directory=~/.config/git - -# Check if the directory exists -if [ ! -d "$directory" ]; then - # If not, create directory - echo "Git directory not found. Creating..." - mkdir $directory -else - echo "Git directory exists." -fi - -# Navigate to the directory -cd $directory - -# Check if ignore file exists -if [ ! -f "ignore" ]; then - # If not, create file - echo "Ignore file not found. Creating..." - touch ignore -else - echo "Ignore file exists." -fi - -# Append the string to the file -echo "Appending string to the file..." -echo "*_cp_aux.v" >> ignore - -# Display the contents of the file -echo "Contents of the ignore file:" -cat ignore \ No newline at end of file diff --git a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/checkProofs.ts b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/checkProofs.ts index ac771628..93606ce4 100644 --- a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/checkProofs.ts +++ b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/checkProofs.ts @@ -7,6 +7,7 @@ import { } from "../../../../../../core/coqProofChecker"; import { stringifyAnyValue } from "../../../../../../utils/printers"; +import { Uri } from "../../../../../../utils/uri"; import { BenchmarkingLogger } from "../../../../logging/benchmarkingLogger"; import { LogsIPCSender } from "../../../../utils/subprocessUtils/ipc/onParentProcessCallExecutor/logsIpcSender"; import { TimeMark } from "../../measureUtils"; @@ -37,12 +38,20 @@ export namespace CheckProofsImpl { try { const timeMark = new TimeMark(); + const fileUri = Uri.fromPath(args.fileUri); + + // TODO: [@Gleb Solovev] Pay Atteniton that it was previously done by the CoqProofChecker + await coqLspClient.openTextDocument(fileUri); + const proofCheckResults = await coqProofChecker.checkProofs( - args.sourceFileDirPath, - args.sourceFileContentPrefix, - args.prefixEndPosition, + fileUri, + args.documentVersion, + args.checkAtPosition, args.preparedProofs ); + + await coqLspClient.closeTextDocument(fileUri); + const proofsValidationMillis = timeMark.measureElapsedMillis(); return buildSuccessResult( proofCheckResults, diff --git a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts index ea392959..92e67a59 100644 --- a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts +++ b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/internalSignature.ts @@ -7,9 +7,10 @@ export namespace CheckProofsInternalSignature { export interface Args { workspaceRootPath: string | undefined; - sourceFileDirPath: string; - sourceFileContentPrefix: string[]; - prefixEndPosition: Position; + fileUri: string; + documentVersion: number; + checkAtPosition: Position; + preparedProofs: string[]; } @@ -79,16 +80,13 @@ export namespace CheckProofsInternalSignature { type: "string", nullable: true, }, - sourceFileDirPath: { + fileUri: { type: "string", }, - sourceFileContentPrefix: { - type: "array", - items: { - type: "string", - }, + documentVersion: { + type: "number", }, - prefixEndPosition: positionSchema, + checkAtPosition: positionSchema, preparedProofs: { type: "array", items: { @@ -96,12 +94,7 @@ export namespace CheckProofsInternalSignature { }, }, }, - required: [ - "sourceFileDirPath", - "sourceFileContentPrefix", - "prefixEndPosition", - "preparedProofs", - ], + required: ["fileUri", "documentVersion", "preparedProofs"], additionalProperties: false, }; diff --git a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/proofsCheckerUtils.ts b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/proofsCheckerUtils.ts index 502a1758..2af4eb88 100644 --- a/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/proofsCheckerUtils.ts +++ b/src/benchmark/framework/benchmarkingCore/singleCompletionGeneration/proofsCheckers/implementation/proofsCheckerUtils.ts @@ -2,7 +2,6 @@ import { CompletionContext, SourceFileEnvironment, } from "../../../../../../core/completionGenerationContext"; -import { getTextBeforePosition } from "../../../../../../core/exposedCompletionGeneratorUtils"; import { WorkspaceRoot, @@ -28,12 +27,9 @@ export namespace ProofsCheckerUtils { workspaceRootPath: isStandaloneFilesRoot(workspaceRoot) ? undefined : workspaceRoot.directoryPath, - sourceFileDirPath: sourceFileEnvironment.dirPath, - sourceFileContentPrefix: getTextBeforePosition( - sourceFileEnvironment.fileLines, - completionContext.prefixEndPosition - ), - prefixEndPosition: completionContext.prefixEndPosition, + fileUri: sourceFileEnvironment.fileUri.toString(), + documentVersion: sourceFileEnvironment.documentVersion, + checkAtPosition: completionContext.admitRange.start, preparedProofs: preparedProofs, }; } diff --git a/src/benchmark/framework/parseDataset/cacheHandlers/cacheReader.ts b/src/benchmark/framework/parseDataset/cacheHandlers/cacheReader.ts index 8a04ecf1..73182765 100644 --- a/src/benchmark/framework/parseDataset/cacheHandlers/cacheReader.ts +++ b/src/benchmark/framework/parseDataset/cacheHandlers/cacheReader.ts @@ -150,8 +150,7 @@ namespace BuildCacheHoldersFromModels { return new CacheHolderData.CachedCoqFileData( theorems, readCachedFile.filePathRelativeToWorkspace, - readCachedFile.fileLines, - readCachedFile.fileVersion, + readCachedFile.documentVersion, workspacePath ); } diff --git a/src/benchmark/framework/parseDataset/cacheHandlers/cacheUpdater.ts b/src/benchmark/framework/parseDataset/cacheHandlers/cacheUpdater.ts index e8558af2..76c9730b 100644 --- a/src/benchmark/framework/parseDataset/cacheHandlers/cacheUpdater.ts +++ b/src/benchmark/framework/parseDataset/cacheHandlers/cacheUpdater.ts @@ -77,13 +77,12 @@ namespace UpdateCacheHolders { ); } - if (cachedFile.getFileVersion() !== parsedFile.fileVersion) { + if (cachedFile.getDocumentVersion() !== parsedFile.documentVersion) { cacheUpdaterLogger.debug( - `* file version update: ${cachedFile.getFileVersion()} -> ${parsedFile.fileVersion}` + `* file version update: ${cachedFile.getDocumentVersion()} -> ${parsedFile.documentVersion}` ); } - cachedFile.updateFileLines(parsedFile.fileLines); - cachedFile.updateFileVersion(parsedFile.fileVersion); + cachedFile.updateDocumentVersion(parsedFile.documentVersion); for (const fileTarget of parsedFileHolder.targets()) { let cachedTheorem = cachedFile.getCachedTheorem( @@ -161,8 +160,7 @@ namespace UpdateCacheHolders { return new CacheHolderData.CachedCoqFileData( cachedTheoremsMap, relativizeAbsolutePaths(workspacePath, parsedFile.filePath), - parsedFile.fileLines, - parsedFile.fileVersion, + parsedFile.documentVersion, workspacePath ); } diff --git a/src/benchmark/framework/parseDataset/cacheHandlers/cacheWriter.ts b/src/benchmark/framework/parseDataset/cacheHandlers/cacheWriter.ts index a03380cc..8de7c2f6 100644 --- a/src/benchmark/framework/parseDataset/cacheHandlers/cacheWriter.ts +++ b/src/benchmark/framework/parseDataset/cacheHandlers/cacheWriter.ts @@ -119,8 +119,7 @@ namespace SerializeCacheHolders { ) ) ), - fileLines: cachedCoqFileData.getFileLines(), - fileVersion: cachedCoqFileData.getFileVersion(), + documentVersion: cachedCoqFileData.getDocumentVersion(), filePathRelativeToWorkspace: cachedCoqFileData.filePathRelativeToWorkspace, }; diff --git a/src/benchmark/framework/parseDataset/cacheStructures/cacheHolders.ts b/src/benchmark/framework/parseDataset/cacheStructures/cacheHolders.ts index 9ec2bc3f..b89eae07 100644 --- a/src/benchmark/framework/parseDataset/cacheStructures/cacheHolders.ts +++ b/src/benchmark/framework/parseDataset/cacheStructures/cacheHolders.ts @@ -91,8 +91,7 @@ export namespace CacheHolderData { constructor( private readonly theorems: Map, readonly filePathRelativeToWorkspace: string, - private fileLines: string[], - private fileVersion: number, + private documentVersion: number, readonly workspacePath: string ) {} @@ -104,24 +103,16 @@ export namespace CacheHolderData { return this.theorems.get(theoremName); } - getFileLines(): string[] { - return this.fileLines; - } - - getFileVersion(): number { - return this.fileVersion; + getDocumentVersion(): number { + return this.documentVersion; } addCachedTheorem(cachedTheorem: CachedTheoremData) { this.theorems.set(cachedTheorem.theoremData.name, cachedTheorem); } - updateFileLines(fileLines: string[]) { - this.fileLines = fileLines; - } - - updateFileVersion(fileVersion: number) { - this.fileVersion = fileVersion; + updateDocumentVersion(documentVersion: number) { + this.documentVersion = documentVersion; } restoreParsedCoqFileData(): ParsedCoqFileData { @@ -131,8 +122,7 @@ export namespace CacheHolderData { (_: string, cachedTheorem: CachedTheoremData) => cachedTheorem.theoremData ), - this.fileLines, - this.fileVersion, + this.documentVersion, joinPaths(this.workspacePath, this.filePathRelativeToWorkspace) ); } diff --git a/src/benchmark/framework/parseDataset/cacheStructures/cacheModels.ts b/src/benchmark/framework/parseDataset/cacheStructures/cacheModels.ts index f7aecfba..2b8cb791 100644 --- a/src/benchmark/framework/parseDataset/cacheStructures/cacheModels.ts +++ b/src/benchmark/framework/parseDataset/cacheStructures/cacheModels.ts @@ -21,9 +21,7 @@ export namespace DatasetCacheModels { * Ones that don't end with `Qed.` are also included. */ allFileTheorems: CachedTheoremsByNames; - - fileLines: string[]; - fileVersion: number; + documentVersion: number; filePathRelativeToWorkspace: string; } @@ -95,13 +93,7 @@ export namespace DatasetCacheModels { type: "object", properties: { allFileTheorems: cachedTheoremsByNamesSchema, - fileLines: { - type: "array", - items: { - type: "string", - }, - }, - fileVersion: { + documentVersion: { type: "number", }, filePathRelativeToWorkspace: { @@ -110,8 +102,7 @@ export namespace DatasetCacheModels { }, required: [ "allFileTheorems", - "fileLines", - "fileVersion", + "documentVersion", "filePathRelativeToWorkspace", ], additionalProperties: false, diff --git a/src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts b/src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts index d99acf17..3343edc2 100644 --- a/src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts +++ b/src/benchmark/framework/parseDataset/coqProjectParser/implementation/parseCoqProject.ts @@ -74,13 +74,17 @@ export namespace ParseCoqProjectImpl { coqLspClient: CoqLspClient, logger: Logger ): Promise { - const mockFileVersion = 1; + const mockDocumentVersion = 1; const sourceFileUri = Uri.fromPath(filePath); await coqLspClient.openTextDocument(sourceFileUri); + // TODO: [@Gleb Solovev] Do not create this Abort Controller but pass + // the one created at the top + const abortController = new AbortController(); const sourceFileEnvironment = await createSourceFileEnvironment( - mockFileVersion, + mockDocumentVersion, sourceFileUri, - coqLspClient + coqLspClient, + abortController.signal ); const serializedParsedFile: SerializedParsedCoqFile = { serializedTheoremsByNames: packIntoMappedObject( @@ -93,15 +97,11 @@ export namespace ParseCoqProjectImpl { (serializedTheorem) => serializedTheorem.name, (serializedTheorem) => serializedTheorem ), - fileLines: sourceFileEnvironment.fileLines, - fileVersion: sourceFileEnvironment.fileVersion, + documentVersion: sourceFileEnvironment.documentVersion, filePath: filePath, }; const foundTheoremsLog = `found ${Object.keys(serializedParsedFile.serializedTheoremsByNames).length} theorem(s)`; - const readLinesLog = `read ${serializedParsedFile.fileLines.length} lines`; - logger.debug( - `Successfully parsed "${filePath}": ${foundTheoremsLog}, ${readLinesLog}` - ); + logger.debug(`Successfully parsed "${filePath}": ${foundTheoremsLog}`); return serializedParsedFile; } @@ -208,26 +208,28 @@ export namespace ParseCoqProjectImpl { ): Promise { let serializedGoal = knownGoal; if (serializedGoal === undefined) { - const goal = await coqLspClient.getFirstGoalAtPoint( + const goals = await coqLspClient.getGoalsAtPoint( proofStep.range.start, Uri.fromPath(serializedParsedFile.filePath), - serializedParsedFile.fileVersion + serializedParsedFile.documentVersion ); const startPosition = deserializeCodeElementPosition( proofStep.range.start ); - if (goal instanceof Error) { + if (goals.err) { + const goal = goals.val; const stack = goal.stack === undefined ? "" : `\n${goal.stack}`; logger.error( `Failed to retrieve target goal at point: "${goal.message}" at ${startPosition}, "${serializedParsedFile.filePath}"${stack}` ); throw goal; } else { + const goal = coqLspClient.getFirstGoalOrThrow(goals); logger.debug( `Successfully retrieved target goal at point: "${goal.ty}" at ${startPosition}, "${serializedParsedFile.filePath}"` ); + serializedGoal = serializeGoal(goal); } - serializedGoal = serializeGoal(goal); } return { diff --git a/src/benchmark/framework/structures/benchmarkingCore/completionGenerationTask.ts b/src/benchmark/framework/structures/benchmarkingCore/completionGenerationTask.ts index e558ff20..80768ffc 100644 --- a/src/benchmark/framework/structures/benchmarkingCore/completionGenerationTask.ts +++ b/src/benchmark/framework/structures/benchmarkingCore/completionGenerationTask.ts @@ -32,8 +32,7 @@ export class CompletionGenerationTask getCompletionContext(): CompletionContext { return { proofGoal: this.targetGoalToProve, - prefixEndPosition: this.targetPositionRange.start, - admitEndPosition: this.targetPositionRange.end, + admitRange: this.targetPositionRange, }; } diff --git a/src/benchmark/framework/structures/parsedCoqFile/parsedCoqFileData.ts b/src/benchmark/framework/structures/parsedCoqFile/parsedCoqFileData.ts index e9c1b4e5..d9a509f9 100644 --- a/src/benchmark/framework/structures/parsedCoqFile/parsedCoqFileData.ts +++ b/src/benchmark/framework/structures/parsedCoqFile/parsedCoqFileData.ts @@ -3,12 +3,12 @@ import { JSONSchemaType } from "ajv"; import { SourceFileEnvironment } from "../../../../core/completionGenerationContext"; import { Theorem } from "../../../../coqParser/parsedTypes"; +import { Uri } from "../../../../utils/uri"; import { fromMappedObject, mapValues, toMappedObject, } from "../../utils/collectionUtils/mapUtils"; -import { getDirectoryPath } from "../../utils/fileUtils/fs"; import { SerializedTheorem, @@ -25,8 +25,7 @@ export class ParsedCoqFileData { * Ones that don't end with `Qed.` are also included. */ readonly theoremsByNames: Map, - readonly fileLines: string[], - readonly fileVersion: number, + readonly documentVersion: number, readonly filePath: string ) {} @@ -43,11 +42,10 @@ export class ParsedCoqFileData { constructSourceFileEnvironment(): SourceFileEnvironment { return { fileTheorems: this.getOrderedFileTheorems().filter( - (theorem) => theorem.proof && !theorem.proof.is_incomplete + (theorem) => !theorem.proof.is_incomplete ), - fileLines: this.fileLines, - fileVersion: this.fileVersion, - dirPath: getDirectoryPath(this.filePath), + documentVersion: this.documentVersion, + fileUri: Uri.fromPath(this.filePath), }; } } @@ -58,9 +56,7 @@ export interface SerializedParsedCoqFile { * Ones that don't end with `Qed.` are also included. */ serializedTheoremsByNames: SerializedTheoremsByNames; - - fileLines: string[]; - fileVersion: number; + documentVersion: number; filePath: string; } @@ -84,25 +80,14 @@ export const serializedParsedCoqFileSchema: JSONSchemaType deserializeTheoremData(serializedTheorem) ), - serializedParsedCoqFile.fileLines, - serializedParsedCoqFile.fileVersion, + serializedParsedCoqFile.documentVersion, serializedParsedCoqFile.filePath ); } @@ -132,8 +116,7 @@ export function serializeParsedCoqFile( serializeTheoremData(theoremData) ) ), - fileLines: parsedCoqFileData.fileLines, - fileVersion: parsedCoqFileData.fileVersion, + documentVersion: parsedCoqFileData.documentVersion, filePath: parsedCoqFileData.filePath, }; } diff --git a/src/benchmark/framework/structures/parsedCoqFile/theoremData.ts b/src/benchmark/framework/structures/parsedCoqFile/theoremData.ts index 92d45f34..be01b871 100644 --- a/src/benchmark/framework/structures/parsedCoqFile/theoremData.ts +++ b/src/benchmark/framework/structures/parsedCoqFile/theoremData.ts @@ -33,7 +33,7 @@ export interface SerializedTheorem { name: string; statement_range: SerializedCodeElementRange; statement: string; - proof: SerializedTheoremProof | undefined; + proof: SerializedTheoremProof; initial_goal: SerializedGoal | undefined; fileTheoremsIndex: number; } @@ -100,7 +100,6 @@ export const serializedTheoremSchema: JSONSchemaType = { proof: { type: "object", oneOf: [serializedTheoremProofSchema], - nullable: true, }, initial_goal: { type: "string", @@ -118,15 +117,12 @@ export function deserializeTheoremData( serializedTheorem: SerializedTheorem ): TheoremData { const serializedTheoremProof = serializedTheorem.proof; - let theoremProof: TheoremProof | null = null; - if (serializedTheoremProof !== undefined) { - theoremProof = new TheoremProof( - serializedTheoremProof.proof_steps.map(deserializeProofStep), - deserializeCodeElementRange(serializedTheoremProof.end_pos), - serializedTheoremProof.is_incomplete, - serializedTheoremProof.holes.map(deserializeProofStep) - ); - } + const theoremProof = new TheoremProof( + serializedTheoremProof.proof_steps.map(deserializeProofStep), + deserializeCodeElementRange(serializedTheoremProof.end_pos), + serializedTheoremProof.is_incomplete, + serializedTheoremProof.holes.map(deserializeProofStep) + ); const serializedInitialGoal = serializedTheorem.initial_goal; const initialGoal = serializedInitialGoal === undefined @@ -148,15 +144,12 @@ export function serializeTheoremData( theoremData: TheoremData ): SerializedTheorem { const theoremProof = theoremData.proof; - let serializedTheoremProof: SerializedTheoremProof | undefined = undefined; - if (theoremProof !== null) { - serializedTheoremProof = { - proof_steps: theoremProof.proof_steps.map(serializeProofStep), - end_pos: serializeCodeElementRange(theoremProof.end_pos), - is_incomplete: theoremProof.is_incomplete, - holes: theoremProof.holes.map(serializeProofStep), - }; - } + const serializedTheoremProof = { + proof_steps: theoremProof.proof_steps.map(serializeProofStep), + end_pos: serializeCodeElementRange(theoremProof.end_pos), + is_incomplete: theoremProof.is_incomplete, + holes: theoremProof.holes.map(serializeProofStep), + }; const initialGoal = theoremData.sourceTheorem.initial_goal; const serializedInitialGoal = initialGoal === null ? undefined : serializeGoal(initialGoal); diff --git a/src/coqLsp/coqLspBuilders.ts b/src/coqLsp/coqLspBuilders.ts index 8ff9386e..934e18ad 100644 --- a/src/coqLsp/coqLspBuilders.ts +++ b/src/coqLsp/coqLspBuilders.ts @@ -1,17 +1,21 @@ import { OutputChannel, window } from "vscode"; -import { CoqLspClient } from "./coqLspClient"; +import { EventLogger } from "../logging/eventLogger"; + +import { CoqLspClient, CoqLspClientImpl } from "./coqLspClient"; import { CoqLspClientConfig, CoqLspConfig } from "./coqLspConfig"; export async function createCoqLspClient( coqLspServerPath: string, - logOutputChannel: OutputChannel = window.createOutputChannel( - "CoqPilot: coq-lsp events" - ) + logOutputChannel?: OutputChannel, + eventLogger?: EventLogger, + abortController?: AbortController ): Promise { return createAbstractCoqLspClient( CoqLspConfig.createClientConfig(coqLspServerPath), - logOutputChannel + logOutputChannel, + eventLogger, + abortController ); } @@ -30,12 +34,16 @@ async function createAbstractCoqLspClient( coqLspClientConfig: CoqLspClientConfig, logOutputChannel: OutputChannel = window.createOutputChannel( "CoqPilot: coq-lsp events" - ) + ), + eventLogger?: EventLogger, + abortController?: AbortController ): Promise { const coqLspServerConfig = CoqLspConfig.createServerConfig(); - return await CoqLspClient.create( + return await CoqLspClientImpl.create( coqLspServerConfig, coqLspClientConfig, - logOutputChannel + logOutputChannel, + eventLogger, + abortController ); } diff --git a/src/coqLsp/coqLspClient.ts b/src/coqLsp/coqLspClient.ts index bba4ebe7..6bf7b16f 100644 --- a/src/coqLsp/coqLspClient.ts +++ b/src/coqLsp/coqLspClient.ts @@ -1,57 +1,75 @@ import { Mutex } from "async-mutex"; import { readFileSync } from "fs"; +import { Err, Ok, Result } from "ts-results"; import { OutputChannel } from "vscode"; import { BaseLanguageClient, Diagnostic, - Disposable, - Position, - ProtocolNotificationType, - RequestType, - TextDocumentIdentifier, - VersionedTextDocumentIdentifier, -} from "vscode-languageclient"; -import { - DidChangeTextDocumentNotification, - DidChangeTextDocumentParams, DidCloseTextDocumentNotification, DidCloseTextDocumentParams, DidOpenTextDocumentNotification, DidOpenTextDocumentParams, + Disposable, LogTraceNotification, + Position, + ProtocolNotificationType, PublishDiagnosticsNotification, + RequestType, + TextDocumentIdentifier, + VersionedTextDocumentIdentifier, } from "vscode-languageclient"; +import { throwOnAbort } from "../extension/extensionAbortUtils"; +import { EventLogger } from "../logging/eventLogger"; import { Uri } from "../utils/uri"; import { CoqLspClientConfig, CoqLspServerConfig } from "./coqLspConfig"; import { CoqLspConnector } from "./coqLspConnector"; -import { Goal, GoalAnswer, GoalRequest, PpString } from "./coqLspTypes"; -import { FlecheDocument, FlecheDocumentParams } from "./coqLspTypes"; -import { CoqLspError, CoqLspStartupError } from "./coqLspTypes"; - -export interface CoqLspClientInterface extends Disposable { - getFirstGoalAtPoint( +import { + CoqLspError, + CoqLspStartupError, + FlecheDocument, + FlecheDocumentParams, + Goal, + GoalAnswer, + GoalRequest, + PpString, +} from "./coqLspTypes"; + +export interface CoqLspClient extends Disposable { + /** + * Fetches all goals present at the given position in the document. + * This method doesn't open the document implicitly, therefore + * it assumes that openTextDocument has been called before. + * @param position Position in the document where to fetch the goals + * @param documentUri Uri of the document + * @param version Version of the document + * @param command Optional command to execute before fetching the goals + * @returns All goals present at the given position, not only the first one + */ + getGoalsAtPoint( position: Position, documentUri: Uri, version: number, - command: string - ): Promise | Error>; - - openTextDocument(uri: Uri, version: number): Promise; + command?: string + ): Promise[], Error>>; - getDocumentSymbols(uri: Uri): Promise; + /** + * Returns a FlecheDocument for the given uri. + * This method doesn't open the document implicitly, therefore + * it assumes that openTextDocument has been called before. + */ + getFlecheDocument(uri: Uri): Promise; - updateTextDocument( - oldDocumentText: string[], - appendedSuffix: string, - uri: Uri, - version: number - ): Promise; + openTextDocument(uri: Uri, version?: number): Promise; closeTextDocument(uri: Uri): Promise; - getFlecheDocument(uri: Uri): Promise; + /** + * + * @param goals + */ + getFirstGoalOrThrow(goals: Result[], Error>): Goal; } const goalReqType = new RequestType, void>( @@ -66,20 +84,26 @@ const flecheDocReqType = new RequestType< export type DiagnosticMessage = string | undefined; -export class CoqLspClient implements CoqLspClientInterface { +export class CoqLspClientImpl implements CoqLspClient { private client: BaseLanguageClient; private subscriptions: Disposable[] = []; private mutex = new Mutex(); - private constructor(coqLspConnector: CoqLspConnector) { + private constructor( + coqLspConnector: CoqLspConnector, + public readonly eventLogger?: EventLogger, + public readonly abortController?: AbortController + ) { this.client = coqLspConnector; } static async create( serverConfig: CoqLspServerConfig, clientConfig: CoqLspClientConfig, - logOutputChannel: OutputChannel - ): Promise { + logOutputChannel: OutputChannel, + eventLogger?: EventLogger, + abortController?: AbortController + ): Promise { const connector = new CoqLspConnector( serverConfig, clientConfig, @@ -91,23 +115,18 @@ export class CoqLspClient implements CoqLspClientInterface { clientConfig.coq_lsp_server_path ); }); - return new CoqLspClient(connector); - } - - async getDocumentSymbols(uri: Uri): Promise { - return await this.mutex.runExclusive(async () => { - return this.getDocumentSymbolsUnsafe(uri); - }); + return new CoqLspClientImpl(connector, eventLogger, abortController); } - async getFirstGoalAtPoint( + async getGoalsAtPoint( position: Position, documentUri: Uri, version: number, command?: string - ): Promise | Error> { + ): Promise[], Error>> { return await this.mutex.runExclusive(async () => { - return this.getFirstGoalAtPointUnsafe( + throwOnAbort(this.abortController?.signal); + return this.getGoalsAtPointUnsafe( position, documentUri, version, @@ -121,43 +140,70 @@ export class CoqLspClient implements CoqLspClientInterface { version: number = 1 ): Promise { return await this.mutex.runExclusive(async () => { + throwOnAbort(this.abortController?.signal); return this.openTextDocumentUnsafe(uri, version); }); } - async updateTextDocument( - oldDocumentText: string[], - appendedSuffix: string, - uri: Uri, - version: number = 1 - ): Promise { - return await this.mutex.runExclusive(async () => { - return this.updateTextDocumentUnsafe( - oldDocumentText, - appendedSuffix, - uri, - version - ); - }); - } - async closeTextDocument(uri: Uri): Promise { return await this.mutex.runExclusive(async () => { + throwOnAbort(this.abortController?.signal); return this.closeTextDocumentUnsafe(uri); }); } async getFlecheDocument(uri: Uri): Promise { return await this.mutex.runExclusive(async () => { + throwOnAbort(this.abortController?.signal); return this.getFlecheDocumentUnsafe(uri); }); } + getFirstGoalOrThrow( + goals: Result[], Error> + ): Goal { + if (goals.err) { + throw new CoqLspError( + "Call to `getFirstGoalOrThrow` with a Error type" + ); + } else if (goals.val.length === 0) { + throw new CoqLspError( + "Call to `getFirstGoalOrThrow` with an empty set of goals" + ); + } + + return goals.val[0]; + } + + /** + * Dirty due to the fact that the client sends no pure + * error: https://github.com/ejgallego/coq-lsp/blob/f98b65344c961d1aad1e0c3785199258f21c3abc/controller/request.ml#L29 + */ + cleanLspError(errorMsg?: string): string | undefined { + const errorMsgPrefixRegex = /^Error in .* request: (.*)$/s; + if (!errorMsg) { + return undefined; + } + const match = errorMsg.match(errorMsgPrefixRegex); + return match ? match[1] : undefined; + } + + removeTraceFromLspError(errorMsgWithTrace: string): string | undefined { + const traceStartString = "Raised at"; + + if (!errorMsgWithTrace.includes(traceStartString)) { + return errorMsgWithTrace.split("\n").shift(); + } + + return errorMsgWithTrace + .substring(0, errorMsgWithTrace.indexOf(traceStartString)) + .trim(); + } + filterDiagnostics( diagnostics: Diagnostic[], position: Position ): string | undefined { - const traceStartString = "Raised at"; const diagnosticMessageWithTrace = diagnostics .filter((diag) => diag.range.start.line >= position.line) .filter((diag) => diag.severity === 1) // 1 is error @@ -165,30 +211,17 @@ export class CoqLspClient implements CoqLspClientInterface { if (!diagnosticMessageWithTrace) { return undefined; - } else if (!diagnosticMessageWithTrace.includes(traceStartString)) { - return diagnosticMessageWithTrace.split("\n").shift(); + } else { + return this.removeTraceFromLspError(diagnosticMessageWithTrace); } - return diagnosticMessageWithTrace - .substring(0, diagnosticMessageWithTrace.indexOf(traceStartString)) - .trim(); } - private async getDocumentSymbolsUnsafe(uri: Uri): Promise { - let textDocument = TextDocumentIdentifier.create(uri.uri); - let params: any = { textDocument }; - - return await this.client.sendRequest( - "textDocument/documentSymbol", - params - ); - } - - private async getFirstGoalAtPointUnsafe( + private async getGoalsAtPointUnsafe( position: Position, documentUri: Uri, version: number, command?: string - ): Promise | Error> { + ): Promise[], Error>> { let goalRequestParams: GoalRequest = { textDocument: VersionedTextDocumentIdentifier.create( documentUri.uri, @@ -197,23 +230,39 @@ export class CoqLspClient implements CoqLspClientInterface { position, // eslint-disable-next-line @typescript-eslint/naming-convention pp_format: "Str", + command: command, }; - if (command) { - goalRequestParams.command = command; - // goalRequestParams.mode = "After"; - } - - const goals = await this.client.sendRequest( - goalReqType, - goalRequestParams - ); - const goal = goals?.goals?.goals?.shift() ?? undefined; - if (!goal) { - return new CoqLspError("no goals at point"); + try { + const goalAnswer = await this.client.sendRequest( + goalReqType, + goalRequestParams + ); + const goals = goalAnswer?.goals?.goals; + + if (!goals) { + return Err(CoqLspError.unknownError()); + } + + return Ok(goals); + } catch (e) { + if (e instanceof Error) { + const errorMsg = this.cleanLspError( + this.removeTraceFromLspError(e.message) + ); + if (errorMsg) { + return Err(new CoqLspError(errorMsg)); + } + return Err( + new CoqLspError( + "Unable to parse CoqLSP error, please report this issue: " + + e.message + ) + ); + } + + return Err(CoqLspError.unknownError()); } - - return goal; } private sleep(ms: number): Promise> { @@ -312,43 +361,6 @@ export class CoqLspClient implements CoqLspClientInterface { ); } - private getTextEndPosition(lines: string[]): Position { - return Position.create( - lines.length - 1, - lines[lines.length - 1].length - ); - } - - private async updateTextDocumentUnsafe( - oldDocumentText: string[], - appendedSuffix: string, - uri: Uri, - version: number = 1 - ): Promise { - const updatedText = oldDocumentText.join("\n") + appendedSuffix; - const oldEndPosition = this.getTextEndPosition(oldDocumentText); - - const params: DidChangeTextDocumentParams = { - textDocument: { - uri: uri.uri, - version: version, - }, - contentChanges: [ - { - text: updatedText, - }, - ], - }; - - return await this.waitUntilFileFullyChecked( - DidChangeTextDocumentNotification.type, - params, - uri, - version, - oldEndPosition - ); - } - private async closeTextDocumentUnsafe(uri: Uri): Promise { const params: DidCloseTextDocumentParams = { textDocument: { @@ -372,5 +384,6 @@ export class CoqLspClient implements CoqLspClientInterface { dispose(): void { this.subscriptions.forEach((d) => d.dispose()); + this.client.stop(); } } diff --git a/src/coqLsp/coqLspConfig.ts b/src/coqLsp/coqLspConfig.ts index d2e3360e..075591df 100644 --- a/src/coqLsp/coqLspConfig.ts +++ b/src/coqLsp/coqLspConfig.ts @@ -21,7 +21,7 @@ export interface CoqLspClientConfig { export namespace CoqLspConfig { export function createServerConfig(): CoqLspServerConfig { return { - client_version: "0.1.9", + client_version: "0.2.2", eager_diagnostics: true, goal_after_tactic: false, show_coq_info_messages: false, diff --git a/src/coqLsp/coqLspConnector.ts b/src/coqLsp/coqLspConnector.ts index 4f2b9d41..8f648aa5 100644 --- a/src/coqLsp/coqLspConnector.ts +++ b/src/coqLsp/coqLspConnector.ts @@ -79,8 +79,4 @@ export class CoqLspConnector extends LanguageClient { private logStatusUpdate = (status: "started" | "stopped") => { this.eventLogger?.log("coq-lsp-status-change", status); }; - - restartLspClient() { - this.stop().then(() => this.start()); - } } diff --git a/src/coqLsp/coqLspTypes.ts b/src/coqLsp/coqLspTypes.ts index a6e22aa3..94d14863 100644 --- a/src/coqLsp/coqLspTypes.ts +++ b/src/coqLsp/coqLspTypes.ts @@ -157,6 +157,12 @@ export class CoqLspError extends Error { super(message); this.name = "CoqLspError"; } + + static unknownError(): CoqLspError { + return new CoqLspError( + "Unknown CoqLSP error, please report this issue" + ); + } } export class CoqParsingError extends CoqLspError { diff --git a/src/coqParser/parseCoqFile.ts b/src/coqParser/parseCoqFile.ts index 32acf62c..d306139b 100644 --- a/src/coqParser/parseCoqFile.ts +++ b/src/coqParser/parseCoqFile.ts @@ -1,20 +1,33 @@ import { readFileSync } from "fs"; +import { Result } from "ts-results"; import { Position, Range } from "vscode-languageclient"; import { CoqLspClient } from "../coqLsp/coqLspClient"; import { CoqParsingError, FlecheDocument, + Goal, + PpString, RangedSpan, } from "../coqLsp/coqLspTypes"; +import { throwOnAbort } from "../extension/extensionAbortUtils"; +import { EventLogger } from "../logging/eventLogger"; import { Uri } from "../utils/uri"; import { ProofStep, Theorem, TheoremProof, Vernacexpr } from "./parsedTypes"; +/** + * As we have decided that premises = only theorems/definitions + * with existing proofs, parseCoqFile ignores items without proofs + * and does not add them into the resulting array. + */ export async function parseCoqFile( uri: Uri, - client: CoqLspClient + client: CoqLspClient, + abortSignal: AbortSignal, + extractTheoremInitialGoal: boolean = true, + eventLogger?: EventLogger ): Promise { return client .getFlecheDocument(uri) @@ -22,7 +35,15 @@ export async function parseCoqFile( const documentText = readFileSync(uri.fsPath) .toString() .split("\n"); - return parseFlecheDocument(doc, documentText, client, uri); + return parseFlecheDocument( + doc, + documentText, + client, + uri, + abortSignal, + extractTheoremInitialGoal, + eventLogger + ); }) .catch((error) => { throw new CoqParsingError( @@ -35,7 +56,10 @@ async function parseFlecheDocument( doc: FlecheDocument, textLines: string[], client: CoqLspClient, - uri: Uri + uri: Uri, + abortSignal: AbortSignal, + extractTheoremInitialGoal: boolean, + eventLogger?: EventLogger ): Promise { if (doc === null) { throw Error("could not parse file"); @@ -43,6 +67,8 @@ async function parseFlecheDocument( const theorems: Theorem[] = []; for (let i = 0; i < doc.spans.length; i++) { + throwOnAbort(abortSignal); + const span = doc.spans[i]; try { const vernacType = getVernacexpr(getExpr(span)); @@ -63,14 +89,9 @@ async function parseFlecheDocument( const nextExprVernac = getVernacexpr(getExpr(doc.spans[i + 1])); if (i + 1 >= doc.spans.length) { - theorems.push( - new Theorem( - thrName, - doc.spans[i].range, - thrStatement, - null, - null - ) + eventLogger?.log( + "premise-has-no-proof", + `Could not parse the proof in theorem/definition ${thrName}.` ); } else if (!nextExprVernac) { throw new CoqParsingError("unable to parse proof"); @@ -81,26 +102,27 @@ async function parseFlecheDocument( Vernacexpr.VernacEndProof, ].includes(nextExprVernac) ) { - theorems.push( - new Theorem( - thrName, - doc.spans[i].range, - thrStatement, - null, - null - ) + eventLogger?.log( + "premise-has-no-proof", + `Could not parse the proof in theorem/definition ${thrName}.` ); } else { - const initialGoal = await client.getFirstGoalAtPoint( - doc.spans[i + 1].range.start, - uri, - 1 - ); - - if (initialGoal instanceof Error) { - throw new CoqParsingError( - `unable to get initial goal for theorem: ${thrName}` + // TODO: Cover with tests, might be a source of bugs if somewhere + // absense of initialGoal is not handled properly or invariants are broken + let initialGoal: Result[], Error> | null = + null; + if (extractTheoremInitialGoal) { + initialGoal = await client.getGoalsAtPoint( + doc.spans[i + 1].range.start, + uri, + 1 ); + + if (initialGoal.err) { + throw new CoqParsingError( + `unable to get initial goal for theorem: ${thrName}` + ); + } } const proof = parseProof(i + 1, doc.spans, textLines); @@ -110,7 +132,7 @@ async function parseFlecheDocument( doc.spans[i].range, thrStatement, proof, - initialGoal + initialGoal?.val[0] ) ); } diff --git a/src/coqParser/parsedTypes.ts b/src/coqParser/parsedTypes.ts index a965c24d..530aa504 100644 --- a/src/coqParser/parsedTypes.ts +++ b/src/coqParser/parsedTypes.ts @@ -143,23 +143,19 @@ export class Theorem { public name: string, public statement_range: Range, public statement: string, - public proof: TheoremProof | null = null, + public proof: TheoremProof, public initial_goal: Goal | null = null ) {} public toString(): string { let text = this.statement; - if (this.proof !== null) { - text += "\n" + this.proof.toString(); - } + text += "\n" + this.proof.toString(); return text; } public onlyText(): string { let text = this.statement; - if (this.proof !== null) { - text += "\n" + this.proof.onlyText(); - } + text += "\n" + this.proof.onlyText(); return text; } } diff --git a/src/core/completionGenerationContext.ts b/src/core/completionGenerationContext.ts index 32eaf2a2..3af5601f 100644 --- a/src/core/completionGenerationContext.ts +++ b/src/core/completionGenerationContext.ts @@ -1,4 +1,4 @@ -import { Position } from "vscode-languageclient"; +import { Range } from "vscode-languageclient"; import { LLMServices } from "../llm/llmServices"; import { ModelsParams } from "../llm/llmServices/modelParams"; @@ -6,22 +6,21 @@ import { ModelsParams } from "../llm/llmServices/modelParams"; import { ProofGoal } from "../coqLsp/coqLspTypes"; import { Theorem } from "../coqParser/parsedTypes"; +import { Uri } from "../utils/uri"; import { ContextTheoremsRanker } from "./contextTheoremRanker/contextTheoremsRanker"; import { CoqProofChecker } from "./coqProofChecker"; export interface CompletionContext { proofGoal: ProofGoal; - prefixEndPosition: Position; - admitEndPosition: Position; + admitRange: Range; } export interface SourceFileEnvironment { // `fileTheorems` contain only ones that successfully finish with Qed. fileTheorems: Theorem[]; - fileLines: string[]; - fileVersion: number; - dirPath: string; + documentVersion: number; + fileUri: Uri; } export interface ProcessEnvironment { diff --git a/src/core/completionGenerator.ts b/src/core/completionGenerator.ts index f5c6f8ef..2574262c 100644 --- a/src/core/completionGenerator.ts +++ b/src/core/completionGenerator.ts @@ -1,9 +1,12 @@ import { LLMSequentialIterator } from "../llm/llmIterator"; import { GeneratedProof } from "../llm/llmServices/generatedProof"; -import { createCoqLspClient } from "../coqLsp/coqLspBuilders"; import { CoqLspTimeoutError } from "../coqLsp/coqLspTypes"; +import { + CompletionAbortError, + throwOnAbort, +} from "../extension/extensionAbortUtils"; import { EventLogger } from "../logging/eventLogger"; import { asErrorOrRethrow, buildErrorCompleteLog } from "../utils/errorsUtils"; import { stringifyAnyValue } from "../utils/printers"; @@ -13,10 +16,9 @@ import { ProcessEnvironment, SourceFileEnvironment, } from "./completionGenerationContext"; -import { CoqProofChecker, ProofCheckResult } from "./coqProofChecker"; +import { ProofCheckResult } from "./coqProofChecker"; import { buildProofGenerationContext, - getTextBeforePosition, prepareProofToCheck, } from "./exposedCompletionGeneratorUtils"; @@ -46,8 +48,8 @@ export async function generateCompletion( completionContext: CompletionContext, sourceFileEnvironment: SourceFileEnvironment, processEnvironment: ProcessEnvironment, + abortSignal: AbortSignal, eventLogger?: EventLogger, - workspaceRootPath?: string, perProofTimeoutMillis: number = 15000 ): Promise { const context = buildProofGenerationContext( @@ -68,10 +70,6 @@ export async function generateCompletion( processEnvironment.services, eventLogger ); - const sourceFileContentPrefix = getTextBeforePosition( - sourceFileEnvironment.fileLines, - completionContext.prefixEndPosition - ); try { /** newlyGeneratedProofs = generatedProofsBatch from iterator + @@ -79,6 +77,7 @@ export async function generateCompletion( let newlyGeneratedProofs: GeneratedProof[] = []; for await (const generatedProofsBatch of iterator) { + throwOnAbort(abortSignal); newlyGeneratedProofs.push(...generatedProofsBatch); eventLogger?.log( "core-new-proofs-ready-for-checking", @@ -87,12 +86,11 @@ export async function generateCompletion( ); const fixedProofsOrCompletion = await checkAndFixProofs( newlyGeneratedProofs, - sourceFileContentPrefix, completionContext, sourceFileEnvironment, processEnvironment, + abortSignal, eventLogger, - workspaceRootPath, perProofTimeoutMillis ); if (fixedProofsOrCompletion instanceof SuccessGenerationResult) { @@ -102,14 +100,14 @@ export async function generateCompletion( } while (newlyGeneratedProofs.length > 0) { + throwOnAbort(abortSignal); const fixedProofsOrCompletion = await checkAndFixProofs( newlyGeneratedProofs, - sourceFileContentPrefix, completionContext, sourceFileEnvironment, processEnvironment, + abortSignal, eventLogger, - workspaceRootPath, perProofTimeoutMillis ); if (fixedProofsOrCompletion instanceof SuccessGenerationResult) { @@ -137,6 +135,8 @@ export async function generateCompletion( FailureGenerationStatus.TIMEOUT_EXCEEDED, error.message ); + } else if (error instanceof CompletionAbortError) { + throw error; } else { return new FailureGenerationResult( FailureGenerationStatus.ERROR_OCCURRED, @@ -148,22 +148,19 @@ export async function generateCompletion( async function checkAndFixProofs( newlyGeneratedProofs: GeneratedProof[], - sourceFileContentPrefix: string[], completionContext: CompletionContext, sourceFileEnvironment: SourceFileEnvironment, processEnvironment: ProcessEnvironment, + abortSignal: AbortSignal, eventLogger?: EventLogger, - workspaceRootPath?: string, perProofTimeoutMillis: number = 15000 ): Promise { // check proofs and finish with success if at least one is valid const proofCheckResults = await checkGeneratedProofs( newlyGeneratedProofs, - sourceFileContentPrefix, completionContext, sourceFileEnvironment, processEnvironment, - workspaceRootPath, perProofTimeoutMillis ); const completion = getFirstValidProof(proofCheckResults); @@ -181,7 +178,7 @@ async function checkAndFixProofs( }; } ); - const fixedProofs = await fixProofs(proofsWithFeedback); + const fixedProofs = await fixProofs(proofsWithFeedback, abortSignal); eventLogger?.log( "core-proofs-fixed", "Proofs were fixed", @@ -195,11 +192,9 @@ async function checkAndFixProofs( async function checkGeneratedProofs( generatedProofs: GeneratedProof[], - sourceFileContentPrefix: string[], completionContext: CompletionContext, sourceFileEnvironment: SourceFileEnvironment, processEnvironment: ProcessEnvironment, - workspaceRootPath?: string, perProofTimeoutMillis = 15000 ): Promise { const preparedProofBatch = generatedProofs.map( @@ -207,17 +202,10 @@ async function checkGeneratedProofs( prepareProofToCheck(generatedProof.proof()) ); - if (workspaceRootPath) { - processEnvironment.coqProofChecker.dispose(); - const client = await createCoqLspClient(workspaceRootPath); - const coqProofChecker = new CoqProofChecker(client); - processEnvironment.coqProofChecker = coqProofChecker; - } - return processEnvironment.coqProofChecker.checkProofs( - sourceFileEnvironment.dirPath, - sourceFileContentPrefix, - completionContext.prefixEndPosition, + sourceFileEnvironment.fileUri, + sourceFileEnvironment.documentVersion, + completionContext.admitRange.start, preparedProofBatch, perProofTimeoutMillis ); @@ -229,12 +217,14 @@ interface ProofWithFeedback { } async function fixProofs( - proofsWithFeedback: ProofWithFeedback[] + proofsWithFeedback: ProofWithFeedback[], + abortSignal: AbortSignal ): Promise { const fixProofsPromises = []; // build fix promises for (const proofWithFeedback of proofsWithFeedback) { + throwOnAbort(abortSignal); const generatedProof = proofWithFeedback.generatedProof; if (!generatedProof.canBeFixed()) { continue; diff --git a/src/core/contextTheoremRanker/contextTheoremsRanker.ts b/src/core/contextTheoremRanker/contextTheoremsRanker.ts index 0f5c7c41..821448c1 100644 --- a/src/core/contextTheoremRanker/contextTheoremsRanker.ts +++ b/src/core/contextTheoremRanker/contextTheoremsRanker.ts @@ -6,4 +6,6 @@ export interface ContextTheoremsRanker { theorems: Theorem[], completionContext: CompletionContext ): Theorem[]; + + needsUnwrappedNotations: boolean; } diff --git a/src/core/contextTheoremRanker/distanceContextTheoremsRanker.ts b/src/core/contextTheoremRanker/distanceContextTheoremsRanker.ts index 7de99f0d..b48d52f4 100644 --- a/src/core/contextTheoremRanker/distanceContextTheoremsRanker.ts +++ b/src/core/contextTheoremRanker/distanceContextTheoremsRanker.ts @@ -4,6 +4,8 @@ import { CompletionContext } from "../completionGenerationContext"; import { ContextTheoremsRanker } from "./contextTheoremsRanker"; export class DistanceContextTheoremsRanker implements ContextTheoremsRanker { + readonly needsUnwrappedNotations = false; + rankContextTheorems( theorems: Theorem[], completionContext: CompletionContext @@ -11,7 +13,7 @@ export class DistanceContextTheoremsRanker implements ContextTheoremsRanker { const theoremsBeforeCompletionPosition = theorems.filter( (theorem) => theorem.statement_range.start.line < - completionContext.prefixEndPosition.line + completionContext.admitRange.start.line ); // Sort theorems such that closer theorems are first theoremsBeforeCompletionPosition.sort((a, b) => { @@ -21,7 +23,7 @@ export class DistanceContextTheoremsRanker implements ContextTheoremsRanker { const theoremsAfterCompletionPosition = theorems.filter( (theorem) => theorem.statement_range.start.line > - completionContext.prefixEndPosition.line + completionContext.admitRange.start.line ); theoremsAfterCompletionPosition.sort((a, b) => { diff --git a/src/core/contextTheoremRanker/euclidContextTheoremRanker.ts b/src/core/contextTheoremRanker/euclidContextTheoremRanker.ts index aaffc345..0be8058d 100644 --- a/src/core/contextTheoremRanker/euclidContextTheoremRanker.ts +++ b/src/core/contextTheoremRanker/euclidContextTheoremRanker.ts @@ -11,6 +11,8 @@ import { goalAsTheoremString } from "./tokenUtils"; * */ export class EuclidContextTheoremsRanker implements ContextTheoremsRanker { + readonly needsUnwrappedNotations = true; + rankContextTheorems( theorems: Theorem[], completionContext: CompletionContext diff --git a/src/core/contextTheoremRanker/jaccardIndexContextTheoremsRanker.ts b/src/core/contextTheoremRanker/jaccardIndexContextTheoremsRanker.ts index b5b885ac..389bf6ca 100644 --- a/src/core/contextTheoremRanker/jaccardIndexContextTheoremsRanker.ts +++ b/src/core/contextTheoremRanker/jaccardIndexContextTheoremsRanker.ts @@ -14,6 +14,8 @@ import { goalAsTheoremString } from "./tokenUtils"; export class JaccardIndexContextTheoremsRanker implements ContextTheoremsRanker { + readonly needsUnwrappedNotations = true; + rankContextTheorems( theorems: Theorem[], completionContext: CompletionContext diff --git a/src/core/contextTheoremRanker/randomContextTheoremsRanker.ts b/src/core/contextTheoremRanker/randomContextTheoremsRanker.ts index c12d79e7..97b90c31 100644 --- a/src/core/contextTheoremRanker/randomContextTheoremsRanker.ts +++ b/src/core/contextTheoremRanker/randomContextTheoremsRanker.ts @@ -4,6 +4,8 @@ import { CompletionContext } from "../completionGenerationContext"; import { ContextTheoremsRanker } from "./contextTheoremsRanker"; export class RandomContextTheoremsRanker implements ContextTheoremsRanker { + readonly needsUnwrappedNotations = false; + private shuffleArray(array: any[]) { for (let i = array.length - 1; i > 0; i--) { const j = Math.floor(Math.random() * (i + 1)); diff --git a/src/core/contextTheoremRanker/weightedJaccardIndexTheoremRanker.ts b/src/core/contextTheoremRanker/weightedJaccardIndexTheoremRanker.ts index 801d6019..03db43dd 100644 --- a/src/core/contextTheoremRanker/weightedJaccardIndexTheoremRanker.ts +++ b/src/core/contextTheoremRanker/weightedJaccardIndexTheoremRanker.ts @@ -14,6 +14,8 @@ import { goalAsTheoremString } from "./tokenUtils"; export class WeightedJaccardIndexContextTheoremsRanker implements ContextTheoremsRanker { + readonly needsUnwrappedNotations = true; + rankContextTheorems( theorems: Theorem[], completionContext: CompletionContext diff --git "a/src/core/contextTheoremRanker/\321\201osineContextTheoremRanker.ts" "b/src/core/contextTheoremRanker/\321\201osineContextTheoremRanker.ts" index 308f6bf3..cd31d402 100644 --- "a/src/core/contextTheoremRanker/\321\201osineContextTheoremRanker.ts" +++ "b/src/core/contextTheoremRanker/\321\201osineContextTheoremRanker.ts" @@ -12,6 +12,8 @@ import { goalAsTheoremString } from "./tokenUtils"; * ```cosine(A, B) = |A ∩ B| / sqrt(|A| * |B|)``` */ export class CosineContextTheoremsRanker implements ContextTheoremsRanker { + readonly needsUnwrappedNotations = true; + rankContextTheorems( theorems: Theorem[], completionContext: CompletionContext diff --git a/src/core/coqProofChecker.ts b/src/core/coqProofChecker.ts index 46db99e8..7774b9a4 100644 --- a/src/core/coqProofChecker.ts +++ b/src/core/coqProofChecker.ts @@ -1,6 +1,4 @@ import { Mutex } from "async-mutex"; -import { appendFileSync, existsSync, unlinkSync, writeFileSync } from "fs"; -import * as path from "path"; import { Position } from "vscode-languageclient"; import { CoqLspClient } from "../coqLsp/coqLspClient"; @@ -18,10 +16,11 @@ type Proof = string; export interface CoqProofCheckerInterface { checkProofs( - sourceDirPath: string, - sourceFileContentPrefix: string[], - prefixEndPosition: Position, - proofs: Proof[] + fileUri: Uri, + documentVersion: number, + checkAtPosition: Position, + proofs: Proof[], + coqLspTimeoutMillis?: number ): Promise; dispose(): void; @@ -33,9 +32,9 @@ export class CoqProofChecker implements CoqProofCheckerInterface { constructor(private coqLspClient: CoqLspClient) {} async checkProofs( - sourceDirPath: string, - sourceFileContentPrefix: string[], - prefixEndPosition: Position, + fileUri: Uri, + documentVersion: number, + checkAtPosition: Position, proofs: Proof[], coqLspTimeoutMillis: number = 15000 ): Promise { @@ -54,9 +53,9 @@ export class CoqProofChecker implements CoqProofCheckerInterface { return Promise.race([ this.checkProofsUnsafe( - sourceDirPath, - sourceFileContentPrefix, - prefixEndPosition, + fileUri, + documentVersion, + checkAtPosition, proofs ), timeoutPromise, @@ -64,98 +63,39 @@ export class CoqProofChecker implements CoqProofCheckerInterface { }); } - private buildAuxFileUri( - sourceDirPath: string, - holePosition: Position, - unique: boolean = true - ): Uri { - const holeIdentifier = `${holePosition.line}_${holePosition.character}`; - const defaultAuxFileName = `hole_${holeIdentifier}_cp_aux.v`; - let auxFilePath = path.join(sourceDirPath, defaultAuxFileName); - if (unique && existsSync(auxFilePath)) { - const randomSuffix = Math.floor(Math.random() * 1000000); - auxFilePath = auxFilePath.replace( - /\_cp_aux.v$/, - `_${randomSuffix}_cp_aux.v` - ); - } - - return Uri.fromPath(auxFilePath); - } - private checkIfProofContainsAdmit(proof: Proof): boolean { return forbiddenAdmitTactics.some((tactic) => proof.includes(tactic)); } private async checkProofsUnsafe( - sourceDirPath: string, - sourceFileContentPrefix: string[], - prefixEndPosition: Position, + fileUri: Uri, + documentVersion: number, + checkAtPosition: Position, proofs: Proof[] ): Promise { - // 1. Write the text to the aux file - const auxFileUri = this.buildAuxFileUri( - sourceDirPath, - prefixEndPosition - ); - const sourceFileContent = sourceFileContentPrefix.join("\n"); - writeFileSync(auxFileUri.fsPath, sourceFileContent); - const results: ProofCheckResult[] = []; - try { - // 2. Issue open text document request - await this.coqLspClient.openTextDocument(auxFileUri); - let auxFileVersion = 1; - - // 3. Iterate over the proofs and сheck them - for (const proof of proofs) { - // 3.1. Check if the proof contains admit - if (this.checkIfProofContainsAdmit(proof)) { - results.push({ - proof: proof, - isValid: false, - diagnostic: "Proof contains admit", - }); - continue; - } - - auxFileVersion += 1; - // 3.2. Append the proof the end of the aux file - appendFileSync(auxFileUri.fsPath, proof); - // 3.3. Issue update text request - const diagnosticMessage = - await this.coqLspClient.updateTextDocument( - sourceFileContentPrefix, - proof, - auxFileUri, - auxFileVersion - ); - - // 3.4. Check diagnostics + for (const proof of proofs) { + if (this.checkIfProofContainsAdmit(proof)) { results.push({ proof: proof, - isValid: diagnosticMessage === undefined, - diagnostic: diagnosticMessage, + isValid: false, + diagnostic: "Proof contains admit", }); - - // 3.5. Bring file to the previous state - writeFileSync(auxFileUri.fsPath, sourceFileContent); - - // 3.6. Issue update text request - auxFileVersion += 1; - await this.coqLspClient.updateTextDocument( - sourceFileContentPrefix, - "", - auxFileUri, - auxFileVersion - ); + continue; } - } finally { - // 4. Issue close text document request - await this.coqLspClient.closeTextDocument(auxFileUri); - // 5. Remove the aux file - unlinkSync(auxFileUri.fsPath); + const goalResult = await this.coqLspClient.getGoalsAtPoint( + checkAtPosition, + fileUri, + documentVersion, + proof + ); + + results.push({ + proof: proof, + isValid: goalResult.ok, + diagnostic: goalResult.err ? goalResult.val.message : undefined, + }); } return results; diff --git a/src/core/inspectSourceFile.ts b/src/core/inspectSourceFile.ts index 0d29aeb6..befd0914 100644 --- a/src/core/inspectSourceFile.ts +++ b/src/core/inspectSourceFile.ts @@ -1,10 +1,8 @@ -import { readFileSync } from "fs"; -import * as path from "path"; - import { CoqLspClient } from "../coqLsp/coqLspClient"; import { parseCoqFile } from "../coqParser/parseCoqFile"; import { ProofStep, Theorem } from "../coqParser/parsedTypes"; +import { EventLogger } from "../logging/eventLogger"; import { Uri } from "../utils/uri"; import { @@ -15,18 +13,24 @@ import { type AnalyzedFile = [CompletionContext[], SourceFileEnvironment]; export async function inspectSourceFile( - fileVersion: number, + documentVersion: number, shouldCompleteHole: (hole: ProofStep) => boolean, fileUri: Uri, - client: CoqLspClient + client: CoqLspClient, + abortSignal: AbortSignal, + needsTheoremInitialGoals: boolean = true, + eventLogger?: EventLogger ): Promise { const sourceFileEnvironment = await createSourceFileEnvironment( - fileVersion, + documentVersion, fileUri, - client + client, + abortSignal, + needsTheoremInitialGoals, + eventLogger ); const completionContexts = await createCompletionContexts( - fileVersion, + documentVersion, shouldCompleteHole, sourceFileEnvironment.fileTheorems, fileUri, @@ -35,7 +39,7 @@ export async function inspectSourceFile( const sourceFileEnvironmentWithCompleteProofs: SourceFileEnvironment = { ...sourceFileEnvironment, fileTheorems: sourceFileEnvironment.fileTheorems.filter( - (thr) => thr.proof && !thr.proof.is_incomplete + (thr) => !thr.proof.is_incomplete ), }; @@ -43,7 +47,7 @@ export async function inspectSourceFile( } async function createCompletionContexts( - fileVersion: number, + documentVersion: number, shouldCompleteHole: (hole: ProofStep) => boolean, fileTheorems: Theorem[], fileUri: Uri, @@ -57,17 +61,19 @@ async function createCompletionContexts( let completionContexts: CompletionContext[] = []; for (const hole of holesToComplete) { - const goal = await client.getFirstGoalAtPoint( + const goals = await client.getGoalsAtPoint( hole.range.start, fileUri, - fileVersion + documentVersion ); - if (!(goal instanceof Error)) { - completionContexts.push({ - proofGoal: goal, - prefixEndPosition: hole.range.start, - admitEndPosition: hole.range.end, - }); + if (goals.ok) { + const firstGoal = goals.val.shift(); + if (firstGoal) { + completionContexts.push({ + proofGoal: firstGoal, + admitRange: hole.range, + }); + } } } @@ -75,31 +81,24 @@ async function createCompletionContexts( } export async function createSourceFileEnvironment( - fileVersion: number, + documentVersion: number, fileUri: Uri, - client: CoqLspClient + client: CoqLspClient, + abortSignal: AbortSignal, + needsTheoremInitialGoals: boolean = true, + eventLogger?: EventLogger ): Promise { - const fileTheorems = await parseCoqFile(fileUri, client); - const fileText = readFileSync(fileUri.fsPath); - const dirPath = getSourceFolderPath(fileUri); - if (!dirPath) { - throw Error( - `unable to get source folder path from \`fileUri\`: ${fileUri}` - ); - } + const fileTheorems = await parseCoqFile( + fileUri, + client, + abortSignal, + needsTheoremInitialGoals, + eventLogger + ); return { fileTheorems: fileTheorems, - fileLines: fileText.toString().split("\n"), - fileVersion: fileVersion, - dirPath: dirPath, + documentVersion: documentVersion, + fileUri: fileUri, }; } - -function getSourceFolderPath(documentUri: Uri): string | undefined { - try { - return path.dirname(documentUri.fsPath); - } catch (error) { - return undefined; - } -} diff --git a/src/extension/coqPilot.ts b/src/extension/coqPilot.ts index 55250dbc..10c8ab4e 100644 --- a/src/extension/coqPilot.ts +++ b/src/extension/coqPilot.ts @@ -1,13 +1,10 @@ import { - ExtensionContext, - ProgressLocation, TextEditor, + ExtensionContext as VSCodeContext, commands, - window, workspace, } from "vscode"; -import { createCoqLspClient } from "../coqLsp/coqLspBuilders"; import { CoqLspStartupError } from "../coqLsp/coqLspTypes"; import { @@ -30,7 +27,6 @@ import { Uri } from "../utils/uri"; import { buildTheoremsRankerFromConfig, - parseCoqLspServerPath, readAndValidateUserModelsParams, } from "./configReaders"; import { @@ -38,36 +34,33 @@ import { highlightTextInEditor, insertCompletion, } from "./documentEditor"; -import { suggestAddingAuxFilesToGitignore } from "./editGitignoreCommand"; import { EditorMessages, showMessageToUser, showMessageToUserWithSettingsHint, } from "./editorMessages"; -import { GlobalExtensionState } from "./globalExtensionState"; +import { CompletionAbortError } from "./extensionAbortUtils"; import { subscribeToHandleLLMServicesEvents } from "./llmServicesEventsHandler"; +import { PluginContext } from "./pluginContext"; +import { PluginStatusIndicator } from "./pluginStatusIndicator"; import { positionInRange, toVSCodePosition, toVSCodeRange, } from "./positionRangeUtils"; +import { SessionState } from "./sessionState"; import { SettingsValidationError } from "./settingsValidationError"; -import { cleanAuxFiles, hideAuxFiles } from "./tmpFilesCleanup"; export const pluginId = "coqpilot"; export const pluginName = "CoqPilot"; export class CoqPilot { - private readonly globalExtensionState: GlobalExtensionState; - private readonly vscodeExtensionContext: ExtensionContext; - - constructor(vscodeExtensionContext: ExtensionContext) { - hideAuxFiles(); - suggestAddingAuxFilesToGitignore(); - - this.vscodeExtensionContext = vscodeExtensionContext; - this.globalExtensionState = new GlobalExtensionState(); - + private constructor( + private readonly vscodeContext: VSCodeContext, + private readonly pluginContext: PluginContext, + private sessionState: SessionState, + toggleCommand: string + ) { this.registerEditorCommand( "perform_completion_under_cursor", this.performCompletionUnderCursor.bind(this) @@ -81,7 +74,35 @@ export class CoqPilot { this.performCompletionForAllAdmits.bind(this) ); - this.vscodeExtensionContext.subscriptions.push(this); + this.registerEditorCommand( + toggleCommand, + this.sessionState.toggleCurrentSession.bind(this.sessionState) + ); + + this.vscodeContext.subscriptions.push(this); + } + + static async create(vscodeContext: VSCodeContext) { + const globalExtensionState = new PluginContext(); + + const toggleCommand = `toggle_current_session`; + const pluginStatusIndicator = new PluginStatusIndicator( + `${pluginId}.${toggleCommand}`, + vscodeContext + ); + + const sessionExtensionState = await SessionState.create( + globalExtensionState.logOutputChannel, + globalExtensionState.eventLogger, + pluginStatusIndicator + ); + + return new CoqPilot( + vscodeContext, + globalExtensionState, + sessionExtensionState, + toggleCommand + ); } async performCompletionUnderCursor(editor: TextEditor) { @@ -108,45 +129,52 @@ export class CoqPilot { shouldCompleteHole: (hole: ProofStep) => boolean, editor: TextEditor ) { - await window.withProgress( - { - location: ProgressLocation.Window, - title: `${pluginName}: In progress`, - }, - async () => { - try { - await this.performSpecificCompletions( - shouldCompleteHole, - editor - ); - } catch (e) { - if (e instanceof SettingsValidationError) { - e.showAsMessageToUser(); - } else if (e instanceof CoqLspStartupError) { - showMessageToUserWithSettingsHint( - EditorMessages.coqLspStartupFailure(e.path), - "error", - `${pluginId}.coqLspServerPath` - ); - } else { - showMessageToUser( - e instanceof Error - ? EditorMessages.errorOccurred(e.message) - : EditorMessages.objectWasThrownAsError(e), - "error" - ); - console.error(buildErrorCompleteLog(e)); - } + if (!this.sessionState.isSessionActive) { + showMessageToUser(EditorMessages.extensionIsPaused, "warning"); + return; + } + try { + this.sessionState.showInProgressSpinner(); + + await this.performSpecificCompletions( + shouldCompleteHole, + editor, + this.sessionState.abortController.signal + ); + } catch (e) { + if (e instanceof SettingsValidationError) { + e.showAsMessageToUser(); + } else if (e instanceof CoqLspStartupError) { + showMessageToUserWithSettingsHint( + EditorMessages.coqLspStartupFailure(e.path), + "error", + `${pluginId}.coqLspServerPath` + ); + } else if (e instanceof CompletionAbortError) { + if (!this.sessionState.userNotifiedAboutAbort) { + showMessageToUser(EditorMessages.completionAborted, "info"); + this.sessionState.userReceivedAbortNotification(); } + } else { + showMessageToUser( + e instanceof Error + ? EditorMessages.errorOccurred(e.message) + : EditorMessages.objectWasThrownAsError(e), + "error" + ); + console.error(buildErrorCompleteLog(e)); } - ); + } finally { + this.sessionState.hideInProgressSpinner(); + } } private async performSpecificCompletions( shouldCompleteHole: (hole: ProofStep) => boolean, - editor: TextEditor + editor: TextEditor, + abortSignal: AbortSignal ) { - this.globalExtensionState.eventLogger.log( + this.pluginContext.eventLogger.log( "completion-started", "CoqPilot has started the completion process" ); @@ -163,9 +191,10 @@ export class CoqPilot { await this.prepareForCompletions( shouldCompleteHole, editor.document.version, - editor.document.uri.fsPath + editor.document.uri.fsPath, + abortSignal ); - this.globalExtensionState.eventLogger.log( + this.pluginContext.eventLogger.log( "completion-preparation-finished", `CoqPilot has successfully parsed the file with ${sourceFileEnvironment.fileTheorems.length} theorems and has found ${completionContexts.length} admits inside chosen selection` ); @@ -177,8 +206,8 @@ export class CoqPilot { const unsubscribeFromLLMServicesEventsCallback = subscribeToHandleLLMServicesEvents( - this.globalExtensionState.llmServices, - this.globalExtensionState.eventLogger + this.pluginContext.llmServices, + this.pluginContext.eventLogger ); try { @@ -188,7 +217,8 @@ export class CoqPilot { completionContext, sourceFileEnvironment, processEnvironment, - editor + editor, + abortSignal ); } ); @@ -203,27 +233,26 @@ export class CoqPilot { completionContext: CompletionContext, sourceFileEnvironment: SourceFileEnvironment, processEnvironment: ProcessEnvironment, - editor: TextEditor + editor: TextEditor, + abortSignal: AbortSignal ) { const result = await generateCompletion( completionContext, sourceFileEnvironment, processEnvironment, - this.globalExtensionState.eventLogger + abortSignal, + this.pluginContext.eventLogger ); if (result instanceof SuccessGenerationResult) { const flatProof = this.prepareCompletionForInsertion(result.data); - const vscodeHoleRange = toVSCodeRange({ - start: completionContext.prefixEndPosition, - end: completionContext.admitEndPosition, - }); + const vscodeHoleRange = toVSCodeRange(completionContext.admitRange); const completionRange = toVSCodeRange({ - start: completionContext.prefixEndPosition, + start: completionContext.admitRange.start, end: { - line: completionContext.prefixEndPosition.line, + line: completionContext.admitRange.start.line, character: - completionContext.prefixEndPosition.character + + completionContext.admitRange.start.character + flatProof.length, }, }); @@ -232,7 +261,7 @@ export class CoqPilot { await insertCompletion( editor, flatProof, - toVSCodePosition(completionContext.prefixEndPosition) + toVSCodePosition(completionContext.admitRange.start) ); highlightTextInEditor(completionRange); } else if (result instanceof FailureGenerationResult) { @@ -248,7 +277,7 @@ export class CoqPilot { break; case FailureGenerationStatus.SEARCH_FAILED: const completionLine = - completionContext.prefixEndPosition.line + 1; + completionContext.admitRange.start.line + 1; showMessageToUser( EditorMessages.noProofsForAdmit(completionLine), "info" @@ -268,34 +297,35 @@ export class CoqPilot { private async prepareForCompletions( shouldCompleteHole: (hole: ProofStep) => boolean, - fileVersion: number, - filePath: string + documentVersion: number, + filePath: string, + abortSignal: AbortSignal ): Promise< [CompletionContext[], SourceFileEnvironment, ProcessEnvironment] > { const fileUri = Uri.fromPath(filePath); - const coqLspServerPath = parseCoqLspServerPath(); - const client = await createCoqLspClient( - coqLspServerPath, - this.globalExtensionState.logOutputChannel - ); const contextTheoremsRanker = buildTheoremsRankerFromConfig(); - const coqProofChecker = new CoqProofChecker(client); + const coqProofChecker = new CoqProofChecker( + this.sessionState.coqLspClient + ); const [completionContexts, sourceFileEnvironment] = await inspectSourceFile( - fileVersion, + documentVersion, shouldCompleteHole, fileUri, - client + this.sessionState.coqLspClient, + abortSignal, + contextTheoremsRanker.needsUnwrappedNotations, + this.pluginContext.eventLogger ); const processEnvironment: ProcessEnvironment = { coqProofChecker: coqProofChecker, modelsParams: readAndValidateUserModelsParams( workspace.getConfiguration(pluginId), - this.globalExtensionState.llmServices + this.pluginContext.llmServices ), - services: this.globalExtensionState.llmServices, + services: this.pluginContext.llmServices, theoremRanker: contextTheoremsRanker, }; @@ -310,11 +340,12 @@ export class CoqPilot { `${pluginId}.` + command, fn ); - this.vscodeExtensionContext.subscriptions.push(disposable); + this.vscodeContext.subscriptions.push(disposable); } dispose(): void { - cleanAuxFiles(); - this.globalExtensionState.dispose(); + this.vscodeContext.subscriptions.forEach((d) => d.dispose()); + this.sessionState.dispose(); + this.pluginContext.dispose(); } } diff --git a/src/extension/editGitignoreCommand.ts b/src/extension/editGitignoreCommand.ts deleted file mode 100644 index cb2012c2..00000000 --- a/src/extension/editGitignoreCommand.ts +++ /dev/null @@ -1,52 +0,0 @@ -import { appendFile, existsSync, readFileSync } from "fs"; -import * as path from "path"; -import { window, workspace } from "vscode"; - -import { showMessageToUser } from "./editorMessages"; - -export async function suggestAddingAuxFilesToGitignore() { - const workspaceFolders = workspace.workspaceFolders; - if (!workspaceFolders) { - return; - } - - for (const folder of workspaceFolders) { - const gitIgnorePath = path.join(folder.uri.fsPath, ".gitignore"); - if (!existsSync(gitIgnorePath)) { - // .gitignore not found. Exit. - return; - } - - const data = readFileSync(gitIgnorePath, "utf8"); - const auxExt = "*_cp_aux.v"; - if (data.indexOf(auxExt) === -1) { - // Not found. Ask user if we should add it. - await window - .showInformationMessage( - 'Do you want to add "*_cp_aux.v" to .gitignore?', - "Yes", - "No" - ) - .then((choice) => { - if (choice === "Yes") { - const rule = `\n# CoqPilot auxiliary files\n${auxExt}`; - appendFile(gitIgnorePath, rule, (err) => { - if (err) { - showMessageToUser( - `Unexpected error writing to .gitignore: ${err.message}`, - "error" - ); - } else { - showMessageToUser( - 'Successfully added "*_cp_aux.v" to .gitignore', - "info" - ); - } - }); - } - }); - } else { - return; - } - } -} diff --git a/src/extension/editorMessages.ts b/src/extension/editorMessages.ts index 902d69ed..cd22d2c1 100644 --- a/src/extension/editorMessages.ts +++ b/src/extension/editorMessages.ts @@ -31,6 +31,12 @@ export namespace EditorMessages { export const reportUnexpectedError = (errorDescription: string) => `Coqpilot got an unexpected error: ${errorDescription}. Please report this crash by opening an issue in the Coqpilot GitHub repository.`; + export const completionAborted = + "Completion generation was forcefully aborted, stopping Coq-LSP server. Please hit the CoqPilot Status Bar button again to restart the server and continue using CoqPilot."; + + export const extensionIsPaused = + "You have stopped CoqPilot. To resume, click on the CoqPilot icon in the status bar."; + export const objectWasThrownAsError = (e: any) => reportUnexpectedError( `object was thrown as error, ${stringifyAnyValue(e)}` diff --git a/src/extension/extensionAbortUtils.ts b/src/extension/extensionAbortUtils.ts new file mode 100644 index 00000000..27486216 --- /dev/null +++ b/src/extension/extensionAbortUtils.ts @@ -0,0 +1,15 @@ +export class CompletionAbortError extends Error { + private static readonly abortMessage = + "User has triggered a session abort: Stopping all completions"; + + constructor() { + super(CompletionAbortError.abortMessage); + this.name = "CompletionAbortError"; + } +} + +export function throwOnAbort(abortSignal?: AbortSignal) { + if (abortSignal?.aborted) { + throw abortSignal.reason; + } +} diff --git a/src/extension/globalExtensionState.ts b/src/extension/pluginContext.ts similarity index 95% rename from src/extension/globalExtensionState.ts rename to src/extension/pluginContext.ts index b1640a5b..727bcb93 100644 --- a/src/extension/globalExtensionState.ts +++ b/src/extension/pluginContext.ts @@ -1,7 +1,7 @@ import * as fs from "fs"; import * as path from "path"; import * as tmp from "tmp"; -import { WorkspaceConfiguration, window, workspace } from "vscode"; +import { Disposable, WorkspaceConfiguration, window, workspace } from "vscode"; import { LLMServices, disposeServices } from "../llm/llmServices"; import { GrazieService } from "../llm/llmServices/grazie/grazieService"; @@ -14,7 +14,7 @@ import { EventLogger, Severity } from "../logging/eventLogger"; import { pluginId } from "./coqPilot"; import VSCodeLogWriter from "./vscodeLogWriter"; -export class GlobalExtensionState { +export class PluginContext implements Disposable { public readonly eventLogger: EventLogger = new EventLogger(); public readonly logWriter: VSCodeLogWriter = new VSCodeLogWriter( this.eventLogger, diff --git a/src/extension/pluginStatusIndicator.ts b/src/extension/pluginStatusIndicator.ts new file mode 100644 index 00000000..30182c7f --- /dev/null +++ b/src/extension/pluginStatusIndicator.ts @@ -0,0 +1,49 @@ +import { + ExtensionContext, + StatusBarAlignment, + StatusBarItem, + window, +} from "vscode"; + +import { pluginName } from "./coqPilot"; + +export class PluginStatusIndicator { + private readonly statusBarItem: StatusBarItem; + + constructor( + invocationCommand: string, + private readonly context: ExtensionContext + ) { + this.statusBarItem = window.createStatusBarItem( + StatusBarAlignment.Left, + 0 + ); + this.statusBarItem.show(); + + this.context.subscriptions.push(this.statusBarItem); + this.statusBarItem.command = invocationCommand; + } + + updateStatusBar(isActive: boolean) { + if (isActive) { + this.statusBarItem.text = `$(debug-stop) ${pluginName}: Running`; + this.statusBarItem.tooltip = "Click to stop the extension"; + } else { + this.statusBarItem.text = `$(debug-start) ${pluginName}: Stopped`; + this.statusBarItem.tooltip = "Click to start the extension"; + } + } + + showInProgressSpinner() { + this.statusBarItem.text = `$(sync~spin) ${pluginName}: In progress`; + this.statusBarItem.tooltip = "Operation in progress..."; + } + + hideInProgressSpinner(isActive: boolean) { + this.updateStatusBar(isActive); + } + + dispose() { + this.statusBarItem.dispose(); + } +} diff --git a/src/extension/sessionState.ts b/src/extension/sessionState.ts new file mode 100644 index 00000000..c9621cba --- /dev/null +++ b/src/extension/sessionState.ts @@ -0,0 +1,137 @@ +import { Disposable, OutputChannel } from "vscode"; + +import { createCoqLspClient } from "../coqLsp/coqLspBuilders"; +import { CoqLspClient } from "../coqLsp/coqLspClient"; + +import { EventLogger } from "../logging/eventLogger"; + +import { parseCoqLspServerPath } from "./configReaders"; +import { CompletionAbortError } from "./extensionAbortUtils"; +import { PluginStatusIndicator } from "./pluginStatusIndicator"; + +export class SessionState implements Disposable { + private _isSessionActive = true; + private _coqLspClient: CoqLspClient; + private _abortController: AbortController; + + // When user triggers abort for completions + // and there are multiple completions in progress, + // we want to notify the user only once. + private _userNotifiedAboutAbort = false; + + throwOnInactiveSession(): void { + if (!this._isSessionActive) { + throw new Error("Trying to access a disposed session state"); + } + } + + get isSessionActive(): boolean { + return this._isSessionActive; + } + + get userNotifiedAboutAbort(): boolean { + return this._userNotifiedAboutAbort; + } + + get coqLspClient(): CoqLspClient { + this.throwOnInactiveSession(); + return this._coqLspClient; + } + + get abortController(): AbortController { + this.throwOnInactiveSession(); + return this._abortController; + } + + private constructor( + coqLspClient: CoqLspClient, + abortController: AbortController, + private readonly logOutputChannel: OutputChannel, + private readonly eventLogger: EventLogger, + private readonly pluginStatusIndicator: PluginStatusIndicator + ) { + this._coqLspClient = coqLspClient; + this._abortController = abortController; + } + + static async create( + logOutputChannel: OutputChannel, + eventLogger: EventLogger, + pluginStatusIndicator: PluginStatusIndicator + ): Promise { + const abortController = new AbortController(); + const coqLspServerPath = parseCoqLspServerPath(); + + const coqLspClient = await createCoqLspClient( + coqLspServerPath, + logOutputChannel, + eventLogger, + abortController + ); + + pluginStatusIndicator.updateStatusBar(true); + + return new SessionState( + coqLspClient, + abortController, + logOutputChannel, + eventLogger, + pluginStatusIndicator + ); + } + + userReceivedAbortNotification(): void { + this._userNotifiedAboutAbort = true; + } + + showInProgressSpinner(): void { + this.pluginStatusIndicator.showInProgressSpinner(); + } + + hideInProgressSpinner(): void { + this.pluginStatusIndicator.hideInProgressSpinner(this._isSessionActive); + } + + async toggleCurrentSession(): Promise { + if (this._isSessionActive) { + this.abort(); + } else { + await this.startNewSession(); + } + } + + abort(): void { + this._isSessionActive = false; + this._abortController.abort(new CompletionAbortError()); + this._coqLspClient.dispose(); + + this.pluginStatusIndicator.updateStatusBar(false); + + this.eventLogger.log( + "session-abort", + "User has triggered a session abort: Stopping all completions" + ); + } + + async startNewSession(): Promise { + this._isSessionActive = true; + this._abortController = new AbortController(); + + const coqLspServerPath = parseCoqLspServerPath(); + this._coqLspClient = await createCoqLspClient( + coqLspServerPath, + this.logOutputChannel, + this.eventLogger, + this._abortController + ); + + this.pluginStatusIndicator.updateStatusBar(true); + + this.eventLogger.log("session-start", "User has started a new session"); + } + + dispose(): void { + this._abortController.abort(); + this._coqLspClient.dispose(); + } +} diff --git a/src/extension/tmpFilesCleanup.ts b/src/extension/tmpFilesCleanup.ts deleted file mode 100644 index c0b18344..00000000 --- a/src/extension/tmpFilesCleanup.ts +++ /dev/null @@ -1,39 +0,0 @@ -import * as glob from "glob"; -import * as path from "path"; -import { Uri, workspace } from "vscode"; - -export function hideAuxFiles() { - // Hide files generated to check proofs - let activationConfig = workspace.getConfiguration(); - let fexc: any = activationConfig.get("files.exclude"); - activationConfig.update("files.exclude", { - ...fexc, - // eslint-disable-next-line @typescript-eslint/naming-convention - "**/*_cp_aux.v": true, - }); -} - -export function cleanAuxFiles() { - // Glob *_cp_aux.v files and delete them - const workspaceFolders = workspace.workspaceFolders; - if (!workspaceFolders) { - return; - } - - workspaceFolders.forEach((folder) => { - glob( - "**/*_cp_aux.v", - { sync: false, cwd: folder.uri.fsPath }, - (err, files) => { - if (err) { - return; - } - - files.forEach((file) => { - const filePath = path.resolve(folder.uri.fsPath, file); - workspace.fs.delete(Uri.file(filePath)); - }); - } - ); - }); -} diff --git a/src/logging/timeMeasureDecorator.ts b/src/logging/timeMeasureDecorator.ts new file mode 100644 index 00000000..a1041ad6 --- /dev/null +++ b/src/logging/timeMeasureDecorator.ts @@ -0,0 +1,45 @@ +/** + * A decorator that logs the execution time of a method. + * Execution time is logged into console in milliseconds. + * + * (Note: typescript supports decorators only for class methods). + */ +export function logExecutionTime( + _target: any, + propertyKey: string, + descriptor: PropertyDescriptor +) { + const originalMethod = descriptor.value; + + descriptor.value = function (this: any, ...args: any[]) { + const start = performance.now(); + + const result = originalMethod.apply(this, args); + + const logTime = (duration: number) => { + console.log( + `${propertyKey} took ${duration.toFixed(2)}ms to execute` + ); + }; + + if (result && typeof result.then === "function") { + return result + .then((res: any) => { + const duration = performance.now() - start; + logTime(duration); + return res; + }) + .catch((err: any) => { + const duration = performance.now() - start; + logTime(duration); + throw err; + }); + } else { + const duration = performance.now() - start; + logTime(duration); + return result; + } + }; + + return descriptor; +} diff --git a/src/mainNode.ts b/src/mainNode.ts index 7516115a..4a931eb5 100644 --- a/src/mainNode.ts +++ b/src/mainNode.ts @@ -5,7 +5,7 @@ import { CoqPilot } from "./extension/coqPilot"; export let extension: CoqPilot | undefined; export async function activate(context: ExtensionContext): Promise { - extension = new CoqPilot(context); + extension = await CoqPilot.create(context); context.subscriptions.push(extension); } diff --git a/src/test/commonTestFunctions/checkProofs.ts b/src/test/commonTestFunctions/checkProofs.ts index 6a56cc89..bf9cace7 100644 --- a/src/test/commonTestFunctions/checkProofs.ts +++ b/src/test/commonTestFunctions/checkProofs.ts @@ -3,7 +3,6 @@ import { GeneratedProof } from "../../llm/llmServices/generatedProof"; import { CompletionContext } from "../../core/completionGenerationContext"; import { ProofCheckResult } from "../../core/coqProofChecker"; import { prepareProofToCheck } from "../../core/exposedCompletionGeneratorUtils"; -import { getTextBeforePosition } from "../../core/exposedCompletionGeneratorUtils"; import { PreparedEnvironment } from "./prepareEnvironment"; @@ -12,14 +11,10 @@ export async function checkProofs( completionContext: CompletionContext, environment: PreparedEnvironment ): Promise { - const sourceFileContentPrefix = getTextBeforePosition( - environment.sourceFileEnvironment.fileLines, - completionContext.prefixEndPosition - ); return await environment.coqProofChecker.checkProofs( - environment.sourceFileEnvironment.dirPath, - sourceFileContentPrefix, - completionContext.prefixEndPosition, + environment.sourceFileEnvironment.fileUri, + environment.sourceFileEnvironment.documentVersion, + completionContext.admitRange.start, proofsToCheck ); } diff --git a/src/test/commonTestFunctions/coqFileParser.ts b/src/test/commonTestFunctions/coqFileParser.ts index 9648f459..a73137e8 100644 --- a/src/test/commonTestFunctions/coqFileParser.ts +++ b/src/test/commonTestFunctions/coqFileParser.ts @@ -19,7 +19,12 @@ export async function parseTheoremsFromCoqFile( const client = await createTestCoqLspClient(rootDir); await client.openTextDocument(fileUri); - const document = await parseCoqFile(fileUri, client); + const abortController = new AbortController(); + const document = await parseCoqFile( + fileUri, + client, + abortController.signal + ); await client.closeTextDocument(fileUri); return document; diff --git a/src/test/commonTestFunctions/prepareEnvironment.ts b/src/test/commonTestFunctions/prepareEnvironment.ts index 0698ae3d..d4e51847 100644 --- a/src/test/commonTestFunctions/prepareEnvironment.ts +++ b/src/test/commonTestFunctions/prepareEnvironment.ts @@ -38,11 +38,13 @@ export async function prepareEnvironment( const coqProofChecker = new CoqProofChecker(client); await client.openTextDocument(fileUri); + const abortController = new AbortController(); const [completionContexts, sourceFileEnvironment] = await inspectSourceFile( 1, (_hole) => true, fileUri, - client + client, + abortController.signal ); await client.closeTextDocument(fileUri); diff --git a/src/test/coqLsp/coqLspGetGoals.test.ts b/src/test/coqLsp/coqLspGetGoals.test.ts index 76d1ff83..bbb7bb1d 100644 --- a/src/test/coqLsp/coqLspGetGoals.test.ts +++ b/src/test/coqLsp/coqLspGetGoals.test.ts @@ -1,7 +1,8 @@ import { expect } from "earl"; +import { Result } from "ts-results"; import { createTestCoqLspClient } from "../../coqLsp/coqLspBuilders"; -import { ProofGoal } from "../../coqLsp/coqLspTypes"; +import { Goal, PpString } from "../../coqLsp/coqLspTypes"; import { Uri } from "../../utils/uri"; import { resolveResourcesDir } from "../commonTestFunctions/pathsResolver"; @@ -11,7 +12,7 @@ suite("Retrieve goals from Coq file", () => { points: { line: number; character: number }[], resourcePath: string[], projectRootPath?: string[] - ): Promise<(ProofGoal | Error)[]> { + ): Promise[], Error>[]> { const [filePath, rootDir] = resolveResourcesDir( resourcePath, projectRootPath @@ -22,7 +23,7 @@ suite("Retrieve goals from Coq file", () => { await client.openTextDocument(fileUri); const goals = await Promise.all( points.map(async (point) => { - return await client.getFirstGoalAtPoint(point, fileUri, 1); + return await client.getGoalsAtPoint(point, fileUri, 1); }) ); await client.closeTextDocument(fileUri); @@ -30,7 +31,7 @@ suite("Retrieve goals from Coq file", () => { return goals; } - function unpackGoal(goal: ProofGoal): { hyps: string[]; ty: string } { + function unpackGoal(goal: Goal): { hyps: string[]; ty: string } { return { hyps: goal.hyps.map((hyp) => `${hyp.names.join(" ")} : ${hyp.ty}`), ty: goal.ty as string, @@ -49,7 +50,11 @@ suite("Retrieve goals from Coq file", () => { }; expect(goals).toHaveLength(1); - expect(unpackGoal(goals[0] as ProofGoal)).toEqual(expectedGoal); + expect(goals[0].ok).toEqual(true); + if (goals[0].ok) { + expect(goals[0].val).toHaveLength(1); + expect(unpackGoal(goals[0].val[0])).toEqual(expectedGoal); + } }); test("Check correct goals requests", async () => { @@ -89,8 +94,10 @@ suite("Retrieve goals from Coq file", () => { expect(goals).toHaveLength(5); for (const [i, goal] of goals.entries()) { - expect(goals[i]).not.toBeA(Error); - expect(unpackGoal(goal as ProofGoal)).toEqual(expectedGoals[i]); + expect(goal).not.toBeA(Error); + if (goal.ok) { + expect(unpackGoal(goal.val[0])).toEqual(expectedGoals[i]); + } } }); @@ -99,16 +106,32 @@ suite("Retrieve goals from Coq file", () => { [ { line: 5, character: 0 }, { line: 6, character: 0 }, - { line: 9, character: 10 }, { line: 10, character: 9 }, + ], + ["small_document.v"] + ); + + expect(goals).toHaveLength(3); + for (const goal of goals) { + expect(goal.err).toEqual(true); + } + }); + + test("Retreive goals where no more goals", async () => { + const goals = await getGoalsAtPoints( + [ + { line: 9, character: 10 }, { line: 10, character: 3 }, ], ["small_document.v"] ); - expect(goals).toHaveLength(5); + expect(goals).toHaveLength(2); for (const goal of goals) { - expect(goal).toBeA(Error); + expect(goal.ok).toEqual(true); + if (goal.ok) { + expect(goal.val).toBeEmpty(); + } } }); @@ -140,8 +163,13 @@ suite("Retrieve goals from Coq file", () => { expect(goals).toHaveLength(3); for (const [i, goal] of goals.entries()) { - expect(goals[i]).not.toBeA(Error); - expect(unpackGoal(goal as ProofGoal)).toEqual(expectedGoals[i]); + if (goal.err) { + console.error("ERROR", i, goal.val.message); + } + expect(goal.ok).toEqual(true); + if (goal.ok) { + expect(unpackGoal(goal.val[0])).toEqual(expectedGoals[i]); + } } }); }); diff --git a/src/test/coqLsp/coqLspGoalsWithCommandExec.test.ts b/src/test/coqLsp/coqLspGoalsWithCommandExec.test.ts new file mode 100644 index 00000000..1c284985 --- /dev/null +++ b/src/test/coqLsp/coqLspGoalsWithCommandExec.test.ts @@ -0,0 +1,225 @@ +import { expect } from "earl"; +import { Result } from "ts-results"; + +import { createTestCoqLspClient } from "../../coqLsp/coqLspBuilders"; +import { Goal, PpString } from "../../coqLsp/coqLspTypes"; + +import { Uri } from "../../utils/uri"; +import { resolveResourcesDir } from "../commonTestFunctions/pathsResolver"; + +suite("Request goals with `command/pretac` argument", () => { + async function getGoalsAtPosition( + position: { line: number; character: number }, + resourcePath: string[], + command: string, + projectRootPath?: string[] + ): Promise[], Error>> { + const [filePath, rootDir] = resolveResourcesDir( + resourcePath, + projectRootPath + ); + const fileUri = Uri.fromPath(filePath); + + const client = await createTestCoqLspClient(rootDir); + let goals: Result[], Error> | undefined; + + try { + await client.openTextDocument(fileUri); + goals = await client.getGoalsAtPoint(position, fileUri, 1, command); + } finally { + await client.closeTextDocument(fileUri); + client.dispose(); + } + + if (goals === undefined) { + throw new Error("The goals were not received."); + } + + return goals; + } + + function checkSuccessfullGoalConcls( + goals: Result[], Error>, + goalConclusions: string[] + ): void { + expect(goals.ok).toEqual(true); + if (goals.ok) { + expect(goals.val).toHaveLength(goalConclusions.length); + for (let i = 0; i < goalConclusions.length; i++) { + expect(goals.val[i].ty).toEqual(goalConclusions[i]); + } + } + } + + function checkCommandApplicationError( + goals: Result[], Error>, + expectedError: string + ): void { + expect(goals.err).toEqual(true); + expect(goals.val).toBeA(Error); + if (goals.err) { + expect(goals.val.message).toEqual(expectedError); + } + } + + test("One Coq sentence: fail to solve with invalid goal", async () => { + const goals = await getGoalsAtPosition( + { line: 9, character: 4 }, + ["small_document.v"], + "reflexivity." + ); + + checkCommandApplicationError( + goals, + 'In environment\nn : nat\nUnable to unify "n" with\n "0 + n + 0".' + ); + }); + + test("One Coq sentence: fail to solve with invalid tactic", async () => { + const goals = await getGoalsAtPosition( + { line: 9, character: 4 }, + ["small_document.v"], + "reflexivit." + ); + + checkCommandApplicationError( + goals, + "The reference reflexivit was not found in the current\nenvironment." + ); + }); + + test("One Coq sentence: successfully solve no goals left", async () => { + const goals = await getGoalsAtPosition( + { line: 9, character: 4 }, + ["small_document.v"], + "auto." + ); + + checkSuccessfullGoalConcls(goals, []); + }); + + test("One Coq sentence: successfully solve 1 goal left", async () => { + const goals = await getGoalsAtPosition( + { line: 9, character: 4 }, + ["test_many_subgoals.v"], + "auto." + ); + + checkSuccessfullGoalConcls(goals, ["S n + 0 = S n"]); + }); + + test("One Coq sentence: successfully solve 2 goals left", async () => { + const goals = await getGoalsAtPosition( + { line: 22, character: 4 }, + ["test_many_subgoals.v"], + "auto." + ); + + checkSuccessfullGoalConcls(goals, [ + "Second = First \\/ Second = Second \\/ Second = Third", + "Third = First \\/ Third = Second \\/ Third = Third", + ]); + }); + + test("One Coq sentence wrapped into curly braces: solve successfully", async () => { + const goals = await getGoalsAtPosition( + { line: 9, character: 4 }, + ["small_document.v"], + " { auto. }" + ); + + checkSuccessfullGoalConcls(goals, []); + }); + + test("One Coq sentence wrapped into curly braces: invalid proof", async () => { + const goals = await getGoalsAtPosition( + { line: 9, character: 4 }, + ["small_document.v"], + " { kek. }" + ); + + checkCommandApplicationError( + goals, + "The reference kek was not found in the current\nenvironment." + ); + }); + + test("One Coq sentence wrapped into curly braces: valid proof, test indent", async () => { + const goals = await getGoalsAtPosition( + { line: 2, character: 12 }, + ["test_many_subgoals.v"], + "{ auto. }" + ); + + checkSuccessfullGoalConcls(goals, []); + }); + + test("Many Coq sentences: valid proof", async () => { + const goals = await getGoalsAtPosition( + { line: 2, character: 12 }, + ["test_many_subgoals.v"], + "simpl. induction n. reflexivity. auto." + ); + + checkSuccessfullGoalConcls(goals, []); + }); + + test("Many Coq sentences: invalid proof", async () => { + const goals = await getGoalsAtPosition( + { line: 2, character: 12 }, + ["test_many_subgoals.v"], + "simpl. induction n. reflexivity. reflexivity." + ); + + checkCommandApplicationError( + goals, + 'In environment\nn : nat\nIHn : n + 0 = n\nUnable to unify "S n" with\n "S n + 0".' + ); + }); + + test("Many Coq sentences: valid proof with multiple curly braces", async () => { + const goals = await getGoalsAtPosition( + { line: 2, character: 12 }, + ["test_many_subgoals.v"], + "{ simpl. \n induction n. \n { reflexivity. }\n auto. \n }" + ); + + checkSuccessfullGoalConcls(goals, []); + }); + + test("Many Coq sentences: invalid proof with multiple curly braces", async () => { + const goals = await getGoalsAtPosition( + { line: 2, character: 12 }, + ["test_many_subgoals.v"], + "{ simpl. \n induction n. \n { reflexivity. }\n reflexivity. \n }" + ); + + checkCommandApplicationError( + goals, + 'In environment\nn : nat\nIHn : n + 0 = n\nUnable to unify "S n" with\n "S n + 0".' + ); + }); + + test("Many Coq sentences: valid proof with bullets", async () => { + const goals = await getGoalsAtPosition( + { line: 2, character: 12 }, + ["test_many_subgoals.v"], + "{ \n simpl. \n induction n. \n - reflexivity.\n - auto. \n }" + ); + + checkSuccessfullGoalConcls(goals, []); + }); + + test("Many Coq sentences: invalid proof with bullets", async () => { + const goals = await getGoalsAtPosition( + { line: 2, character: 12 }, + ["test_many_subgoals.v"], + "{ \n simpl. \n induction n. \n - reflexivity.\n - reflexivity. \n }" + ); + + checkCommandApplicationError( + goals, + 'In environment\nn : nat\nIHn : n + 0 = n\nUnable to unify "S n" with\n "S n + 0".' + ); + }); +}); diff --git a/src/test/coqParser/parseCoqFile.test.ts b/src/test/coqParser/parseCoqFile.test.ts index 1d00ce1d..cc4c06fd 100644 --- a/src/test/coqParser/parseCoqFile.test.ts +++ b/src/test/coqParser/parseCoqFile.test.ts @@ -100,13 +100,8 @@ suite("Coq file parser tests", () => { "test_7", ]; - const theoremsWithoutProof = doc.filter((theorem) => !theorem.proof); - const theoremsWithProof = doc.filter((theorem) => theorem.proof); - const theoremNames = theoremsWithProof.map((theorem) => theorem.name); - + const theoremNames = doc.map((theorem) => theorem.name); expect(theoremNames).toEqual(theoremData); - expect(theoremsWithoutProof).toHaveLength(1); - expect(theoremsWithoutProof[0].name).toEqual("test_5"); }); test("Test parse file which is part of project", async () => { diff --git a/src/test/core/completionGenerator.test.ts b/src/test/core/completionGenerator.test.ts index 6855ee7a..d7fddc75 100644 --- a/src/test/core/completionGenerator.test.ts +++ b/src/test/core/completionGenerator.test.ts @@ -32,21 +32,32 @@ suite("Completion generation tests", () => { modelsParams: createPredefinedProofsModelsParams(predefinedProofs), services: createDefaultServices(), }; + const abortController = new AbortController(); try { - return await Promise.all( + await environment.coqLspClient.openTextDocument( + environment.sourceFileEnvironment.fileUri + ); + + const generationResult = await Promise.all( environment.completionContexts.map( async (completionContext) => { const result = await generateCompletion( completionContext, environment.sourceFileEnvironment, - processEnvironment + processEnvironment, + abortController.signal ); return result; } ) ); + + return generationResult; } finally { disposeServices(processEnvironment.services); + await environment.coqLspClient.closeTextDocument( + environment.sourceFileEnvironment.fileUri + ); } } diff --git a/src/test/core/coqProofChecker.test.ts b/src/test/core/coqProofChecker.test.ts index f9ecc454..ef864a39 100644 --- a/src/test/core/coqProofChecker.test.ts +++ b/src/test/core/coqProofChecker.test.ts @@ -1,12 +1,11 @@ import { expect } from "earl"; -import { readFileSync } from "fs"; -import * as path from "path"; import { createTestCoqLspClient } from "../../coqLsp/coqLspBuilders"; import { CoqProofChecker } from "../../core/coqProofChecker"; import { ProofCheckResult } from "../../core/coqProofChecker"; +import { Uri } from "../../utils/uri"; import { resolveResourcesDir } from "../commonTestFunctions/pathsResolver"; suite("`CoqProofChecker` tests", () => { @@ -20,21 +19,22 @@ suite("`CoqProofChecker` tests", () => { resourcePath, projectRootPath ); - const fileDir = path.dirname(filePath); + const fileUri = Uri.fromPath(filePath); + const documentVersion = 1; - const fileLines = readFileSync(filePath).toString().split("\n"); const client = await createTestCoqLspClient(rootDir); const coqProofChecker = new CoqProofChecker(client); + await client.openTextDocument(fileUri); + const preparedProofs = proofsToCheck.map((proofs) => proofs.map(prepareProofBeforeCheck) ); - return Promise.all( + const proofRes = await Promise.all( positions.map(async (position, i) => { - const textPrefix = getTextBeforePosition(fileLines, position); const proofCheckRes = await coqProofChecker.checkProofs( - fileDir, - textPrefix, + fileUri, + documentVersion, position, preparedProofs[i] ); @@ -46,6 +46,11 @@ suite("`CoqProofChecker` tests", () => { }); }) ); + + await client.closeTextDocument(fileUri); + client.dispose(); + + return proofRes; } function prepareProofBeforeCheck(proof: string) { @@ -60,18 +65,6 @@ suite("`CoqProofChecker` tests", () => { .trim(); } - function getTextBeforePosition( - textLines: string[], - position: { line: number; character: number } - ): string[] { - const textPrefix = textLines.slice(0, position.line + 1); - textPrefix[position.line] = textPrefix[position.line].slice( - 0, - position.character - ); - return textPrefix; - } - test("Check simple admits", async () => { const filePath = ["small_document.v"]; const proofs = [["reflexivity.", "auto."]]; diff --git a/src/test/legacyBenchmark/benchmarkingFramework.ts b/src/test/legacyBenchmark/benchmarkingFramework.ts index cd2d4ac7..84374d8a 100644 --- a/src/test/legacyBenchmark/benchmarkingFramework.ts +++ b/src/test/legacyBenchmark/benchmarkingFramework.ts @@ -98,7 +98,6 @@ export async function runTestBenchmark( eventLogger, maxPremisesNumber, reportHolder, - workspaceRootPath, perProofTimeoutMillis ); consoleLog( @@ -123,7 +122,6 @@ export async function runTestBenchmark( eventLogger, maxPremisesNumber, reportHolder, - workspaceRootPath, perProofTimeoutMillis ); consoleLog( @@ -200,7 +198,6 @@ export async function benchmarkTargets( eventLogger: EventLogger, maxPremisesNumber?: number, reportHolder?: BenchmarkReportHolder, - workspaceRootPath?: string, perProofTimeoutMillis: number = 15000 ): Promise { const totalCompletionsNumber = targets.length; @@ -216,7 +213,6 @@ export async function benchmarkTargets( eventLogger, maxPremisesNumber, reportHolder, - workspaceRootPath, perProofTimeoutMillis ); if (success) { @@ -239,10 +235,9 @@ async function benchmarkCompletionGeneration( eventLogger: EventLogger, maxPremisesNumber?: number, reportHolder?: BenchmarkReportHolder, - workspaceRootPath?: string, perProofTimeoutMillis: number = 15000 ): Promise { - const completionPosition = completionContext.admitEndPosition; + const completionPosition = completionContext.admitRange.start; consoleLog( `Completion position: ${completionPosition.line}:${completionPosition.character}` ); @@ -271,12 +266,13 @@ async function benchmarkCompletionGeneration( premisesNumber: maxPremisesNumber, }; + const abortController = new AbortController(); const result = await generateCompletion( completionContext, sourceFileEnvironmentWithFilteredContext, processEnvironmentWithPremisesNumber, + abortController.signal, undefined, - workspaceRootPath, perProofTimeoutMillis ); let message = "unknown"; @@ -392,10 +388,10 @@ async function prepareForBenchmarkCompletions( await client.openTextDocument(fileUri); const coqProofChecker = new CoqProofChecker(client); - const mockFileVersion = 1; + const mockDocumentVersion = 1; const [completionTargets, sourceFileEnvironment] = await extractCompletionTargets( - mockFileVersion, + mockDocumentVersion, shouldCompleteHole, fileUri, client @@ -423,18 +419,20 @@ async function prepareForBenchmarkCompletions( } async function extractCompletionTargets( - fileVersion: number, + documentVersion: number, shouldCompleteHole: (hole: ProofStep) => boolean, fileUri: Uri, client: CoqLspClient ): Promise<[BenchmarkingCompletionTargets, SourceFileEnvironment]> { + const abortController = new AbortController(); const sourceFileEnvironment = await createSourceFileEnvironment( - fileVersion, + documentVersion, fileUri, - client + client, + abortController.signal ); const completionTargets = await createCompletionTargets( - fileVersion, + documentVersion, shouldCompleteHole, sourceFileEnvironment.fileTheorems, fileUri, @@ -443,7 +441,7 @@ async function extractCompletionTargets( const sourceFileEnvironmentWithCompleteProofs: SourceFileEnvironment = { ...sourceFileEnvironment, fileTheorems: sourceFileEnvironment.fileTheorems.filter( - (thr) => thr.proof && !thr.proof.is_incomplete + (thr) => !thr.proof.is_incomplete ), }; @@ -456,7 +454,7 @@ interface ParentedProofStep { } async function createCompletionTargets( - fileVersion: number, + documentVersion: number, shouldCompleteHole: (hole: ProofStep) => boolean, fileTheorems: Theorem[], fileUri: Uri, @@ -486,13 +484,13 @@ async function createCompletionTargets( return { admitTargets: await resolveProofStepsToCompletionContexts( admitHolesToComplete, - fileVersion, + documentVersion, fileUri, client ), theoremTargets: await resolveProofStepsToCompletionContexts( firstProofSteps, - fileVersion, + documentVersion, fileUri, client ), @@ -501,24 +499,26 @@ async function createCompletionTargets( async function resolveProofStepsToCompletionContexts( parentedProofSteps: ParentedProofStep[], - fileVersion: number, + documentVersion: number, fileUri: Uri, client: CoqLspClient ): Promise { let completionContexts: BenchmarkingCompletionContext[] = []; for (const parentedProofStep of parentedProofSteps) { - const goal = await client.getFirstGoalAtPoint( + const goals = await client.getGoalsAtPoint( parentedProofStep.proofStep.range.start, fileUri, - fileVersion + documentVersion ); - if (!(goal instanceof Error)) { - completionContexts.push({ - proofGoal: goal, - prefixEndPosition: parentedProofStep.proofStep.range.start, - admitEndPosition: parentedProofStep.proofStep.range.end, - parentTheorem: parentedProofStep.parentTheorem, - }); + if (goals.ok) { + const firstGoal = goals.val.shift(); + if (firstGoal) { + completionContexts.push({ + proofGoal: firstGoal, + admitRange: parentedProofStep.proofStep.range, + parentTheorem: parentedProofStep.parentTheorem, + }); + } } } return completionContexts; diff --git a/src/test/resources/benchmarking/singleTaskRunnerExampleInput/cached_auto_benchmark.json b/src/test/resources/benchmarking/singleTaskRunnerExampleInput/cached_auto_benchmark.json index d99b27bc..06b4b401 100644 --- a/src/test/resources/benchmarking/singleTaskRunnerExampleInput/cached_auto_benchmark.json +++ b/src/test/resources/benchmarking/singleTaskRunnerExampleInput/cached_auto_benchmark.json @@ -88,54 +88,6 @@ } } ], - "fileLines": [ - "Theorem test : forall (A : Type) (P : A -> Prop) (x : A), P x -> P x.", - "Proof.", - " admit.", - "Admitted.", - "", - "(* Theorem test2 : forall (A : Type) (P : A -> Prop) (x : A), P x -> P x.", - "Proof.", - " intros A P x H.", - " admit.", - "Admitted.", - "", - "Theorem test2nat1 : forall n : nat, n = 0 \\/ n <> 0.", - "Proof.", - " intros n.", - " destruct n.", - " - admit.", - " - right.", - " discriminate.", - "Admitted.", - "", - "Theorem test2nat2 : forall n : nat, n = 0 \\/ n <> 0.", - "Proof.", - " intros n.", - " destruct n.", - " {", - " admit.", - " }", - " {", - " admit.", - " }", - "Admitted.", - "", - "Theorem test_thr : forall n:nat, 0 + n = n.", - "Proof.", - " intros n. Print plus.", - " admit.", - " (* reflexivity. *)", - "Admitted.", - "", - "Lemma test_thr1 : forall n:nat, 0 + n + 0 = n.", - "Proof.", - " intros n. Print plus.", - " admit.", - " (* reflexivity. *)", - "Admitted. *)", - "" - ], - "fileVersion": 1, + "documentVersion": 1, "filePath": "auto_benchmark.v" } \ No newline at end of file diff --git a/src/test/resources/test_many_subgoals.v b/src/test/resources/test_many_subgoals.v new file mode 100644 index 00000000..f388f68c --- /dev/null +++ b/src/test/resources/test_many_subgoals.v @@ -0,0 +1,26 @@ +Lemma one_subgoal : forall n:nat, 0 + n + 0 = n. +Proof. + intros. admit. +Admitted. + +Lemma two_subgoals : forall n:nat, n + 0 = n. +Proof. + intros. + induction n. + admit. + admit. +Admitted. + +Inductive MyType : Type := +| First : MyType +| Second : MyType +| Third : MyType. + +Theorem three_subgoals : forall t : MyType, + (t = First) \/ (t = Second) \/ (t = Third). +Proof. + intros t. destruct t. + admit. + admit. + admit. +Admitted. \ No newline at end of file