Release 2.2

[rjbou]

[ejgallego]

@rlepigre your coq/dune file is:

(coq.theory
 (name bug)
 (stdlib no)
 (package bug))

So indeed, unless I'm missing something, how are thing supposed to work if you don't declare the dependency to your plugin?

[ejgallego]

Declaring the plugin we get a bit further:

$ (cd _build/default && /home/egallego/.opam/coq-v8.19/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -noinit -boot -I /home/egallego/.opam/coq-v8.19/lib/curl -I /home/egallego/.opam/coq-v8.19/lib/ocaml -I lib -R coq bug coq/bug.v)

File "./coq/bug.v", line 1, characters 0-31:
Error:
Findlib error: bug.plugin not found in:
/home/egallego/.opam/coq-v8.19/lib/curl
/home/egallego/.opam/coq-v8.19/lib/ocaml
lib
/home/egallego/.opam/coq-v8.19/lib

For some reason it seems that Coq is not reading OCAMLPATH ?

That seems bizarre to me.

[rlepigre]

So indeed, unless I'm missing something, how are thing supposed to work if you don't declare the dependency to your plugin?

Indeed, seems like I forgot this while minimizing.

[rlepigre]

For some reason it seems that Coq is not reading OCAMLPATH ?

That is always the case when you try running such commands shown by dune, you need to run with OCAMLPATH=_build/install/default/lib or something like that. At least that's what I do so that local plugins are found.

[ejgallego]

After a bit more hackery I'm back to the original error:

Dynlink error: no implementation available for Curl
Raised at Dynlink_common.Make.check_implementation_imports.(fun) in file "otherlibs/dynlink/dynlink_common.ml", line 173, characters 54-118
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dynlink_common.Make.check.(fun) in file "otherlibs/dynlink/dynlink_common.ml", line 235, characters 11-70
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Dynlink_common.Make.check in file "otherlibs/dynlink/dynlink_common.ml", line 233, characters 6-183
Called from Dynlink_common.Make.load in file "otherlibs/dynlink/dynlink_common.ml", line 333, characters 24-64
Re-raised at Dynlink_common.Make.load in file "otherlibs/dynlink/dynlink_common.ml", line 345, characters 8-17
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Fl_dynload.load_pkg in file "fl_dynload.ml", line 37, characters 5-227

[ejgallego]

There is something very strange going on here, will have look into this later on when i allocate the time to head towards dune-coq 1.0 language.