Merge pull request #127 from GaloisInc/sc/cn-b9daa22

CN server: update Cerberus/CN dependencies
GaloisInc · Nov 4, 2024 · ccd67a0 · ccd67a0
2 parents a258e83 + 146aab2
commit ccd67a0
Show file tree

Hide file tree

Showing 5 changed files with 35 additions and 28 deletions.
diff --git a/cn-lsp/server/cnlsp.opam b/cn-lsp/server/cnlsp.opam
@@ -8,9 +8,9 @@ depends: [
   "dune" {>= "3.12"}
   "ocaml" {>= "4.14.1" & < "6.0.0"}
   "base" {>= "v0.16.3" & < "v0.18"}
-  "cerberus" {= "f1f118b26"}
-  "cerberus-lib" {= "f1f118b26"}
-  "cn" {= "f1f118b26"}
+  "cerberus" {= "b9daa22"}
+  "cerberus-lib" {= "b9daa22"}
+  "cn" {= "b9daa22"}
   "jsonrpc" {>= "1.17.0" & < "2.0.0"}
   "linol" {>= "0.6" & < "1.0"}
   "linol-lwt" {>= "0.6" & < "1.0"}
@@ -34,15 +34,15 @@ build: [
 ]
 pin-depends: [
   [
-    "cerberus.f1f118b26"
-    "git+https://github.com/rems-project/cerberus.git#f1f118b26"
+    "cerberus.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
   ]
   [
-    "cerberus-lib.f1f118b26"
-    "git+https://github.com/rems-project/cerberus.git#f1f118b26"
+    "cerberus-lib.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
   ]
   [
-    "cn.f1f118b26"
-    "git+https://github.com/rems-project/cerberus.git#f1f118b26"
+    "cn.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
   ]
 ]
diff --git a/cn-lsp/server/cnlsp.opam.locked b/cn-lsp/server/cnlsp.opam.locked
@@ -11,10 +11,10 @@ depends: [
   "base-bytes" {= "base"}
   "base-threads" {= "base"}
   "base-unix" {= "base"}
-  "cerberus" {= "f1f118b26"}
-  "cerberus-lib" {= "f1f118b26"}
+  "cerberus" {= "b9daa22"}
+  "cerberus-lib" {= "b9daa22"}
   "cmdliner" {= "1.3.0"}
-  "cn" {= "f1f118b26"}
+  "cn" {= "b9daa22"}
   "conf-bash" {= "1"}
   "conf-c++" {= "1.0"}
   "conf-findutils" {= "1"}
@@ -84,15 +84,15 @@ build: [
 ]
 pin-depends: [
   [
-    "cerberus.f1f118b26"
-    "git+https://github.com/rems-project/cerberus.git#f1f118b26"
+    "cerberus.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
   ]
   [
-    "cerberus-lib.f1f118b26"
-    "git+https://github.com/rems-project/cerberus.git#f1f118b26"
+    "cerberus-lib.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
   ]
   [
-    "cn.f1f118b26"
-    "git+https://github.com/rems-project/cerberus.git#f1f118b26"
+    "cn.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
   ]
 ]
diff --git a/cn-lsp/server/cnlsp.opam.template b/cn-lsp/server/cnlsp.opam.template
@@ -1,14 +1,14 @@
 pin-depends: [
   [
-    "cerberus.f1f118b26"
-    "git+https://github.com/rems-project/cerberus.git#f1f118b26"
+    "cerberus.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
   ]
   [
-    "cerberus-lib.f1f118b26"
-    "git+https://github.com/rems-project/cerberus.git#f1f118b26"
+    "cerberus-lib.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
   ]
   [
-    "cn.f1f118b26"
-    "git+https://github.com/rems-project/cerberus.git#f1f118b26"
+    "cn.b9daa22"
+    "git+https://github.com/rems-project/cerberus.git#b9daa22"
   ]
 ]
diff --git a/cn-lsp/server/dune-project b/cn-lsp/server/dune-project
@@ -25,11 +25,11 @@
     (>= v0.16.3)
     (< v0.18)))
   (cerberus
-   (= "f1f118b26"))
+   (= "b9daa22"))
   (cerberus-lib
-   (= "f1f118b26"))
+   (= "b9daa22"))
   (cn
-   (= "f1f118b26"))
+   (= "b9daa22"))
   (jsonrpc
    (and
     (>= 1.17.0)

diff --git a/cn-lsp/server/lib/lspCn.ml b/cn-lsp/server/lib/lspCn.ml
@@ -99,9 +99,16 @@ module Cerb = struct
   ;;
 
   let frontend ((conf, impl, stdlib) : env) (filename : string) =
+    let cn_init_scope : CF.Cn_desugaring.init_scope =
+      { predicates = [ Cn.Alloc.Predicate.(str, sym, Some loc) ]
+      ; functions =
+          List.map Cn.Builtins.cn_builtin_fun_names ~f:(fun (str, sym) -> str, sym, None)
+      ; idents = [ Cn.Alloc.History.(str, sym, Some loc) ]
+      }
+    in
     let* _, ail_prog_opt, prog0 =
       CB.Pipeline.c_frontend_and_elaboration
-        ~cnnames:Cn.Builtins.cn_builtin_fun_names
+        ~cn_init_scope
         (conf, Cn.Setup.io)
         (stdlib, impl)
         ~filename