projects as dependencies

Stream: general

[Jared green]

how do i make 'leanprover/super', which i have downloaded, one of the dependencies of my file? i'm using VSCode.

[Scott Morrison]

leanpkg add <url> [branch] is probably what you're looking for.

[Jared green]

my file isnt on github.

[Scott Morrison]

But your dependency is. The url should be the url of the git repository you want to depend on.

[Jared green]

what does 'branch' refer to?

[Scott Morrison]

It's optional; typically you just want the master branch, in which case you can just leave it off.

[Jared green]

how do i link it to my file, specifically?

[Johan Commelin]

@Jared green individual Lean files can't have dependencies. So you want to start your own new project, and add super as dependency to that project.

[Jared green]

i have had to port super2 to the version of lean i am using.(both super and super2 are incompatible, and super had an error i couldnt fix at all) in my version of lean, by_contradiction expects a 'name' as input. at lines 150-159 of prover.lean, (nothing else of consequence has changed) i gave 'better_contradiction' the input type 'option name', then gave 'none' to its only call. it type checks, but i'm pretty sure its wrong. im addressing Gabriel Ebner: what did better_contradiction do, and is the call to tactic.by_contradiction absolutely necessary?

[Eric Wieser]

@Gabriel Ebner ^

[Gabriel Ebner]

super2 is a half-finished rewrite of super, but I've given up on any further work in Lean 3 due to performance issues. It should still be able to do some easy stuff. I've updated super2 to Lean 3.34 now.