[WIP] Turn on jemalloc, turn off custom allocators by default

[Kha]

tl;dr: 20% faster, 20% less memory :)

Not 100% sure the CI configs are correct yet.

CUSTOM_ALLOCATORS=ON, JEMALLOC=OFF, TCMALLOC=OFF:

	compilation 4.34s
	decl post-processing 797ms
	elaboration 69.4s
	elaboration: tactic compilation 12.6s
	elaboration: tactic execution 29.3s
	parsing 13.9s
	saving .olean 1.09s
	type checking 520ms
...
	User time (seconds): 125.32
        Maximum resident set size (kbytes): 505388

CUSTOM_ALLOCATORS=ON, JEMALLOC=ON:

	compilation 3.69s
	decl post-processing 703ms
	elaboration 52.7s
	elaboration: tactic compilation 9.01s
	elaboration: tactic execution 21.7s
	parsing 10.6s
	saving .olean 772ms
	type checking 423ms
...
	User time (seconds): 94.83
        Maximum resident set size (kbytes): 465244

CUSTOM_ALLOCATORS=OFF, JEMALLOC=ON:

	compilation 3.81s
	decl post-processing 654ms
	elaboration 53.2s
	elaboration: tactic compilation 8.74s
	elaboration: tactic execution 22.3s
	parsing 11.1s
	saving .olean 803ms
	type checking 439ms
...
	User time (seconds): 96.11
	Maximum resident set size (kbytes): 402700

CUSTOM_ALLOCATORS=OFF, TCMALLOC=ON:

	compilation 4.32s
	decl post-processing 747ms
	elaboration 64.1s
	elaboration: tactic compilation 11.3s
	elaboration: tactic execution 27.5s
	parsing 12.8s
	saving .olean 1.02s
	type checking 492ms
...
	User time (seconds): 113.37
	Maximum resident set size (kbytes): 354648

[Kha]

So, some observations:

• Linux: The release build fails when trying to statically link both glibc and jemalloc. This is a known issue with jemalloc that was fixed in a later version. However, we could also just stop linking glibc statically (which I believe is regarded as a bad idea anyway, as seen with our libpthread troubles).
• OS X: The debug build got faster, but the release build is timing out??
• Mingw: No change - presumably because the mingw-w64-jemalloc package has all functions prefixed with je_, so we're still using the default malloc/free.
• MSVC: There is a vcpkg jemalloc package, but building it fails.

I can change the behavior of the STATIC flag, but it would be great if others could investigate the other platforms (and measure whether it's an actually beneficial change there).

[ras0219-msft]

Fixed the vcpkg jemalloc package (on vcpkg's master now) -- it looks like a patchfile got corrupted by some editor trimming a trailing space :(

[Kha]

@ras0219-msft Thanks, building jemalloc is working now! It looks like jemalloc.h is missing a reference to their strings.h compatibility header (which sounds like an upstream bug), but we can live without it.

[Kha]

However, we could also just stop linking glibc statically (which I believe is regarded as a bad idea anyway, as seen with our libpthread troubles).

@leodemoura What do you think about changing STATIC? If you agree, I will open a new PR to enable jemalloc by default just on Linux.

[leodemoura]

@leodemoura What do you think about changing STATIC? If you agree, I will open a new PR to enable jemalloc by default just on Linux.

@Kha I think we can remove the STATIC flag. We originally added it because we wanted to be able to create a Linux binary that works in any distribution. For example, it would not depend on a particular version of glibc. I think this kind of feature is only relevant for closed source systems. For open source project like Lean, we can tell users to build Lean on their own non-standard Linux distributions if there isn't an official binary release for it.
Moreover, in Lean4, we will depend on LLVM, and it seems crazy to statically link it.

[leodemoura]

BTW, I will try this PR today on OSX and MSys2.

[Kha]

I think we can remove the STATIC flag

Fine with me.
Thanks for looking into it! Btw, do you think it makes sense to keep using Msys2 over MSVC for the release builds? I don't know which build is faster right now, though that may also depend on which of the two we get jemalloc working for.

[leodemoura]

Btw, do you think it makes sense to keep using Msys2 over MSVC for the release builds?

I think so. At least for me, Msys2 is the preferred way of building Lean on Windows.

[leodemoura]

Here is some information for the PR.
I managed to build Lean on OSX using
AppleClang 9.0.0.9000039 and jemalloc 5.0.1
I installed jemalloc using brew install jemalloc
It worked with the following two configurations:

1. cmake -D JEMALLOC=ON -D CUSTOM_ALLOCATORS=OFF -G Ninja ../../src
2. cmake -D JEMALLOC=ON -G Ninja ../../src

Time to build core lib with configuration 1) is 41 secs. The default configuration takes 50.1 secs.