Simple programs run for many seconds

[yurivict]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Simple type programs run for many seconds. For instance, this example runs for many seconds both on the website and when run from the terminal.

Versions

Version: 3.48.0

[gebner]

I can't reproduce this issue. The live version on the website takes a couple of seconds to load (no matter the file), but after that your example is instantaneous.

[yurivict]

Is C++ compiled version instantaneous for you on simple scripts? Then I need to profile it.

[gebner]

It takes around 350ms.

[yurivict]

Simple program takes ~22 sec on FreeBSD:

$ time lean simple.lean 
m : ℕ

real	0m22.868s
user	0m51.723s
sys	0m0.505s

[yurivict]

I got this profile:

Some functions are called 1.5+ billion times, and many functions are called over 500 million times. I don't think you even have so many objects of any kind. Some of the algorithms are obviously inefficient.

C++ library is different on FreeBSD, this might have causes the compiler to interpret some code differently.

[yurivict]

I am pretty sure that there is a C++ problem in the code. Maybe some shared_ptr is copied often when this isn't needed - passing by address usually suffices.

[gebner]

I think all you need to do is:

cd lean/library
lean --make

[yurivict]

This solved the problem.

But why isn't this done in the course of normal build? There is the code for this in CMakeLists.txt, but it isn't run for some reason.