Skip to content

Can't rebuild standard library files on Windows #4989

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

Closed
robin-aws opened this issue Jan 16, 2024 · 1 comment · Fixed by #4824 · May be fixed by #5060
Closed

Can't rebuild standard library files on Windows #4989

robin-aws opened this issue Jan 16, 2024 · 1 comment · Fixed by #4824 · May be fixed by #5060
Assignees
Labels
kind: language development speed Slows down development of Dafny the language, flaky tests platform: windows Windows-specific issues

Comments

@robin-aws
Copy link
Member

Follow up from #4824

The check-binary Make targets work by rebuilding the doo files, then comparing them to the checked in copies. They do this by unzipping and comparing the contents. Because the currently committed doo files are generally built on Macs, this means if a developer makes changes and rebuilds them on a Windows machine, the comparison fails because of the difference in line endings.

I propose fixing this by standardizing line endings inside doo files. This does imply altering program content when serializing to doo files, but this is already happening (merging multiple original source files into one, not yet maintaining comments or formatting of expressions in general) and needs to be allowed in general in order to optimize doo files in the future.

@robin-aws robin-aws added platform: windows Windows-specific issues kind: language development speed Slows down development of Dafny the language, flaky tests labels Jan 16, 2024
@robin-aws robin-aws self-assigned this Jan 16, 2024
@MikaelMayer
Copy link
Member

Yeah I agree. Before parsing the source files that will eventually generate the doo files, we should convert line endings to be "\n" in any case so that it will solve the problem on Windows.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: language development speed Slows down development of Dafny the language, flaky tests platform: windows Windows-specific issues
Projects
None yet
2 participants