olean caching

Stream: general

[Simon Hudon]

I just created a PR to get git to preserve your olean files and restore them when you switch branches. I'd like to know if it works for people. Please let me know if you try it and if it helps.

[Kenny Lau]

:D

[Simon Hudon]

In particular, I'd like to know if it needs to be adapter for windows because I use shell scripts

[Patrick Massot]

If you manage to allow us to switch mathlib branches back and forth without recompiling I phone the inquisition.

[Simon Hudon]

Let me just delete a branch, one sec

[Patrick Massot]

That would be one sorcery prowess too many for your own good.

[Simon Hudon]

Can the quota be negotiated?

[Simon Hudon]

If you want to try it before the branch is merged, here are the files

cache_olean.zip

[Simon Hudon]

You unzip them in your mathlib directory and call ./install_hooks.sh

[Patrick Massot]

I'll negociate for you if you manage to convince Travis to put mathlib olean for linux somewhere git will find them each we git pull mathlib

[Simon Hudon]

What it does is:

* when you commit, it makes a copy of your olean files
* when you checkout a branch, it checks if a cache exists for that branch and restores it if one exists
* when you rebase a branch A on top of branch B, it caches the files of A and restores the files of B

[Kenny Lau]

just the olean files?

[Simon Hudon]

Yes, just the olean files

[Simon Hudon]

I'll negociate for you if you manage to convince Travis to put mathlib olean for linux somewhere git will find them each we git pull mathlib

That's a tall order. You're asking for a complete new feature, all I did was a small hack :P

[Simon Hudon]

Actually ... that's feasible

[Simon Hudon]

Actually, I think doing it half-way is more than half-way useful

[Simon Hudon]

Do you guys feel like giving it a spin?

[Patrick Massot]

I'll definitely try tomorrow, but I really need to go to bed now

[Simon Hudon]

I thought you enjoyed working with Lean

[Simon Hudon]

Sleep well :)

[Bryan Gin-ge Chen]

@Simon Hudon Does this work the same way for packages that include mathlib as a dependency?

[Bryan Gin-ge Chen]

Wait, maybe that question doesn't make sense.

[Simon Hudon]

You can make it work in that situation I believe. Once you configured the package, go in _target/deps/mathlib and call ./install_hooks.sh. If different versions of the same package use different branches of mathlib, switching between the versions of your package might get cheaper (we'd have to test it to make sure)

[Bryan Gin-ge Chen]

hint: The '.git/hooks/post-checkout' hook was ignored because it's not set as executable.
hint: You can disable this warning with `git config advice.ignoredHook false`.

Should I change the permissions on these files?

[Simon Hudon]

Yes good idea. And I'll make fixes to the scripts

[Simon Hudon]

Any luck?

[Bryan Gin-ge Chen]

I've been switching back and forth between master and tutorials and running lean --make and each time it does a full rebuild. If I do lean --make does that force a rebuild no matter what?

[Bryan Gin-ge Chen]

I'm on my macbook.

[Scott Morrison]

No, it doesn't/

[Bryan Gin-ge Chen]

Hmm, my master was out of date. Let me try again.

[Scott Morrison]

The problem is likely that master has introduced changes to stuff way down the dependency tree.

[Scott Morrison]

If you rebase tutorial onto master it should make life better.

[Bryan Gin-ge Chen]

I think I see what you're saying, but shouldn't caching all the olean files associated to a given commit also preserve the build status?

[Simon Hudon]

It should. Can you ls .bin/branches and tell me what you get?

[Bryan Gin-ge Chen]

Where's .bin?

[Bryan Gin-ge Chen]

Oh I see, I guess .bin somehow hasn't been created.

[Simon Hudon]

It is created when you commit or rebase. You can also manually call .git/hooks/cache_olean.sh

[Bryan Gin-ge Chen]

I ran cache_olean.sh after building on tutorials and master, and the olean files seem to be in .bin/branches/ but running lean --make still starts a rebuild.

[Simon Hudon]

What if you run restore_olean.sh before rebuilding?

[Scott Morrison]

./install_hooks.sh
cp: .git/hooks: Not a directory

[Scott Morrison]

Just needs a mkdir -p .git/hooks in install_hooks.sh.

[Bryan Gin-ge Chen]

I tried running restore_olean.sh and it's rebuilding again.

[Scott Morrison]

I pushed a commit that fixes this.

[Simon Hudon]

@Bryan Gin-ge Chen Can you check what the time stamp is on the most recently modified file in .bin/branches/tutorial? I'm assuming that's the one you're trying to cache.

[Simon Hudon]

@Scott Morrison You're too fast! Thanks!

[Scott Morrison]

Ah, but I fixed the wrong problem.

[Scott Morrison]

The actual problem is that I don't have a .git directory.

[Scott Morrison]

I have a .git file, because I'm using a submodule.

[Scott Morrison]

Crap...

[Scott Morrison]

This is not going to affect many people at all, but I guess I want a fix myself. :-)

