Skip to content

ocp-index locate returns the wrong location #167

Open
@mlemerre

Description

Hi,

First, thank you for ocp-index. I don't know why I did not know the tool before, it should definitively be part of the tools officially recommended!

One issue though is that it does not return the correct locations. If I type:

$ ocp-index locate Z.one
/home/matthieu/.opam/4.14.1+BER/.opam-switch/build/zarith.1.13/z.mli:62:0

this is incorrect.

If I look at the doc, the location where z.mli is looked up is obtained by opam var lib, whose value is

/home/matthieu/.opam/4.14.1+BER/lib

in my case.

And indeed, if I do

$ ocp-index locate Z.one --no-opamlib

Then there is no result.

So my guess is that there is some changes in the path done by ocp-index, which should return instead

./lib/zarith/z.mli

or

./.opam-switch/sources/zarith.1.13/z.mli

Is there something wrong in my setup? I only did opam install ocp-index.

Thanks
Matthieu

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions