feat(leanpkg): Teach leanpkg to preserve new 'olean_url' field

[bentoner]

We want to create an olean cache for LTE. A project needs to be able to record somewhere the location of the olean cache and @PatrickMassot proposes to do this in leanpkg.toml - see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/CI.20for.20liquid.20tensor.20experiment/near/244008489 . The issue is that leanpkg will not preserve this field on e.g. upgrades. This pull request causes leanpkg to preserve but otherwise ignore this new field.

[bentoner]

Hi Gabriel, this isn't ready to be merged.

Per the chat in Zulip with Patrick, which I'll repeat here, we need to decide how to proceed. I see at least 3 options:

1. Proceed as per this pull request. This results in minimal changes to leanpkg, but it is not so nice because now leanpkg has to know about the olean_url field even though it doesn't do anything with it.
2. Extend leanpkg to preserve but ignore fields in leanpkg.toml that it doesn't understand. This seems nicer but we lose the benefits of having a schema.
3. Not make any changes to leanpkg. We can tell users to avoid it and use leanproject instead.

I'm fine with any of the above (or whatever else you/Patrick prefer).

Secondly, I realize my implementation of option 1 is incomplete, as described on zulip, which is the other reason why this isn't ready to be merged. I'll fix this later tonight so there's something concrete to decide on.

[gebner]

I think you should be aware that Lean 3 (and leanpkg and leanproject) is pretty much on life support mode now. I hope that a year from now we'll have mostly moved over to Lean 4, and I'd be surprised if anybody uses Lean 3 two years from now. Keep that in mind when putting a lot of effort into Lean 3 tooling.

I'm happy with all of the options you've listed. I think the cleanest approach would be to just reimplement the remaining two(?) commands in leanproject and forget about leanpkg.

This seems nicer but we lose the benefits of having a schema.

The benefits of being able to store extra information in the leanpkg.toml file outweigh the untidyness of lacking a schema in my opinion.

[bentoner]

Hi Gabriel.

I think the cleanest approach would be to just reimplement the remaining two(?) commands in leanproject and forget about leanpkg.

Okay, let's do that then -- I'll close this. Thanks!