Lakefile — run for effect

Stream: new members

[Rob Simmons]

I have a piece of syntax in Main.lean that I defined for an effect (it writes a file) and I'd like lake build to run that file and produce that effect.

This doesn't work: it errors because there's no main

name = "leanvite"
defaultTargets = ["Main"]

[[lean_exe]]
name = "Main"
root = "Main"

This doesn't work: the file isn't run for its effect at all:

name = "leanvite"
defaultTargets = ["Main"]

[[lean_lib]]
name = "Main"
root = "Main"

is there a way to get the thing I'm looking for here?

[Eric Wieser]

You need to define a custom target; you could look at doc-gen4 for some quite complex examples of this

[Rob Simmons]

Hmm, ok!