diff --git a/cn-client/package.json b/cn-client/package.json index 2d06245..1ed72d0 100644 --- a/cn-client/package.json +++ b/cn-client/package.json @@ -49,6 +49,11 @@ "default": null, "description": "Location of the LSP server" }, + "CN.debugPath": { + "type": "string", + "default": null, + "description": "Location of the CN-DAP executable" + }, "CN.showGillianDebugLenses": { "type": "boolean", "default": false, diff --git a/cn-client/src/extension.ts b/cn-client/src/extension.ts index a6639c2..f83c023 100644 --- a/cn-client/src/extension.ts +++ b/cn-client/src/extension.ts @@ -31,12 +31,20 @@ export async function activate(context: vsc.ExtensionContext): Promise { // or retrieved in a server configuration, should we try again? } + const workspaceFolders = vsc.workspace.workspaceFolders; + let logPath = "CN-lsp-server.log"; + if (workspaceFolders && workspaceFolders.length > 0) { + const workspaceRoot = workspaceFolders[0].uri.fsPath; + logPath = path.join(workspaceRoot, "CN-lsp-server.log"); + } + const serverOptions: ct.Executable = { command: serverContext.serverPath, transport: ct.TransportKind.pipe, options: { env, }, + args: ["--log", logPath] }; const clientOptions: ct.LanguageClientOptions = { @@ -81,6 +89,13 @@ export async function activate(context: vsc.ExtensionContext): Promise { client.sendRequest(req, params); }); + context.subscriptions.push( + vsc.debug.registerDebugAdapterDescriptorFactory( + "CN", + new CNDebugAdaptorDescriptorFactory(serverContext.debugPath) + ) + ); + client.start(); console.log("started client"); } @@ -93,9 +108,45 @@ export function deactivate(): Thenable | undefined { } } +class CNDebugAdaptorDescriptorFactory + implements vsc.DebugAdapterDescriptorFactory { + private debugPath: string; + + constructor(debugPath: string | undefined) { + this.debugPath = debugPath ?? "cn-debug"; + } + + createDebugAdapterDescriptor( + _session: vsc.DebugSession, + executable: vsc.DebugAdapterExecutable | undefined + ): vsc.ProviderResult { + let langCmd: string = this.debugPath; + + const config = vsc.workspace.getConfiguration("gillianDebugger"); + console.log("Configuring debugger!...", { config }); + + const workspaceFolders = vsc.workspace.workspaceFolders; + let logPath = "CN-debug.log"; + if (workspaceFolders && workspaceFolders.length > 0) { + const workspaceRoot = workspaceFolders[0].uri.fsPath; + logPath = path.join(workspaceRoot, "CN-debug.log"); + } + + let args = [ + "--log", + logPath + ]; + + executable = new vsc.DebugAdapterExecutable(langCmd, args); + + return executable; + } +} + interface ServerContext { serverPath: string; cerbRuntime?: string; + debugPath?: string; } async function newServerContext( @@ -122,40 +173,58 @@ async function newServerContext( } let serverPath = path.join(opamDir, "bin", "cn-lsp-server"); + let debugPath = path.join(opamDir, "bin", "cn-debug"); let cerbRuntime = path.join(opamDir, "lib", "cerberus", "runtime"); - if (fs.existsSync(serverPath) && fs.existsSync(cerbRuntime)) { + if (fs.existsSync(serverPath) && fs.existsSync(debugPath) && fs.existsSync(cerbRuntime)) { return { serverPath, cerbRuntime, + debugPath }; } } } + let serverPath: Maybe = undefined; + let debugPath: Maybe = undefined; + console.log("Looking in $CN_LSP_SERVER"); console.log(process.env); let envPath = process.env.CN_LSP_SERVER; if (envPath !== undefined) { - return { serverPath: envPath }; + serverPath = envPath; } - console.log("Looking on $PATH"); - const out = child_process.spawnSync("which", ["cn-lsp-server"], { - encoding: "utf-8", - }); - if (out.status === 0) { - let serverPath = out.stdout.trim(); - return { serverPath }; + if (serverPath === undefined) { + console.log("Looking on $PATH"); + const out = child_process.spawnSync("which", ["cn-lsp-server"], { + encoding: "utf-8", + }); + if (out.status === 0) { + serverPath = out.stdout.trim(); + } + } + + if (debugPath === undefined) { + console.log("Looking on $PATH"); + const out = child_process.spawnSync("which", ["cn-debug"], { + encoding: "utf-8", + }); + if (out.status === 0) { + debugPath = out.stdout.trim(); + } } - return undefined; + + return serverPath ? { serverPath, debugPath } : undefined; } function getConfiguredServerContext(): Maybe { let conf = vsc.workspace.getConfiguration("CN"); let serverPath: Maybe = conf.get("serverPath"); let cerbRuntime: Maybe = conf.get("cerbRuntime"); + let debugPath: Maybe = conf.get("debugPath"); // In practice, despite the type annotations, `conf.get` seems capable of // returning `null` values, so we need to check them @@ -165,9 +234,12 @@ function getConfiguredServerContext(): Maybe { serverPath !== "" && cerbRuntime !== null && cerbRuntime !== undefined && - cerbRuntime !== "" + cerbRuntime !== "" && + debugPath !== null && + debugPath !== undefined && + debugPath !== "" ) { - return { serverPath, cerbRuntime }; + return { serverPath, cerbRuntime, debugPath }; } else { return undefined; } @@ -185,4 +257,9 @@ async function setConfiguredServerContext(serverContext: ServerContext) { serverContext.serverPath, vsc.ConfigurationTarget.Global ); + await conf.update( + "debugPath", + serverContext.debugPath, + vsc.ConfigurationTarget.Global + ); } diff --git a/cn-dap/debugger/README.md b/cn-dap/debugger/README.md new file mode 100644 index 0000000..2e35481 --- /dev/null +++ b/cn-dap/debugger/README.md @@ -0,0 +1,5 @@ +# Installation +Pin Gillian +```bash +opam pin gillian git@github.com:GillianPlatform/Gillian.git#0c14d64 --with-version "0c14d64" +``` diff --git a/cn-dap/debugger/cndap.opam b/cn-dap/debugger/cndap.opam index c31740a..8c227bc 100644 --- a/cn-dap/debugger/cndap.opam +++ b/cn-dap/debugger/cndap.opam @@ -12,7 +12,7 @@ depends: [ "cerberus-lib" {= "b9daa22"} "cn" {= "b9daa22"} "dap" {>= "1.0.6" & < "2.0.0"} - "gillian" {= "c6802c5"} + "gillian" {= "0c14d64"} "logs" {>= "0.7.0" & < "1.0.0"} "odoc" {with-doc} ] diff --git a/cn-dap/debugger/dune-project b/cn-dap/debugger/dune-project index 6399383..bf49f26 100644 --- a/cn-dap/debugger/dune-project +++ b/cn-dap/debugger/dune-project @@ -34,7 +34,7 @@ (>= 1.0.6) (< 2.0.0))) (gillian - (= "c6802c5")) + (= "0c14d64")) (logs (and (>= 0.7.0) diff --git a/cn-lsp/lib/server.ml b/cn-lsp/lib/server.ml index 39313c5..c976ce7 100644 --- a/cn-lsp/lib/server.ml +++ b/cn-lsp/lib/server.ml @@ -273,6 +273,14 @@ class lsp_server (env : LspCn.cerb_env) = return () | Some (diag_uri, diag) -> self#publish_diagnostics_for notify_back diag_uri [ diag ]) + | exception e -> + let backtrace = Backtrace.Exn.most_recent_for_exn e in + let backtrace_str = + Option.map ~f:Backtrace.to_string backtrace + |> Option.value ~default:"" in + Log.d (sprintf "Verification failed with exception: %s, backtrace: %s" (Exn.to_string e) backtrace_str); + return () + method clear_diagnostics_for (notify_back : Rpc.notify_back)