feat: add basic file I/O implementations

alex-chew commented 1 year ago

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 https://github.com/dafny-lang/dafny/issues/2989 and https://github.com/dafny-lang/dafny/issues/2045.

This PR was migrated from https://github.com/dafny-lang/dafny/pull/3018 for further development.

Fixes #50.

TODO:

[x] Add doc comments to Dafny APIs
[x] Add README explaining how to consume the module (other than the code examples)
[x] Preserve exception stack traces
[x] When writing, create parent directories if needed
[x] 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 commented 1 year ago

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 commented 1 year ago

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

alex-chew commented 1 year ago

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 commented 1 year ago

(CI is failing for unrelated reasons, but should pass once https://github.com/dafny-lang/libraries/pull/61 is merged.)

alex-chew commented 1 year ago

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 commented 1 year ago

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.

dafny-lang / libraries

feat: add basic file I/O implementations #60