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

--output-split units documented as bytes, but appears to be closer to lines #1615

Closed
veripoolbot opened this issue Nov 27, 2019 · 3 comments
Closed

Comments

@veripoolbot
Copy link

@veripoolbot veripoolbot commented Nov 27, 2019


Author Name: Julien Margetts
Original Redmine Issue: 1615 from https://www.veripool.org


The manual states the units of the --output-split option as bytes in both the summary and the full description, but internally splitSize() is counting lines (roughly)

There may be some double counting, since in my case with --output-split 100000, all output files have a line count of ~50000

@veripoolbot

This comment has been minimized.

Copy link
Author

@veripoolbot veripoolbot commented Nov 27, 2019


Original Redmine Comment
Author Name: Julien Margetts
Original Date: 2019-11-27T10:58:09Z


It would also be worth mentioning that VM_PARALLEL_BUILDS needs to be set to 1 on the make command line to exploit parallel compilation of the split files.

@veripoolbot

This comment has been minimized.

Copy link
Author

@veripoolbot veripoolbot commented Nov 27, 2019


Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2019-11-27T11:12:55Z


Thanks, will update these in the docs.

Output-split is roughly number of statements.

@veripoolbot

This comment has been minimized.

Copy link
Author

@veripoolbot veripoolbot commented Dec 1, 2019


Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2019-12-01T17:43:54Z


Fixed in git.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
1 participant
You can’t perform that action at this time.