diff --git a/.github/workflows/coqpilot.yml b/.github/workflows/coqpilot.yml
index 2f75afd8..644ca95a 100644
--- a/.github/workflows/coqpilot.yml
+++ b/.github/workflows/coqpilot.yml
@@ -68,4 +68,19 @@ jobs:
env:
COQ_LSP_PATH: ${{ env.coqlsppath }}
run: npm test -- -ex='simpleSolver.test.js'
- if: runner.os != 'Linux'
\ No newline at end of file
+ if: runner.os != 'Linux'
+
+ create-release:
+ runs-on: ubuntu-latest
+ needs: [build]
+ if: github.ref == 'refs/heads/main'
+ steps:
+ - uses: actions/checkout@v4
+ - uses: actions/setup-node@v3
+ with:
+ node-version: 16.x
+ - name: Publish to Visual Studio Marketplace
+ uses: HaaLeo/publish-vscode-extension@v1
+ with:
+ pat: ${{ secrets.VSCE_ACCESS_TOKEN }}
+ registryUrl: https://marketplace.visualstudio.com
\ No newline at end of file
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3398dfd1..af5cef88 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,12 @@
# Change Log
+### 1.4.2
+- Now no need to add dot in the end of the tactic, when configuring a single tactic solver.
+- Automatic reload settings on change in the settings file. Not all settings are reloaded automatically,
+but the most ones are. The ones that are not automatically reloaded: `useGpt`, `coqLspPath`, `parseFileOnInit`.
+- Added command that solves admits in selected region. Also added that command to the context menu (right click in the editor).
+- Fix toggle extension.
+
### 1.4.1
- Add a possibility to configure a single tactic solver.
diff --git a/README.md b/README.md
index 1a4111a4..f7e01f68 100644
--- a/README.md
+++ b/README.md
@@ -12,13 +12,19 @@ Now `coqpilot` is in early beta and seeks for feedbacks. Please feel free to ope
`Coqpilot` could be run to analyse the opened `coq` file, fetch proofs of successfully typechecked theorems inside it, parse them and use as a message history to present to LLM.
-Later on, on demand, it could perform a request to an LLM with an admitted theorem and a message history and get a list of potential proofs. It then uses `coq-lsp` to typecheck them and substitute the first valid proof in the editor.
+Later on, on demand, it could perform a request to an LLM with an admitted theorem and a message history and get a list of potential proofs. It then uses `coq-lsp` to typecheck them and substitute the first valid proof in the editor. Moreover, coqpilot was designed to fetch multiple LLMs, so that many ways of proof generation could be used at once. Right now, apart from GPT, coqpilot also tries substituting single-line proofs from the `coqpilot.extraCommandsList` setting.
User can:
- Run `coqpilot` at a given cursor point inside theorem to try substitute the current goal.
+- Run `coqpilot` with some chosen selection to try substitute all admits in this selection.
+
+
+
+- Run `coqpilot` to try substitute all admits in the file.
+
## Requirements
* `coq-lsp` version 0.1.7 is currently required to run the extension.
@@ -56,18 +62,30 @@ This extension contributes the following settings:
* `coqpilot.logFolderPath`: A path to the folder where logs should be saved. If `None` is specified and logAttemps is `true` then logs will be saved in the `coqpilot` plugin folder in the `logs` subfolder.
* `coqpilot.parseFileOnInit`: Whether to start parsing the file into message history on extension startup.
* `coqpilot.parseFileOnEditorChange`: Whether to start re-parsing the file each time the editor has changed.
+* `coqpilot.extraCommandsList`: A list of tactics that would also be used to try generating proofs. Commands in the list must be valid coq commands available in your environment. Might or might not end with a dot, if it does not, then a dot will be added automatically.
+* `coqpilot.coqLspPath`: Path to the coq-lsp binary, by default, search in PATH.
+* `coqpilot.useGpt`: Whether to use gpt as one of the used LLMs. Right now otherwise only single tactics would be used to generate proofs.
+
+**REMARK**: `useGpt`, `coqLspPath`, `parseFileOnInit` are NOT auto reloaded on setting change, they need plugin restart.
## Contributed Commands
* `coqpilot.init_history`: Parse current file and initialize llm gistory with theorems from it.
* `coqpilot.run_generation`: Try to generate proof for the goal under the cursor.
+* `coqpilot.toggle`: Toggle the plugin.
+* `coqpilot.prove_all_holes`: Try to prove all holes (admitted goals) in the current file.
+* `coqpilot.prove_in_selection`: Try to prove holes in selection.
## Planned Features
-It is planned to implement a proof repair feature for the proofs which will establish a dialogue between `coq-lsp` and the LLM. When LLM generates an incorrect proof, the error would be sent to LLM as a next message and the process would be repeated until a valid proof is found or the limit of attempts is reached.
+### Milestone 2.0.0
+
+It is planned to implement a proof repair feature for the proofs which will establish a dialogue between `coq-lsp` and the LLM. When LLM generates an incorrect proof, the error would be sent to LLM as a next message and the process would be repeated until a valid proof is found or the limit of attempts is reached. Also it is planned to fetch proofs from different LLMs not at once in the beggining, but asynchronously and one by one, if it fails to find a proof in the first LLM, it will try the next one.
## Release Notes
+More detailed release notes could be found in the [CHANGELOG.md](https://github.com/K-dizzled/coqpilot/blob/main/CHANGELOG.md) file.
+
### 1.1.0
Now proof generation could be run in any position inside the theorem. There is no need to retake file snapshot after each significant file change.
diff --git a/etc/gif/solve-in-selection.gif b/etc/gif/solve-in-selection.gif
new file mode 100644
index 00000000..d58a084b
Binary files /dev/null and b/etc/gif/solve-in-selection.gif differ
diff --git a/package-lock.json b/package-lock.json
index 9c34e5ce..3cdb4984 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -1,12 +1,12 @@
{
"name": "coqpilot",
- "version": "1.4.0",
+ "version": "1.4.2",
"lockfileVersion": 2,
"requires": true,
"packages": {
"": {
"name": "coqpilot",
- "version": "1.4.0",
+ "version": "1.4.2",
"dependencies": {
"@codemirror/autocomplete": "^6.9.1",
"cli-progress": "^3.12.0",
diff --git a/package.json b/package.json
index f1dea71a..1617e943 100644
--- a/package.json
+++ b/package.json
@@ -8,7 +8,7 @@
"url": "https://github.com/K-dizzled/coqpilot"
},
"publisher": "JetBrains-Research",
- "version": "1.4.1",
+ "version": "1.4.2",
"engines": {
"vscode": "^1.82.0"
},
@@ -43,18 +43,6 @@
"command": "coqpilot.run_generation",
"title": "Coqpilot: Try to generate proof for the goal under the cursor."
},
- {
- "command": "coqpilot.coq-lsp.restart",
- "title": "Coqpilot: Restart the underlying coq-lsp server."
- },
- {
- "command": "coqpilot.coq-lsp.toggle",
- "title": "Coqpilot: Toggle the underlying coq-lsp server."
- },
- {
- "command": "coqpilot.coq-lsp.stop",
- "title": "Coqpilot: Stop the coq-lsp server."
- },
{
"command": "coqpilot.toggle",
"title": "Coqpilot: Toggle the plugin"
@@ -62,12 +50,21 @@
{
"command": "coqpilot.prove_all_holes",
"title": "Coqpilot: Try to prove all holes (admitted goals) in the current file."
- },
+ },
{
- "command": "coqpilot.reload_config",
- "title": "Reload the settings (trigger this if you have changed the settings after plugin start and want to see the updates)."
+ "command": "coqpilot.prove_in_selection",
+ "title": "Coqpilot: Try to prove holes in selection."
}
],
+ "menus": {
+ "editor/context": [
+ {
+ "command": "coqpilot.prove_in_selection",
+ "when": "editorTextFocus && editorHasSelection && resourceLangId == coq",
+ "group": "queries"
+ }
+ ]
+ },
"configuration": [
{
"type": "object",
@@ -131,7 +128,7 @@
},
"coqpilot.parseFileOnInit": {
"type": "boolean",
- "default": true,
+ "default": false,
"markdownDescription": "Whether to start parsing the file into message history on extension startup."
},
"coqpilot.parseFileOnEditorChange": {
@@ -145,7 +142,7 @@
"type": "string"
},
"default": [],
- "markdownDescription": "A list of tactics that would also be used to try generating proofs. Commands in the list must be valid coq commands available in your environment and must finish with a dot."
+ "markdownDescription": "A list of tactics that would also be used to try generating proofs. Commands in the list must be valid coq commands available in your environment."
},
"coqpilot.coqLspPath": {
"type": "string",
diff --git a/src/coqLlmInteraction/gpt35.ts b/src/coqLlmInteraction/gpt35.ts
index cfd1e7f9..92c2b91b 100644
--- a/src/coqLlmInteraction/gpt35.ts
+++ b/src/coqLlmInteraction/gpt35.ts
@@ -2,24 +2,32 @@ import { LLMInterface } from "./llmInterface";
import { LLMPrompt } from "./llmPromptInterface";
import OpenAI from 'openai';
import logger from "../extension/logger";
+import { CoqpilotConfigWrapper } from "../extension/config";
type GptRole = "function" | "user" | "system" | "assistant";
export class GPT35 implements LLMInterface {
history: { role: GptRole; content: string; }[];
- readonly apiKey: string;
readonly requestAttempts: number;
- readonly model: string;
+ readonly config: CoqpilotConfigWrapper;
openai: OpenAI;
+ apiKey: string;
- constructor(apiKey: string, requestAttempts: number = 3, model: string = "gpt-3.5-turbo-0301") {
- this.apiKey = apiKey;
+ constructor(config: CoqpilotConfigWrapper, requestAttempts: number = 3) {
+ this.config = config;
this.requestAttempts = requestAttempts;
- this.model = model;
this.history = [];
+ this.apiKey = config.config.openaiApiKey;
this.openai = new OpenAI({ apiKey: this.apiKey });
}
+ private updateOpenAi() {
+ if (this.config.config.openaiApiKey !== this.apiKey) {
+ this.apiKey = this.config.config.openaiApiKey;
+ this.openai = new OpenAI({ apiKey: this.apiKey });
+ }
+ }
+
initHistory(llmPrompt: LLMPrompt): void {
this.history = [];
const prompt = llmPrompt.getSystemMessage();
@@ -34,6 +42,7 @@ export class GPT35 implements LLMInterface {
}
async sendMessageWithoutHistoryChange(message: string, choices: number): Promise {
+ this.updateOpenAi();
let attempts = this.requestAttempts;
let completion = null;
logger.info("Start sending message to open-ai");
@@ -42,7 +51,7 @@ export class GPT35 implements LLMInterface {
logger.info("Sending request with history: " + JSON.stringify(this.history.concat([{role: "user", content: message}])));
completion = await this.openai.chat.completions.create({
messages: this.history.concat([{role: "user", content: message}]),
- model: this.model,
+ model: this.config.config.gptModel,
n: choices
});
logger.info("Request to open-ai succeeded");
diff --git a/src/coqLlmInteraction/singleTacticSolver.ts b/src/coqLlmInteraction/singleTacticSolver.ts
index 0c3c2c4d..cd64a986 100644
--- a/src/coqLlmInteraction/singleTacticSolver.ts
+++ b/src/coqLlmInteraction/singleTacticSolver.ts
@@ -1,11 +1,12 @@
import { LLMInterface } from "./llmInterface";
import { LlmPromptInterface } from "./llmPromptInterface";
+import { CoqpilotConfigWrapper } from "../extension/config";
export class SingleTacticSolver implements LLMInterface {
- private tactics: string[];
+ private configWrapped: CoqpilotConfigWrapper;
- constructor(tactics: string[]) {
- this.tactics = tactics;
+ constructor(configWrapped: CoqpilotConfigWrapper) {
+ this.configWrapped = configWrapped;
}
initHistory(_llmPrompt: LlmPromptInterface): void {
@@ -13,7 +14,7 @@ export class SingleTacticSolver implements LLMInterface {
}
async sendMessageWithoutHistoryChange(_message: string, _choices: number): Promise {
- return this.tactics.map((tactic) => {
+ return this.configWrapped.config.extraCommandsList.map((tactic) => {
return `Proof. ${tactic} Qed.`;
});
}
diff --git a/src/coqLspClient/coqLspClient.ts b/src/coqLspClient/coqLspClient.ts
index 34c019d2..b7605aab 100644
--- a/src/coqLspClient/coqLspClient.ts
+++ b/src/coqLspClient/coqLspClient.ts
@@ -13,7 +13,7 @@ import {
import logger from "../extension/logger";
import { CoqLspServerConfig } from "./config";
import { StatusBarButton } from "../editor/enableButton";
-import { CoqpilotConfig } from "../extension/config";
+import { CoqpilotConfigWrapper } from "../extension/config";
export class CoqLspClient extends LanguageClient {
private statusItem: StatusBarButton;
@@ -21,7 +21,7 @@ export class CoqLspClient extends LanguageClient {
constructor(
statusItem: StatusBarButton,
wsConfig: WorkspaceConfiguration,
- extensionConfig: CoqpilotConfig,
+ extensionConfig: CoqpilotConfigWrapper,
path?: Uri
) {
const initializationOptions = CoqLspServerConfig.create();
@@ -36,7 +36,7 @@ export class CoqLspClient extends LanguageClient {
markdown: { isTrusted: true, supportHtml: true },
middleware: {
handleDiagnostics: (uri, diagnostics, _next) => {
- logger.info(`Diagnostics received for file ${uri}: ${diagnostics.map((d) => d.message).join(", ")}`);
+ logger.debug(`Diagnostics received for file ${uri}: ${diagnostics.map((d) => d.message).join(", ")}`);
}
}
};
@@ -52,13 +52,14 @@ export class CoqLspClient extends LanguageClient {
};
}
+ const extConfig = extensionConfig.config;
const serverOptions: ServerOptions = {
- command: extensionConfig.coqLspPath,
+ command: extConfig.coqLspPath,
args: wsConfig.args,
};
super(
- extensionConfig.coqLspPath,
+ extConfig.coqLspPath,
"Coq LSP Server",
serverOptions,
clientOptions
diff --git a/src/extension.ts b/src/extension.ts
index 451a2a55..07ef4c00 100644
--- a/src/extension.ts
+++ b/src/extension.ts
@@ -18,7 +18,7 @@ import { StatusBarButton } from "./editor/enableButton";
import { LLMPrompt } from "./coqLlmInteraction/llmPromptInterface";
import { CoqPromptKShot } from "./coqLlmInteraction/coqLlmPrompt";
import { LLMInterface } from "./coqLlmInteraction/llmInterface";
-import { CoqpilotConfig } from "./extension/config";
+import { CoqpilotConfig, CoqpilotConfigWrapper } from "./extension/config";
import {
Interactor,
GenerationStatus,
@@ -29,6 +29,8 @@ import { VsCodeSpinningWheelProgressBar } from "./extension/vscodeProgressBar";
import logger from "./extension/logger";
import { makeAuxfname } from "./coqLspClient/utils";
import * as lspUtils from "./coqLspClient/utils";
+import { ProofStep } from "./lib/pvTypes";
+import * as utils from "./coqLspClient/utils";
export class Coqpilot implements Disposable {
@@ -39,7 +41,7 @@ export class Coqpilot implements Disposable {
private statusItem: StatusBarButton;
private llmPrompt: LLMPrompt | undefined;
private llm: LLMInterface;
- public config: CoqpilotConfig;
+ private config: CoqpilotConfigWrapper = CoqpilotConfig.getNew();
private constructor(
context: ExtensionContext,
@@ -47,17 +49,16 @@ export class Coqpilot implements Disposable {
this.excludeAuxFiles();
this.context = context;
- this.reloadConfig();
this.llm = CoqpilotConfig.getLlm(this.config);
this.disposables.push(this.statusItem);
this.disposables.push(this.textEditorChangeHook);
this.registerCommand("toggle", this.toggleLspClient.bind(this));
- this.registerCommand("reload_config", this.reloadConfig.bind(this));
this.registerEditorCommand("init_history", this.initHistory.bind(this));
this.registerEditorCommand("run_generation", this.runGeneration.bind(this));
this.registerEditorCommand("prove_all_holes", this.runProveAllAdmitted.bind(this));
+ this.registerEditorCommand("prove_in_selection", this.runProveAdmittedInSelection.bind(this));
this.context.subscriptions.push(this);
}
@@ -65,7 +66,7 @@ export class Coqpilot implements Disposable {
initialHistoryFetch = async (editor: TextEditor | undefined) => {
if (!editor) {
return;
- } else if (editor.document.languageId !== "coq" || !this.config.parseFileOnInit) {
+ } else if (editor.document.languageId !== "coq" || !this.config.config.parseFileOnInit) {
return;
}
@@ -76,7 +77,7 @@ export class Coqpilot implements Disposable {
textEditorChangeHook = window.onDidChangeActiveTextEditor((editor) => {
if (!editor) {
return;
- } else if (editor.document.languageId !== "coq" || !this.config.parseFileOnEditorChange) {
+ } else if (editor.document.languageId !== "coq" || !this.config.config.parseFileOnEditorChange) {
return;
}
@@ -126,7 +127,7 @@ export class Coqpilot implements Disposable {
logger.info(`Theorems retrieved:\n${thrs}`);
- this.llmPrompt = new CoqPromptKShot(thrs, this.config.maxNumberOfTokens);
+ this.llmPrompt = new CoqPromptKShot(thrs, this.config.config.maxNumberOfTokens);
}
async initializeClient() {
@@ -139,10 +140,11 @@ export class Coqpilot implements Disposable {
await this.client.start();
this.context.subscriptions.push(this.proofView);
+ this.context.subscriptions.push(this.client);
}
private checkConditions(editor: TextEditor) {
- if (this.config.useGpt && this.config.openaiApiKey === "None") {
+ if (this.config.config.useGpt && this.config.config.openaiApiKey === "None") {
wm.showApiKeyNotProvidedMessage(); return false;
} else if (editor.document.languageId !== "coq") {
wm.showIncorrectFileFormatMessage(); return false;
@@ -153,13 +155,6 @@ export class Coqpilot implements Disposable {
return true;
}
- private reloadConfig() {
- this.config = CoqpilotConfig.create(
- workspace.getConfiguration('coqpilot')
- );
- CoqpilotConfig.checkRequirements(this.config);
- }
-
private async generateAtPoint(
editor: TextEditor,
position: Position
@@ -189,9 +184,9 @@ export class Coqpilot implements Disposable {
this.llmPrompt,
this.llm,
progressBar,
- this.config.logAttempts,
- this.config.proofAttemsPerOneTheorem,
- this.config.logFolderPath
+ this.config.config.logAttempts,
+ this.config.config.proofAttemsPerOneTheorem,
+ this.config.config.logFolderPath
);
const proof = await interactor.runProofGeneration(
thrName,
@@ -218,12 +213,8 @@ export class Coqpilot implements Disposable {
}
}
- async runProveAllAdmitted(editor: TextEditor) {
- await this.initHistory(editor);
- const admittedTheorems = this.llmPrompt?.admittedTheorems;
- const proofHoles = admittedTheorems.map((thr) => thr.proof.holes).flat();
- logger.info(`Proof holes: ${proofHoles.map((hole) => `${hole.range.start.line} ${hole.range.start.character}`).join(", ")}`);
- for (const hole of proofHoles) {
+ async proveHoles(editor: TextEditor, holes: ProofStep[]) {
+ for (const hole of holes) {
// Run proof generation at the start of the hole
const position = lspUtils.toVPosition(hole.range.start);
const proof = await this.generateAtPoint(editor, position);
@@ -248,16 +239,32 @@ export class Coqpilot implements Disposable {
}
}
- toggleLspClient() {
+ async runProveAllAdmitted(editor: TextEditor) {
+ await this.initHistory(editor);
+ const admittedTheorems = this.llmPrompt?.admittedTheorems;
+ const proofHoles = admittedTheorems.map((thr) => thr.proof.holes).flat();
+ await this.proveHoles(editor, proofHoles);
+ }
+
+ async runProveAdmittedInSelection(editor: TextEditor) {
+ await this.initHistory(editor);
+ const allTheorems = this.llmPrompt?.theoremsFromFile;
+ const proofHoles = allTheorems
+ .map((thr) => thr.proof.holes)
+ .flat()
+ .filter((hole) => editor.selection.contains(
+ utils.toVPosition(hole.range.start)
+ ));
+ await this.proveHoles(editor, proofHoles);
+ }
+
+ async toggleLspClient() {
logger.info("Toggle Extension");
if (this.client?.isRunning()) {
- this.client?.stop();
- this.client?.dispose();
- this.proofView?.dispose();
+ this.client?.dispose(2000)
+ .then(() => this.proofView?.dispose());
} else {
- this.client?.start();
- this.proofView = new ProofView(this.client, this.statusItem);
- this.context.subscriptions.push(this.proofView);
+ await this.initializeClient();
}
}
diff --git a/src/extension/config.ts b/src/extension/config.ts
index 8a65fdab..813c65a8 100644
--- a/src/extension/config.ts
+++ b/src/extension/config.ts
@@ -3,6 +3,8 @@ import { SingleTacticSolver } from '../coqLlmInteraction/singleTacticSolver';
import { LLMAdapter } from '../coqLlmInteraction/llmAdapter';
import { MockLlmPrompt } from '../test/mock/mockllm';
import { LLMInterface } from '../coqLlmInteraction/llmInterface';
+import * as vscode from 'vscode';
+import logger from "./logger";
export interface CoqpilotConfig {
openaiApiKey: string;
@@ -18,7 +20,39 @@ export interface CoqpilotConfig {
extraCommandsList: string[];
}
+export class CoqpilotConfigWrapper {
+ private _config: CoqpilotConfig;
+ private autoUpdate: boolean;
+
+ get config(): CoqpilotConfig {
+ if (!this.autoUpdate) {
+ return this._config;
+ }
+
+ this._config = CoqpilotConfig.create(
+ vscode.workspace.getConfiguration('coqpilot')
+ );
+ CoqpilotConfig.checkRequirements(this._config);
+ logger.info("Successfully updated config: " + JSON.stringify(this._config));
+
+ return this._config;
+ }
+
+ constructor(conf: CoqpilotConfig | undefined = undefined, autoUpdate: boolean = true) {
+ this._config = conf ?? CoqpilotConfig.create(
+ vscode.workspace.getConfiguration('coqpilot')
+ )!;
+ this.autoUpdate = autoUpdate;
+ CoqpilotConfig.checkRequirements(this._config);
+ logger.info("Successfully created config.");
+ }
+}
+
export namespace CoqpilotConfig {
+ export function getNew() {
+ return new CoqpilotConfigWrapper();
+ }
+
export function create(
wsConfig: any
): CoqpilotConfig | undefined {
@@ -34,7 +68,7 @@ export namespace CoqpilotConfig {
parseFileOnInit: wsConfig.parseFileOnInit,
coqLspPath: wsConfig.coqLspPath,
useGpt: wsConfig.useGpt,
- extraCommandsList: wsConfig.extraCommandsList
+ extraCommandsList: preprocessExtraCommands(wsConfig.extraCommandsList)
};
} catch (error) {
console.error(error);
@@ -42,6 +76,17 @@ export namespace CoqpilotConfig {
}
}
+ function preprocessExtraCommands(commands: string[]): string[] {
+ // If the command does not end with a dot, add it
+ return commands.map((command) => {
+ if (command.endsWith(".")) {
+ return command;
+ } else {
+ return command + ".";
+ }
+ });
+ }
+
export function checkRequirements(config: CoqpilotConfig): void {
const nullableParams = [
"logFolderPath"
@@ -53,20 +98,21 @@ export namespace CoqpilotConfig {
}
}
- export function getLlm(config: CoqpilotConfig): LLMInterface {
+ export function getLlm(configWrapped: CoqpilotConfigWrapper): LLMInterface {
+ const config = configWrapped.config;
if (config.gptModel === OtherModels.MOCK) {
return new MockLlmPrompt();
} else {
let gptModel: LLMInterface | null = null;
if (config.useGpt) {
if (Object.values(GptModel).map(v => v.toString()).includes(config.gptModel)) {
- gptModel = new GPT35(config.openaiApiKey, 3, config.gptModel);
+ gptModel = new GPT35(configWrapped, 3);
} else {
throw new Error(`Unknown model ${config.gptModel}`);
}
}
- const simplestModel = new SingleTacticSolver(config.extraCommandsList);
+ const simplestModel = new SingleTacticSolver(configWrapped);
const allModels = [
gptModel, simplestModel
diff --git a/src/test/coqLlmInteractionTests/lspClient.test.ts b/src/test/coqLlmInteractionTests/lspClient.test.ts
index 53991233..3d2e0573 100644
--- a/src/test/coqLlmInteractionTests/lspClient.test.ts
+++ b/src/test/coqLlmInteractionTests/lspClient.test.ts
@@ -2,14 +2,17 @@ import { CoqLspClient } from '../../coqLspClient/coqLspClient';
import { StatusBarButton, StatusBarState } from '../../editor/enableButton';
import { workspace } from 'vscode';
import * as assert from 'assert';
-import { CoqpilotConfig } from "../../extension/config";
+import { CoqpilotConfig, CoqpilotConfigWrapper } from "../../extension/config";
import { updateCoqpilotConfig } from "../common";
suite('CoqLspClient tests', () => {
test('coq-lsp correctly modifying ui', async () => {
const statusItem = new StatusBarButton();
const wsConfig = workspace.getConfiguration("coqpilot");
- const extensionConfig = updateCoqpilotConfig(CoqpilotConfig.create(wsConfig));
+ const extensionConfig = new CoqpilotConfigWrapper(
+ updateCoqpilotConfig(CoqpilotConfig.create(wsConfig)), false
+ );
+ console.log("EXTCONFIG", extensionConfig);
const client = new CoqLspClient(statusItem, wsConfig, extensionConfig);
assert.strictEqual(statusItem.runStatus, StatusBarState.Activating);
diff --git a/src/test/coqLlmInteractionTests/proofView.test.ts b/src/test/coqLlmInteractionTests/proofView.test.ts
index c11e8fe1..b752d03d 100644
--- a/src/test/coqLlmInteractionTests/proofView.test.ts
+++ b/src/test/coqLlmInteractionTests/proofView.test.ts
@@ -26,13 +26,15 @@ import * as path from 'path';
import * as assert from 'assert';
import { makeAuxfname } from '../../coqLspClient/utils';
import * as common from '../common';
-import { CoqpilotConfig } from "../../extension/config";
+import { CoqpilotConfig, CoqpilotConfigWrapper } from "../../extension/config";
suite('ProofView auxTheorem tests', () => {
const statusItem = new StatusBarButton();
const wsConfig = workspace.getConfiguration("coqpilot");
const dirname = path.dirname(path.dirname(path.dirname(__dirname)));
- const extensionConfig = common.updateCoqpilotConfig(CoqpilotConfig.create(wsConfig));
+ const extensionConfig = new CoqpilotConfigWrapper(
+ common.updateCoqpilotConfig(CoqpilotConfig.create(wsConfig)), false
+ );
interface TestData {
fileRoot: string,
@@ -119,7 +121,9 @@ suite('ProofView checkTheorems tests', () => {
const statusItem = new StatusBarButton();
const wsConfig = workspace.getConfiguration("coqpilot");
const dirname = path.dirname(path.dirname(path.dirname(__dirname)));
- const extensionConfig = common.updateCoqpilotConfig(CoqpilotConfig.create(wsConfig));
+ const extensionConfig = new CoqpilotConfigWrapper(
+ common.updateCoqpilotConfig(CoqpilotConfig.create(wsConfig)), false
+ );
interface TestData {
context: string,
@@ -204,7 +208,9 @@ suite('ProofView parseFile tests', () => {
const statusItem = new StatusBarButton();
const wsConfig = workspace.getConfiguration("coqpilot");
const dirname = path.dirname(path.dirname(path.dirname(__dirname)));
- const extensionConfig = common.updateCoqpilotConfig(CoqpilotConfig.create(wsConfig));
+ const extensionConfig = new CoqpilotConfigWrapper(
+ common.updateCoqpilotConfig(CoqpilotConfig.create(wsConfig)), false
+ );
interface TheoremData {
statementRange: Range,
diff --git a/src/test/coqLlmInteractionTests/simpleSolver.test.ts b/src/test/coqLlmInteractionTests/simpleSolver.test.ts
index f262277e..45ac6d8f 100644
--- a/src/test/coqLlmInteractionTests/simpleSolver.test.ts
+++ b/src/test/coqLlmInteractionTests/simpleSolver.test.ts
@@ -16,7 +16,7 @@ suite('Simple single-tactic solver tests', () => {
test('Check prove using simple single-tactic prover', async () => {
const { filePath, tacticsToTry, solvedAmount } = {
filePath: path.join(dirname, 'src', 'test', 'resources', 'with_admits_test.v'),
- tacticsToTry: ['auto.'],
+ tacticsToTry: ['auto'],
solvedAmount: 6,
};