## Stream: general

### Topic: strange build behavior

#### Rob Lewis (Oct 14 2019 at 13:06):

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 (Oct 14 2019 at 13:08):

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

#### Jesse Michael Han (Oct 14 2019 at 13:09):

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

Usually find src | grep "[.]olean$" | xargs touch fixes it for me #### Rob Lewis (Oct 14 2019 at 13:12): Usually find src | grep "[.]olean$" | xargs touch fixes it for me

That does it. Thanks!

#### Rob Lewis (Oct 14 2019 at 13:12):

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

#### Simon Hudon (Oct 14 2019 at 13:13):

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

#### Simon Hudon (Oct 14 2019 at 13:22):

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 (Oct 14 2019 at 13:41):

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 (Oct 14 2019 at 16:38):

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 (Oct 14 2019 at 21:11):

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 (Oct 15 2019 at 03:31):

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 (Dec 01 2019 at 16:32):

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?

Last updated: May 13 2021 at 18:26 UTC