Zulip Chat Archive

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

Johan Commelin (Oct 14 2019 at 13:10):

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: Dec 20 2023 at 11:08 UTC