Figure out how to properly use nix-env + minors

.gitignore

@@ -15,4 +15,8 @@ src/test/resources/coqProj/.vscode
 **/*.aux
 src/test/resources/coqProj/.Makefile.coq.d
 src/test/resources/coqProj/Makefile.coq
-src/test/resources/coqProj/Makefile.coq.conf
+src/test/resources/coqProj/Makefile.coq.conf
+
+# Ignore the generated build files in datatests inside benchmarks
+src/test/benchmark/dataset/**/result
+src/test/benchmark/dataset/**/.vscode/

.gitmodules

@@ -0,0 +1,5 @@
+[submodule "src/test/benchmark/dataset/imm"]
+	path = src/test/benchmark/dataset/imm
+	url = https://github.com/weakmemory/imm.git
+	brach = coq819
+	ignore = dirty

.vscodeignore

@@ -9,4 +9,5 @@ vsc-extension-quickstart.md
 **/*.map
 **/*.ts
 logs/**
-_opam/**
+_opam/**
+./out/test/**

README.md

@@ -119,6 +119,37 @@ Each of these settings are modified in `settings.json` and contain an array of m
 
 - Add benchmarking options for various models: soon. 
 
+## Benchmark
+
+To run benchmarks on some project, apart from installing and building CoqPilot manually as described above, you will need to download the necessary projects that are used as datasets for the benchmarks. These projects are added as submodules to the repository. To download them, run the following commands:
+```bash
+git submodule init
+git submodule update
+```
+After that, you need to build the projects. And be careful, the actively maintained way to build this projects is `nix`. Moreover, when adding your own projects, make sure that they are built using `coq-8.19.0`. 
+
+First things first, the process of running the benchmark is not perfectly automated yet. We are working on it. For now, one project (one unit containing nix environment) shall be ran at a time. Let's say you are going to run the benchmark on the `imm` project. You will have to do the following: 
+
+1. Install nix, as specified in the [here](https://nixos.org/download.html). 
+
+2. Install needed caches: 
+    ```bash
+    nix-env -iA nixpkgs.cachix && cachix use coq && cachix use coq-community && cachix use math-comp
+    cachix use weakmemory
+    ```
+
+3. Go to the `imm` subdirectory, apply the nix environment (without it the project will NOT build) and build the project: 
+    ```bash
+    cd src/test/benchmark/dataset/imm 
+    nix-shell 
+    nix-build
+    ```
+4. Return to the project root not exiting the nix-shell. Run the benchmark: 
+    ```bash
+    cd ../../../../..
+    npm run benchmark
+    ```    
+
 ## Release Notes
 
 Release notes could be found in the [CHANGELOG.md](https://github.com/JetBrains-Research/coqpilot/blob/refactor/CHANGELOG.md) file.

src/coqLsp/coqLspConnector.ts

@@ -2,6 +2,7 @@ import { Uri } from "vscode";
 import {
     LanguageClientOptions,
     RevealOutputChannelOn,
+    Trace,
 } from "vscode-languageclient";
 import { LanguageClient, ServerOptions } from "vscode-languageclient/node";
 
@@ -58,6 +59,7 @@ export class CoqLspConnector extends LanguageClient {
     }
 
     override async start(): Promise<void> {
+        super.setTrace(Trace.Verbose);
         await super
             .start()
             .then(this.logStatusUpdate.bind(this, "started"))

src/logging/outputChannelEmulator.ts

@@ -0,0 +1,49 @@
+import { appendFileSync, existsSync, writeFileSync } from "fs";
+import { OutputChannel, ViewColumn } from "vscode";
+
+export class OutputChannelEmulator implements OutputChannel {
+    name: string;
+
+    constructor(
+        private logFilePath: string,
+        name: string = "OutputChannelEmulator"
+    ) {
+        this.name = name;
+        if (!existsSync(this.logFilePath)) {
+            writeFileSync(this.logFilePath, "");
+        }
+    }
+
+    append(value: string): void {
+        appendFileSync(this.logFilePath, value);
+    }
+
+    appendLine(value: string): void {
+        appendFileSync(this.logFilePath, value + "\n");
+    }
+
+    replace(value: string): void {
+        writeFileSync(this.logFilePath, value);
+    }
+
+    clear(): void {
+        writeFileSync(this.logFilePath, "");
+    }
+
+    show(preserveFocus?: boolean | undefined): void;
+
+    show(
+        column?: ViewColumn | undefined,
+        preserveFocus?: boolean | undefined
+    ): void;
+
+    show(_column?: unknown, _preserveFocus?: unknown): void {
+        throw new Error("Method not implemented.");
+    }
+
+    hide(): void {
+        throw new Error("Method not implemented.");
+    }
+
+    dispose(): void {}
+}

src/test/benchmark/runBenchmark.test.ts

@@ -43,7 +43,19 @@ const mixedAutoBenchmark: Benchmark = {
     timeoutMinutes: 1,
 };
 
-const benchmarks: Benchmark[] = [simpleAutoBenchmark, mixedAutoBenchmark];
+const immBenchmark: Benchmark = {
+    name: "Complete imm with auto",
+    items: [new DatasetItem("imm/src/basic/Events.v", "imm")],
+    modelsParams: onlyAutoModelsParams,
+    requireAllAdmitsCompleted: false,
+    timeoutMinutes: 60,
+};
+
+const benchmarks: Benchmark[] = [
+    simpleAutoBenchmark,
+    mixedAutoBenchmark,
+    immBenchmark,
+];
 
 suite("Benchmark", () => {
     const benchmarkDir = getBenchmarkDir();