CI for liquid tensor experiment

Stream: general

[Johan Commelin]

Hey all, a post about the liquid tensor experiment in #general. I'm looking for some help with CI thingies. We have CI that builds the project, but I would like to have two other things:

1. Setup CI to check that thm95 stays sorry-free lean-liquid#37
2. Setup olean caches lean-liquid#38

Regarding (1). I think Mario at some point posted some meta code that checks which axioms are used by some decl. We would want to use something like that.
If you want to help out with one of these, that would be great!

[Johan Commelin]

We clearly also need to enable the unused_arguments linter.

[Johan Commelin]

I'm still looking for some help here. Especially (1) would be great to get working. Because if we start working on the second part of the project, we'll want to add sorry again, and it's great if we can easily certify that this doesn't affect the first milestone.

[Ben Toner]

@Johan Commelin I'm happy to help with this. Some questions:

1. Is it okay to use the same Azure account for olean storage that mathlib uses? If so, can a maintainer (who is the right person to ping?) please create a lean-liquid container and add the SAS URL as the AZURE_SAS_TOKEN secret to the lean-liquid repository.
2. The Azure clean up script may need modification. Again, who is the right person to ping?
3. I need to record the olean cache location in the repository somewhere so that leanproject will know where to look for oleans. I was thinking the URL could go in a .mathlibtools or .leanproject config file in the root of the repository, but open to wherever you or others think would be preferable.
4. Do you just want the unused_arguments linter or do you want all the linters?

[Ben Toner]

The CI part of this is now (mostly) done, subject to changes based on the questions above and anything that comes up in additional testing or review. I also still need to update leanproject.

This is what the build will look like if the proof of Theorem 9.5 depends on something with a sorry: https://github.com/bentoner/lean-liquid/runs/2920399967?check_suite_focus=true

I was thinking that the new CI could run alongside the existing CI for a while, until we're confident that it's robust. If you're okay with temporarily storing oleans in a separate Azure account I made today, I could prepare a pull request for review soon. Switching to the official Azure account later would be easy: you would just need to replace the AZURE_SAS_TOKEN secret, and update the URL in .mathlibtools (or wherever you decide to put it per question 3 above).

[Johan Commelin]

@Ben Toner Thank you so much for helping out!

For (1) and (2), I hope that @Rob Lewis or @Bryan Gin-ge Chen can help with the Azure token.
For (3), @Patrick Massot what do you think is the best strategy?

For (4), I think unused_arguments would be good to start with. There are lots of missing docstrings, but once we have those, we can add another linter, and gradually move to enabling all linters.

[Patrick Massot]

Which oleans are we talking about?

[Johan Commelin]

LTE oleans

[Patrick Massot]

So you would want leanproject get-cache to also look for remote oleans?

[Johan Commelin]

I think LTE is large enough to justify it, and in the next half a year, it might double in size.

[Ben Toner]

@Patrick Massot oleans for the lean-liquid project. I want to enable leanproject to download cached oleans for projects other than mathlib, without hard coding the URL in the leanproject repository as is done for mathlib.

[Patrick Massot]

For the record only a default value of the url is hardcoded in leanproject, you can set it by running leanproject set-url (which simply writes the url in some configuration file)

[Patrick Massot]

Modifying leanproject to fetch non-mathlib oleans remotely is trivial, I can do that very soon

[Johan Commelin]

Ideally leanproject get-cache would fetch caches for the project and all dependencies (whenever they are configured to have remote cache stores)

[Yaël Dillies]

And what about the proposed setup of Sebastian? I mean the idea that you wouldn't have to download all the oleans every time because it would manage them better. Is it relevant?

[Patrick Massot]

Yael, I don't know what you are referring to

[Johan Commelin]

@Yaël Dillies that's for Lean 4, right?

[Yaël Dillies]

Sebastian talked about it in the context on Lean 4, but can't we have it for Lean 3? Or does it use something that changed?

