Use dune coq top when enabled by a setting.

- Add `coqtop.useDune` and dune path to settings.
- spawnCoqTop: use dune coq top
- Skip `_CoqProject` when `useDune` is set.

README.md

@@ -74,6 +74,7 @@ The recommended way to install VsCoq is via the [Visual Studio Marketplace](http
 * `"coqtop.args": []` -- an array of strings specifying additional command line arguments for coqtop
 * `"coqtop.loadCoqProject": true` -- set to `false` to ignore <span>_CoqProject</span>
 * `"coqtop.coqProjectRoot": "."` -- where to expect the <span>_CoqProject</span> relative to the workspace root
+* `"coqtop.useDune": false` -- set to `true` to use `dune coq top` instead of parsing settings from `_CoqProject`.
 
 ## Install a local version
 

package.json

@@ -60,6 +60,11 @@
       "type": "object",
       "title": "Coq configuration",
       "properties": {
+        "coqtop.dunePath": {
+          "type": "string",
+          "default": "dune",
+          "markdownDescription": "Full path to dune binary (`dune` included)."
+        },
         "coqtop.binPath": {
           "type": "string",
           "default": "",
@@ -89,6 +94,10 @@
           "default": "open-script",
           "markdownDescription": "When to start an instance of coqtop: when a Coq script is opened (`open-script`) or else when the user begins interaction (`interaction`; default)."
         },
+        "coqtop.useDune": {
+          "type": "boolean",
+          "markdownDescription": "(Experimental) Use `dune coq top` to run ."
+        },
         "coq.loadCoqProject": {
           "type": "boolean",
           "default": true,

server/src/CoqProject.ts

@@ -86,7 +86,8 @@ export class CoqProject {
       this.coqProjectRoot = newSettings.coq.coqProjectRoot;
       this.console.log("Updated project root to " + this.getCoqProjectRoot());
     }
-    if(newSettings.coq.loadCoqProject ) {
+    if(newSettings.coq.loadCoqProject && !newSettings.coqtop.useDune) {
+      // ^^ CoqProject settings aren't needed when using dune
       this.watchCoqProject();
       await this.loadCoqProject();
     } else {

server/src/coqtop/CoqTop8.ts

@@ -223,13 +223,14 @@ export class CoqTop extends IdeSlave8 implements coqtop.CoqTop {
   private spawnCoqTop(mainAddr : string, controlAddr: string) {
     var topfile : string[] = [];
     var scriptPath = this.scriptPath;
-    if (semver.satisfies(this.coqtopVersion, ">= 8.10") && scriptPath !== undefined) {
+    if (semver.satisfies(this.coqtopVersion, ">= 8.10") && !this.settings.useDune && scriptPath != undefined) {
+      // Dune computes this internally, so we skip it.
       topfile = ['-topfile', scriptPath];
     }
     if (semver.satisfies(this.coqtopVersion, ">= 8.9")) {
       var coqtopModule = this.coqidetopBin;
       // var coqtopModule = 'cmd';
-      var args = [
+      var coqArgs = [
         // '/D /C', this.coqPath + '/coqtop.exe',
         '-main-channel', mainAddr,
         '-control-channel', controlAddr,
@@ -238,16 +239,27 @@ export class CoqTop extends IdeSlave8 implements coqtop.CoqTop {
     } else {
       var coqtopModule = this.coqtopBin;
       // var coqtopModule = 'cmd';
-      var args = [
+      var coqArgs = [
         // '/D /C', this.coqPath + '/coqtop.exe',
         '-main-channel', mainAddr,
         '-control-channel', controlAddr,
         '-ideslave',
         '-async-proofs', 'on'
         ].concat(this.settings.args);
     }
-    this.console.log('exec: ' + coqtopModule + ' ' + args.join(' '));
-    return spawn(coqtopModule, args, {detached: false, cwd: this.projectRoot});
+    if (this.settings.useDune) {
+      var binary = this.settings.dunePath
+      if (scriptPath === undefined)
+        throw new CoqtopSpawnError("", "File was not saved to local file system");
+      var args = ["coq", "top", "--toplevel=" + coqtopModule,
+        scriptPath, "--"].concat(coqArgs);
+    } else {
+      var binary = coqtopModule
+      var args = coqArgs
+    }
+
+    this.console.log('exec: ' + binary + ' ' + args.join(' '));
+    return spawn(binary, args, { detached: false, cwd: this.projectRoot });
   }
 
   public /* override */ async coqInterrupt() : Promise<boolean> {

server/src/protocol.ts

@@ -41,6 +41,8 @@ export interface CoqTopSettings {
   args: string[];
   /** When should an instance of coqtop be started for a Coq script */
   startOn: "open-script" | "interaction",
+  useDune: boolean;
+  dunePath: string;
 }
 
 export interface AutoFormattingSettings {

server/test/coqtop.8.7.ts

@@ -45,6 +45,8 @@ describe("Coqtop 8.6", function() {
     coqidetopExe: "coqidetop.opt",
     args: [],
     startOn: "open-script",
+    dunePath: "",
+    useDune: false
   }
 
   let dummyConsole: RemoteConsole = {