Listing Lake facets?

Stream: lean4

[Siddharth Bhat]

It seems the doc facet from doc-gen4 was renamed to docs, and I only discovered this thanks to @Henrik Böving reading the sources.

How does one actually list all targets / facets available from lake?

CC @Mac Malone

[Henrik Böving]

In fixing this I discovered a (I claim) bug.

Say that you have a lakefile.lean configured with doc-gen like so:

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

on leanprover/lean4:v4.3.0-rc1

Now you compile your package normally with lake build. Then you decide that you wish to build docs so you run:

λ lake -Kenv=dev build Std:docs
error: unknown library facet `docs`

Well that's confusing :), after a bit of tinkering I figured out I can run:

λ lake -Kenv=dev -R build Std:docs

and this works. So forcing lake to re-elaborate the cached config file apparently ends up working? is this a caching bug or intended? I can hardly imagine stuff like this is on purpose right?

[Jon Eugster]

@Mac Malone explained the -R option to me here a few days ago: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deleting.20lakefile.2Eolean

and I understood the explanation that it is intended design and you should liberally use lake -R everywhere now.

[Mac Malone]

The issue here is a design decision that I delayed. Namely, what should Lake do when -K is passed with an existing saved configuration without -R. I see two solutions to the current confusion:

1. Automatically reconfigure with the new options. To unset options, though, -R would still be needed.
2. Ignore the options and produce an error if -R is not passed.

Presently, as mentioned in v4.1.0 release notes, the options are just ignored. I am currently inclined to see (2) as the proper solution as it does not produce an incongruency between when no-option and some-option configurations are reconfigured.

[Mac Malone]

(One thing to note is the saved configuration is not meant solely as a cache is is also meant to save the full state including options for future lake commands -- like the server -- so they do not have to be repeated.)

[Jon Eugster]

Would in (1) mean that

lake -KoptA build
lake -KoptB build

results in both options being set in the second build? That would indeed sound confusing, while (2) sounds helpful and instructive.

[Siddharth Bhat]

Automatically reconfigure with the new options. To unset options, though, -R would still be needed.

@Mac Malone in my mind, as an end-user, this is what I would expect to see:

/* clean state */
lake -KoptA build (1) -- lake builds a cache with `optA`
lake -KoptB build (2) -- lake flushes cache, rebuilds cache w/ `optB`
/* project changes */
lake -KoptB build (3) -- lake reuses prior cache

[Mac Malone]

@Siddharth Bhat what do you expect lake build (with no -K) to do in each of those circumstances?

[Siddharth Bhat]

/* clean state */
lake build (1) -- lake builds a cache with `no options`
lake build (2) -- lake reuses prior cache (env did not change)
/* project changes */
lake build (3) -- lake reuses prior cache (env did not change)

I feel like I'm missing something here?

[Henrik Böving]

Mac Malone said:

Siddharth Bhat what do you expect lake build (with no -K) to do in each of those circumstances?

Can't you load the lake state (if it's there) and check if your -Ks match the one that the cached state knows about? That should be very cheap to compare correct? And based on the result of that you can either keep going or re-elaborate.

[Mac Malone]

@Siddharth Bhat Sorry, no , I mean the following:

lake build -KoptA -- saved iwth `optA`
lake build -- does this have `optA` or not?

[Henrik Böving]

Doesn't have it IMO

[Henrik Böving]

You could run these commands far apart from each other and have completely forgotten about the fact that you ran with different options before

[Mac Malone]

Ah, in that case, the goal here is different. The point of the current design is to enable saving options (and environment state) so they do not have to be repeated -- not solely a cache.

[Mac Malone]

That is:

ENVA=foo lake buld -KoptA=bar -KoptB=baz ...
lake serve -- should run with previous options

[Mac Malone]

Configuration options are not meant to generally vary per command, but be an initial configuration set like Cargo features or CMake options.

[Henrik Böving]

Shouldn't behavior that persists across invocations be part of a human readable config file instead of a binary blob?

Mac Malone said:

Configuration options are not meant variant per action, but an initial configuration set like Cargo features.

