strange build behavior

Stream: general

[Rob Lewis]

I'm seeing some strange build behavior possibly related to cache-olean. I don't have time to confirm right now, but I think I saw similar with update-mathlib earlier.

Steps:

• Get a fresh clone of mathlib and run leanpkg configure, git reset --hard origin/lean-3.4.2, cache-olean --fetch. This is successful and populates src with olean files.
• Create a new file blah.lean with the following content (sufficient, probably not necessary):

import tactic.fin_cases
import tactic.apply_fun
import linear_algebra.finite_dimensional
import analysis.normed_space.basic
import linear_algebra.dual
import linear_algebra.basis

• Run lean blah.lean --make. It terminates after ~5 seconds, and appears to compile a few files in logic and data.
• Run lean blah.lean --make again. It appears to recompile everything.

[Rob Lewis]

I can't spare the CPU time for more testing right this second. Does anyone recognize this behavior?

[Jesse Michael Han]

i've also occasionally been getting this behavior after leanpkg-configure -> update-mathlib

[Johan Commelin]

Usually find src | grep "[.]olean$" | xargs touch fixes it for me

[Rob Lewis]

Usually find src | grep "[.]olean$" | xargs touch fixes it for me

That does it. Thanks!

[Rob Lewis]

Should this be part of the cache-olean/update-mathlib script?

[Simon Hudon]

find src -name *.olean -exec touch {} \; might be a bit less clunky

[Simon Hudon]

We could add it to cache-olean / update-mathlib. I don't know if we should do it every time though. It would be worth testing

[Reid Barton]

find src -name *.olean -exec touch {} \; might be a bit less clunky

This one probably won't work. Using xargs makes the timestamps all equal (as long as all the .olean file names fit on a single command line).

[Floris van Doorn]

I've been using find src -name *.olean -exec touch + by default now, and it seems to work well.
I'm guessing that the relative timestamps of the .olean files don't matter, but it only matters that foo.olean is newer than foo.lean.

[Sebastian Ullrich]

No, the .olean file is rebuilt if any transitive dependencies are newer: https://github.com/leanprover/lean/blob/master/src/library/module_mgr.cpp#L184-L187
However, xargs --show-limits tells me that it supports 131072 bytes per command (on my machine), so if find uses anywhere near that, it's most probably doing a single call...

[Reid Barton]

On Windows the -exec option is also likely to work because I think by default the timestamp granularity of the filesystem is only 1 second

[Kevin Buzzard]

I still find myself having to do this find src | grep "[.]olean$" | xargs touch thing (in this case when editing mathlib after a git checkout lean-3.4.2 with all the fancy hooks set up so that cache-olean triggered automatically). Is this issue understood?