updated gillian to work with main branch

cn-client/package.json

@@ -48,9 +48,25 @@
                     "type": "string",
                     "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,
+                    "description": "Show code lenses that activate Gillian debugging. Note that this functionality relies on the Gillian debugging extension (https://gillianplatform.github.io/sphinx/debugger.html) being installed, or run in a development host context."
                 }
             }
         },
+        "debuggers": [
+            {
+                "type": "CN",
+                "label": "CN Debugger"
+            }
+        ],
         "grammars": [
             {
                 "path": "./syntaxes/cn.tmLanguage.json",

cn-client/src/extension.ts

@@ -31,12 +31,21 @@ export async function activate(context: vsc.ExtensionContext): Promise<void> {
         // 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 +90,13 @@ export async function activate(context: vsc.ExtensionContext): Promise<void> {
         client.sendRequest(req, params);
     });
 
+    context.subscriptions.push(
+        vsc.debug.registerDebugAdapterDescriptorFactory(
+            "CN",
+            new CNDebugAdaptorDescriptorFactory(serverContext.debugPath)
+        )
+    );
+
     client.start();
     console.log("started client");
 }
@@ -93,9 +109,45 @@ export function deactivate(): Thenable<void> | 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<vsc.DebugAdapterDescriptor> {
+        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 +174,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<string> = undefined;
+    let debugPath: Maybe<string> = 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<ServerContext> {
     let conf = vsc.workspace.getConfiguration("CN");
     let serverPath: Maybe<string> = conf.get("serverPath");
     let cerbRuntime: Maybe<string> = conf.get("cerbRuntime");
+    let debugPath: Maybe<string> = 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 +235,12 @@ function getConfiguredServerContext(): Maybe<ServerContext> {
         serverPath !== "" &&
         cerbRuntime !== null &&
         cerbRuntime !== undefined &&
-        cerbRuntime !== ""
+        cerbRuntime !== "" && 
+        debugPath !== null &&
+        debugPath !== undefined &&
+        debugPath !== ""
     ) {
-        return { serverPath, cerbRuntime };
+        return { serverPath, cerbRuntime, debugPath };
     } else {
         return undefined;
     }
@@ -185,4 +258,9 @@ async function setConfiguredServerContext(serverContext: ServerContext) {
         serverContext.serverPath,
         vsc.ConfigurationTarget.Global
     );
+    await conf.update(
+        "debugPath",
+        serverContext.debugPath,
+        vsc.ConfigurationTarget.Global
+    );
 }

cn-dap/debugger/README.md

@@ -0,0 +1,5 @@
+# Installation
+Pin Gillian
+```bash
+opam pin gillian [email protected]:GillianPlatform/Gillian.git#0c14d64 --with-version "0c14d64"
+```

cn-dap/debugger/bin/dune

@@ -0,0 +1,5 @@
+(executable
+ (public_name cn-debug)
+ (name main)
+ (package cndap)
+ (libraries cndap logs))

cn-dap/debugger/bin/main.ml

@@ -0,0 +1,32 @@
+
+open Cndap
+
+let log_setup (log_path : string option) : unit =
+  let log_file = Option.value log_path ~default:"/tmp/cn-debug-log.txt" in
+  let log_channel = Out_channel.open_text log_file in
+  let formatter = Format.formatter_of_out_channel log_channel in
+  let reporter = Logs.format_reporter ~app:formatter ~dst:formatter () in
+  let () = Logs.set_level (Some Logs.Debug) in
+  let () = Logs.set_reporter reporter in
+  ()
+;;
+
+type options = { log_path : string option }
+
+let parse_arguments () : options =
+  let log_file_ref : string option ref = ref None in
+  let populate r s = r := Some s in
+  let usage = String.concat " " [ "Usage: cn-debug"; "--log <log-file>" ] in
+  let arglist = [ "--log", Arg.String (populate log_file_ref), "Path to log file" ] in
+  let handle_positional _ = () in
+  let () = Arg.parse arglist handle_positional usage in
+  { log_path = !log_file_ref }
+;;
+
+let main () : unit =
+  let options = parse_arguments () in
+  log_setup options.log_path;
+  Adapter.run_stdio ()
+;;
+
+let () = main ()

cn-dap/debugger/cndap.opam

@@ -0,0 +1,50 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "CN Debug Adapter"
+description: "A debug adapter protocol implementation for CN state dumps"
+maintainer: ["Sam Cowger" "Kiran Gopinathan"]
+authors: ["Sam Cowger" "Kiran Gopinathan"]
+depends: [
+  "dune" {>= "3.12"}
+  "ocaml" {>= "4.14.1" & < "6.0.0"}
+  "base" {>= "v0.16.3" & < "v0.18"}
+  "cerberus" {= "b9daa22"}
+  "cerberus-lib" {= "b9daa22"}
+  "cn" {= "b9daa22"}
+  "dap" {>= "1.0.6" & < "2.0.0"}
+  "gillian" {= "0c14d64"}
+  "logs" {>= "0.7.0" & < "1.0.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+pin-depends: [
+  [
+    "cerberus.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
+  ]
+  [
+    "cerberus-lib.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
+  ]
+  [
+    "cn.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
+  ]
+  [
+    "gillian.c6802c5"
+    "git+https://github.com/GillianPlatform/Gillian.git#c6802c5"
+  ]
+]

cn-dap/debugger/cndap.opam.template

@@ -0,0 +1,18 @@
+pin-depends: [
+  [
+    "cerberus.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
+  ]
+  [
+    "cerberus-lib.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
+  ]
+  [
+    "cn.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
+  ]
+  [
+    "gillian.c6802c5"
+    "git+https://github.com/GillianPlatform/Gillian.git#c6802c5"
+  ]
+]

cn-dap/debugger/dune-project

@@ -0,0 +1,41 @@
+(lang dune 3.12)
+
+(name cndap)
+
+(generate_opam_files true)
+
+(authors "Sam Cowger" "Kiran Gopinathan")
+
+(maintainers "Sam Cowger" "Kiran Gopinathan")
+
+(package
+ (name cndap)
+ (synopsis "CN Debug Adapter")
+ (description "A debug adapter protocol implementation for CN state dumps")
+ (depends
+  dune
+  (ocaml
+   (and
+    (>= 4.14.1)
+    (< 6.0.0)))
+  ;;
+  (base
+   (and
+    (>= v0.16.3)
+    (< v0.18)))
+  (cerberus
+   (= "b9daa22"))
+  (cerberus-lib
+   (= "b9daa22"))
+  (cn
+   (= "b9daa22"))
+  (dap
+   (and
+    (>= 1.0.6)
+    (< 2.0.0)))
+  (gillian
+   (= "0c14d64"))
+  (logs
+   (and
+    (>= 0.7.0)
+    (< 1.0.0)))))