user attributes

Stream: lean4

[Yakov Pechersky]

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]

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

[Mario Carneiro]

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

[Yakov Pechersky]

initialize ... doesn't work either

[Bryan Gin-ge Chen]

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]

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]

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

[Sebastian Ullrich]

Try applying it in a different file

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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

[Mario Carneiro]

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]

You need to use leanpkg and absolute imports for multiple files

[Sebastian Ullrich]

@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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

also what's import runtime?

[Daniel Selsam]

@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]

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

[Daniel Selsam]

(typing in emacs, will paste when done)

[Daniel Selsam]

• 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]

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

[Jannis Limperg]

FYI user attributes (and more generally user env extensions) are implemented now. :tada:

https://github.com/leanprover/lean4/commit/cdd1dbbb36ce06608352e5d8ccf21089b2d4e91a
https://github.com/leanprover/lean4/commit/a77598f7cfcb058da41cf3af8a7120aeca68fe8c

Be aware of this little issue though.