simple performance testing

Stream: lean4

[Kevin Lacker]

Hey, I thought I'd do some simple benchmark-type testing to poke around with Lean 4, compare to c++, and share the results. Basically just converting integers to strings and inserting into a hash table ten million times. Lean 4 code:

import Std.Data.HashMap

def insert_n (map : Std.HashMap String Nat) (n : Nat) : Std.HashMap String Nat := do
  map.insert (toString n) n

def main (args : List String) : IO Unit := do
  let mut map : Std.HashMap String Nat := Std.HashMap.empty
  for n in [0:10000000] do
    map := insert_n map n
  IO.print "ran "
  IO.print (toString map.size)
  IO.print " map inserts\n"

C++ code:

#include <iostream>
#include <string>
#include <unordered_map>

int main() {
  std::unordered_map<std::string, int> map;
  for (int i = 0; i < 10000000; i++) {
    map[std::to_string(i)] = i;
  }
  std::cout << "ran " << map.size() << " map inserts\n";
  return 0;
}

C++ version about 5x faster on my machine, this is the first Lean 4 I've written so I could be doing something non-optimal here, but really within 5x of C++ on a benchmark like this might be pretty good. Code at https://github.com/lacker/lean4perf if people are curious to tweak it

[Yakov Pechersky]

Compiled or interpreted?

[Yakov Pechersky]

Your README suggests interpreted

[Kevin Lacker]

what's a better command to run here

[Yakov Pechersky]

I think the slides from the other day show the lean > olean > .c > .o workflow

[Kevin Lacker]

hmm, there is a flag in lean to create a .c file, but it doesn't look like it's independently usable, it requires a lean/lean.himport

[Sebastian Ullrich]

Use leanmake bin

[Sebastian Ullrich]

Are you compiling the C++ code without optimizations??

[Kevin Lacker]

plain old g++, the exact command lines are in that repo

[Kevin Lacker]

leanmake bin doesn't work for me, a bunch of errors like /nix/store/08fwy6y1fjp8pa68kq3bffif1xjya3j1-ccache-3.4.1/bin/ccache: No such file or directory. does leanmake only work when you use lean4 with nix?

[Kevin Lacker]

I tried out the different g++ optimization flags, they do make a bit of difference, -O3 makes the c++ version about 25% faster

[Yakov Pechersky]

I'm looking at https://github.com/leanprover/lean4/blob/eba3983658faef2d41b7ad00fc2c2e540a1e43e6/stage0/src/lean.mk.in

[Yakov Pechersky]

so, lean -O3 -DNDEBUG -o benchmark.olean --c=benchmark.c benchmark.lean I think?

[Kevin Lacker]

invalid option -- 'O'

[Mario Carneiro]

leanc

[Yakov Pechersky]

Nope, misread the file, one sec

[Kevin Lacker]

hmm more nix errors when I run leanc. line 36: /nix/store/08fwy6y1fjp8pa68kq3bffif1xjya3j1-ccache-3.4.1/bin/ccache: No such file or directory

[Mario Carneiro]

which line are you looking at @Yakov Pechersky ?

[Yakov Pechersky]

https://github.com/leanprover/lean4/blob/eba3983658faef2d41b7ad00fc2c2e540a1e43e6/stage0/src/lean.mk.in

[Kevin Lacker]

i'm not running nix at all, I tried to keep this lean4 installation minimalist and only did an elan install

[Yakov Pechersky]

try it without any -O3 -DNDEBUG

[Mario Carneiro]

line

[Kevin Lacker]

I get the same /nix error when running leanc without those flags

[Mario Carneiro]

there are like 6 lean invocation lines in that script

[Yakov Pechersky]

https://github.com/leanprover/lean4/blob/eba3983658faef2d41b7ad00fc2c2e540a1e43e6/stage0/src/lean.mk.in#L59

[Yakov Pechersky]

lean -o benchmark.olean --c=benchmark.c benchmark.lean

[Yakov Pechersky]

i'm trying to find what LEAN_EXTRA_MAKE_OPTS they pass at any point

[Mario Carneiro]

I think it comes from an environment variable

[Mario Carneiro]

so probably empty

[Kevin Lacker]

that works but now benchmark.c includes a lean/lean.h

