cloud computing possibilities

Stream: general

[Rob Lewis]

Right now we use MS Azure to host and distribute olean caches for leanproject. This isn't expensive, ~$15/mo. Suppose that we had a reasonably large, but not infinite, amount of money to spend on whatever Azure services we wanted. We're talking enough to dwarf our current costs, but not enough to move all mathlib CI to fast servers. What could we do with it for Lean/mathlib resources?

Two ideas to start: daily benchmark builds on reliable/fast hardware, and computing power for testing/benchmarking expensive tools like the hypothetical LeanHammer.

[Jalex Stark]

I think @Jannis Limperg and @Ryan Lahfa both have thoughts

[Jannis Limperg]

I tested one of Azure's f8s_v2 "compute" VMs (8 cores, ~200$/mo if we reserve it for 1 year) in search of fast CI. It compiles mathlib in 55min on 4 threads and 43min on 8 threads. Assuming that a full build takes at most double this time and assuming full utilisation (on 4 threads per job), we'd get 25 builds per day out of this VM. However, the improved build time is still quite long, so this probably doesn't make enough of a difference to justify the setup and maintenance hassle.

Benchmark builds wouldn't be hard to set up. Since these don't need to be fast, only consistent, their cheapest VM would suffice. I did a few 8-thread runs on the f8s_v2 VM and the time fluctuations seemed acceptable (+/- 1min).

[Gabriel Ebner]

Is this the time with 3.13 or 3.12?

[Gabriel Ebner]

BTW, since you sound knowledgeable on Azure: how hard is to spawn a VM on demand, execute something (like building mathlib), and then stop it again? Kinda like remote docker, if you this makes it clearer?

[Jannis Limperg]

These are 3.12 times. I can repeat the tests with 3.13 if that helps.

I don't know much about Azure (or any of these cloud platforms), sorry. I imagine that they'd support stuff like this (is this what 'Lambda' or 'serverless' is?), but also that it would be even more expensive than a regular VM.

[Gabriel Ebner]

Azure functions is only for short running stuff (like one or two minutes). I was wondering if there's a command-line tool for this. From what I gather, you're starting a VM via the web interface and then ssh into it?

[Rob Lewis]

So basically it's twice as fast as Actions. Whether or not that ratio holds with 3.13, I agree it's not worth it for faster CI.

[Rob Lewis]

There must be better uses of the resources.

[Jannis Limperg]

Gabriel Ebner said:

Azure functions is only for short running stuff (like one or two minutes). I was wondering if there's a command-line tool for this. From what I gather, you're starting a VM via the web interface and then ssh into it?

There is an Azure command-line client. I haven't worked with it yet, but the documentation references it frequently and it seems quite powerful.

[Ryan Lahfa]

Gabriel Ebner said:

BTW, since you sound knowledgeable on Azure: how hard is to spawn a VM on demand, execute something (like building mathlib), and then stop it again? Kinda like remote docker, if you this makes it clearer?

In general, this is not hard, but the problem is how fast does your cloud provider spawns the VM and how fast can you provision a machine to do things like building mathlib (installing Lean, etc. Though, you can quick-restore from an already-built Docker container, which bring the issue of having an up-to-date Docker image!)

Also, what is interesting is to use this technique with spot pricing, so that you can let the cloud providers ping you when he can spawn an VM at a super cheap price for you (but can interrupt you like 30-45 minutes after)

Some providers does this really quickly (Scaleway) and some not that much (Packet.com takes ~5-10 minutes I believe.)

[Rob Lewis]

Suppose that we had a reasonably large, but not infinite, amount of money to spend on whatever Azure services we wanted.

The hypothesis from last month has come true. We have $10k USD to spend on Azure before the end of the year (unless we manage to prolong this grant). This is a shorter time period than we were expecting, so we need ideas, and possibly people to implement them!

[Rob Lewis]

Jannis Limperg said:

I tested one of Azure's f8s_v2 "compute" VMs (8 cores, ~200$/mo if we reserve it for 1 year) in search of fast CI. It compiles mathlib in 55min on 4 threads and 43min on 8 threads. Assuming that a full build takes at most double this time and assuming full utilisation (on 4 threads per job), we'd get 25 builds per day out of this VM. However, the improved build time is still quite long, so this probably doesn't make enough of a difference to justify the setup and maintenance hassle.

Benchmark builds wouldn't be hard to set up. Since these don't need to be fast, only consistent, their cheapest VM would suffice. I did a few 8-thread runs on the f8s_v2 VM and the time fluctuations seemed acceptable (+/- 1min).

Coming back to this from a while ago. @Jannis Limperg would you be willing to look into setting up benchmark builds on Azure? We already have the scripts that @Scott Morrison uses for his bot in the #travis stream. Your experiments imply that we'd have much more consistent results than with Scott's server, and he'd get to stop wasting his CPU time and power.

[Rob Lewis]

Disclaimer that I don't know exactly how to do this myself, but: it seems reasonable to set up a GH Action that spawns a new VM and runs the build every time a commit hits master. We can also have a (maintainer-triggered?) action to run it on a PR build if we're suspicious of the changes.

[Jannis Limperg]

@Rob Lewis Sorry, forgot about this topic. Yes, I can set up some basic script for benchmarking.

[Rob Lewis]

Thanks! I"ll send you some info. We can also talk about it on Thursday.

[Rob Lewis]

Getting @Scott Morrison 's build time bot scripts would be a good place to start I guess.

[Scott Morrison]

Sorry, I've been disorganised about this, and keep planning to clean them up before posting them. Here are my (very hacky) scripts:

• build-time-bot.sh

cd "${0%/*}"
./time-mathlib-master.sh $1 | tee -a build-time-bot.log | /usr/local/bin/zulip-send --stream travis --subject "build time bot"

• time-mathlib-master.sh

mkdir -p ~/scratch/
cd ~/scratch/
rm -rf ~/scratch/time-mathlib-master-$1
git clone https://github.com/leanprover-community/mathlib.git time-mathlib-master-$1 2> /dev/null
cd time-mathlib-master-$1/
git checkout $1 > /dev/null
leanpkg configure > /dev/null
leanproject -f up > /dev/null
cd src/
REV=`git rev-parse HEAD`
printf "Building https://github.com/leanprover-community/mathlib/commit/$REV takes "
{ { time ~/bin/profile-mathlib ; } 2>&1 ; } | grep user | cut -f2
~/bin/rsyncs -q profile_output.json tqft.net:tqft.net/lean/mathlib/$REV.json
~/bin/rsyncs -q profile.log tqft.net:tqft.net/lean/mathlib/$REV.log
printf -- "per file compilation times at https://tqft.net/lean/mathlib/$REV.json\n"
printf -- "--profile output at https://tqft.net/lean/mathlib/$REV.log\n"
printf "\n"

• profile-mathlib

#!/usr/bin/env bash

if [[ $# = 2 ]]; then
  dir="$1"
  out="$2"
else
  dir="."
  out="profile_output.json"
fi

echo "{" > $out
for filename in $(find $dir -name '*.lean'); do
  [ -e "$filename" ] || continue
  echo $filename
  echo "----" >> profile.log
  echo $filename >> profile.log
  # gtime is homebrew's gnu-time; replace with /usr/bin/time on linux
  gtime -a -o $out -f"\"$filename\":[%U,%S,%e]," lean -j0 --profile $filename >> profile.log
done
# strip comma from last line
sed -i '' '$ s/.$//' $out
echo "}" >> $out

[Jannis Limperg]

Thank you!