Making Libraries and Packages

Stream: general

[Fredson Aguiar]

Hello. I'm in a project, developing a knowledge base in Lean (a common sense base), and we've got to the point were we'd like to generate some kind of package with this theory. How should it be done? Do you guys have suggestions? Some references, or sites would be great!

[Mario Carneiro]

The lean package management stuff mostly assumes that you are putting the package as a github repo

[Mario Carneiro]

What do you mean by "knowledge base"?

[Fredson Aguiar]

Sorry. An ontology. A set of axioms and definitions that try to describe a theory.

For example, spatial theory have some axioms describing positions, positional relations, attributes, etc.

[Mario Carneiro]

There are lots of projects based on mathlib, for example https://github.com/flypitch/flypitch and https://github.com/leanprover-community/lean-perfectoid-spaces . You can find a tutorial on how to set up your own project here, and I would recommend following those instructions first and then double checking against the established projects to see if your setup is reasonable

[Fredson Aguiar]

Sure, I understand. I'm gonna try this. Thanks!