This PR:
- turns the shell script into a python script
- fixes the unexpected by error. The old code was assuming something of
the form `:= sorry` to be replaced with `:= by tac` but now it's
substituting inside of a tactic block
- brings the script into the age of multi core CPUs, though care needs
to be taken when running with too many jobs as some of this stuff can be
quite memory hungry
- uses `lake lean` so you can actually run it multiple times in a row
without cleaning a lake cache (assuming you haven't actually compiled
the benchmark files of course)