Zulip Chat Archive

Stream: lean4

Topic: runFrontend on a lakefile.lean

Arthur Paulino (Jan 13 2023 at 18:56):

Hi all!
I'm trying to call runFrontend on a lakefile.lean and I'm getting errors like

lakefile.lean:4:0: error: unknown attribute [package]
lakefile.lean:6:0: error: unknown attribute [lean_lib]
lakefile.lean:6:2: error: unknown attribute [default_target]
lakefile.lean:13:0: error: unknown attribute [target]

Do I need to do some prior setup before being able to do that? How does Lake do it? Thanks!

Arthur Paulino (Jan 13 2023 at 18:58):

#xy: I want to build a helper CLI for bumping Lake packages and I don't want to implement weird workarounds for parsing lakefile.lean files, so I thought that calling the actual Lean 4 parser/compiler would be the correct way

Arthur Paulino (Jan 17 2023 at 15:51):

Bumping... I'm still stuck at this

Sebastian Ullrich (Jan 17 2023 at 16:04):

You might want docs4#Lean.enableInitializersExecution

Mac (Jan 17 2023 at 16:08):

Arthur Paulino said:

How does Lake do it?

See elabConfigFile. Also note that Lake sets the Lean search path before invoking that function (see here).

Arthur Paulino (Jan 17 2023 at 16:16):

Thanks! Will try later

Last updated: Dec 20 2023 at 11:08 UTC