Alperen Keles (Oct 26 2022 at 17:55): 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?
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
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?
Emilio Jesús Gallego Arias (Oct 26 2022 at 19:12):Use ocamlfind or a build system
Emilio Jesús Gallego Arias (Oct 26 2022 at 19:12):what documentation did you infer that command from?
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
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
Emilio Jesús Gallego Arias (Oct 26 2022 at 20:11):aha
Emilio Jesús Gallego Arias (Oct 26 2022 at 20:15):what Coq version are you?
Emilio Jesús Gallego Arias (Oct 26 2022 at 20:15):ocamlfind list | grep quick doesn't show QC libs?
Emilio Jesús Gallego Arias (Oct 26 2022 at 20:15):You can check here https://github.com/QuickChick/QuickChick/blob/master/plugin/dune
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)
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?
Emilio Jesús Gallego Arias (Oct 27 2022 at 09:52):Aren't you trying to build an executable?
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: Oct 13 2024 at 01:02 UTC