Using CSLib as a dependency

Stream: computer science

[Iván Renison]

Hi, do you know what do I have to make to use CSLib as a dependency?
I tried to do something similar to the "Using mathlib4 as a dependency" explanation, and I ran: lake +leanprover/cslib:lean-toolchain new ProjectName math, but it didn't work

[Kevin Buzzard]

I would just make a new repository and then add to your lakefile.toml

[[require]]
name = "cslib"
git = "https://github.com/leanprover/cslib.git"

and then check it works by making a new file and putting import Cslib at the top.

[Iván Renison]

I get the error error: /home/ivan/Desktop/TeoFundArit/.lake/packages/cslib: revision not found 'master'
Maybe it has to do with the fact that CSLib has a main branch instead of a master branch

[Shreyas Srinivas]

You need to add rev = "main"

[Iván Renison]

This worked, but Cslib was build in my computer. lake exe cache get only downloaded Mathlib cache

[Iván Renison]

Thank you

[Shreyas Srinivas]

yeah that's something for the FRO to fix and they are working on adding a general cache for all projects

[Chris Henson]

Yes, cache does not get CSLib. But at this point it is relatively quick to build, so it's not too painful.

[Chris Henson]

Note also that there are tags for each release if you need that for any reason.