Merge pull request #1240 from rocq-prover/resilient-init

2.4.3 with resilient init

Author: gares

client/package.json

@@ -4,7 +4,7 @@
   "description": "VsRocq is an extension for Visual Studio Code with support for the Rocq Prover",
   "publisher": "rocq-prover",
   "license": "MIT",
-  "version": "2.4.2",
+  "version": "2.4.3",
   "repository": {
     "type": "git",
     "url": "https://github.com/rocq-prover/vsrocq.git"

client/src/utilities/toolchain.ts

@@ -105,32 +105,44 @@ export default class VsRocqToolchainManager implements Disposable {
         const config = workspace.getConfiguration('vsrocq').get('args') as string[];
         const options = ["-without-project-file", "-where"].concat(config);
         const cmd = [this._vsrocqtopPath].concat(options).join(' ');
+        // fallback for < 2.4.0
+        const pre240options = ["-where"].concat(config);
+        const pre240cmd = [this._vsrocqtopPath].concat(pre240options).join(' ');
 
         return new Promise((resolve, reject: ((reason: ToolchainError) => void)) => {
-            exec(cmd, {cwd: workspace.rootPath}, (error, stdout, stderr) => {
 
+            const onSuccess = (stdout: string) => {
+                this._rocqPath = stdout;
+                this.rocqVersion().then(
+                    () => resolve(),
+                    (err) => reject({
+                        status: ToolChainErrorCode.launchError,
+                        message: `${this._vsrocqtopPath} crashed with the following message: ${err}.
+                        This could be due to a bad Rocq installation or an incompatible Rocq version`
+                    })
+                );
+            };
+
+            const onError = (stderr: string) => {
+                reject({
+                    status: ToolChainErrorCode.launchError,
+                    message: `${this._vsrocqtopPath} crashed with the following message: ${stderr}
+                    This could be due to a bad Rocq installation or an incompatible Rocq version.`
+                });
+            };
+
+            exec(cmd, {cwd: workspace.rootPath}, (error, stdout, stderr1) => {
                 if(error) {
-                    reject({
-                        status: ToolChainErrorCode.launchError, 
-                        message: `${this._vsrocqtopPath} crashed with the following message: ${stderr}
-                        This could be due to a bad Rocq installation or an incompatible Rocq version.`
+                    exec(pre240cmd, {cwd: workspace.rootPath}, (error, stdout, stderr2) => {
+                        if(error) {
+                            onError(`${cmd}\n${stderr1}\n\n${pre240cmd}\n${stderr2}\n`);
+                        } else {
+                            onSuccess(stdout);
+                        }
                     });
                 } else {
-                    this._rocqPath = stdout;
-                    this.rocqVersion().then(
-                        () => {
-                            resolve();
-                        },
-                        (err) => {
-                            reject({
-                                status: ToolChainErrorCode.launchError,
-                                message: `${this._vsrocqtopPath} crashed with the following message: ${err}.
-                                This could be due to a bad Rocq installation or an incompatible Rocq version`
-                            });
-                        }
-                    );
+                    onSuccess(stdout);
                 }
-                
             });
         });
     };

client/src/utilities/versioning.ts

@@ -57,7 +57,8 @@ const versionRequirements : VersionReq = {
     '2.3.4': '2.3.3',
     '2.4.0': '2.4.0',
     '2.4.1': '2.4.0',
-    '2.4.2': '2.4.0'
+    '2.4.2': '2.4.0',
+    '2.4.3': '2.3.3'
 };
 
 //We will add version ranges as we start releasing

flake.nix

@@ -23,7 +23,7 @@
       vscodeExtPublisher = "rocq-prover";
       vscodeExtName = "vsrocq";
       vscodeExtUniqueId = "rocq-prover.vsrocq";
-      vsrocq_version = "2.4.2";
+      vsrocq_version = "2.4.3";
       rocq = (import nixpkgs {inherit system;}).rocq-core.override { version = rocq-master.outPath; };
     in rec {
       formatter = nixpkgs.legacyPackages.${system}.alejandra;

language-server/vsrocqtop/lspManager.ml

@@ -46,7 +46,7 @@ let conf_request_id = max_int
 
 let server_info = InitializeResult.create_serverInfo
   ~name:"vsrocq-language-server"
-  ~version:"2.4.2"
+  ~version:"2.4.3"
   ()
 
 type lsp_event =