C++17

Stream: lean4

[Eric Frazer]

Hi all. Eric F here. I'm on the MSR team, and helping to move the build along into the year 2022. As such, we'd like to move the compilers to all use C++17 so we can use std::thread and some standardized filesystem stuff. This didn't work in the past, but we're pretty sure with the latest OS revisions, this is worth a shot. I've compiled lean on windows, WSL (on windows), and the mac, and run the tests, and so far so good. Any big red flags I should be aware of?

[Eric Frazer]

hm. spoke too soon. test #936 "leancomptest_foreign" failed. What do you know! Will have Lovett look into it. heh.

[Eric Frazer]

that was on the macOS, btw

[Sebastian Ullrich]

@Eric Frazer Thanks for doing it! There are two usual caveats that you may already know, but I'll just repeat them here for the sake of completeness:

• There may be a future where either the Lean runtime or all of Lean is free of C++, so we might not want to move existing filesystem primitives implemented using C APIs to C++ unless there is a specific reason to do so
• We have avoided std::thread so far because it does not let us customize the thread stack size

[Eric Frazer]

Stack size: since we ultimately hope to get away from even C++, is the thread stack size a super big issue?

[Eric Frazer]

moving from C to C++: The code as I've seen it, is much simpler in the new form, than the existing stuff, it can only help the transition to something better.

[Eric Frazer]

image.png

[Eric Frazer]

is the stack size concern mostly paranoia, or did we run up against a wall in the past and go "splat"?

[Sebastian Ullrich]

Yes, as a functional language it is very easy to consume loads of stack using non-tail recursion in Lean!

[Sebastian Ullrich]

Fun line: https://github.com/kha/lean4/blob/25ebc68b875f87f04e7b6ad35e5f239e1a750e8a/src/CMakeLists.txt#L128

[Eric Frazer]

Isn't the stack size for new threads the default stack size for the running OS? Is it settable somewhere in the OS settings? I imagine whatever machine is running gigantic Lean proofs is probably somewhat dedicated to that task, and one could set the default stack size?

[Eric Frazer]

this article is unusually informative, in various places....

[Eric Frazer]

https://stackoverflow.com/questions/13871763/how-to-set-the-stacksize-with-c11-stdthread/20502804

[Eric Frazer]

ha. Leo is one of the commenters in that article.

[Eric Frazer]

How did we get past the 512K limit on mac OS? was that an old mac OS limitation?

[Sebastian Ullrich]

Is there a limit? The linked question seems to only talk about defaults

[Sebastian Ullrich]

We have perfectly working custom thread stack sizes on all platforms right now, so I don't understand why we would want to move away from that

[Eric Frazer]

the code has a lot of switches in it right now for one OS or another. it's somewhat messy. especially the pthread stuff and the file iterator stuff. In an effort to unify the code and getting it looking the same, and then ultimately getting it to compile "the right way" on Windows, it'd be nice to move the C++ code forward into the 21st century and get it reasonably standard. So, why not move it to std::thread, and monkey with the linker thread stack sizes and see what works and what doesn't, and go from there?

[Eric Frazer]

c++11 is so last-year. ha ha.

[Eric Frazer]

if we can set the default thread stack size for the process, even with std::thread, I would imagine this is sufficient. Can't see how a Lean program would want one stack size for one thread, and another for a different thread. Especially since it's simply a reservation, not an actual allocation.

[Sebastian Ullrich]

Yeah, that would work. But is there really an API for that?

[Chris Lovett]

One question Sebastian, can Lean customers request a stack size for new threads when they are implementing some crazy algorithm that is known to explode recursion? I'm hoping we have not given customers that power yet...

[Mario Carneiro]

why not? functional programs are known to have deep recursions, especially if put on the C stack

[Mario Carneiro]

(also, "users" is a more appropriate appellation than "customers", since lean is a programming language not a company)

[Chris Lovett]

users works too, but it is not uncommon terminology even for open source projects
image.png
it more clearly delineates people not working on the internals of the Lean compiler.

[Chris Lovett]

@Eric, can you do a test using this apple doc page and see if setStackSize works with std::thread? I don't see a max stack size listed there. I thought I saw that some place else, but looks like that other source was wrong.

[Scott Morrison]

(I don't want to bikeshed, but I am anyway: a large fraction of Lean's users are mathematicians, who are typically highly allergic to the word "customer".)

[Reid Barton]

(In that quote I think the word "customer" refers to clients of a commercial product which is developed by the author of the testimonial, not Rust users/programmers.)

[Eric Frazer]

I'm going to test setting the global program stack size on the 3 platform types, tonight, and run some whopper recursion tests.

[Eric Frazer]

I saw some code today that takes a std::thread, and on each of the platforms, runs some dirty-dog tricks to get behind the thread and into OS-specific code and set the stack size, but it made some of my hair fall out.