Support DeepSeek in benchmarks and plugin

package.json

@@ -119,7 +119,7 @@
                 },
                 "temperature": {
                   "type": "number",
-                  "description": "Temperature of the OpenAI model.",
+                  "description": "Temperature of the OpenAI model. Should be in range [0, 2], otherwise an error will be produced.",
                   "default": 1
                 },
                 "apiKey": {
@@ -306,7 +306,7 @@
                 },
                 "temperature": {
                   "type": "number",
-                  "description": "Temperature of the LM Studio model.",
+                  "description": "Temperature of the LM Studio model. Should be in range [0, 2], otherwise an error will be produced.",
                   "default": 1
                 },
                 "port": {
@@ -376,6 +376,93 @@
             "markdownDescription": "List of configurations that fetch completions from a locally running LLM inside [LM Studio](https://lmstudio.ai).",
             "order": 3
           },
+          "coqpilot.deepSeekModelsParameters": {
+            "type": "array",
+            "items": {
+              "type": "object",
+              "properties": {
+                "modelId": {
+                  "type": "string",
+                  "markdownDescription": "Unique identifier of this model to distinguish it from others. Could be any string.",
+                  "default": "deep-seek-v3"
+                },
+                "modelName": {
+                  "type": "string",
+                  "markdownDescription": "Model to use from the DeepSeek public API. List of models known to CoqPilot: \n * deepseek-chat \n * deepseek-reasoner",
+                  "default": "deepseek-chat"
+                },
+                "temperature": {
+                  "type": "number",
+                  "description": "Temperature of the DeepSeek model. Should be in range [0, 2], otherwise an error will be produced.",
+                  "default": 1
+                },
+                "apiKey": {
+                  "type": "string",
+                  "description": "Api key to communicate with the DeepSeek api. You can get one [here](https://platform.deepseek.com/api_keys).",
+                  "default": "None"
+                },
+                "choices": {
+                  "type": "number",
+                  "description": "Number of attempts to generate proof for one hole with this model. All attempts are made as a single request, so this parameter should not have a significant impact on performance. However, more choices mean more tokens spent on generation.",
+                  "default": 15
+                },
+                "systemPrompt": {
+                  "type": "string",
+                  "description": "Prompt for the DeepSeek model to begin a chat with. It is sent as a system message, which means it has more impact than other messages.",
+                  "default": "Generate proof of the theorem from user input in Coq. You should only generate proofs in Coq. Never add special comments to the proof. Your answer should be a valid Coq proof. It should start with 'Proof.' and end with 'Qed.'."
+                },
+                "maxTokensToGenerate": {
+                  "type": "number",
+                  "description": "Number of tokens that the model is allowed to generate as a response message (i.e. message with proof).",
+                  "default": 2048
+                },
+                "tokensLimit": {
+                  "type": "number",
+                  "description": "Total length of input and generated tokens, it is determined by the model.",
+                  "default": 4096
+                },
+                "maxContextTheoremsNumber": {
+                  "type": "number",
+                  "description": "Maximum number of context theorems to include in the prompt sent to the DeepSeek model as examples for proof generation. Lower values reduce token usage but may decrease the likelihood of generating correct proofs.",
+                  "default": 100
+                },
+                "multiroundProfile": {
+                  "type": "object",
+                  "properties": {
+                    "maxRoundsNumber": {
+                      "type": "number",
+                      "description": "Maximum number of rounds to generate and further fix the proof. Default value is 1, which means each proof will be only generated, but not fixed.",
+                      "default": 1
+                    },
+                    "proofFixChoices": {
+                      "type": "number",
+                      "description": "Number of attempts to generate a proof fix for each proof in one round. Warning: increasing `proofFixChoices` can lead to exponential growth in generation requests if `maxRoundsNumber` is relatively large.",
+                      "default": 1
+                    },
+                    "proofFixPrompt": {
+                      "type": "string",
+                      "description": "Prompt for the proof-fix request that will be sent as a user chat message in response to an incorrect proof. It may include the `${diagnostic}` substring, which will be replaced by the actual compiler diagnostic.",
+                      "default": "Unfortunately, the last proof is not correct. Here is the compiler's feedback: `${diagnostic}`. Please, fix the proof."
+                    },
+                    "maxPreviousProofVersionsNumber": {
+                      "type": "number",
+                      "description": "Maximum number of previous proof versions to include in the proof-fix chat, each presented as a dialogue: the user's diagnostic followed by the assistant's corresponding proof attempt. The most recent proof version being fixed is always included and is not affected by this parameter.",
+                      "default": 100
+                    }
+                  },
+                  "default": {
+                    "maxRoundsNumber": 1,
+                    "proofFixChoices": 1,
+                    "proofFixPrompt": "Unfortunately, the last proof is not correct. Here is the compiler's feedback: `${diagnostic}`. Please, fix the proof.",
+                    "maxPreviousProofVersionsNumber": 100
+                  }
+                }
+              }
+            },
+            "default": [],
+            "markdownDescription": "List of configurations for DeepSeek models. Each configuration will be fetched for completions independently in the order they are listed.",
+            "order": 4
+          },
           "coqpilot.contextTheoremsRankerType": {
             "type": "string",
             "enum": [
@@ -390,7 +477,7 @@
             ],
             "description": "Context of the LLM is limited. Usually not all theorems from the file may be used in the completion request. This parameter defines the way theorems are selected for the completion.",
             "default": "distance",
-            "order": 4
+            "order": 5
           },
           "coqpilot.loggingVerbosity": {
             "type": "string",
@@ -404,13 +491,13 @@
             ],
             "description": "The verbosity of the logs.",
             "default": "info",
