importing from another file

Stream: lean4

[Dean Young]

Can someone link me to an example of how to import a lean 4 file from elsewhere on my computer in a MacOSX directory?

[Martin Dvořák]

Import into your project? What do you refer to?

[Dean Young]

Yeah, I've got a Main.lean and Project.lean file which I compile from the terminal.

[Dean Young]

Elsewhere on my Mac I have another Main.lean and Project.lean file (and the other files that lake projects automatically make)

[Arthur Paulino]

You need the file to be either in the same Lake project or in a Lake project you use as a dependency

[Dean Young]

What about imports like Mathlib? How do you make a library?

[Arthur Paulino]

Mathlib files only import other files from the same project or from the projects it depends on (Std, Qq, Aesop)

[Arthur Paulino]

I think there's some noise in the communication. What are you trying to do exactly?

[Arthur Paulino]

I'd say that the easiest way to create a Lean package is using Lake: https://github.com/leanprover/lake/#creating-and-building-a-package

[Dean Young]

I have one file with the definition of the category of categories:

import Init.Data.ToString.Basic
universe u
universe v
structure Cat where
  Obj : Type u
  Hom : ∀(_:Obj),∀(_:Obj), Type v
  Idn : ∀(X:Obj),Hom X X
  Cmp : ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(_:Hom X Y),∀(_:Hom Y Z),Hom X Z
  Id1 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X Y Y) f (Idn Y) = f
  Id2 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X X Y) (Idn X) f = f
  Ass : ∀(W:Obj),∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(f:Hom W X),∀(g:Hom X Y),∀(h:Hom Y Z),(Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h
def Cmp {C : Cat} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g

def Hom {C : Cat} (X : C.Obj) (Y : C.Obj) := C.Hom X Y
--notation X "➔" Y => Hom X Y

def Idn {C : Cat} (X : C.Obj) := C.Idn X
--notation "𝟙" X => Idn X
structure Fun (C : Cat) (D : Cat) where
   Obj : ∀(_ : C.Obj),D.Obj
   Mor : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Mor X X (C.Idn X) = D.Idn (Obj X)
   Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),D.Cmp (Obj X) (Obj Y) (Obj Z) (Mor X Y f) (Mor Y Z g) = Mor X Z (C.Cmp X Y Z (f) (g))
def CatIdn (C : Cat) : Fun C C :=
{Obj := fun(X : C.Obj)=>X, Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>f, Idn := fun(X : C.Obj)=>Eq.refl (C.Idn X),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>Eq.refl (C.Cmp X Y Z f g)}
def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : Fun C D) (G : Fun D E) : (Fun C E):=
{Obj := fun(X : C.Obj)=>(G.Obj (F.Obj X)),Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>(G.Mor) (F.Obj X) (F.Obj Y) ((F.Mor) X Y f),Idn := fun(X : C.Obj)=> ((Eq.trans) (congrArg (G.Mor (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>((Eq.trans) (G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Mor X Y f) (F.Mor Y Z g)) (congrArg (G.Mor (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))}
def CatId1 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F
def CatId2 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F
def CatAss (B : Cat) (C : Cat) (D : Cat) (E : Cat) (F : Fun B C) (G : Fun C D) (H : Fun D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) := Eq.refl (CatCmp B C E F (CatCmp C D E G H))
def Cats : Cat := {Obj := Cat,Hom := Fun,Idn := CatIdn,Cmp := CatCmp,Id1 := CatId1,Id2 := CatId2,Ass := CatAss}

def f (p : Prop) : Prop := ¬p
def g (n : Nat): Nat := n + 1

class Elephant (T : Type) where
  fn : T → T

instance prop_elephant : Elephant Prop where
  fn := f

instance int_elephant : Elephant Nat where
  fn := g

def elephant {T : Type} [E : Elephant T] (t : T) : T := E.fn t

#check elephant (2 : Nat)
#reduce elephant (2 : Nat)
#eval elephant (2 : Nat)

#check elephant True
#reduce elephant True

#check elephant (0 : Nat)

notation "𓃰" t => elephant t
#eval 𓃰 (2 : Nat)
def main := IO.println ""

This went in the Main.lean file in a lake project. Now I want to store that in its own file and import it as a ... package, I guess. I don't know anything about packages so I'll read up on the link you sent.

[Martin Dvořák]

If I understand correctly, you want them to be not just separate files but in different projects.
Then this is probably relevant: https://github.com/leanprover/lake/#syntax-of-require

[Arthur Paulino]

I'm not convinced that another project is the structure intended by the OP :thinking:
I suspect Kind Bubble just wants to factor out part of the code to a dedicated file

[Dean Young]

Oh right, yes different projects. Sorry I wasn't clear about that.

[Dean Young]

--Dean

[Martin Dvořák]

Are you @Kind Bubble aware that you can have more than just two files Main.lean and Project.lean in the same project?

[Dean Young]

Oh good question, that reminds me to explain what I'm after here:

I am looking to finish my first project and I want to put it away for a while. But ultimately, I would like to treat some files as libraries which I can import from elsewhere on the computer, in a different project entirely.

[Martin Dvořák]

It seems to me that Lake is not really intuitive to use. Are there any plans on expanding the VS Code plugin with "Add dependency" GUI?

[Dean Young]

I also wanted to make .lean files that my friends can import and use in their projects, and so they'd necessarily be different projects. I prefer running lean from the terminal in general. But you could be right that there's interest in that.

[Kevin Buzzard]

The only sensible way to distribute Lean files is as projects. A standalone Lean file cannot explain which version of Lean it works with; the point of a project is to do precisely this.

[Dean Young]

What files should a project contain? I wanted to make my own version of lake new and lake build.

Edit: I meant lean 4

[Dean Young]

linearlibrary.net

I am building something here which I'm going to get to run lean 4.

[Eric Wieser]

Running Lean4 in-browser and dealing with multiple packages in the absence of a real filesystem sounds like a big project of questionable utility. A glance at the source for your site suggests it has nothing relevant to that task so far, and we already have https://lean.math.hhu.de/ so the niche feels somewhat filled.

[Dean Young]

When I set out with this question I wanted a simple way to import the materials of a different project, but that looks impossible. So what is a package? Can someone explain how to create and import a package?

[Arthur Paulino]

1. Push your project to Github
2. On the downstream project, add the other project as a dependency

[Dean Young]

Ok thanks!

[Andrés Goens]

Arthur Paulino said:

1. Push your project to Github
2. On the downstream project, add the other project as a dependency

you can also just do it locally, without having to upload to github:

require foo from "path"/"to"/"local"/"package" with NameMap.empty