feat: revamp file IO, this time Windows compatible #4950
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
hargoniX
added
the
release-ci
github-actions
bot
added
the
changes-stage0
|
The failing check is a race condition introduced by a different bug on master. The key point of this PR: Make bootstrapping and in general Lean compile and run on all architectures again. is achieved so this is fine to merge. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This implements a naive version of
getlinebecause Windows does not havegetline. Given the fact thatFILEhas buffered IO, callingfgetcin a loop is not as big of a performance hazard as it might seem at first glance.The proper solution to this would of course be to have our own buffered IO so we are fully in charge of the buffer. In this situation we could check the entire buffer for a newline at once instead of char by char. However that is not going to happen for the near future so I propose we stay with this implementation. If reading individual lines of a file does truly end up being the performance bottle neck we have already won^^.