Envvar dependency path

Stream: lean4

[Leni Aniva]

Is it possible to use an environment variable as the path to a dependency in lakefile.{toml,lean}, as opposed to a git hash?

[Mac Malone]

I am not quite sure what you mean. Perhaps require ... from run_io IO.getEnv "PKG_PATH" would do what you want in lakefile.lean?

[Leni Aniva]

Mac Malone said:

I am not quite sure what you mean. Perhaps require ... from run_io IO.getEnv "PKG_PATH" would do what you want in lakefile.lean?

this is perfect

[Leni Aniva]

wouldn't this interfere with the lock file?

[Mac Malone]

Yes. One would need to run lake -R update <env-pkg-name> whenever the locked path should change.

[Leni Aniva]

well this couldnt be used with nix then

[Mac Malone]

It is also possible to just remove the environment-dependent dependency from the lockfile-- then it will always follow the configured path. The configuration itself is also cached, so Lake would need to be run with lake -R whenever it should recheck the enviroment (by reconfiguring).

[Mac Malone]

(The reason for all this caching is that Lake is aiming for eproducible builds and thus attempts to avoid dynamic, shifting state.)