diff --git a/README.md b/README.md
index 5056db344..a9380c49e 100644
--- a/README.md
+++ b/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 _CoqProject
* `"coqtop.coqProjectRoot": "."` -- where to expect the _CoqProject 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
diff --git a/package.json b/package.json
index 2a55e5b04..3c3f4b5a9 100644
--- a/package.json
+++ b/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,
diff --git a/server/src/CoqProject.ts b/server/src/CoqProject.ts
index bbdcd1b12..83fdcdcac 100644
--- a/server/src/CoqProject.ts
+++ b/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 {
diff --git a/server/src/coqtop/CoqTop8.ts b/server/src/coqtop/CoqTop8.ts
index 00bfd0f55..19148fbf3 100644
--- a/server/src/coqtop/CoqTop8.ts
+++ b/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,7 +239,7 @@ 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,
@@ -246,8 +247,19 @@ export class CoqTop extends IdeSlave8 implements coqtop.CoqTop {
'-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 {
diff --git a/server/src/protocol.ts b/server/src/protocol.ts
index 89495786a..5b910eea1 100644
--- a/server/src/protocol.ts
+++ b/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 {
diff --git a/server/test/coqtop.8.7.ts b/server/test/coqtop.8.7.ts
index ae97bd16b..212bc762a 100644
--- a/server/test/coqtop.8.7.ts
+++ b/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 = {