[Yakov Pechersky]

Or things passed in via lean --make

[Sebastian Ullrich]

Oh, the released leanc looks broken... that path should not be there

[Yakov Pechersky]

well, it's in include/lean/lean.h if you want to try Kevin

[Mario Carneiro]

does it work if you just call leanc on the file anyway?

[Mario Carneiro]

what is leanc anyway? If it's reading c files then it must be a wrapper around gcc or something?

[Kevin Lacker]

i tried gcc -I /home/lacker/.elan/toolchains/leanprover-lean4-4.0.0-m1/include/ benchmark.c but then I am getting a ton of errors like

/tmp/ccLduRU9.o: In function `lean_alloc_small_object':
benchmark.c:(.text+0x14f): undefined reference to `lean_alloc_small'
/tmp/ccLduRU9.o: In function `lean_alloc_ctor_memory':
benchmark.c:(.text+0x1b3): undefined reference to `lean_alloc_small'
/tmp/ccLduRU9.o: In function `lean_dec_ref':
benchmark.c:(.text+0x34f): undefined reference to `lean_del'

and I feel like this rabbit hole keeps going a ways

[Kevin Lacker]

even leanc --help is failing for me with some "/nix/blahblahblah not found" so perhaps some bug is in the leanc release and I should patiently wait for it to be magically fixed

[Sebastian Ullrich]

Yeah, look forward to a nightly soon. But not today/tomorrow.

[Kevin Lacker]

is it helpful to file github issues or report bugs in some formal way, or nah

[Sebastian Ullrich]

We're still figuring out some guidelines on that

[Sebastian Ullrich]

Btw, if you don't want to wait, feel free to just remove those paths from your installed leanc manually. elan shouldn't mind.

[Kevin Lacker]

I don't mind waiting, my goal was really to poke around and see if I discovered anything interesting and I judge that goal to be a success. but my installed leanc appears to be some opaque binary, anyway, not an editable script

[Sebastian Ullrich]

The one in .elan/toolchains

[Kevin Lacker]

ok. it looks like it needs to run a binary called ccache in that nix directory? ... i'm inclined to just wait

[Reid Barton]

You could try a version of the incantation here with the -I and -L paths adjusted to your installation

[Wojciech Nawrocki]

@Kevin Lacker using the Nix shell, the following works for me:

$ nix-shell -A nix # Or nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
$ nix build .#stage1 # Populates the result/ directory
$ cd klbench/ # I put the benchmarks here
$ g++ main.cpp -O3 -o main_cpp
$ exit # Exit the Nix shell, otherwise linking fails on my system
$ cd klbench/
$ ../result/bin/leanmake bin PKG=main # Builds main.lean
$ time ./build/bin/main
ran 10000000 map inserts

real    0m10.745s
user    0m10.450s
sys 0m0.283s

$ time ./main_cpp
ran 10000000 map inserts

real    0m7.472s
user    0m7.199s
sys 0m0.264s

Note this is on a custom build of Lean with my own changes, so massive disclaimer -- performance not representative of anything.

[Kevin Lacker]

sweet, that seems promising.

[Kevin Lacker]

i know it's a pretty small/artificial benchmark, but this makes me think that we will want a way to compile tactics for mathlib even if the "math" parts of the library are interpreted

[Kevin Lacker]

this got about 5x faster, if tactics also could be about 5x faster then it would be worth some build weirdness

[Sebastian Ullrich]

For any comparison between the interpreter and compiler you'll want to use -Dinterpreter.prefer_native=false with --run or anything in the stdlib will not be interpreted. Also note that the Lean 4 interpreter is (quite?) a bit faster than the Lean 3 one IIRC.

[Reid Barton]

I made the following changes to leanc locally:

• remove the ccache usage, so the line starts $LEAN_CXX (I guess you could try using a system ccache, I don't really know what it does);
• add -no-pie to ldflags_ext (apparently Ubuntu wants to build PIE by default but the Lean binary distribution has non-PIE libraries);
• remove the nix path from the for loop;
• add > /dev/null to the two command -v invocations to make the build a little more quiet

[Sebastian Ullrich]

@Reid Barton Thanks for checking, should now be covered by https://github.com/leanprover/lean4/pull/256