feat: Per-backend code support in standard libraries, FileIO library #4790
Conversation
This reverts commit 9a91cf0.
…-backend-code-support-in-stdlibs # Conflicts: # Source/DafnyDriver/Commands/DafnyCli.cs # Source/DafnyPipeline/DafnyPipeline.csproj # Source/DafnyStandardLibraries/Makefile # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo # Source/DafnyStandardLibraries/src/dfyconfig.toml
…erage-report-per-module-breakdown
(just capturing to come back to later)
This reverts commit 56cd2b4.
…in-aws/dafny into per-backend-code-support-in-stdlibs # Conflicts: # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-arithmetic.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
robin-aws
changed the title
robin-aws
changed the title
| * | ||
| * File path symbols including . and .. are allowed. | ||
| */ | ||
| module DafnyStdLibs.FileIO { |
There was a problem hiding this comment.
nit: It seems a bit strange to name this file with all the different target languages it supports. In particular, once we add support for another target language, we'd change the filename but not its contents.
edit: I see now that the Makefile uses the filename to detect in which languages the file should be included - this seems a bit hacky, but I don't think it's a blocker for now.
There was a problem hiding this comment.
It is definitely a bit hacky, but the cleanest thing I could figure out without a lot of code duplication. We'll want to design a better solution for all multi-target Dafny projects in the future for sure.
| // But it makes debugging the translated output a little clearer. | ||
| {:compile false} | ||
| {:extern "DafnyStdLibs_FileIOInternalExterns"} | ||
| {:dummyImportMember "INTERNAL__ReadBytesFromFile", false} |
There was a problem hiding this comment.
(not blocking) What does this attribute do? I don't see it in (the current development version of) the reference manual.
...ce/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy
Show resolved
Hide resolved
Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns.py
Outdated
Show resolved
Hide resolved
...andardLibraries/src/DafnyStdLibs_FileIOInternalExterns/DafnyStdLibs_FileIOInternalExterns.go
Outdated
Show resolved
Hide resolved
Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com>
…n-aws/dafny into per-backend-code-support-in-stdlibs # Conflicts: # Source/DafnyStandardLibraries/CONTRIBUTING.md
Appears to be a race condition
|
Awesome! |
Description
Adds build support for standard libraries with different Dafny and target language source code per backend, and imports the
FileIOlibrary.The build support mainly adds a set of
DafnyStandardLibraries-<target>.doofiles, and a commonDafnyStandardLibraries-notarget.doofile with only the abstract interface. The pattern looks a lot like replaceable modules, but is less efficient for now because it re-verifies common code rather than relying on refinement.Please pay particular attention to the documentation updates as this does slightly affect the user experience with standard libraries!
Major changes to
FileIOon the way in:README.mdsince it's all automatic now (yay!)Other supporting changes:
_dafny.Sequenceand[]byte.make update-binary, since failing to do that and therefore not picking up the new versions of the.doofiles was a common gotcha..doofiles against fresh builds of them was failing for what looks like whitespace/newline variation. It makes more sense to stick to Mac OS for verification of production Dafny code anyway, however, since most contributors are developing on macs and verification is not guaranteed to be consistent across platforms.How has this been tested?
StandardLibraries_TargetSpecific.dfyfor the general support,FileIOExamples.dfyforFileIOitself (mainly the same as the original library, adapted as Dafny tests instead of lit tests)By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.