chore: add file append (#163)

Co-authored-by: Robin Salkeld <[email protected]>

.github/workflows/reusable-tests.yml

@@ -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
 

examples/Collections/Arrays/BinarySearch.dfy

@@ -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
 

examples/WrappersExamples.dfy

@@ -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

src/FileIO/FileIO.dfy

@@ -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
@@ -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
    */
@@ -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)
 }