Most basic example of definition of category in Lean4?

Stream: lean4

[Daniel Donnelly]

Can someone translate the definition of category from Lean3 to Lean4, or is that like a multi-month project? Or can someone give me a simple definition of category to work with? (Lean4)

[Henrik Böving]

docs4#CategoryTheory.Category

[Daniel Donnelly]

Henrik Böving said:

docs4#CategoryTheory.Category

Thanks!

[Daniel Donnelly]

@Henrik Böving so how does one go about using that definition? I'm not all the way through TPIL 4, but by the end I will probably still ask the same question - usage example for category. Thanks.

[Daniel Donnelly]

For example, how does one first import that library file?

[Henrik Böving]

You first create a lake project that depends on mathlib4, there is actually a built-in template for that: lake new projectname math and in that project you just import the file

[Daniel Donnelly]

image.png

[Daniel Donnelly]

@Henrik Böving Can't see how to import given data on that page

[Henrik Böving]

Well sure you are just not copying all from the page: import Mathlib.CategoryTheory.Category.Basic

[Daniel Donnelly]

@Henrik Böving
image.png

[Henrik Böving]

Right, the next issue is that you opened the parent directoy as a project inn vscode but in order for vscode to pick up on your project you need to open your project's directoy directly in vscode, not its parent.

[Daniel Donnelly]

image.png

@Henrik Böving
Yes, good idea. But I tried that and got that Lean4 couldn't start up.

[Henrik Böving]

Hm, interesting I don't know about that one I don't use vscode so I don't know why it acts like it does here.

[Adam Topaz]

What happens when you restart vscode? Again, to clarify, you should open the folder of the project you created.

[Daniel Donnelly]

image.png

@Adam Topaz restarted VScode, opened correct folder, and same issue

[Daniel Donnelly]

image.png

[Daniel Donnelly]

I re-installed using Elan and keep getting this:
image.png

[Kevin Buzzard]

Try deleting the entire repository and then starting again following the instructions here in that post and the one after. Does this fix the problem?

[Daniel Donnelly]

@Kevin Buzzard Hi, we were just watching a YT video of yours about Lean4 proofs. Anyway, are you saying clone that repository and then open the project's root folder in VS code? I'll try it...

[Kevin Buzzard]

nonono, I meant "follow the instructions in the precise message I linked to, and the one after it, to make a working Lean 4 project which depends on mathlib"

[Kevin Buzzard]

I'll post the instructions again:

Start again with lake new hello math. This is the recommended way to make a project called hello which has mathlib as a dependency.

Then change directory into the new hello directory and type

lake update
lake exe cache get
lake build

and it should all work.

Now you can make project files, e.g. change the contents of Hello.lean to the line import Hello.test, make a Hello subdirectory and put a file test.lean in that subdirectory saying import Mathlib.CategoryTheory.Category.Basic. Then type lake build in the root folder and it should work fine.

[Kevin Buzzard]

I am unclear about how much variation you are allowed in the choice of hello v Hello.

[Daniel Donnelly]

@Kevin Buzzard cd hello then lake update gives:

PS C:\Users\fruit\OneDrive\Desktop\Lean4\hello> lake update
mathlib: no manifest entry; deleting .\lean_packages\mathlib and cloning again
cloning https://github.com/leanprover-community/mathlib4.git to .\lean_packages\mathlib
error: .\lean_packages\mathlib\lakefile.lean:17:2: error:
unknown attribute [default_target]
error: .\lean_packages\mathlib\lakefile.lean:21:2: error:
unknown attribute [default_target]
error: .\lean_packages\mathlib\lakefile.lean: package configuration has errors
PS C:\Users\fruit\OneDrive\Desktop\Lean4\hello>

[Kalle Kytölä]

I think I have experienced something similar. Does cp lake-packages/mathlib/lean-toolchain . before the lake exe cache get solve the problem?

[Henrik Böving]

The issue is that your Lean version is not up to date as evident by the fact that you are using lean_packages

[Kevin Buzzard]

Why isn't the system using the version of lean suggested by mathlib? If the instructions I've posted are not 100% correct, how do I correct them?

[Henrik Böving]

I'm guessing he is using a vversion of lean that did already have the math template but did not figure out the proper version based on the latest mathlib toolchain yet

[Henrik Böving]

And I guess the simplest way to fix this would be to make sure that you are running a kind of recent nightly as your default toolchain

[Daniel Donnelly]

We used this setup process:
Starting in our project parent dir. Mkdir "my_project", Cd "my_project", lake init my_project math, lake build, lake update

But I still get no import suggestions as depicted here:

image.png

[Daniel Donnelly]

@Henrik Böving , @Kevin Buzzard

[Sebastian Ullrich]

That would be because import completion is not implemented yet