Zulip Chat Archive

Stream: lean4

Topic: simple performance testing


view this post on Zulip Kevin Lacker (Jan 06 2021 at 22:50):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 22:52):

Compiled or interpreted?

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 22:52):

Your README suggests interpreted

view this post on Zulip Kevin Lacker (Jan 06 2021 at 22:53):

what's a better command to run here

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 22:54):

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

view this post on Zulip Kevin Lacker (Jan 06 2021 at 22:58):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 23:00):

Use leanmake bin

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 23:01):

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

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:01):

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

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:02):

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?

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:09):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:09):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:10):

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

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:12):

invalid option -- 'O'

view this post on Zulip Mario Carneiro (Jan 06 2021 at 23:12):

leanc

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:13):

Nope, misread the file, one sec

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:13):

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

view this post on Zulip Mario Carneiro (Jan 06 2021 at 23:13):

which line are you looking at @Yakov Pechersky ?

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:13):

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

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:13):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:13):

try it without any -O3 -DNDEBUG

view this post on Zulip Mario Carneiro (Jan 06 2021 at 23:13):

line

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:14):

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

view this post on Zulip Mario Carneiro (Jan 06 2021 at 23:14):

there are like 6 lean invocation lines in that script

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:14):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:14):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:15):

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

view this post on Zulip Mario Carneiro (Jan 06 2021 at 23:15):

I think it comes from an environment variable

view this post on Zulip Mario Carneiro (Jan 06 2021 at 23:15):

so probably empty

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:16):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:16):

Or things passed in via lean --make

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 23:16):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 23:17):

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

view this post on Zulip Mario Carneiro (Jan 06 2021 at 23:17):

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

view this post on Zulip Mario Carneiro (Jan 06 2021 at 23:18):

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

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:20):

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

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:24):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 23:26):

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

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:28):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 23:30):

We're still figuring out some guidelines on that

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 23:31):

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

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:34):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 23:35):

The one in .elan/toolchains

view this post on Zulip Kevin Lacker (Jan 06 2021 at 23:39):

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

view this post on Zulip Reid Barton (Jan 07 2021 at 00:00):

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

view this post on Zulip Wojciech Nawrocki (Jan 07 2021 at 00:18):

@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.

view this post on Zulip Kevin Lacker (Jan 07 2021 at 00:25):

sweet, that seems promising.

view this post on Zulip Kevin Lacker (Jan 07 2021 at 17:12):

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

view this post on Zulip Kevin Lacker (Jan 07 2021 at 17:13):

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

view this post on Zulip Sebastian Ullrich (Jan 09 2021 at 10:25):

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.

view this post on Zulip Reid Barton (Jan 09 2021 at 16:36):

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

view this post on Zulip Sebastian Ullrich (Jan 09 2021 at 21:01):

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


Last updated: May 07 2021 at 12:15 UTC