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

Crash whith Mono when loading large log files #33

Open
fpoli opened this issue Aug 26, 2021 · 2 comments
Open

Crash whith Mono when loading large log files #33

fpoli opened this issue Aug 26, 2021 · 2 comments
Labels
bug Something isn't working

Comments

@fpoli
Copy link
Member

fpoli commented Aug 26, 2021

When running the axiom profiler with Mono, loading any log file of nontrivial size (more than a few megabytes) seems to cause a crash. Using Mono is currently the only way to run the axiom profiler on non-Windows OSs, so this issue might affect many users that want to try the profiler.

Probably related to this, the wiki of FStar reports the following:

Using mono, the profiler seems too slow to process any trace of nontrivial size (with a 15 Mo z3.log, it ran for an hour before I kill it);

@fpoli fpoli added the bug Something isn't working label Aug 26, 2021
@fpoli
Copy link
Member Author

fpoli commented Aug 26, 2021

PR #25 might fix this, but it seems the changes were lost in the migration to GitHub.

@bobismijnnaam
Copy link

bobismijnnaam commented Feb 21, 2022

We (the VerCors developers) run into this frequently. Especially since our files are often several hundred megabytes. Even cutting log files down to 2mb, axiom profiler still seems to have problems.

The crash I am currently getting is that axiom profiler spends some time loading a file, then suddenly closes and prints "Eliminated" (in dutch) in my terminal. I will probably soon try analyzing this file on windows, to see if the problem is with axiom profiler or this specific log file.

EDIT: Our experiences are probably because of issue #35, as I get the exact same behaviour with my log files on linux as the behaviour described in that issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants