Strange Performance Behavior of "process"

Stream: lean4

[Tomaz Gomes]

So, I have a Lean script that simply receives as parameter the name of a lean file and runs Lean.Elab.process on it. It also loads some oleans that are in the same folder of the target file. Weirdly, the first time I run this script on some file it takes a lot more time than the following times. The one I am testing took 3.5s in the first run and 0.6s in the second, and keep 0.6s in all the following runs... what is going on?

[Henrik Böving]

Random guess would be that Linux is smart enough to cache the mmap stuff that we do in order to load a .olean

[Henrik Böving]

But that should be verifiable/measurable somehow although I do not know from the top of my head how.