Using stdlib as an external dependency

[picrin]

I'd like to use subset.antisymm from stdlib/data/set/ in my pet project.

I've specified stdlib as a dependency using the following leanpkg.toml

[package]
name = "picrin-lean"
version = "0.0.0"

[dependencies]
stdlib = {git = "https://github.com/leanprover/stdlib", rev = "6d9072821b60d6a4a7293c943c07fba65041f25e"}

and run leanpkg --configure. This step created a local directory _target with the desired dependency.

But I'm not sure how to import subset.antisymm in my project.

I couldn't find any documentation, and I've tried various combinations of import/open and subset.antisymm with various different prefixes, from both VSCode extension and command line, but without luck.

I can provide more detail, and a smaller example, but the specific file I'm talking about (along with leanpkg.toml) is here:

https://github.com/picrin/lean/blob/master/topology.lean#L53

[digama0]

You should just need import data.set.basic and then refer to it as set.subset.antisymm, or open set and use subset.antisymm.

[picrin]

Thanks, this worked. I just had to include the path to $PROJECT_DIR/_target/stdlib/ in my LEAN_PATH.

This is less than ideal, but I'm happy with it for now.

Ideally, either lean or VSCode would read the file "leanpkg.path", which was automatically created by running leanpkg --configure, but I can't figure out how to make either of these tools do it.

[gebner]

Lean will automatically pick up the path from the generated leanpkg.path file (you may need to restart the Lean server for this to take effect). However if you set the environment variable LEAN_PATH manually, then it overrides leanpkg.path.

[picrin]

Thanks, that explains it -- I thought I needed custom LEAN_PATH, because I've compiled lean from source code and the executable, which resides in $LEAN_SOURCE_DIR/bin/ couldn't see the library which resides in $LEAN_SOURCE_DIR/library.

The problem with this set-up is that I'll need a custom $LEAN_PATH for each project, which means I'll have to source it, in a manner similar to python's virtualenv

[gebner]

which resides in $LEAN_SOURCE_DIR/bin/ couldn't see the library which resides in $LEAN_SOURCE_DIR/library.

This should definitely work. Can you please try again without the LEAN_PATH environment variable, and report a bug if it doesn't work?

[picrin]

I'd like to, but I don't know how to use lean without LEAN_PATH:

Thanks, that explains it -- I thought I needed custom LEAN_PATH, because I've compiled lean from source code and the executable, which resides in $LEAN_SOURCE_DIR/bin/ couldn't see the library which resides in $LEAN_SOURCE_DIR/library.

when I remove LEAN_PATH I'm just getting lots of errors complaining about missing core files from the lean source code.

[picrin]

I've worked around it -- just modified the leanpkg.path to include path to the core library, and unset $LEAN_PATH. Yes it works, which is again, fine by me.

Problems would only begin if I wanted to share my leanpkg.path with somebody else -- they may not have lean installed at the same path as me.

[gebner]

The leanpkg.path file should not be checked in anyhow. Could you post the output of lean -p?

[picrin]

That's it:

{
  "is_user_leanpkg_path": false,
  "leanpkg_path_file": "/home/picrin/programming/picrin-lean/leanpkg.path",
  "path": [
    "/home/picrin/programming/lean/library",
    "/home/picrin/programming/picrin-lean/_target/deps/stdlib/.",
    "/home/picrin/programming/picrin-lean/./."
  ]
}

[picrin]

Feel free to close this issue -- and thanks for your help. The setup I've got is good enough, if I ever encounter problems in the future I'll raise a separate issue.