Cargo features too are passed to libraries in plain text in Cargo.toml instead of some hidden thingy

[Siddharth Bhat]

Mac Malone said:

Configuration options are not meant variant per action, but an initial configuration set like Cargo features or CMake options.

I was going to say, the only build system that I know of with similar behavior is CMake, and I personally dislike the CMakeCache.

[Mac Malone]

Henrik Böving said:

Cargo features too are passed to libraries in plain text in Cargo.toml instead of some hidden thingy

Yes. to downstream packages. But, for the root package, they are passed via CLI. (As they in both cases in Lake.)

[Siddharth Bhat]

Mac Malone said:

Henrik Böving said:

Cargo features too are passed to libraries in plain text in Cargo.toml instead of some hidden thingy

Yes to downstream packages, but they are not to the root package (they are passed via CLI (as they in both cases in Lake.)

Wow, I did not know this about cargo :sob:

[Mac Malone]

Oh, well here are the docs on Cargo's features.

[Siddharth Bhat]

Siddharth Bhat said:

Mac Malone said:

Henrik Böving said:

Cargo features too are passed to libraries in plain text in Cargo.toml instead of some hidden thingy

Yes to downstream packages, but they are not to the root package (they are passed via CLI (as they in both cases in Lake.)

Wow, I did not know this about cargo :sob:

@Mac Malone I understood this to mean that cargo build also holds onto invisible, mutable state across executions based on command line configuration flags. Is that right?

[Mac Malone]

Kind of, if you run cargo build --feature blah and then cargo test, it is my understanding the feature will be invisibly preserved.

[Siddharth Bhat]

I understand test (and lake serve, FWIW) choosing to reuse the build configuration, but do two invocations of

cargo build --feature blah
cargo build # does this implicitly imply `--feature`?

[Henrik Böving]

Mac Malone said:

Kind of, if you run cargo build --feature blah and then cargo test, it is my understanding the feature will be invisibly preserved.

I gotta admit, I have never seen that a person set a cargo feature from the command line so I wouldn't know.

[Henrik Böving]

I'm gonna check this behavior

[Siddharth Bhat]

To be productive, another solution that I would be happy with is:

lake configure -KoptA=valA
lake build # has optA=valA
lake configure -KoptB=valB
lake build # has optB=valB
lake configure --append -KoptC=valC
lake build # has optB=valB, optC=valC

[Jon Eugster]

Mac Malone said:

lake build -KoptA -- saved iwth `optA`
lake build -- does this have `optA` or not?

Although I didnt realise immediately, I think my use case actually aligns with your currently implemented solution, namely that it keeps the option ever after

i.e. I am running

lake update -R -Kuse.local.dev.depend
lake build -- potentially repeatedly after changes

[Mac Malone]

@Henrik Böving Admittedly, I have not verified the preserved state either. But I am not sure what else it would do. Furthermore, you can also set features via environment variables which definitely can be preserved across commands.

[Mac Malone]

Siddharth Bhat said:

To be productive, another solution that I would be happy with is:

lake configure -KoptA=valA
lake build # has optA=valA
lake configure -KoptB=valB
lake build # has optB=valB
lake configure --append -KoptC=valC
lake build # has optB=valB, optC=valC

Yes, this is the final intention.

[Siddharth Bhat]

Siddharth Bhat said:

To be productive, another solution that I would be happy with is:

lake configure -KoptA=valA
lake build # has optA=valA
lake configure -KoptB=valB
lake build # has optB=valB
lake configure --append -KoptC=valC
lake build # has optB=valB, optC=valC

I prefer this, because it's clear to me which options mutate this hidden state, and which operations keep the mutable state.

[Mac Malone]

Me too. -R and the current auto-configure just exist to reduce the number of commands required to perform a build, which I know is a goal of a lot of the math people. (And the lack of configure is just due to backlog.)

[Henrik Böving]

Mac Malone said:

Henrik Böving Admittedly, I have not verified the preserved state either. But I am not sure what else it would do. Furthermore, you can also set features via environment variables which definitely can be preserved across commands.

Cargo does not act like this:

λ cat Cargo.toml src/main.rs
[package]
name = "mine"
version = "0.1.0"
edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
[features]
hello = []
world = []
fn main() {
    #[cfg(feature = "hello")]
    println!("Hello");
    #[cfg(feature = "world")]
    println!("World");
}

λ cargo run
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
     Running `target/debug/mine`
λ cargo run --features hello
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
     Running `target/debug/mine`
Hello
λ cargo run
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
     Running `target/debug/mine`
λ cargo build --features world                                                      <<<
   Compiling mine v0.1.0 (/home/nix/Desktop/rust/mine)
    Finished dev [unoptimized + debuginfo] target(s) in 0.14s
λ cargo run
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
     Running `target/debug/mine`
λ cargo run --features world
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
     Running `target/debug/mine`
World

[Mac Malone]

@Henrik Böving From its output, It does not recompile, so how is that working? What happens when you run the binary directly?

[Mac Malone]

I suspect is is performing a runtime check on the environment variable.

[Henrik Böving]

ligurien:~/Desktop/rust/mine|master
λ cargo build --features world
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
ligurien:~/Desktop/rust/mine|master
λ cargo build                                                                       <<<
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
ligurien:~/Desktop/rust/mine|master
λ ./target/debug/mine
ligurien:~/Desktop/rust/mine|master

Nothing, I think it might just be so fast to recompile that it doesn't even measure it properly? Unclear.

[Henrik Böving]

That said it seems to keep a bunch of incremental build artefacts around:

λ tree target
target
├── CACHEDIR.TAG
└── debug
    ├── build
    ├── deps
    │   ├── libmine-5599a1cf35f8afea.rmeta
    │   ├── libmine-59cdf6782576d786.rmeta
    │   ├── mine-24043507f9f731c1
    │   ├── mine-24043507f9f731c1.d
    │   ├── mine-5599a1cf35f8afea.d
    │   ├── mine-59cdf6782576d786.d
    │   ├── mine-b90cc72d39bcb107
    │   ├── mine-b90cc72d39bcb107.d
    │   ├── mine-fa080969f27f2053
    │   └── mine-fa080969f27f2053.d
    ├── examples
    ├── incremental
    │   ├── mine-1zvd1w7zv712t
    │   │   ├── s-gqlhvcegw5-16eq0ds-8nk6kh24miwfpb1pzvk2tvn5y
    │   │   │   ├── 1aq49z2q662ja0ge.o
    │   │   │   ├── 2379j1b0m5z0emoj.o
    │   │   │   ├── 5edpcnpjgyvidush.o
    │   │   │   ├── dep-graph.bin
    │   │   │   ├── fknko5h9wjn6cpi.o
    │   │   │   ├── hasfm8b61wclylo.o
    │   │   │   ├── query-cache.bin
    │   │   │   └── work-products.bin
    │   │   └── s-gqlhvcegw5-16eq0ds.lock
    │   ├── mine-20tbrvg6e9x35
    │   │   ├── s-gqlhvqnmnb-17305wh-dzz0ltxkn6fcku5hf8vnzjjz2
    │   │   │   ├── 2jsfb0ftzpbd2fw5.o
    │   │   │   ├── 3w3rfdw356hqahie.o
    │   │   │   ├── 478gw85nnras31zs.o
    │   │   │   ├── 4cxzivuuj1mj9q34.o
    │   │   │   ├── 5cyrdqmow68ul05g.o
    │   │   │   ├── c2kgn36td7i1k0b.o
    │   │   │   ├── dep-graph.bin
    │   │   │   ├── query-cache.bin
    │   │   │   └── work-products.bin
    │   │   └── s-gqlhvqnmnb-17305wh.lock
    │   ├── mine-38vnh5ay7usv9
    │   │   ├── s-gqlhwwstd2-1yriovp-8ivc1fwn2n1t4n8m4z20qwah2
    │   │   │   ├── 17ti41rx9l3ccxnt.o
    │   │   │   ├── 1onbuctrgru0i7vp.o
    │   │   │   ├── 2xnxudfgrhbx0jrp.o
    │   │   │   ├── 4dj41tw4kzqki0j3.o
    │   │   │   ├── 4o0x0pmg72xo4frm.o
    │   │   │   ├── dep-graph.bin
    │   │   │   ├── query-cache.bin
    │   │   │   ├── sxaptfaomtf93r7.o
    │   │   │   └── work-products.bin
    │   │   └── s-gqlhwwstd2-1yriovp.lock
    │   ├── mine-ag5rbzj8rkgv
    │   │   ├── s-gqlhv2q8aq-jjezk6-9my3xbkn24r0n3jquoectweo3
    │   │   │   ├── dep-graph.bin
    │   │   │   ├── query-cache.bin
    │   │   │   └── work-products.bin
    │   │   └── s-gqlhv2q8aq-jjezk6.lock
    │   └── mine-qpilry2ztwwh
    │       ├── s-gqlhv2q8bw-pvkqvc-1rmlythn49ud8oged19szgckq
    │       │   ├── dep-graph.bin
    │       │   ├── query-cache.bin
    │       │   └── work-products.bin
    │       └── s-gqlhv2q8bw-pvkqvc.lock
    ├── mine
    └── mine.d

I would not be surprised if these are for different feature constellations

[Mac Malone]

@Henrik Böving What does the following do?

λ cargo build --features world
λ ./target/debug/mine

[Henrik Böving]

λ cargo build --features world
    Finished dev [unoptimized + debuginfo] target(s) in 0.00s
ligurien:~/Desktop/rust/mine|master
λ ./target/debug/mine
World

If that would have been any different I would have thrown Rust right out of the window.

[Mac Malone]

@Henrik Böving Okay, so it appears Cargo does require you specify the options at each step but it stores the results for different configurations separately so it can easily switch between them. Whereas, e.g., CMake saves a single configuration. So it is a question of space and repeativeness.

[Mac Malone]

Personally, I like the configure then build, run, etc. approach more than the repeat the configuration at each step.

[Mac Malone]

Technically, it also makes save a configuration to be used by the server easier than having to configure it separately via options in the extension.

[Mac Malone]

Actually, that raises a question. Does Rust/Cargo's VS Code extension have a features option?

[Siddharth Bhat]

@Mac Malone I would prefer the transient behaviour (before we get to the separate lake configure that modifies configuration and lake build that builds) to be like cargo.

[Mac Malone]

@Siddharth Bhat Well, each require about the same amount of time to add, so I would probably just add lake configure.

[Henrik Böving]

Right if we make this with lake configure I think it's cool, I merely found the idea of setting an option while build-ing very unintuitive.

On a more general note: Are we planning on having a rust style dev-dependencies type of thing?

[Mac Malone]

Henrik Böving said:

I merely found the idea of setting an option while build-ing very unintuitive.

Agreed. As I mentioned, this was mostly a compromise to just allow simple one liners for math users and me just not finding the time to also add lake configure. :sweat_smile:

[Mac Malone]

Henrik Böving said:

On a more general note: Are we planning on having a rust style dev-dependencies type of thing?

What do you mean? How are you envisioning this to be different from the current meta if?

[Henrik Böving]

Well dev-dependencies is a more implicit thing in cargo. Basically you have two lists of dependencies the [dependencies] and the [dev-dependencies] one. dependencies are the one your consumers get to see (they can also be gated behind feature gates) dev-dependencies are automatically activated (note the word activated, they don't have to be compiled, like e.g. doc-gen) if the Cargo thing you are building is the root module (I am not sure how it interacts with workspaces) So what you commonly see in the cargo world is that you declare testing frameworks, benchmarkings etc. as dev-dependencies so that only your developers have to build them.

It is not really semantically different from a feature and could well be emulated by it but it is a whole lot easier to use due to its implicit nature and improved usability I would say. Both of these (especially the improved usability with respect to meta if config.... would be present in lake as well

[Henrik Böving]

Another thing that I've been thinking about: It would be pretty nice if we had a global cache for package source downloads like cargo does. I've gotten like half a dozen mathlibs laying around by now, my poor hard drive ^^

[Ruben Van de Velde]

Are they the same version of mathlib, though?

[Henrik Böving]

at least 3 of them are very close to each other although I don't know if they are the same.

That said, given the fact that we check them out as git repos and do not (yet) distribute them as source packages should allow us to share regardless.

[Mac Malone]

Henrik Böving said:

Both of these (especially the improved usability with respect to meta if config.... would be present in lake as well

One current plan is to replace meta if cond then require ... with require ... if cond. I could also add an isRoot util for determining if a package is the root package. Thus, requiring doc-gen could work like require doc-gen4 if isRoot ... Would that be ergonomic to you? Or would you prefer something like require dev doc-gen4?

[Henrik Böving]

I think that's much better than the meta if thing already, if it comes down to it we could always add the require dev later :thumbs_up:

[Scott Morrison]

Siddharth Bhat said:

... which options mutate this hidden state, and which operations keep the mutable state ...

I would prefer to not have any mutatable hidden state in the first place? All state should be in human readable text files.

[Siddharth Bhat]

Scott Morrison said:

Siddharth Bhat said:

... which options mutate this hidden state, and which operations keep the mutable state ...

I would prefer to not have any mutatable hidden state in the first place? All state should be in human readable text files.

That would be nice, but in the interest of balancing usability with purity... :smile:

[Scott Morrison]

I don't think there's a usability question here at all, is there?

[Scott Morrison]

The only reason this mutable hidden state exists at all is the lakefile.olean trick, which was introduced solely as a performance workaround.

[Siddharth Bhat]

Scott Morrison said:

I don't think there's a usability question here at all, is there?

Hm, so the suggestion would be that these are in some kind of toml configuration file that lake reads? Sure, that works for me. It might still be nice to have CLI commands to edit this file via lake configure.

[Mac Malone]

Scott Morrison said:

The only reason this mutable hidden state exists at all is the lakefile.olean trick, which was introduced solely as a performance workaround.

I am not sure what qualifies as "mutable hidden state" here. The entire build system involves what I would call 'mutable hidden state" (build artifacts are a kind of mutable state and they are not all transparent and things like the trace files are especially so).

[Mario Carneiro]

Build caches are an acceptable form of mutable state only because they do not change the result of any command, only the amount of time required to run the command. Mutable state that changes the result of later commands is IMO unacceptable, unless it is stored in plain text files or at least has a very clear and well documented CLI interface for showing and setting the state. As far as I know there is no such state in cargo.

[Mario Carneiro]

(For example, elan/rustup has caches for toolchains, and mutable state for setting toolchain overrides and the default toolchain, but there are very explicit commands for displaying what the current state is and many of the other commands remind you what the current state is. Even so this mutable state can trip people up.)

[Mario Carneiro]

If you want to set features (for the root project) in cargo, you do actually have to pass --feature=foo to every single cargo command you run, if you forget one then it will recompile the project without the feature.

[Mario Carneiro]

Normally what I will do if this gets too annoying is modify Cargo.toml to set the default features to what I am using ATM, and try not to commit it

[Mac Malone]

Mario Carneiro said:

Build caches are an acceptable form of mutable state only because they do not change the result of any command, only the amount of time required to run the command.

Given that one can run arbitrary IO in a Lean file rebuilding or not can easy change the result of a command. Lake (and Cargo in build scripts) can also do additional arbitrary actions on build which can save and store state, so it seems weird to me to assume that no state exists.

[Mario Carneiro]

you shouldn't make the problem any worse than it already is

[Mario Carneiro]

yes, build scripts can do arbitrary IO, but people writing build scripts should "know what they are doing" and in particular should know that they are not always called and should try to act as though they don't have any mutable state besides caches because otherwise lake will act strangely

[Mario Carneiro]

if they don't do so and weird things happen, the fault lies with the build script doing shenanigans

[Mario Carneiro]

It's not that "no state exists", it's that the presence of this state should not affect end user behavior. If it does, it becomes an additional thing the user has to think about and they can't just blindly run lake build to get everything in a coherent state anymore, now they are doing some maze solving with lake commands as the actions

[Sebastian Ullrich]

Gentle reminder that one very similar hidden mutable state, elan toolchain override, has turned out to be a terrible idea and desperately wants to be replaced with a file-based solution that one can actually see in git status

[Mac Malone]

Mario Carneiro said:

they can't just blindly run lake build to get everything in a coherent state anymore, now they are doing some maze solving with lake commands as the actions

A user can still nuke .lake to blindly get back to a fully fresh state. IMO the big problem with elan toolchain override was that the state was not in the directory it controlled but rather part of the central configuration. If there was a file anywhere in the directory, even ignored, one could look for to indicate that there was an override much of the confusion would have been mitigated.

[Mario Carneiro]

no, that is not good enough

[Mario Carneiro]

that's just saying that you can make a mess with the state

[Mario Carneiro]

"you can always just throw the maze away and reset"

[Mario Carneiro]

the goal here is not to delete all state, and if the user needs to do this then they will be deleting a lot of state that they would prefer not to (like build caches) in order to fix the mutable state that is causing the problem

[Mario Carneiro]

your usage of the term "nuke" already underscores this, it is a simple but very destructive solution to a problem with many downsides

[Mac Malone]

Scott Morrison said:

All state should be in human readable text files.

One thing I forgot to note is that with lean4#2842, the options used to produce the lakefile.olean will be in a human-readable text file (lakefile.olean.trace).

[Mac Malone]

Mario Carneiro said:

the goal here is not to delete all state, and if the user needs to do this then they will be deleting a lot of state that they would prefer not to (like build caches)

If the user wants to be more precise, they could just delete the compiled configuration files (e.g., lakefile.olean) or just use the -R to regenerate it. My point with the nuking is that if one wants to make sure any and all potential state is cleared for a specific project, they can nuke the whole .lake directory.

[Mario Carneiro]

Mac Malone said:

Scott Morrison said:

All state should be in human readable text files.

One thing I forgot to note is that with lean4#2842, the options used to produce the lakefile.olean will be in a human-readable text file (lakefile.olean.trace).

Thanks, although I think this is a really bad name for it, .trace files are currently hashes of the corresponding file so one would not expect it to be human readable, plus this is not a "trace of the olean of the lakefile", this is "default configuration options" and it should have a name reflecting that like lake-config.json or whatever format it is in

[Mario Carneiro]

Mac Malone said:

If the user wants to be more precise, they could just delete the compiled configuration files (e.g., lakefile.olean) or just use the -R to regenerate it. My point with the nuking is that if one wants to make sure any and all potential state is cleared for a specific project, they can nuke the whole .lake directory.

Unless I specifically opt in to having sticky mutable state hanging around, I don't want to have to deal with it! Where's the sticky mutable state to make -R the default? (But without having to pay a performance cost for doing so.)

[Mario Carneiro]

lakefile.olean is a cache file, nothing more. Please don't make it more than that

[Scott Morrison]

I don't want to hold up https://github.com/leanprover/lean4/pull/2842 on this question, because I really want it in before cutting rc2.

[Scott Morrison]

But I agree:

• a .trace file should not be storing options!
• lakefile.olean is a workaround for a performance issue (perhaps a fundamental one without moving to a toml file for simple configurations, but nevertheless), and we should not make it bear any more weight than it absolutely has to
• there should be as little mutable state as possible in the system

[Mario Carneiro]

I don't think these are blocking issues for lean4#2842, the new version is not any worse than what already exists

[Mario Carneiro]

how about a .lakeopts file which contains -K options (and is a human readable and writable text file) that is implicitly passed to every lake invocation in the containing folder?

[Mario Carneiro]

If you don't have such a file, there is no mutable state, if you do there is still no implicit mutable state since this file is never edited by lake

[Mario Carneiro]

the fact that you can create such a file is squirreled away in an "advanced options" section so that it doesn't cause problems for the 90%