[Johan Commelin]

I think that requires changes to lean, and setting up a whole nix build system. It doesn't seem to be completely settled down for lean 4 either. So even though it is probably better in the long run, I think it still takes work to get there.

[Johan Commelin]

The leanproject approach will probably take Patrick < 30 minutes to implement.

[Yaël Dillies]

Yeah okay!

[Johan Commelin]

Ben Toner said:

The CI part of this is now (mostly) done, subject to changes based on the questions above and anything that comes up in additional testing or review. I also still need to update leanproject.

This is what the build will look like if the proof of Theorem 9.5 depends on something with a sorry: https://github.com/bentoner/lean-liquid/runs/2920399967?check_suite_focus=true

I was thinking that the new CI could run alongside the existing CI for a while, until we're confident that it's robust.

Thanks again for doing this! I would be happy to integrate it into current CI.

[Johan Commelin]

Would you mind creating a PR for that?

[Johan Commelin]

Ben Toner said:

If you're okay with temporarily storing oleans in a separate Azure account I made today, I could prepare a pull request for review soon. Switching to the official Azure account later would be easy: you would just need to replace the AZURE_SAS_TOKEN secret, and update the URL in .mathlibtools (or wherever you decide to put it per question 3 above).

This still requires modifications to leanproject, right? Or am I misunderstanding something? If it does, I suggest we wait till Patrick updates leanproject.

[Ben Toner]

Johan Commelin said:

This still requires modifications to leanproject, right? Or am I misunderstanding something? If it does, I suggest we wait till Patrick updates leanproject.

We need modifications to leanproject for users to download the oleans, but the CI can start generating and consuming oleans itself before that happens, provided you're okay with using a temporary account.

I'll make a pull request.

[Patrick Massot]

The cleanest way to go would be to allow something like the following leanpkg.toml:

[package]
name = "lean-liquid"
version = "0.1"
lean_version = "leanprover-community/lean:3.30.0"
path = "src"
olean_url = "https://foo.com/liquid_oleans/"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "ee4fe7432b1f88e857e4b568f01a6435276a1b96", olean_url = "https://bar.com/fancy_mathlib_oleans/"}
lean-gptf = {git = "https://github.com/jesse-michael-han/lean-gptf", rev = "3e20785d65604744e9e2dc9d710a695a7355fd2c"}

adding optional olean_url field both in the package section and in each dependency. The bad side of this is that current leanproject will wipe up this information, at least while upgrading mathlib. So anyone interested in using a project that uses this new feature would need to upgrade leanproject. That seems ok to me, but I'd like confirmation before coding.

[Johan Commelin]

Sounds good to me.

[Eric Rodriguez]

I don't know how much arbitrary code an olean can run, but maybe a warning to check "do you trust such and such" would be nice for security

[Eric Rodriguez]

Just the first time you install a project maybe

[Patrick Massot]

Eric, each time you open a Lean file in VSCode you need to trust it. The Lean extension starts running it immediately and can wipe out your hard drive on line one.

[Julian Berman]

New versions of VSCode seem to ask first now though right?

[Julian Berman]

Mine always asks if I trust the Lean file's author

[Eric Rodriguez]

Yeah that's a new VSCode thing though, separate from Lean

[Patrick Massot]

Returning to the actual topic of this discussion, the situation is more complicated than what I described. Actually leanpkg will also interfere. It probably means it's time to finally get rid of any dependency of leanproject on leanpkg. But it means more work so don't hold you breath.

[Johan Commelin]

@Patrick Massot Would it be possible to have a short shell-script specifically for LTE that does

set the leanproject remote cache location to the LTE store
leanproject get-cache
set the leanproject remote cache back to the mathlib default

[Johan Commelin]

I think that would be good enough for LTE.

[Patrick Massot]

That won't work, remote olean are fetched only for mathlib

[Ben Toner]

