Zulip Chat Archive

Stream: general

Topic: strange build behavior


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Jesse Michael Han (Oct 14 2019 at 13:09):

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

view this post on Zulip Johan Commelin (Oct 14 2019 at 13:10):

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

view this post on Zulip Rob Lewis (Oct 14 2019 at 13:12):

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

That does it. Thanks!

view this post on Zulip Rob Lewis (Oct 14 2019 at 13:12):

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

view this post on Zulip Simon Hudon (Oct 14 2019 at 13:13):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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