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

feat: add basic file I/O implementations #60

Merged
merged 23 commits into from
Dec 2, 2022

Conversation

alex-chew
Copy link
Contributor

@alex-chew alex-chew commented Nov 11, 2022

This PR adds basic file I/O facilities (read bytes from a file, write bytes to a file) to the for C#, Java, Javascript. Python support is nearly complete, but is blocked by what I believe is a missing external-module import in compiled code. Golang support is out of scope for now, since it's blocked by dafny-lang/dafny#2989 and dafny-lang/dafny#2045.

This PR was migrated from dafny-lang/dafny#3018 for further development.

Fixes #50.

TODO:

  • Add doc comments to Dafny APIs
  • Add README explaining how to consume the module (other than the code examples)
  • Preserve exception stack traces
  • When writing, create parent directories if needed
  • Ensure paths work the same across target languages (and if possible, across platforms)
  • Fix Python support (currently unable to reference the newly defined DafnyLibrary from another compiled module) (Python support to be added as a follow-up)

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@alex-chew
Copy link
Contributor Author

For reviewers coming from the original PR (dafny-lang/dafny#3018) - the module/file structure in this PR is much simplified. Because we're no longer concerned with stuffing the internal file I/O implementations into existing runtime module names, we have the freedom to name the containing module in a way that works across all languages. So now including FileIO.dfy is all that's needed to reference the file I/O APIs from every target language - no target-specific includes/modules. During compile/run time, however, users will need to link the corresponding target-specific implementation (FileIO.{cs,java,js,py}) as it's not included in the runtime anymore.

This also means that consumers of the API no longer need to rely on module abstraction - just including and importing FileIO is sufficient. In this PR, for example, there are now only two test files (one for reading bytes and one for writing bytes).

@davidcok
Copy link
Collaborator

Just checking that read from stdin and write to stdout will be possible with this PR

@alex-chew
Copy link
Contributor Author

Just checking that read from stdin and write to stdout will be possible with this PR

This is not in scope for this PR.

@alex-chew
Copy link
Contributor Author

(CI is failing for unrelated reasons, but should pass once #61 is merged.)

@alex-chew alex-chew marked this pull request as ready for review December 1, 2022 19:58
@alex-chew
Copy link
Contributor Author

The tests are failing because somehow the Dafny being run doesn't know about --target and a few other flags:

Dafny: Error: unknown switch: --no-verify
Dafny: Error: unknown switch: --target
Dafny: Error: unknown switch: --input
Dafny: Error: unknown switch: --
Use /help for available options

error: command failed with exit status: 1

Maybe dafny run isn't available in the version of Dafny we're using here?

@MikaelMayer
Copy link
Member

Maybe dafny run isn't available in the version of Dafny we're using here?

Yes I think that's right. We did not update the dafny version in libraries for a long time.

Copy link
Member

@robin-aws robin-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice work, and well polished. I really appreciate the commitment to writing the same documentation in four different language dialects. :)

.github/workflows/tests.yml Show resolved Hide resolved
src/FileIO/FileIO.js Show resolved Hide resolved
src/FileIO/README.md Show resolved Hide resolved
src/FileIO/README.md Show resolved Hide resolved
examples/FileIO/ReadBytesFromFile.dfy Outdated Show resolved Hide resolved
examples/FileIO/ReadBytesFromFile.dfy Outdated Show resolved Hide resolved
examples/FileIO/WriteBytesToFile.dfy Show resolved Hide resolved
Copy link
Member

@atomb atomb left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks very nice!

examples/FileIO/ReadBytesFromFile.dfy Outdated Show resolved Hide resolved
examples/FileIO/WriteBytesToFile.dfy.expect Outdated Show resolved Hide resolved
/// </summary>
public static void INTERNAL_ReadBytesFromFile(ISequence<char> path, out bool isError, out ISequence<byte> bytesRead,
out ISequence<char> errorMsg) {
isError = true;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like that you initialize it this way. Starting out assuming an error and not indicating success until you've explicitly observed it is a nice practice.

src/FileIO/FileIO.dfy Show resolved Hide resolved
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Request: very basic file I/O
5 participants