I've made a pull request for a part that could be broken off, the script to check that Theorem 9.5 remains sorry free https://github.com/leanprover-community/lean-liquid/pull/44 .

I've updated the CI code to look for the olean_url field in package.toml per @Patrick Massot's proposal, but need to test further before making the (bigger) pull request for that.

@Patrick Massot I'm happy to help with changes to leanpkg and leanproject if you would like.

[Patrick Massot]

Ben, if you have time to work on removing every call to leanpkg from leanproject that would be great! The game is to search for 'leanpkg' in lib.py, figure out what we are asking it to do, maybe reading the leanpkg source code, and redo it in python. Globally that would make the whole thing a lot more predictable.

[Ben Toner]

Okay cool, I'll take a look at leanproject tomorrow.

I made a pull request for the CI changes here: https://github.com/leanprover-community/lean-liquid/pull/45 . Do note that I'm on Australian time, so it might be better to not merge today as I won't be around much longer if there's any breakage.

[Johan Commelin]

@Ben Toner Thanks a lot!

[Bryan Gin-ge Chen]

Johan Commelin said:

For (1) and (2), I hope that Rob Lewis or Bryan Gin-ge Chen can help with the Azure token.

(I don't have access to the Azure token; I think Rob has to do this.)

[Ben Toner]

Status: have linting working. Need to clean up and finish testing then will add to pull request. Haven't looked at leanproject yet.

[Ben Toner]

Pull request for Theorem 9.5 sorry-free check: https://github.com/leanprover-community/lean-liquid/pull/44

Main pull request: https://github.com/leanprover-community/lean-liquid/pull/45

• Can be merged before Azure secret is set and everything except Azure upload should still work
• Incorporates previous pull request

Pull request for associated changes to leanpkg: https://github.com/leanprover-community/lean/pull/586

• The CI changes can land before this does -- like the required leanproject changes, this is needed to make it easy for users to fetch the LTE oleans but doesn't block the CI changes.

I had a quick look at leanproject but I didn't do anything yet -- happy to take care of this but it'll need to be a project for say next weekend.

[Kevin Buzzard]

Thank you very much!

[Patrick Massot]

My suggestion was not to modify leanpkg, it was to stop using it in leanproject. If you want to modify leanpkg, it would be much nicer to teach it to ignore every unexpected key, simply copying it over.

[Patrick Massot]

Let me ping @Gabriel Ebner to make sure he sees this before looking at this PR.

[Ben Toner]

@Patrick Massot Apologies that I mischaracterised what you suggested. I will change leanproject to stop using leanpkg but it also seemed important to make leanpkg not delete the new key in case some users use leanpkg directly instead of leanproject. (I originally suggested putting the URL in a new .leanproject file to avoid needing to make changes to leanpkg.)

I agree it would be nicer to teach leanpkg to ignore every unexpected key, but on the flip side there is a benefit to having a schema, so I thought that I’d start with the more minimal change. Happy to proceed either way though.

Maybe we get the best of both worlds if we add a [leanproject] section and make leanpkg preserve everything in that.

[Ben Toner]

With regard to the leanpkg pull request, I also realise that I’ve failed to allow for the optional olean_url field in each dependency. I’ll hold off fixing this though until there is consensus about how to proceed.

[Patrick Massot]

I only wanted to avoid a proliferation of configuration files. It's already confusing to have three commands (lean, leanpkg and leanproject). But I don't deeply care.

[Ben Toner]

Okay great, it worked!

[Ben Toner]

One gotcha with the current state to be aware of: each time you or the bot updates mathlib, leanproject/leanpkg will delete the olean_url field in leanpkg.toml (until I/we fix it). After you have an official olean URL, we should record it on this line https://github.com/leanprover-community/lean-liquid/blob/20a63c58546989e62bae1c87ea71f984746ff3a0/scripts/fetch_olean_cache.sh#L9 -- then it won't matter that the field in leanpkg.toml gets deleted.

[Johan Commelin]

@Ben Toner do you think we can get nolints.txt working for this repository?

[Johan Commelin]

so that we can gradually fix all the linting errors?

[Ben Toner]

@Johan Commelin Is the idea that that would let you turn on all the linters or is it that you need to permanently suppress certain linting errors that you can't do with nolint attributes?

[Johan Commelin]

Well, there's still about 50 (or so) unused arguments that need to be fixed. So either we disable the linter till we've fixed all of them, or we have a week full of :cross_mark:'s, or we try to do some nolints.txt thingy.

[Johan Commelin]

And indeed, with the nolints thing, we could even enable a bunch of other linters as well.

[Ben Toner]

@Johan Commelin I can do a nolints.txt thing but it's not trivial (at least at my current level of lean ability). Would it work instead to just make the linting always be green in CI? That would be a one-line change.

[Johan Commelin]

Let's do that for now.

[Johan Commelin]

Then someone else can chime in and create the nolints.txt at a later point.

[Ben Toner]

I can do the nolints.txt change, just not on a weekday. The thing that makes it nontrivial (for me, at least) is that I think some linters might need to run on the combination of lean-liquid and mathlib(?) and the respective nolints.txt files need to be merged.

[Johan Commelin]

Hmm, good point. I guess this is things like the simp normal form linter?

[Johan Commelin]

Actually, I think I would rather not run linters that need to run on all of mathlib as well.

[Johan Commelin]

Anyway, this isn't very urgent.

[Johan Commelin]

So take your time

[Johan Commelin]

Hmm, the auto-update bot already removed the olean_url field from the .toml....

[Ben Toner]

That's okay - just leave it deleted next time. It's there so users can download the oleans, but they won't be able to do that until leanproject is updated, and leanproject will keep deleting this field anyway until it's updated. Moreover the CI can get the oleans without that field being present (see https://github.com/leanprover-community/lean-liquid/commit/664ddddbd178bc8ce7960103fa728899dedc9691 ).

[Rob Lewis]

Sorry for taking so long to look at the Azure side of this. I have a minor concern: the Azure cleanup script periodically deletes caches unless they come from mathlib master or the head commit of a mathlib branch

[Rob Lewis]

I could whitelist the LTE too, but maybe it would be better to put them in a subdirectory of the Azure blob

[Johan Commelin]

If it can save LTE cache that is less than 3 days old, that would be good enough, I think.

[Rob Lewis]

Do you want only master caches saved, or branches too?

[Rob Lewis]

If it works with whatever leanpkg changes might be planned, using a lean-liquid subdirectory seems cleaner

[Rob Lewis]

Then there's a uniform pattern for any leanprover-community projects that we want to add caches to

[Rob Lewis]

And the cleanup script can detect which repo the caches come from by the directory name

[Johan Commelin]

master is sufficient

[Johan Commelin]

It's just, if you wake up in the morning and the auto-mathlib-bumper or some other person has bumped mathlib, it would be really nice to have oleans within 5s instead of 20 minutes.

[Johan Commelin]

That's probably going to be the main use case.

[Rob Lewis]

The script at https://github.com/leanprover-community/lean-liquid/blob/master/.github/workflows/build.yml is going to upload oleans for every branch

[Rob Lewis]

The cleanup script only has access to the commit hash. So there's no way for it to tell where a cache comes from without looking for its hash in all the possible sources

[Rob Lewis]

Putting these caches in a lean-liquid subdirectory will make it easier to clean them up according to whatever rules we want

[Rob Lewis]

But also if you don't want to store branch caches at all we shouldn't upload them in the first place

[Johan Commelin]

I don't care too much about branches. Frankly they aren't used too much.

[Johan Commelin]

So I guess there is no harm in uploading caches for branches as well.

[Johan Commelin]

If that makes things easier for you (-;

[Ben Toner]

Hi @Rob Lewis Thanks for doing this. Using a subdirectory is a good idea.

For projects other than mathlib it seems less necessary to keep old versions around, so instead of a script, you could use lifecycle rules to auto-delete everything after X days. (On the other hand, for projects like lean-gptf that are intended to be used as dependencies, the current clean-up script's logic is more correct, but this is still something of a theoretical issue as lean-gptf is fast to build.)

[Johan Commelin]

Another question: can we configure LTE so that it cancels a build if a new commit has been pushed to the same branch?

[Johan Commelin]

Because LTE might end up eating precious CI time otherwise. (I just understood that it shares CI time with all other repos in the leanprover-community organization.)

[Johan Commelin]

We might even consider only running CI for master. People can test build their branches locally when needed.

[Bryan Gin-ge Chen]

If I'm reading this right, it looks like runs are canceled on branches other than master: https://github.com/leanprover-community/lean-liquid/blob/master/.github/workflows/build.yml#L21

[Johan Commelin]

Ok, so by removing L25, we get the same behaviour on master. I think that's worth doing. A push to master on LTE happens quite often.

[Johan Commelin]

Thanks @Bryan Gin-ge Chen !

[Ben Toner]

Johan Commelin said:

Ok, so by removing L25, we get the same behaviour on master. I think that's worth doing. A push to master on LTE happens quite often.

@Johan Commelin Okay, sorry, I guessed wrong on that choice. I figured that you would want a build for each push to master so we know which push to blame for e.g. linting regressions, so I disabled cancelling there. Note that build times will go down from 25 min to ~2.5 min once the olean cache is in place.

[Johan Commelin]

@Ben Toner no worries!

[Johan Commelin]

I don't care too much about the occasional regression. We'll probably find out soon enough.

[Johan Commelin]

I agree that maybe we can re-enable it when the olean cache is working.

[Johan Commelin]

But for now, I want to make sure that mathlib PRs get the CI time that they deserve (-;

[Ben Toner]

I wasn't properly accounting for this constraint. I'll make a pull request to disable the "old" CI then so we're not building everything twice. I was thinking you could run them both in parallel, but maybe you'd prefer to turn off the "old" one, if I make it easy to revert to it if the new one breaks for some reason.

[Johan Commelin]

I just commented out L25. Wouldn't that be enough?

[Ben Toner]

"old" CI as in the CI that was in place before last weekend

[Johan Commelin]

aah, yes, that is a good idea

[Rob Lewis]

@Ben Toner azure-scripts#9 and lean-liquid#48 together should do most of this. Archives will get uploaded only from master to a lean-liquid subdirectory, and cleaned when they're 3 days old. The cleanup conditions are easy to change.

[Rob Lewis]

I haven't added the Azure token to lean-liquid yet. Worth having more eyes look over the scripts before they accidentally make a mess.

[Rob Lewis]

I also don't know it/what changes are required for retrieving the caches, since the url now has a lean-liquid in it.

[Bryan Gin-ge Chen]

Will the HEAD commit of lean-liquid master get deleted if there are no commits within 3 days?

[Rob Lewis]

Not anymore!

[Ben Toner]

Hi @Rob Lewis, thanks, that's great! I didn't realize the script was public or I would have done something for you to review. I'll fix retrieving the cache in lean-liquid.

I know my timing is off, but can I suggest a period longer than 3 days, e.g., 30 days and saving branch HEADs too? I think the storage cost would remain under a dollar per month -- looks like you fixed this in a different way though while I was typing this...

[Rob Lewis]

I based that choice off of this:
Johan Commelin said:

If it can save LTE cache that is less than 3 days old, that would be good enough, I think.

Johan Commelin said:

master is sufficient

So right now it always has the latest master commit, and any others less than 3 days old.

[Rob Lewis]

The storage costs for this will be negligible compared to mathlib

[Rob Lewis]

And it's effectively free anyway

[Rob Lewis]

The only reason not to store more is aesthetic, if Johan says it'll never be used there's no point keeping it around.

[Ben Toner]

@Rob Lewis Thanks again for making all this happen.

I updated the URL for retrieving the cache - not entirely sure that the new one's correct but the existing one was already wrong, so I can't have made things worse.

[Rob Lewis]

That URL looks right

[Rob Lewis]

@Johan Commelin if you're happy with these changes, let's merge the two relevant PRs and I'll add the token as a secret

[Rob Lewis]

What's the story with retrieving these caches? Is it only for CI? Or is there a leanproject hook already?

[Rob Lewis]

I guess you could leanproject set-url to the lean-liquid subdirectory on Azure and then leanproject get-cache would work, right?

[Rob Lewis]

Or --from-url or whatever

[Johan Commelin]

I think Ben and/or Patrick are planning to update/extend leanproject so that this will be easy

[Johan Commelin]

@Rob Lewis Please go ahead and merge the PRs! Thanks a lot for helping out

[Rob Lewis]

So here's a 26 second build: https://github.com/leanprover-community/lean-liquid/runs/2955504763

[Rob Lewis]

I couldn't get it to work with leanproject --from-url or leanproject set-url

[Rob Lewis]

Not sure what the trouble is

[Rob Lewis]

For the time being, something like this should replicate it.

wget https://oleanstorage.azureedge.net/mathlib/lean-liquid/"$(git rev-parse HEAD)".tar.xz && tar -xf "$(git rev-parse HEAD)".tar.xz

[Johan Commelin]

I just tried that wget ... but I got a 404 not found error

[Ben Toner]

It's because the upgrade_lean workflow was the last thing commit to master and it doesn't store oleans... will fix within a couple of days.

[Ben Toner]

@Rob Lewis the leanproject commands you're trying are not supposed to be working yet.

Here's what remains, according to my understanding:

1. Enable nolints.txt for lean-liquid. We only want to lint lean-liquid code. Turn on more linters. Enable the nolints.txt unnecessary-line-removing workflow.
2. Make it so oleans are generated after the upgrade-lean workflow runs.
3. Update leanproject.
   a. Make it so leanproject doesn't depend on leanpkg.
   b. Make it so leanproject can do everything leanpkg does.
   c. Update leanproject to get-cache from the URL stored in leanpkg.toml

We decided not to update leanpkg.

My plan is to do 1 and 2 this weekend; the leanproject changes I'm also happy to do, hopefully this weekend, but no guarantees, and also allow time for some back-and-forth with the leanproject maintainers, as necessary.

[Rob Lewis]

Ben Toner said:

It's because the upgrade_lean workflow was the last thing commit to master and it doesn't store oleans... will fix within a couple of days.

You mean the latest commit at the time came from CI and Github doesn't run actions on commits made by other actions?

[Rob Lewis]

I think that's what happened anyway

[Eric Wieser]

A general question about lean CI: mathlib uses lean directly in the action, but https://github.com/leanprover-contrib/lean-build-action uses a docker container. Is there a reason that the latter uses a container?

[Rob Lewis]

Probably because I was new to writing actions at that point and was just copying something else that did things like that, I don't really remember

[Eric Wieser]

I ask only because I was looking at moving the problem matcher to that repo, but it looks quite different to the one used by mathlib and presumably the stuff being done to lean-liquid

[Ben Toner]

Rob Lewis said:

You mean the latest commit at the time came from CI and Github doesn't run actions on commits made by other actions?

I think it's that currently the "continuous integration" workflow that uploads to Azure triggers on push events, and the "upgrade lean" workflow doesn't generate a push event. Will be easy to fix... I was just wanting to think about the best way to do it a bit first.

[Rob Lewis]

The build action is supposed to be just a drop in thing, mathlib and lean-liquid do more complicated stuff so I guess it makes sense they call lean manually. Also mathlib's CI way predates the build action

[Rob Lewis]

But I'm also very sure that the build action isn't optimal

[Ben Toner]

Hi @Rob Lewis, can you please help me with another thing? Not urgent.

The reason the "bump mathlib" action doesn't trigger the CI build is as described by you here: https://github.com/leanprover-contrib/lean-upgrade-action/blame/master/README.md#L76.

The best way to fix this is to use a personal access token. Can you please create one, say from the leanprover-community-bot account or some other suitable account?

Steps (not so much for you but to document):

1. Go to https://github.com/settings/tokens and generate a new token with the public_repo scope.
2. Add token as the PA_TOKEN secret in the lean-liquid repo.
3. The account also needs permission to push to lean-liquid master.

After that is in place one of us can add this to master: https://github.com/leanprover-community/lean-liquid/commit/c8608fc9e40c2d487be54657e7280d6fd31c351f . (I also need the token for the nolints.txt workflow.) Thanks!

[Bryan Gin-ge Chen]

@Ben Toner I think I've set things up the way you asked. Let me know if you need anything else!

[Johan Commelin]

Rob Lewis said:

For the time being, something like this should replicate it.

wget https://oleanstorage.azureedge.net/mathlib/lean-liquid/"$(git rev-parse HEAD)".tar.xz && tar -xf "$(git rev-parse HEAD)".tar.xz

I just tried this wget line again, and it works great! Only thing I needed to compile was the gptf dependency.

[Johan Commelin]

@Ben Toner @Rob Lewis Thank you so much for making this possible!

[Ben Toner]

Linting:

• More linters are now enabled. You can change which linters are enabled by editing this list.
• There is now a nolints.txt file. It is kept updated each night.
• Commits that cause new linting errors will now cause the build to fail. You can change this behaviour here.
• If a commit results in a new linting error, as an alternative to fixing it you can manually trigger the workflow that updates nolints.txt.

The olean cache:

• I've added a script scripts/get-cache.sh which does what it is intended that leanproject get-cache will do, in order to make the leanproject work less pressing:

 ./scripts/get-cache.sh
Looking for local mathlib oleans
Found local mathlib oleans
Trying to download project cache
Found oleans at https://oleanstorage.azureedge.net/mathlib/lean-liquid/
Extracted oleans into src and deleted archive

[Eric Wieser]

Note that with recent changes to mathlibtools/master there's now a clear spot to fill in for other olean cache servers:

https://github.com/leanprover-community/mathlib-tools/blob/111e0dc7b0be85d418326cb002b0c0c473803cd3/mathlibtools/lib.py#L627-L633

I think there's probably also some cleanup to do regarding whether self.cache refers to the mathlib cache url (when mathlib is a dependency) or the cache url of the active lean project.

Regarding leanpkg; can we just create a separate leanpkg-cache.toml file that contains the cache URLs, then we don't have to worry about the current toml being overwritten?

[Riccardo Brasca]

I admit I didn't read the whole conversation, so the answer can very well be already here: is there a way to fetch the olean for the LTE using leanproject or something else? On my machine it doesn't seem to do it automatically.

[Johan Commelin]

./scripts/get-cache.sh in the LTE directory will get you some caches.

[Johan Commelin]

I think this uses leanproject under the hood, and at some point leanproject will do everything.

[Eric Wieser]

It doesn't use leanproject under the hood

[Eric Wieser]

(which means it doesn't backtrack to find older caches)

[Johan Commelin]

Aah, it only uses leanproject to get caches for mathlib, and does something custom for LTE

[Johan Commelin]

there is also ./scripts/fetch_olean_cache.sh which is a longer script.

[Johan Commelin]

It would be good if this functionality gets integrated into LP at some point

[Riccardo Brasca]

We can maybe add this script to the readme file in LTE?

[Johan Commelin]

Sure, go ahead!

[Riccardo Brasca]

Lunch first of all :sweat_smile: