project or package

Stream: general

[Kevin Buzzard]

I've just realised that in some of my docs I use the words "project" and "package" interchangeably when talking about "a directory with a leanpkg.toml file in it". Are the words interchangeable? If not, which one should I be using?

[Gabriel Ebner]

Yes, they're used interchangeably.

[Patrick Massot]

I guess there is a psychological difference, especially you use other people packages in order to work on your own project

[Simon Hudon]

Or you could say that your project is to develop the package that you're interested in.