Stream: Coq users

Topic: No implementations provided for Coq Modules


view this post on Zulip Alperen Keles (Oct 26 2022 at 17:55):

Hi,

To be more clear.

I am trying to use QuickChick as a library inside OCaml.

When I try to link Quickchick_plugin using the locally installed QuickChick using the command below.

ocamlfind ocamlopt -rectypes -I ~/.opam/4.10.2+afl/lib/coq/user-contrib/QuickChick/ ~/.opam/4.10.2+afl/lib/coq/user-contrib/QuickChick/quickchick_plugin.cmxa  foo.ml

I receive the following error message.

Error: No implementations provided for the following modules:
Tacticals referenced from /Users/akeles/.opam/4.10.2+afl/lib/coq/user-contrib/QuickChick/quickchick_plugin.cmxa(Quickchick_plugin)
CAst referenced from /Users/akeles/.opam/4.10.2+afl/lib/coq/user-contrib/QuickChick/quickchick_plugin.cmxa(Quickchick_plugin)
Typing referenced from /Users/akeles/.opam/4.10.2+afl/lib/coq/user-contrib/QuickChick/quickchick_plugin.cmxa(Quickchick_plugin)
Ppconstr referenced from /Users/akeles/.opam/4.10.2+afl/lib/coq/user-contrib/QuickChick/quickchick_plugin.cmxa(Quickchick_plugin)
...

It follows with a long list of modules from coq-core such as Constr, Proofview, Namegen....

Below are the contents of foo.ml

open Quickchick_plugin

let () =
  let s = QuickChick.qcFuzz in
  Printf.printf "hello"

Is there any tooling that will allow me to link these easily, or any other solution?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2022 at 18:06):

Your link command is wrong, it is missing quite a few cmxa because you need to send to the linker all the transitive deps

view this post on Zulip Alperen Keles (Oct 26 2022 at 19:12):

Emilio Jesús Gallego Arias said:

Your link command is wrong, it is missing quite a few cmxa because you need to send to the linker all the transitive deps

Is there any way to get them automatically without searching by hand?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2022 at 19:12):

Use ocamlfind or a build system

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2022 at 19:12):

what documentation did you infer that command from?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2022 at 19:13):

ocamlfind can do that for your in several ways, but using a build system such as Dune will make your life even easier

view this post on Zulip Alperen Keles (Oct 26 2022 at 20:08):

I think the problem is that ocamlfind does not find coq-quickchick as a dependency, perhaps due to the way quickChick is installed. Once ocamlfind failed to automatically find it, I have worked my way through manual trials and that got me where I am right now

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2022 at 20:11):

aha

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2022 at 20:15):

what Coq version are you?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2022 at 20:15):

ocamlfind list | grep quick doesn't show QC libs?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2022 at 20:15):

You can check here https://github.com/QuickChick/QuickChick/blob/master/plugin/dune

view this post on Zulip Emilio Jesús Gallego Arias (Oct 26 2022 at 20:15):

the list of deps, this way you can just pass unix str coq-core.plugins.extraction to ocamlfind (or Dune)

view this post on Zulip Alperen Keles (Oct 26 2022 at 20:37):

Ah, that was very helpful, thank you so much! Can I diverge to another question if possible?

When I try to compile this way with,

ocamlfind ocamlopt -linkpkg -package "unix str coq-core.plugins.extraction" -thread -rectypes -I ~/.opam/4.10.2+afl/lib/coq/user-contrib/QuickChick/ ~/.opam/4.10.2+afl/lib/coq/user-contrib/QuickChick/quickchick_plugin.cmxa foo.ml

I'm receiving

clang: error: no such file or directory: '/Users/akeles/.opam/4.10.2+afl/lib/coq/user-contrib/QuickChick/quickchick_plugin.a'
File "caml_startup", line 1:
Error: Error during linking

This to me feels like I'm doing something slightly wrong to me, somehow ocamlopt thinks quickchick_plugin is a C module maybe?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 27 2022 at 09:52):

Aren't you trying to build an executable?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 27 2022 at 09:53):

Again, what Coq version are you, and what is the output of the grep command I posted above?


Last updated: Feb 09 2023 at 00:03 UTC