Yicheng Qian (Jul 04 2023 at 15:33): 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?
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.
Emilio Jesús Gallego Arias (Jul 04 2023 at 15:38):Hi @Yicheng Qian ,
Emilio Jesús Gallego Arias (Jul 04 2023 at 15:39):Did you use OPAM to install these packages?
Emilio Jesús Gallego Arias (Jul 04 2023 at 15:39):Can you provide:
opam list outputs?
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
Screenshot:
image.png
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
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
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?
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
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.
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.
Gaëtan Gilbert (Jul 04 2023 at 15:51):you probably need to make .merlin
Yicheng Qian (Jul 04 2023 at 15:53):Ok, I'll try to follow this: https://github.com/ocaml/merlin/wiki/Project-configuration
Gaëtan Gilbert (Jul 04 2023 at 15:54):no, coq_makefile has a .merlin target
Emilio Jesús Gallego Arias (Jul 04 2023 at 15:55):Yes, that should hopefully work
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
Emilio Jesús Gallego Arias (Jul 04 2023 at 15:55):but a bit more work indeed
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.
Yicheng Qian (Jul 04 2023 at 15:59):Great! Now it works!
Last updated: Nov 29 2023 at 21:01 UTC