[Simon Hudon]

Darn! How come you work without git?

[Scott Morrison]

The problem is that I work with git for _everything_. My entire home directory is a giant git repository, and everything else is a git submodule, so things get synchronised between my computers.

[Simon Hudon]

Actually, if you go in _target/deps/mathlib and call install_hooks.sh there, I'm hoping that will do the job

[Scott Morrison]

Well, but I mostly want this for mathlib itself.

[Scott Morrison]

Switching between branches that touch tactic/basic.lean is unpleasant...

[Bryan Gin-ge Chen]

The timestamps all seem to be from when I ran cache_olean.sh.

[Scott Morrison]

@Simon Hudon, why do you put cache_olean.sh and restore_olean.sh in the .git/hooks directory, rather than leaving them in the root directory?

[Simon Hudon]

@Bryan Gin-ge Chen That is useful information. I'll look into preserving time stamps properly

[Simon Hudon]

@Scott Morrison I want to be able to use the hooks even on branches where the files aren't in the repo

[Scott Morrison]

Ah, good point.

[Bryan Gin-ge Chen]

The timestamps of the .lean files are bumped when I checkout a new branch. So do we need the timestamps of the olean files to be more recent than that?

[Simon Hudon]

@Bryan Gin-ge Chen do you mean that the .lean timestamps are set to the time at which you checkout the files?

[Bryan Gin-ge Chen]

Yes.

[Simon Hudon]

@Scott Morrison Maybe there's a way to include a search step at the beginning of the script to climb up the directory structure until a .git is found.

[Simon Hudon]

@Bryan Gin-ge Chen What platform are you on?

[Scott Morrison]

There's a nice fix, almost pushed.

[Scott Morrison]

git rev-parse --git-dir tells you where your .git directory really is.

[Scott Morrison]

e.g. for me: /Users/scott/.git/modules/projects/lean/mathlib

[Scott Morrison]

Okay, pushed that change.

[Scott Morrison]

I think we need more hooks. I want my olean files cached even if we don't make a commit!

[Simon Hudon]

Thanks! Did you put that .git dir in a variable?

[Scott Morrison]

e.g. I never commit to master, but I want a cache.

[Simon Hudon]

Yeah, me too! I haven't found a good hook for that

[Scott Morrison]

