Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Warn about backtrace recording in README #58

Closed
wants to merge 1 commit into from
Closed

Warn about backtrace recording in README #58

wants to merge 1 commit into from

Conversation

mpu
Copy link
Contributor

@mpu mpu commented Apr 19, 2020

I was thinking my old laptop really needed to be replaced as it took it more than 20 minutes to load HOL Light. Some investigation revealed that all the time was spent recording backtraces. Disabling the recording brought down the loading time to 2 minutes.

This PR proposes to add a warning in the README about this potential issue. I will let you judge if it belongs where I inserted it.

Thanks!

@jrh13
Copy link
Owner

jrh13 commented May 3, 2020

Very interesting point, something I'd never been aware of.
I'm happy indeed to add a warning to the README. Do you
know any more about the circumstances that in general
lead to the backtrace recording being on by default? I've
not noticed this happening in my own OCaml instances,
which are mainly from the debian or homebrew package
managers.

@mpu
Copy link
Contributor Author

mpu commented May 12, 2020

The problem might not happen to many, so I now think that
adding a step like I did in the README might be a bit overkill.

The reason it hit me is that I had OCAMLRUNPARAM=b set
in my shell configuration (it is handy when doing ocaml
development to print backtraces).

It looks like Jane Street's Base library (a popular stdlib
replacement) also has recording on by default.

@mpu
Copy link
Contributor Author

mpu commented Oct 22, 2020

I'm going to close the PR. If someone has perf problems
maybe Google will be able to help! At least, now you are
also aware of this potential problem.

@mpu mpu closed this Oct 22, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants