purge_olean.sh: a few small improvements#661
Conversation
Only print if an .olean is rm'd. This reduces the noise and reduces the script run time.
|
@spl Welcome back! Long time no see! |
|
@jcommelin Thanks! 😺 |
rwbarton
left a comment
rwbarton
left a comment
There was a problem hiding this comment.
These changes look good to me apart from one small question.
purge_olean.sh
Outdated
| # Delete all empty directories. An empty directory may have been created if it | ||
| # does not contain any .lean files and all of its .olean files were deleted. | ||
|
|
||
| find $dir -type d -empty -delete |
There was a problem hiding this comment.
This will also delete empty subdirectories of .git which I'm not sure is a good idea. How about
| find $dir -type d -empty -delete | |
| find $dir -type d -not -path '*/.git/*' -empty -delete |
|
Why is it faster? |
@cipher1024 Because it doesn't print out every If I understand things correctly, this script will only |
This shouldn't be a problem. There are 338 lean files. If it is slow to write these in a log (which i guess should happen in Travis) we have a serious problem. But I agree to only show the deleted files, otherwise it is hard to read the log files. |
purge_olean.sh
Outdated
| for olean_file in `find $dirs -name "*.olean"` | ||
| do | ||
| echo olean file: $olean_file | ||
| lean_file=`echo $olean_file | sed "s/\.olean/.lean/"` |
There was a problem hiding this comment.
| lean_file=`echo $olean_file | sed "s/\.olean/.lean/"` | |
| lean_file=${olean_file/%.olean/.lean} |
We don't need sed, bash can do the same (I hope other shells too)
There was a problem hiding this comment.
I'm ambivalent about which is better. Changed in de65ffb.
@johoelzl It's not necessarily slow on Travis, but there is the web log interface, which (I'm guessing) is updated on demand from a log. So, for every line (or batch of lines) outputted to the log, there is the added latency of transferring that line from the server to the client and rendering it. Thus, the more output this script produces, the longer one who is watching has to wait to see the rest of the output. (Aside: network latency is noticeable here in South Africa.) Nevertheless, speed was never really a major reason for this PR. It only came up locally for me because I was updating my mathlib |
|
Actually, I would like to see more information in the travis log, as much as is useful. It is often difficult to figure out what the build environment is, especially with regard to the cache state, which can cause huge variation in build times and behavior between the different build stages. I think it would be really helpful to have a report of the state of the cache before running lean --make. It's not clear to me whether this script is doing that exactly, but if it is, it's not a bad thing, even if it slows down the build a bit. (Printing latency is the least of my worries when it comes to lean build time.) |
|
@digama0 This script currently tells you (a) all of the existing |
|
I guess the relevant information is which |
|
@digama0 I think the problem you point out is worth addressing but ultimately, it's outside the scope of this PR. If everyone is satisfied, I think we can merge this. |
|
Update: as far as I can see, all that's missing to merge is for @spl to change the last line to: |
|
I prefer the current line, with I prefer that solution, as it walks into a explicit subset of the directories, in the current case |
|
I agree that we should only look for lean files in |
* purge empty directories * Only print if an .olean is rm'd. This reduces the noise and reduces the script run time. * use git top-level dir to make the script relocatable * only affect src and test dirs * use bash instead of sed
6 participants
echos to reduce noise and speed up the scriptgittop-level directory instead of.