-            "order": 5
+            "order": 6
           },
           "coqpilot.coqLspServerPath": {
             "type": "string",
             "description": "Path to the Coq LSP server. If not specified, CoqPilot will try to find the server automatically at the default location: coq-lsp at PATH.",
             "default": "coq-lsp",
-            "order": 6
+            "order": 7
           }
         }
       }

src/benchmark/framework/experiment/setupDSL/benchmarkingBundleBuilder.ts

@@ -10,7 +10,8 @@ export type LLMServiceStringIdentifier =
     | "predefined"
     | "openai"
     | "grazie"
-    | "lmstudio";
+    | "lmstudio"
+    | "deepseek";
 
 export type CorrespondingInputParams<T extends LLMServiceStringIdentifier> =
     T extends "predefined"
@@ -21,7 +22,9 @@ export type CorrespondingInputParams<T extends LLMServiceStringIdentifier> =
             ? InputBenchmarkingModelParams.GrazieParams
             : T extends "lmstudio"
               ? InputBenchmarkingModelParams.LMStudioParams
-              : never;
+              : T extends "deepseek"
+                ? InputBenchmarkingModelParams.DeepSeekParams
+                : never;
 
 export class BenchmarkingBundle {
     constructor() {}
@@ -46,6 +49,8 @@ export class BenchmarkingBundle {
                 return LLMServiceIdentifier.GRAZIE;
             case "lmstudio":
                 return LLMServiceIdentifier.LMSTUDIO;
+            case "deepseek":
+                return LLMServiceIdentifier.DEEPSEEK;
         }
     }
 }

src/benchmark/framework/structures/common/llmServiceIdentifier.ts

@@ -3,4 +3,5 @@ export enum LLMServiceIdentifier {
     OPENAI = "Open AI",
     GRAZIE = "Grazie",
     LMSTUDIO = "LM Studio",
+    DEEPSEEK = "DeepSeek",
 }

src/benchmark/framework/structures/inputParameters/inputBenchmarkingModelParams.ts

