Stream: Coq devs & plugin devs

Topic: Ocaml-lsp unbound module error


view this post on Zulip Yicheng Qian (Jul 04 2023 at 15:33):

Hi! I'm new to coq plugin dev and I'm trying to contribute to the plugin smtCoq. I installed ocaml-4.11.1, ocaml-lsp and coq-8.13.2 on WSL, cloned the smtCoq repository, and opened the src folder in vscode. However, whenever I open a .ml file, I get a bunch of "Unbound module" errors. Is there a way to fix this?

view this post on Zulip Pierre Roux (Jul 04 2023 at 15:37):

OCaml plugins are very sensitive to the version of Coq (it is not unsual that they only work with a single version of Coq) and 8.13 is already pretty old. So I would first check the version of Coq required by your code of SMTCoq.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:38):

Hi @Yicheng Qian ,

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:39):

Did you use OPAM to install these packages?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:39):

Can you provide:

?

view this post on Zulip Yicheng Qian (Jul 04 2023 at 15:41):

Opam list output:

 Packages matching: installed
# Name                  # Installed # Synopsis
base-bigarray           base
base-threads            base
base-unix               base
cairo2                  0.6.4       Binding to Cairo, a 2D Vector Graphics Library
camlp-streams           5.0.1       The Stream and Genlex libraries for use with Camlp4 and Camlp5
conf-adwaita-icon-theme 2           Virtual package relying on adwaita-icon-theme
conf-cairo              1           Virtual package relying on a Cairo system installation
conf-findutils          1           Virtual package relying on findutils
conf-gmp                4           Virtual package relying on a GMP lib system installation
conf-gtk3               18          Virtual package relying on GTK+ 3
conf-gtksourceview3     0+2         Virtual package relying on a GtkSourceView-3 system installation
conf-pkg-config         2           Check if pkg-config is installed and create an opam switch local pkgconfig folder
coq                     8.13.2      Formal proof management system
coqide                  8.13.2      IDE of the Coq formal proof management system
cppo                    1.6.9       Code preprocessor like cpp for OCaml
csexp                   1.5.2       Parsing and printing of S-expressions in Canonical form
dot-merlin-reader       4.5         Reads config files for merlin
dune                    3.8.2       Fast, portable, and opinionated build system
dune-build-info         3.8.2       Embed build information inside executable
dune-configurator       3.8.2       Helper library for gathering system configuration
lablgtk3                3.1.3       OCaml interface to GTK+3
lablgtk3-sourceview3    3.1.3       OCaml interface to GTK+ gtksourceview library
num                     1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                   4.11.1      The OCaml compiler (virtual package)
ocaml-base-compiler     4.11.1      Official release 4.11.1
ocaml-config            1           OCaml Switch Configuration
ocaml-lsp-server        1.4.1       LSP Server for OCaml
ocamlfind               1.9.6       A library manager for OCaml
ppx_yojson_conv_lib     v0.15.0     Runtime lib for ppx_yojson_conv
result                  1.5         Compatibility Result module
seq                     base        Compatibility package for OCaml's standard iterator type starting from 4.07.
stdlib-shims            0.3.0       Backport some of the new stdlib features to older compiler
yojson                  2.1.0       Yojson is an optimized parsing and printing library for the JSON format
zarith                  1.12        Implements arithmetic and logical operations over arbitrary-precision integers

view this post on Zulip Yicheng Qian (Jul 04 2023 at 15:42):

Screenshot:
image.png

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:43):

I misread coq-lsp vs ocaml-lsp, sorry, this is good in that stream

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:44):

I think the problem here is that ocaml-lsp doesn't understand the build system used in smtCoq

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:44):

Can you try to build smtCoq from the terminal, and see if that problem goes away?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:44):

In general, having an effective dev setup for OCaml projects these days requires the project to use Dune

view this post on Zulip Yicheng Qian (Jul 04 2023 at 15:46):

I installed smtCoq following the Installation from the sources, using opam (not recommended) section in https://github.com/smtcoq/smtcoq/blob/coq-8.13/INSTALL.md and I've built it from terminal by running make and make install.

view this post on Zulip Yicheng Qian (Jul 04 2023 at 15:50):

Emilio Jesús Gallego Arias said:

Did you use OPAM to install these packages?

I used OPAM to install coq and ocaml-lsp, but I built smtCoq from source.

view this post on Zulip Gaëtan Gilbert (Jul 04 2023 at 15:51):

you probably need to make .merlin

view this post on Zulip Yicheng Qian (Jul 04 2023 at 15:53):

Ok, I'll try to follow this: https://github.com/ocaml/merlin/wiki/Project-configuration

view this post on Zulip Gaëtan Gilbert (Jul 04 2023 at 15:54):

no, coq_makefile has a .merlin target

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:55):

Yes, that should hopefully work

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:55):

I have somewhere a dunerized version of smtCoq, that could be very useful for you too

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:55):

but a bit more work indeed

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 15:56):

@Yicheng Qian ocaml-lsp needs some metadata to be generated as to understand where to look for build objects, make .merlin generates that data, not sure if you need to reload the ocaml-lsp server for it to work tho.

Projects using dune don't need that .merlin file anymore.

view this post on Zulip Yicheng Qian (Jul 04 2023 at 15:59):

Great! Now it works!


Last updated: Jul 24 2024 at 12:02 UTC