lake force rebuild

Stream: lean4

[Jon Eugster]

I have a slight problem with my translation package.

Currently it runs the string-extraction the way that there is a command #export_i18n in Project.lean, so that at the end of lake build, it also runs this and saves the files ready for translation.

However, this reads a config.json file, so if I just change some configs and run lake build, nothing happens. I actively have to either modify Project.lean or delete .lake for a rebuild to happen.

What could I do? Is there (a) a post-build-hook for lake, or (b) a way to make it somehow that the hash of config.json is important in the decision that the entire project should be rebuilt, or (c) a way to force rebuilding a file/project, even if .oleans exist?

(an alternative is to just use a lake exe ... command, maybe I resort to that if there is no automated way)

[Jon Eugster]

After reflection, I think lake exe ... is the most reasonable thing to use, actually. (especially since I assume the answer to everything else is "no")

[Mac Malone]

Jon Eugster said:

Is there (b) a way to make it somehow that the hash of config.json is important in the decision that the entire project should be rebuilt.)

There is! It is called extraDepTargets. For example,

package foo where
  extraDepTargets := #[`config]

target config pkg : FilePath :=
  inputFile <| pkg.dir / "config.json"

This will rebuild the package every time a file namedconfig.json in the package's directory changes.

[Jon Eugster]

oh amazing, thanks! Didn't know about that