Skip to content

chore: add file append #163

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.

Sign up for GitHub

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

Merged
robin-aws merged 8 commits into from
Dec 16, 2024
Merged

chore: add file append #163

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
829e463
chore: add file append
ajewellamz Dec 15, 2024
f535e67
m
ajewellamz Dec 15, 2024
6c3ee19
m
ajewellamz Dec 16, 2024
8099db8
m
ajewellamz Dec 16, 2024
d5353a4
m
ajewellamz Dec 16, 2024
f238ad3
m
ajewellamz Dec 16, 2024
952ed61
Revert "m"
robin-aws Dec 16, 2024
b6e11b5
Add link to issue
robin-aws Dec 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions .github/workflows/reusable-tests.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,16 @@ jobs:
- name: Upgrade outdated pip
run: python -m pip install --upgrade pip

- name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
uses: actions/setup-dotnet@v4
with:
dotnet-version: 8.0.x

- name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
uses: actions/setup-dotnet@v4
with:
dotnet-version: 6.0.x

- name: Install lit
run: pip install lit OutputCheck

Expand Down
4 changes: 3 additions & 1 deletion examples/Collections/Arrays/BinarySearch.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// RUN: %run "%s" > "%t"
// RUN: %OutputCheck --file-to-check "%t" "%s"

// OutputCheck is broken, see https://github.com/dafny-lang/libraries/issues/164
// not working: %OutputCheck --file-to-check "%t" "%s"
// CHECK-L: [-6, 0, 1, 3, 7, 7, 9]
// CHECK-NEXT-L: 3

Expand Down
4 changes: 3 additions & 1 deletion examples/WrappersExamples.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// RUN: %run "%s" > "%t"
// RUN: %OutputCheck --file-to-check "%t" "%s"

// OutputCheck is broken, see https://github.com/dafny-lang/libraries/issues/164
// not working: %OutputCheck --file-to-check "%t" "%s"
// CHECK-L: Hello
// CHECK-NEXT-L: Error: 'name' was not found
// CHECK-NEXT-L: Hello
Expand Down
21 changes: 20 additions & 1 deletion src/FileIO/FileIO.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ include "../Wrappers.dfy"
module {:options "-functionSyntax:4"} FileIO {
import opened Wrappers

export provides ReadBytesFromFile, WriteBytesToFile, Wrappers
export provides AppendBytesToFile, ReadBytesFromFile, WriteBytesToFile, Wrappers

/*
* Public API
Expand Down Expand Up @@ -52,6 +52,20 @@ module {:options "-functionSyntax:4"} FileIO {
return if isError then Failure(errorMsg) else Success(());
}

/**
* Attempts to append the given bytes to the file at the given file path,
* creating nonexistent parent directories as necessary.
* If an error occurs, a `Result.Failure` value is returned containing an implementation-specific
* error message (which may also contain a stack trace).
*
* NOTE: See the module description for limitations on the path argument.
*/
method AppendBytesToFile(path: string, bytes: seq<bv8>) returns (res: Result<(), string>)
{
var isError, errorMsg := INTERNAL_AppendBytesToFile(path, bytes);
return if isError then Failure(errorMsg) else Success(());
}

/*
* Private API - these are intentionally not exported from the module and should not be used elsewhere
*/
Expand All @@ -65,4 +79,9 @@ module {:options "-functionSyntax:4"} FileIO {
{:extern "DafnyLibraries.FileIO", "INTERNAL_WriteBytesToFile"}
INTERNAL_WriteBytesToFile(path: string, bytes: seq<bv8>)
returns (isError: bool, errorMsg: string)

method
{:extern "DafnyLibraries.FileIO", "INTERNAL_AppendBytesToFile"}
INTERNAL_AppendBytesToFile(path: string, bytes: seq<bv8>)
returns (isError: bool, errorMsg: string)
}
Loading