diff --git a/cn-lsp/server/cnlsp.opam b/cn-lsp/server/cnlsp.opam index 89e4114..aee3cfc 100644 --- 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 index 0ea75fa..214fe0c 100644 --- 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 index a7a2ed9..367a3a6 100644 --- 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 index 2829d06..c37600e 100644 --- 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 index a4921bc..0332912 100644 --- 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