deleting lakefile.olean

Stream: general

[Jon Eugster]

@Mac Malone , I wonder if lake update (and lake clean) should always delete the lakefile.olean and recreate it?

Before the introduction of the lakefile.olean I had an env variable to switch between a local copy of a dependency or downloading it. As expected, when calling lake update, it would reevaluate the lakefile, choose the right one and update the lake-manifest.json. Now, however, lake update does nothing and I have to resort to rm lakefile.olean && lake update to get a "clean" update. My understanding is that lakefile.olean is a performance optimisation when calling lake (e.g. lake build etc). However, I believe lake update (and lake clean) is only rarely used and getting a consistent result would be much more important than performance.

Here's the relevant lakefile:

Example

I know this is a bit hacky again, but one thing I really like about lake is exactly that you can put some lean code in the lakefile :)

import Lake
open Lake DSL


def LocalGameServer : Dependency := {
  name := `GameServer
  src := Source.path "../lean4game/server"
}

def RemoteGameServer : Dependency := {
  name := `GameServer
  src := Source.git "https://github.com/leanprover-community/lean4game.git" "main" "server"
}

-- do something depending on the env variable `MY_ENV_VAR`
open Lean in
#eval (do
  let gameServerName := if ((← IO.getEnv "MY_ENV_VAR") == "local") then ``LocalGameServer else ``RemoteGameServer
  modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
  : Elab.Command.CommandElabM Unit)

package «TestProject»
lean_lib «TestProject»

[Mac Malone]

@Jon Eugster A cleaner alternative to rm lakefile.olean && lake update is lake update -R (where -R is short for --reconfigure).

Whether re-elaborating the file should be the default for lake update and lake clean is curious question. From a purely performance angel, you are right that the time save is probably doesn't matter to much for commands like lake update and lake clean that are unlikely to invoked frequently. However, lakefile.olean is not purely a performance optimization, it also saves the Lake configuration options (e.g. -K) and other environment-based state. In your case, you do not want that, but in other circumstances this can be quite useful (e.g., to fix a state to be used by the Lean language server in VS Code.)

I am inclined to believe that do the fast thing by default and the slower thing by request (via -R) is generally a good default. However, I am open to being persuaded otherwise.

[Mario Carneiro]

I continue to be hit by olean compatibility issues with lakefile.olean, especially in lean 4 core. I'm hoping your recent work on tightening this up will help, but I'd rather have stable behavior at the cost of some performance loss

[Scott Morrison]

Moreover, saving state in an olean seems like a dangerous idea to begin with, especially if you need to know magic options to clean to reset it!

[Jon Eugster]

Thanks, -R is indeed useful!

[Jon Eugster]

Jon Eugster said:

Before the introduction of the lakefile.olean I had an env variable to switch between a local copy of a dependency or downloading it.

I just realised staring at mathlib's lakefile, that rather than setting an environment variable, the "intended way" would probably be to use the -K that Mac mentions above: lake update -K my.config.option -R and then if get_config? my.config.option |>.isSome then _ else _inside the lakefile.lean. Still needs the -R to have any effect.

I couldn't find -K in the lake docs yet, although it does appear under lake --help. Therefore I thought I leave a note to future me here.