I just have GITDIR=`git rev-parse --git-dir in most of the scripts.

[Scott Morrison]

What if when we checkout, we _first_ restore, _then_ cache.

[Simon Hudon]

I think we might need to get leanpkg or, emacs / VS code to do that after you build

[Bryan Gin-ge Chen]

macOS. Not all of the .lean files have their timestamps bumped, but the ones that don't exist in master certainly do.

[Scott Morrison]

If there was something to restore, then it just harmlessly puts it back again.

[Scott Morrison]

But if there was nothing to restore, then we build a cache?

[Scott Morrison]

hmm...

[Scott Morrison]

no

[Scott Morrison]

because that cache will be wrong. :-)

[Bryan Gin-ge Chen]

All the files that are changed between branches have their timestamps set to the time I do the checkout.

[Scott Morrison]

What if on every checkout we:
1) run cache before checkout (saving the state of the branch we're leaving)

[Scott Morrison]

2) run restore after checkout

[Scott Morrison]

3) run cache after that

[Simon Hudon]

What a bummer. I found this information here. https://confluence.atlassian.com/bbkb/preserving-file-timestamps-with-git-and-mercurial-781386524.html

It recommends a certain build system as a solution

[Simon Hudon]

@Scott Morrison run cache after the restore or after build?

[Scott Morrison]

I was thinking just immediately after the restore.

[Scott Morrison]

This has the effect of actually creating the cache merely by checking out.

[Scott Morrison]

Otherwise I don't see how a cache for master will ever be created

[Bryan Gin-ge Chen]

Could we just touch all the .olean files right before restoring?

[Scott Morrison]

I think the problem is that risk making things worse.

[Simon Hudon]

Yeah

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Simon Hudon]

What I'm thinking of is, after a checkout, look at each lean file and set its time stamp to that of the latest commit that changed it

[Scott Morrison]

oof...

[Scott Morrison]

(Presumably you mean to the time stamp of the corresponding olean file.)

[Reid Barton]

What if you just don't use cp -a?

[Simon Hudon]

The olean files will all be interpreted as up-to-date but some might not be

[Simon Hudon]

(Presumably you mean to the time stamp of the corresponding olean file.)

No. For any source file we need to determine if we need to rebuild it. One information we need is when we last built it which is why we shouldn't overwrite the time stamp of the olean file. The other one is when we last change it which is why we wouldn't want git to overwrite the time stamp of a file but it does.

[Simon Hudon]

I think we'd like to know if the file was built since the last commit that changed it

[Scott Morrison]

This olean caching stuff is really important, and I will be super happy if we can get it working smoothly. I'm not sure I can help at the moment with the timestamp issues, but let me know if there's anything I can do.

[Scott Morrison]

I hope one day we could even build a distributed cache; I could certainly contribute CPU cycles building olean files for central distribution.

[Simon Hudon]

I'll keep at it

[Chris Hughes]

I just have 17 copies of mathlib saved, so I never have to switch branches.

[Johan Commelin]

Diskspace is cheap...

[Simon Hudon]

I used to work like that. As the number of branches changes, I find it hard to manage

[Tobias Grosser]

Interesting. I am not really up-to-speed here, but i might be interesting to look at existing tools which address these issues.

[Tobias Grosser]

Specifically, there is 'ninja' a very fast alternative for make.

[Tobias Grosser]

And 'ccache' which caches the compilation of C/C++ files.

[Tobias Grosser]

If lean would have a way to export the "include" files, it might be possible to adapt these tools (or use at least their design).

[Tobias Grosser]

My feeling is that connecting .olean files to git branches is pretty fragile "hacky".

[Tobias Grosser]

Hashing the source files and having a proxy for returning the right source file in case a hash is already known is a strategy that works well in the OS projects I have been working on.

[Mario Carneiro]

lean already uses ninja for compilation

[Mario Carneiro]

You would have to hash the file plus the hashes of dependent files, git-style

[Tobias Grosser]

Right. The ccache docu explains well what is needed to do this kind of caching.

[Tobias Grosser]

@Mario Carneiro , are you saying lean is using 'ninja' for compiling the lean binary, or is it called as part of 'lean --make'?

[Gabriel Ebner]

ninja can optionally be used to compile lean itself. lean --make doesn't use ninja (the equivalent linja tool in Lean 2 did though). Ninja doesn't do anything more fancy than lean --make, I believe. (Does ninja use content hashes or modification times?) Something like ccache might be interesting when switching between branches.

[Tobias Grosser]

Also, to get the dependent files lean already has a command '--deps'.

[Tobias Grosser]

Ninja does not do anything more fancy than lean --make, I assume.

[Tobias Grosser]

However, it is _very_ fast.

[Tobias Grosser]

in checking if files have been modified.

[Gabriel Ebner]

That is pretty much the least expensive part of running lean --make though.

[Tobias Grosser]

This does not matter for the perf problems we have today, but I feel it will matter in the future.

[Mario Carneiro]

the problem is that the usual dependency analysis will say that too many files are affected and compile them all

[Tobias Grosser]

Right, it's more a difference between 5 seconds and 0.01 second on clean builds. It really improves productivity on large C++ code bases and might be useful for lean as well (especially if we interactively want to update proofs).

[Tobias Grosser]

Right. Most of likely requires changes in lean proper.

[Mario Carneiro]

0.01 second vs 1 second to tell me that nothing needs doing doesn't seem so useful

[Mario Carneiro]

but if you could reason that most of the library is unaffected by a new theorem in logic.basic that would be a HUGE gain

[Mario Carneiro]

like an hour compilation

[Tobias Grosser]

I mean these are orthogonal.

[Mario Carneiro]

is it? I'm talking about proper caching and dependency analysis

[Tobias Grosser]

You need all a) proper dependency analysis, b) good caching, c) worry about how to check if files have changed.

[Tobias Grosser]

ninja is really good in minimizing file IO and stat calls to very quickly check for c)

[Mario Carneiro]

If there were thousands of files then I can see this being a problem

[Mario Carneiro]

but at that point total compile times will dwarf all of this

[Gabriel Ebner]

In server mode we don't even do any file IO? We actually have a precomputed dependency graph.

[Tobias Grosser]

But it does not help with a) and b).

[Tobias Grosser]

I see.

[Tobias Grosser]

So my feeling is at some point we would just need proper caching in server mode.

[Tobias Grosser]

Which would be a lean specific thing, that just needs to be implemented, right?

[Sebastian Ullrich]

"just"

[Sebastian Ullrich]

:)

[Simon Hudon]

I have created a branch of ccache to try and add support for Lean. I saw an issue discussion that suggests that it might be a simple business so I thought I'd try it out: https://github.com/leanprover-community/ccache

[Sebastian Ullrich]

Wow, I've been thinking about doing this for a long time, but didn't think anyone would ever actually go ahead with it...

[Sebastian Ullrich]

Though are you sure you don't want to modify https://github.com/mozilla/sccache instead :) ?

[Sebastian Ullrich]

(No idea if it would actually be easier, just newer code base, cloud support, and my preference for Rust)

[Simon Hudon]

That sounds like an even more useful tool. I don't know what it would take to adapt though

[Simon Hudon]

Do I understand correctly that it allows sharing binaries between team members or community members?

[Sebastian Ullrich]

I assume it's intended for sharing with trusted team members. Securing public r/w access to some cloud storage doesn't sound like a simple issue.

[Simon Hudon]

I think I'll put that issue aside to handle a simpler problem :)

[Patrick Massot]

Sounds like an important issues, I've seen people discussing assuming nat = int, they probably shouldn't be trusted

[Kenny Lau]

how about we remove *.olean from gitignore?

[Simon Hudon]

It is a big no-no. We don't want to keep the history of those files, we just want appropriate binaries. Keeping those binaries will make git slower and will make merging more complicated.

[Chris Hughes]

Also olean is OS dependent

[Simon Hudon]

@Sebastian Ullrich it looks like sccache works with Lean out of the box. You just call sccache leanpkg build. Does that make sense to you?

[Sebastian Ullrich]

I have no idea. Does it look like it actually does anything?

[Sebastian Ullrich]

(@Chris Hughes It's not, AFAIK. Though it will be architecture-dependent in Lean 4)

[Simon Hudon]

It does look like it actually calls leanpkg but I'll have to experiment and see if a cache is created.

[Sebastian Ullrich]

Yes, that would be the important part :smiley:

[Simon Hudon]

If it does work out of the box, the next step would be integration: how do we make it invisible to the Lean user

[Simon Hudon]

I think part of it working with leanpkg and elan is to create a symbolic link so that when lean is called, it calls sccache lean instead. @Sebastian Ullrich Does that sound like that could break the build system?

[Sebastian Ullrich]

That could work

[Simon Hudon]

Right now, I put a shell script called ~/.sccache/bin/lean that just prints "calling lean" and I put it in my path (I checked with which lean) but leanpkg does not seem to call it

[Sebastian Ullrich]

oh https://github.com/leanprover/lean/blob/b13ac127fd83f3724d2f096b1fb85dc6b15e3746/bin/leanpkg#L24

[Simon Hudon]

So how does elan redirect to the right version of lean?

[Sebastian Ullrich]

It doesn't in that case, it just calls the right version of leanpkg :)

[Simon Hudon]

argh!

[Simon Hudon]

Any chance we might hard code ccache or sccache into elan?

[Sebastian Ullrich]

How would that help?

[Simon Hudon]

Maybe it could call a leanpkg-2 bash script instead of leanpkg and also produce the leanpkg-2 script so that the paths are set properly (for sccache). I have a feeling that that bash script did not change a lot between versions. Am I right?

[Sebastian Ullrich]

I see. But if you want to support both sccache leanpkg and sccache lean anyway, are you sure you save any code by making the former call the latter?

[Simon Hudon]

Actually, what I'd like to do is just replace every call to lean to sccache lean. sccache seems to index its cache by command line arguments.

[Simon Hudon]

Actually, it might be enough to have elan rename lean to lean-2 and create a bash script lean in its place to call sccache when elan downloads a version of lean

[Simon Hudon]

@Sebastian Ullrich It's starting to look to me like we may have to alter the way lean --make works for either of sccache or ccache to be useable

[Sebastian Ullrich]

I wouldn't be surprised :)

[Simon Hudon]

Bummer, I was hoping it might be a small(-ish) thing to do

[Sebastian Ullrich]

I was fully prepared that someone might at some point write an alternative leanpkg that fixes many issues with it (and would probably not be written in Lean)

[Simon Hudon]

Is there a way to use lean to export all the dependencies in a project? lean --deps seems to interact poorly with leanpkg.toml files

[Simon Hudon]

If I could use it, maybe I could generate a Makefile (or ninja config?) and that might be a better starting point than lean --make

[Sebastian Ullrich]

I don't think so, you basically have to parse the file header...

[Tobias Grosser]

+1 for 'ninja + make', at best if it's auto-generated from the lean files.

[Simon Hudon]

The other tool I've heard of is Bazel. Have you heard of it and would you endorse it?

[Tobias Grosser]

Never used it.

[Tobias Grosser]

I feel it might be too high level.

[Tobias Grosser]

In the end we know all dependences.

[Tobias Grosser]

And just want to declare them and execute.

[Tobias Grosser]

I mean, you might also try to use cmake:
https://cmake.org/pipermail/cmake/2011-April/043761.html

[Tobias Grosser]

Not sure if this makes things easier.

[Tobias Grosser]

I fell, getting dependences out of lean files is certainly a useful component in any of these tools.

[Simon Hudon]

In the end, we'll probably need to parse the Lean files ourselves though, no? Unless we can get lean to get them out for us.

[Simon Hudon]

In the meantime, I started a branch in sccache and I talked to the developers on how to support Lean. It sounds doable. I just need to learn a bit more of Rust. And they seem willing to take our patch

[Tobias Grosser]

Cool. This sounds very exciting, indeed.

[Tobias Grosser]

What is the problem with --deps?

[Reid Barton]

As far as I can tell, it just doesn't work properly

[Simon Hudon]

I can't get it to work at the scale of a project. It seems to work off of LEAN_PATH which is no longer required (and indeed harmful) to work with leanpkg

[Tobias Grosser]

I see. I have no idea of this code, but fixing it seems the most direct thing to do. In fact, does it do a lot more than parsing the imports?

[Tobias Grosser]

AFAIU it should just parse the imports and then print this to stdout in some way.

[Reid Barton]

Simon, have you gotten it to work under any circumstances?

[Reid Barton]

Oh, I figured out why it is broken. It thinks that the presence of both foo.lean and foo.olean means that the import of foo is ambiguous.

[Reid Barton]

So, this is something we could work around (in principle, at least)

[Simon Hudon]

I was actually thinking that temporarily setting LEAN_PATH might fix it but I'm not done experimenting with it

[Reid Barton]

I looked at strace -e trace=file output and it's clearly not failing to find the files it's looking for

[Reid Barton]

And it is looking in the correct paths as reported by lean -p (and examining the source seems to indicate that lean -p is using the same path information as lean --deps)

[Simon Hudon]

@Sebastian Ullrich Any chance we may get a fix for lean --deps?

[Sebastian Ullrich]

@Simon Hudon Yes, I feel that could be a reasonable change. It would be great if you or someone else could investigate fixing it

[Simon Hudon]

Sure I'll look into it. Do you have a suggestion of where I should start?

[Sebastian Ullrich]

The relevant call should be this one: https://github.com/leanprover/lean/blob/b13ac127fd83f3724d2f096b1fb85dc6b15e3746/src/shell/lean.cpp#L698

[Sebastian Ullrich]

Wow, display_deps is still testing for .hlean and .lua

[Reid Barton]

What I have inferred from looking at the source and the strace output: Say the module imports data.rbmap. display_deps calls

std::string find_file(search_path const & paths, std::string const & base, optional<unsigned> const & rel, name const & fname,
                      std::initializer_list<char const *> const & extensions) {

in src/util/lean_path.cpp. That calls file_path just above, because the import is not relative. That one tries each extension in the given list and pushes all the successes into a list of results.

[Reid Barton]

Because both data/rbmap/default.lean and data/rbmap/default.olean are found, that function raises an "ambiguous import" exception. Then display_deps catches the exception and reports an uninformative "file not found" error message.

[Reid Barton]

You may want to verify this by inserting tracing printfs and/or having display_deps show the original exception

[Simon Hudon]

Wow! you're fast!

[Sebastian Ullrich]

Nice work! This is the code the regular path uses for importing, you may want to adapt that https://github.com/leanprover/lean/blob/b13ac127fd83f3724d2f096b1fb85dc6b15e3746/src/library/module_mgr.cpp

[Reid Barton]

I was just looking into this earlier (see my messages of 42 minutes ago)

[Sebastian Ullrich]

Note that this code already looks completely different in Lean 4. So fixing this would only make sense if it was a big win for Lean 3 users (which a working sccache would probably be)

[Simon Hudon]

I think it would be. It seems like a small fix on the Lean side and I'm hopeful sccache should be easily ported from Lean 3 to Lean 4 (once it works for Lean 3)

[Simon Hudon]

@Reid Barton Can I leave that fix to you?

[Reid Barton]

I can take a shot at it. We should make sure we have some working setup for sccache before upstreaming the change to Lean though. For testing purposes, you should be able to just remove ".olean" from the list of extensions in display_deps.

[Simon Hudon]

we have some working setup for sccache before upstreaming the change to Lean though

I think the fix is usable on its own. Why do you think we should wait?

[Reid Barton]

Only because Lean 3 is currently in this state where it doesn't change without a particularly good reason

[Simon Hudon]

It makes it harder to progress if we wait for everything to be ready before we push anything. If we do the heavy lifting, I don't think they will begrudge us fixing a problem even if the sccache idea doesn't pan out.

[Simon Hudon]

I just tried removing .olean from the list in display_deps and it's working. Is that a good enough fix?

[Reid Barton]

It seems like it should be good enough for us, though there could be other bugs lurking underneath. The other question is whether it would break any other users of Lean and specifically of lean --deps. The only way I could imagine the change breaking a working system is if that system uses out-of-tree builds (output .olean files not located in the same place as the corresponding source files) and also relies on .olean files as inputs without corresponding source .lean files. That seems pretty unlikely to me, considering that lean's library itself is not built out-of-tree, so at a minimum the implicit import of init will fail.

[Simon Hudon]

That's also my impression. I wonder if they had anything else in mind when they put .olean in that list.

[Simon Hudon]

@Sebastian Ullrich Here's the fix that did it for me: https://github.com/cipher1024/lean/commit/d2d81a3539bdf952eaf6126d2be69f2fda0b2f1f

[Simon Hudon]

Also, is --make the only way to produce .olean files? For me, even if I give a file name, it seems to build the whole project. Is there any way around that?

[Reid Barton]

It should only build the file you specify (and its dependencies if necessary)

[Simon Hudon]

You're right, I misinterpreted what I saw

[Simon Hudon]

Now with the fix, I managed to build a make file that discovers dependencies and builds what it needs.

[Tobias Grosser]

Nice!

[Simon Hudon]

I decided to go for bare minimum and only use make. We can make it more sophisticated once we see it is working.

[Tobias Grosser]

Seems like a good idea. Looking forward to checkout the make file.

[Simon Hudon]

I'll push it in a branch in a moment. If you have comments, I'd love to hear them

[Simon Hudon]

It won't be functional because I hard coded a path to my Lean version

[Sebastian Ullrich]

You can use elan to manage your local Lean fork :)

[Simon Hudon]

Niiice! How?

[Sebastian Ullrich]

elan help toolchain link

[Sebastian Ullrich]

"crate", oops

[Simon Hudon]

Haha! I didn't even notice! I was thinking that you've been pretty thorough in replacing Rust with Lean :)

[Simon Hudon]

Btw, have you looked at my commit?

[Sebastian Ullrich]

Yeah, I think it should be fine. You can remove ".lua" too.

[Simon Hudon]

Will do!

[Simon Hudon]

Here we go: https://github.com/leanprover/lean/pull/1978

[Simon Hudon]

Is it possible to use elan to refer to a specific git commit on github?

[Simon Hudon]

@Tobias Grosser here is what I did for the Makefile. It generates dependency files for each .lean file before it gets started building any files and the first time you get a lot of error messages because they are missing.

https://github.com/leanprover-community/mathlib/commit/d090d711c0b438223479635b663e720dab2d07e7

[Simon Hudon]

@Sebastian Ullrich You use emacs right? What do you use for Rust?

[Tobias Grosser]

Nice.

@Tobias Grosser here is what I did for the Makefile. It generates dependency files for each .lean file before it gets started building any files and the first time you get a lot of error messages because they are missing.

https://github.com/leanprover-community/mathlib/commit/d090d711c0b438223479635b663e720dab2d07e7

Now just the sccache needs to work. I feel this might indeed be a great improvement.

Best Tobias

[Johan Commelin]

My laptop just crashed while compiling mathlib. This is the first time it crashed in a couple of years. We really need to make mathlib easier on prehistoric hardware :dragon:

[Simon Hudon]

I'm sciencing as fast as I can ... it's coming

[Kenny Lau]

or we can make mathlib compile faster

[Simon Hudon]

I don't think we should pick just one

[Scott Morrison]

Hi @Simon Hudon, would you have time to give a status update on sccache integration, in particular pointing out if there are places someone else could help write code/investigate issues/do some research?

[Simon Hudon]

Sure. I can push what I currently have

[Simon Hudon]

What I did is provide a way for sscache to determine if an olean file is outdated or not through hashing.

[Simon Hudon]

I'm still struggling to get the tests to pass. I think once that work, we should have a version sscache that can locally cache any lean build we like.

[Simon Hudon]

I wrote a Makefile to take advantage of it and I pushed it on leanprover-community. I also made a patch to lean itself to fix the way it computes dependencies

[Simon Hudon]

After I'm done with this part, one possible extension (if you want to spend the time) is figure out how to get some cloud storage to store a Lean cache. That would involve configuring sccache itself and setting up instructions for people who want to access the cache.

[Simon Hudon]

At this point I see that more as goody than as a must have though

[Scott Morrison]

I pushed two minor changes to the build-system branch.

[Scott Morrison]

Where is that "is an olean file outdated, via hashing" code?

[Scott Morrison]

Using timestamps to decide whether to recompile makes life really difficult. Do we know an obstacle (besides patching Lean), to instead have each olean file contain a hash of its source file and of the olean files for each of its imports? To decide if an olean file is stale or not you would read those hash from the olean file, and compare them against the current hashes of those files.

[Scott Morrison]

Once one .lean file changes, this would propagate staleness of all dependent .olean files.

[Scott Morrison]

And no timestamps would ever be considered.

[Scott Morrison]

Or, @Simon Hudon, is this what you've already done?

[Simon Hudon]

That's what I'm working on yes. More exactly, when calling sccache lean --make foo.lean, we get the list of modules imported (directly or indirectly) by foo.lean, we hash all of them (including foo.lean) and recompile only if that hash changes.

[Scott Morrison]

I see -- you hash the source files of the imports, or the olean files?

[Scott Morrison]

And this is all being done by the sccache wrapper, with no modification of Lean?

[Simon Hudon]

The sources

[Simon Hudon]

That's correct

[Scott Morrison]

But won't we then get burnt still by Lean being wrong about what is stale?

[Simon Hudon]

I'd like to hash the olean but all the ways I have thought of are flawed

[Simon Hudon]

What do you mean?

[Scott Morrison]

Say we have files A < B < C, and A and B are already built correctly, according to their hashes, while C needs to be rebuilt.

[Scott Morrison]

But suppose the timestamps on A.olean and B.olean are messed up.

[Scott Morrison]

When sccache invokes Lean on C.lean, what is to stop Lean from going and recompiling A and B?

[Simon Hudon]

I don't think this will be happening but I have to double check. Maybe @Sebastian Ullrich can tell us. If we call lean --make foo.lean, will Lean attempt to rebuild any of the dependencies? If so, is there a way to tell it not to?

[Simon Hudon]

One thing I have considered is to manually set the modification time of the olean files when they don't need to be rebuilt. That should solve the issue.

[Sebastian Ullrich]

Yeah, that's what I would have proposed, too

[Johan Commelin]

@Scott Morrison @Simon Hudon Any updates on the caching front? (Yes, indeed, I thought of it again because I'm currently recompiling... :lol:)

[Simon Hudon]

Haha! I actually managed to make progress on it today and yesterday. Now I'm testing it and I'm hoping I can roll out a version soon

[Johan Commelin]

Awesome news!

[Simon Hudon]

I managed to build a version that passes all their tests:

https://github.com/leanprover-community/sccache/tree/lean-support-2

[Simon Hudon]

When I try it with my Makefile though, it fails. There seems to be issue with the timing when sccache produces the binaries

[Simon Hudon]

If someone wants to try it for themselves, I can share the Makefile