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

Jump to bottom

--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

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

veripoolbot opened this issue Nov 27, 2019 · 3 comments
Labels
area: documentation Issue involves documentation resolution: fixed Closed; fixed

Comments

@veripoolbot
Copy link
Contributor

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
Copy link
Contributor Author

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
Copy link
Contributor Author

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
Copy link
Contributor Author

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

Fixed in git.

@veripoolbot veripoolbot added area: documentation Issue involves documentation resolution: fixed Closed; fixed labels Dec 22, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
area: documentation Issue involves documentation resolution: fixed Closed; fixed
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@veripoolbot