## Stream: lean4

### Topic: user attributes

#### Yakov Pechersky (Apr 02 2021 at 17:21):

What's the correct syntax for defining a user attribute? The following code does not work for me

import Lean.Attributes
namespace Lean

builtin_initialize extAttr : TagAttribute ←
registerTagAttribute extAttr "mark at ext"

def hasExtAttribute (env : Environment) (n : Name) : Bool :=
extAttr.hasTag env n

end Lean

theorem Prod.Ext {p q : α × β} (h₁ : p.1 = q.1) (h₂ : p.2 = q.2) : p = q := by
cases p with | _ => ?_
cases q with | _ => ?_
simp_all

attribute [extAttr] Prod.Ext


#### Mario Carneiro (Apr 02 2021 at 17:23):

I don't think you are supposed to use the builtin_ version of things unless you are inside the lean 4 repo

#### Mario Carneiro (Apr 02 2021 at 17:23):

unfortunately that means examples of the user facing version are hard to find

#### Yakov Pechersky (Apr 02 2021 at 17:26):

initialize ... doesn't work either

#### Bryan Gin-ge Chen (Apr 02 2021 at 17:46):

This was asked a while ago; I'm not sure if things have changed since then: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/How.20to.20add.20user.20attributes.3F

#### Mario Carneiro (Apr 02 2021 at 17:51):

I've been looking at the source and I can't figure out why the posted code (with initialize in place of builtin_initialize) doesn't work

#### pcpthm (Apr 02 2021 at 17:52):

I think initialize should be used inside a plugin like <https://github.com/leanprover/lean4/tree/master/tests/plugin>.

#### Sebastian Ullrich (Apr 02 2021 at 17:55):

Try applying it in a different file

#### Yakov Pechersky (Apr 02 2021 at 17:57):

failed to register environment, extensions can only be registered during initialization


#### Yakov Pechersky (Apr 02 2021 at 17:58):

That's after making a separate src/Attribute/Ext.lean with

import Lean.Attributes

open Lean

initialize extAttr : TagAttribute ←
registerTagAttribute extAttr "mark at ext"

def hasExtAttribute (env : Environment) (n : Name) : Bool :=
extAttr.hasTag env n


and then in src/Tactic/Ext.lean

import src.Attribute.Ext -- failed to register environment, extensions can only be registered during initialization [1, 1]

theorem Prod.Ext {p q : α × β} (h₁ : p.1 = q.1) (h₂ : p.2 = q.2) : p = q := by -- unknown constant 'sorryAx' [3, 1]; expected token [3, 27]
cases p with | _ => ?_
cases q with | _ => ?_
simp_all

attribute [extAttr] Prod.Ext -- unknown attribute [extAttr] [8,1]


#### Mario Carneiro (Apr 02 2021 at 17:59):

How do you import relative paths like import ..foo ?

#### Mario Carneiro (Apr 02 2021 at 18:00):

apparently lean --make doesn't exist anymore either... my approach of having a single test.lean file in the lean 4 source repo isn't scaling

#### Sebastian Ullrich (Apr 02 2021 at 18:02):

You need to use leanpkg and absolute imports for multiple files

#### Sebastian Ullrich (Apr 02 2021 at 18:03):

@Yakov Pechersky That... might be a bug or simply unimplemented behavior. I'd have to take a closer look at it at some other time.

#### Yakov Pechersky (Apr 02 2021 at 18:04):

Sure thing, no rush. Thanks for taking a look whenever!

#### Mario Carneiro (Apr 02 2021 at 18:04):

How do absolute imports work if I want out of the root directory?

#### Mario Carneiro (Apr 02 2021 at 18:05):

all my imports seem to be coming from some .elan directory

#### Mario Carneiro (Apr 02 2021 at 18:06):

also what's import runtime?

#### Daniel Selsam (Apr 02 2021 at 18:08):

@Mario Carneiro FYI I use vanilla Makefiles and manage my own paths -- in particular, I don't use leanpkg or elan or leanmk or nix. I import files from different directories/modules all the time and my workflow is smooth. Happy to share details if you are interested.

#### Mario Carneiro (Apr 02 2021 at 18:09):

that sounds good to me, I don't like build tools until I can do it by hand

#### Daniel Selsam (Apr 02 2021 at 18:17):

(typing in emacs, will paste when done)

#### Daniel Selsam (Apr 02 2021 at 18:24):

• Lean4

• build <path-to-lean4>/build/release in Release mode
• build <path-to-lean4>/build/debug in Debug mode
• symlink <path-to-lean4>/build/release to <path-to-lean4>/build/current
• (this process is not necessary but makes it easy to swap release/debug when needed)
• Environment variables:

• LEAN4_DIR=<path-to-lean4>/build/current/stage1/
• LEAN_PATH=$LEAN4_DIR/lib/lean • For each project Foo located at <path-to-foo>: • create <path-to-foo>/Makefile PKG = Foo include$(LEAN4_DIR)/share/lean/lean.mk

all: $(BIN_OUT)/test$(BIN_OUT)/test: $(LIB_OUT)/libFoo.a |$(BIN_OUT)
c++ -rdynamic -o $@$^ leanc -print-ldflags


- create <path-to-foo>/Foo.lean and define main : IO Unit in it
- create other files inside the <path-to-foo>/Foo directory, e.g. <path-to-foo>/Foo/Bar/Rig.lean
- In <path-to-foo>, make should now build Foo.lean and all lean files in Foo/
- after your first make (which creates the build directory), concatenate :<path-to-foo>/build to LEAN_PATH
- rough edge: if you make clean and try to remake, you will need to locally change the path during the call to make to avoid importing from the build/ directory you are creating

• For every project whose build/ directory has been added to your LEAN_PATH, you can now import:
• import Foo.Bar.Rig
• (this includes Foo modules importing files within Foo)

#### Sebastian Ullrich (Apr 02 2021 at 20:15):

Mario Carneiro said:

that sounds good to me, I don't like build tools until I can do it by hand

leanpkg prints out every step it's executing

Last updated: May 07 2021 at 13:21 UTC