Key logic_file not bound in state. Have you called the init function for the state pipe/module ?

[BrandonStudio]

Error in extension

Should I do some extra configuration?

[hra687261]

Hello @BrandonStudio,

That's an error from dolmen's LSP server and not a configuration issue of the extension. Which version of dolmen_lsp do you have installed? You can check by running the command opam info dolmen_lsp

[BrandonStudio]

Thank you for your kindly reply.

I just installed opam and dolmen_lsp, following your instruction at https://marketplace.visualstudio.com/items?itemName=hra687261.smt-lsp#dependencies.

Here's the version info.

<><> dolmen_lsp: information on all versions ><><><><><><><><><><><><><><><>  🐫 
name                   dolmen_lsp
all-installed-versions 0.10 [default]
all-versions           0.5  0.6  0.7  0.8  0.8.1  0.9  0.10

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><>  🐫 
version      0.10
repository   default
url.src      "https://github.com/Gbury/dolmen/releases/download/v0.10/dolmen-0.10.tbz"
url.checksum
          "sha256=c5c85f77e3924f378e8d82f166eefe4131b4e041bf9cdeca467410f33c71fa61"
          "sha512=42feb39d13cfdc8a2054abe85ccc47755f45059cda7d95e9261b5a9fd5c730f420732547b3fa19c4af059474f887ef78c119ab5933375a5ea2dbe888f65a3e4f" 
homepage     "https://github.com/Gbury/dolmen"
doc          "https://gbury.github.io/dolmen"
bug-reports  "https://github.com/Gbury/dolmen/issues"
dev-repo     "git+https://github.com/Gbury/dolmen.git"
authors      "Guillaume Bury <guillaume.bury@gmail.com>"
maintainer   "Guillaume Bury <guillaume.bury@gmail.com>"
license      "BSD-2-Clause"
tags         "logic"
             "computation"
             "automated theorem prover"
             "lsp"
             "language server protocol"
depends      "ocaml" {>= "4.02.3"}
             "dolmen" {= version}
             "dolmen_type" {= version}
             "dolmen_loop" {= version}
             "dune" {>= "3.0"}
             "ocaml-syntax-shims"
             "odoc" {with-doc}
             "logs"
             "lsp"
             "linol" {>= "0.4" & < "0.5"}
             "linol-lwt" {>= "0.4" & < "0.5"}
synopsis     A LSP server for automated deduction languages

Did I miss something? I'm just a beginner of all these.

[hra687261]

That is surprising, I am unable to reproduce the error.

I don't think you're missing something, it should work straight away. Did you set the path to the dolmenls executable in the extension's setting? If not it should use the one you have installed in your current switch which is version 0.10 and which works fine for me.

(cc @Gbury, since the error comes from the server maybe you have an idea of what caused it?)

[Gbury]

Hm.. this might actually be a bug in dolmen, let me check. In the meantime, you can try and install older versions of dolmen, using e.g. opam install dolmen_lsp.0.8.1

[BrandonStudio]

I switched to 0.8.1. Now it seems that LSP works fine. But in an SMT file, it marks error:

The following extension was not recognized: '.z3'. Please use a recognised extension or specify an input language on the command line dolmenls

After I changed the file extension to .smt2, it disappeared, but another error was raised at

(declare-sort Name)

while parsing a sort declaration, read a closing parenthesis, but expected a numeral for the arity of the sort being declared. dolmenls

[hra687261]

That is expected, the supported langauge is the SMT-LIB standard (https://smt-lib.org/language.shtml and https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf) with ".smt2" files and its polymorphic variant with ".psmt2" files. To declare a sort with no parameters you should write (declare-sort Name 0) Here are some examples: https://smt-lib.org/examples.shtml

[BrandonStudio]

It seems that my statement corresponds to the Z3 standard. I don't know exactly what are the differences between Z3 and standard SMT-LIB 2, but I wonder if there is a way to just work on Z3, and to check whether the file fits Z3 grammar?

[Gbury]

The Z3 standard is not currently supported by dolmen. That being said, if you want it to be supported, you can open an issue on the dolmen repo, with a link to some kind of specification of what is accepted by Z3, and I'll take a look when I have time.

[hra687261]

AFAIK the z3 standard is essentially an extension of the SMT-LIB standard and some syntactic sugar, but I am not sure if it formalized/documented somewhere. (It's worth noting that z3, and pretty much all other SMT solvers support the SMT-LIB standard, therefore if the problem can be encoded in the SMT-LIB standard, it is preferable to do so IMO)

[Gbury]

Hm.. I can't seem to reproduce the initial error ("Key logic_file not bound in state") and the lsp server v0.10 works on my machine. I also had a quick look at the code and nothing seems obviously wrong. @BrandonStudio do you have any more context on what triggered the error ? Did the lsp work at any point or did it never work ?

@hra687261 can you reproduce (since I'm using neovim and not vscode) ? Also, in the installation instructions, you can mention that binaries (including for windows) are provided in the releases (see e.g. https://github.com/Gbury/dolmen/releases/latest ).

[BrandonStudio]

@Gbury What I did:

1. Install opam
2. Install dolmen
3. Restart VS Code
4. See the log of smt extension, the error is there

I don't know how to capture additional context

[hra687261]

I haven't managed to reproduce the error on vscode. That is weird, the extension is supposed to only call the dolmen_lsp server when an smt file is opened, the error says that no logic_file was provided so it should occur during the call to the server, but for me it works with no issue with dolmen_lsp version 0.10. Does the message error appear when you open an smt file or without opening an smt file?

4. See the log of smt extension, the error is there

Since the extension does not output any messages, there shouldn't be a log window. In the "output" section in vscode I find the log windows of other extensions as well as the "Extension host" that shows that the extension was started correctly, but no log window for the SMT LSP extension. If the extension crashes then a vscode error window appears, is that what happens?

The version of the extension that I use is the latest v1.1.0 installed from vscode marketplace, dolmen_lsp 0.10 was installed with opam, and the vscode version is 1.92.2. Although I am not sure if that is relevant information.

[BrandonStudio]

Does the message error appear when you open an smt file or without opening an smt file?

I think it was when I opened an SMT file, which was when the extension attempted to start parsing.

Since the extension does not output any messages, there shouldn't be a log window.

Yes, only when the error occurred with 0.10 did the SMT log window appear; when I used 0.8, there wasn't a log window for SMT.

I may try more next week. (maybe re-upgrade to 0.10 to see what will happen)