@@ -1,4 +1,5 @@
 import {
+    DeepSeekUserModelParams,
     GrazieUserModelParams,
     LMStudioUserModelParams,
     OpenAiUserModelParams,
@@ -22,4 +23,6 @@ export namespace InputBenchmarkingModelParams {
     export interface GrazieParams extends GrazieUserModelParams, Params {}
 
     export interface LMStudioParams extends LMStudioUserModelParams, Params {}
+
+    export interface DeepSeekParams extends DeepSeekUserModelParams, Params {}
 }

src/benchmark/framework/utils/commonStructuresUtils/llmServicesUtils.ts

@@ -1,4 +1,6 @@
 import { ErrorsHandlingMode } from "../../../../llm/llmServices/commonStructures/errorsHandlingMode";
+import { DeepSeekModelParamsResolver } from "../../../../llm/llmServices/deepSeek/deepSeekModelParamsResolver";
+import { DeepSeekService } from "../../../../llm/llmServices/deepSeek/deepSeekService";
 import { GrazieModelParamsResolver } from "../../../../llm/llmServices/grazie/grazieModelParamsResolver";
 import { GrazieService } from "../../../../llm/llmServices/grazie/grazieService";
 import { LLMService } from "../../../../llm/llmServices/llmService";
@@ -29,6 +31,8 @@ export function getShortName(identifier: LLMServiceIdentifier): string {
             return "Grazie";
         case LLMServiceIdentifier.LMSTUDIO:
             return "LM Studio";
+        case LLMServiceIdentifier.DEEPSEEK:
+            return "DeepSeek";
     }
 }
 
@@ -53,6 +57,9 @@ export function selectLLMServiceBuilder(
         case LLMServiceIdentifier.LMSTUDIO:
             return (eventLogger, errorsHandlingMode) =>
                 new LMStudioService(eventLogger, errorsHandlingMode);
+        case LLMServiceIdentifier.DEEPSEEK:
+            return (eventLogger, errorsHandlingMode) =>
+                new DeepSeekService(eventLogger, errorsHandlingMode);
     }
 }
 
@@ -61,6 +68,7 @@ export interface LLMServicesParamsResolvers {
     openAiModelParamsResolver: OpenAiModelParamsResolver;
     grazieModelParamsResolver: GrazieModelParamsResolver;
     lmStudioModelParamsResolver: LMStudioModelParamsResolver;
+    deepSeekModelParamsResolver: DeepSeekModelParamsResolver;
 }
 
 export function createParamsResolvers(): LLMServicesParamsResolvers {
@@ -70,6 +78,7 @@ export function createParamsResolvers(): LLMServicesParamsResolvers {
         openAiModelParamsResolver: new OpenAiModelParamsResolver(),
         grazieModelParamsResolver: new GrazieModelParamsResolver(),
         lmStudioModelParamsResolver: new LMStudioModelParamsResolver(),
+        deepSeekModelParamsResolver: new DeepSeekModelParamsResolver(),
     };
 }
 
@@ -86,5 +95,7 @@ export function getParamsResolver(
             return paramsResolvers.grazieModelParamsResolver;
         case LLMServiceIdentifier.LMSTUDIO:
             return paramsResolvers.lmStudioModelParamsResolver;
+        case LLMServiceIdentifier.DEEPSEEK:
+            return paramsResolvers.deepSeekModelParamsResolver;
     }
 }

src/extension/pluginContext.ts

@@ -5,6 +5,7 @@ import { Disposable, WorkspaceConfiguration, window, workspace } from "vscode";
 
 import { LLMServices, disposeServices } from "../llm/llmServices";
 import { ErrorsHandlingMode } from "../llm/llmServices/commonStructures/errorsHandlingMode";
+import { DeepSeekService } from "../llm/llmServices/deepSeek/deepSeekService";
 import { GrazieService } from "../llm/llmServices/grazie/grazieService";
 import { LMStudioService } from "../llm/llmServices/lmStudio/lmStudioService";
 import { OpenAiService } from "../llm/llmServices/openai/openAiService";
@@ -67,6 +68,12 @@ export class PluginContext implements Disposable {
             path.join(this.llmServicesLogsDir, "lmstudio-logs.txt"),
             this.llmServicesSetup.debugLogs
         ),
+        deepSeekService: new DeepSeekService(
+            this.llmServicesSetup.eventLogger,
+            this.llmServicesSetup.errorsHandlingMode,
+            path.join(this.llmServicesLogsDir, "deepseek-logs.txt"),
+            this.llmServicesSetup.debugLogs
+        ),
     };
 
     private parseLoggingVerbosity(config: WorkspaceConfiguration): Severity {

src/extension/settings/configReaders.ts

@@ -6,11 +6,13 @@ import { LLMService } from "../../llm/llmServices/llmService";
 import { ModelParams, ModelsParams } from "../../llm/llmServices/modelParams";
 import { SingleParamResolutionResult } from "../../llm/llmServices/utils/paramsResolvers/abstractResolvers";
 import {
+    DeepSeekUserModelParams,
     GrazieUserModelParams,
     LMStudioUserModelParams,
     OpenAiUserModelParams,
     PredefinedProofsUserModelParams,
     UserModelParams,
+    deepSeekUserModelParamsSchema,
     grazieUserModelParamsSchema,
     lmStudioUserModelParamsSchema,
     openAiUserModelParamsSchema,
@@ -108,14 +110,27 @@ export function readAndValidateUserModelsParams(
                 jsonSchemaValidator
             )
         );
+    const deepSeekUserParams: DeepSeekUserModelParams[] =
+        config.deepSeekModelsParameters.map((params: any) =>
+            validateAndParseJson(
+                params,
+                deepSeekUserModelParamsSchema,
+                jsonSchemaValidator
+            )
+        );
 
     validateIdsAreUnique([
         ...predefinedProofsUserParams,
         ...openAiUserParams,
         ...grazieUserParams,
         ...lmStudioUserParams,
+        ...deepSeekUserParams,
     ]);
-    validateApiKeysAreProvided(openAiUserParams, grazieUserParams);
+    validateApiKeysAreProvided(
+        openAiUserParams,
+        grazieUserParams,
+        deepSeekUserParams
+    );
 
     const modelsParams: ModelsParams = {
         predefinedProofsModelParams: resolveParamsAndShowResolutionLogs(
@@ -134,6 +149,10 @@ export function readAndValidateUserModelsParams(
             llmServices.lmStudioService,
             lmStudioUserParams
         ),
+        deepSeekParams: resolveParamsAndShowResolutionLogs(
+            llmServices.deepSeekService,
+            deepSeekUserParams
+        ),
     };
 
     validateModelsArePresent([
@@ -198,7 +217,8 @@ function validateIdsAreUnique(allModels: UserModelParams[]) {
 
 function validateApiKeysAreProvided(
     openAiUserParams: OpenAiUserModelParams[],
-    grazieUserParams: GrazieUserModelParams[]
+    grazieUserParams: GrazieUserModelParams[],
+    deepSeekUserParams: DeepSeekUserModelParams[]
 ) {
     const buildApiKeyError = (
         serviceName: string,
@@ -218,6 +238,9 @@ function validateApiKeysAreProvided(
     if (grazieUserParams.some((params) => params.apiKey === "None")) {
         throw buildApiKeyError("Grazie", "grazie");
     }
+    if (deepSeekUserParams.some((params) => params.apiKey === "None")) {
+        throw buildApiKeyError("Deep Seek", "deepSeek");
+    }
 }
 
 function validateModelsArePresent<T>(allModels: T[]) {

src/extension/settings/settingsValidationError.ts

@@ -34,7 +34,8 @@ export function toSettingName(llmService: LLMService<any, any>): string {
         () => "predefinedProofs",
         () => "openAi",
         () => "grazie",
-        () => "lmStudio"
+        () => "lmStudio",
+        () => "deepSeek"
     );
     return `${pluginId}.${serviceNameInSettings}ModelsParameters`;
 }

src/llm/llmIterator.ts

@@ -36,6 +36,7 @@ export class LLMSequentialIterator
         );
     }
 
+    // TODO: Implement a smarter way of ordering the services
     private createHooks(
         proofGenerationContext: ProofGenerationContext,
         modelsParams: ModelsParams,
@@ -48,6 +49,16 @@ export class LLMSequentialIterator
                 services.predefinedProofsService,
                 "predefined-proofs"
             ),
+            // Here DeepSeek service is reordered to the beginning
+            // of the list, due to it's strong performance and
+            // low costs. Refer to discussion:
+            // https://github.com/JetBrains-Research/coqpilot/pull/56#discussion_r1935180516
+            ...this.createLLMServiceHooks(
+                proofGenerationContext,
+                modelsParams.deepSeekParams,
+                services.deepSeekService,
+                "deepseek"
+            ),
             ...this.createLLMServiceHooks(
                 proofGenerationContext,
                 modelsParams.openAiParams,