Fix build

robin-aws · Nov 16, 2023 · 19424a5 · 19424a5
1 parent c4375b2
commit 19424a5
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 11 deletions.
diff --git a/Source/DafnyStandardLibraries/Makefile b/Source/DafnyStandardLibraries/Makefile
@@ -25,12 +25,12 @@ check-binary: build-binary
 	unzip -o ${DOO_FILE_ARITHMETIC_SOURCE} -d build/current-arithmetic
 	unzip -o ${DOO_FILE_ARITHMETIC_TARGET} -d build/rebuilt-arithmetic
 	diff build/current-arithmetic build/rebuilt-arithmetic
-	make -C src/DafnyStdLibs/FileIO check-binary-all
+	make -C src/DafnyStdLibs/TargetSpecific check-binary-all
 
 update-binary: build-binary
 	cp ${DOO_FILE_SOURCE} ${DOO_FILE_TARGET}
 	cp ${DOO_FILE_ARITHMETIC_SOURCE} ${DOO_FILE_ARITHMETIC_TARGET}
-	make -C src/DafnyStdLibs/FileIO update-binary-all
+	make -C src/DafnyStdLibs/TargetSpecific update-binary-all
 # Rebuild Dafny to pick up the new embedded assets
 	dotnet build ../Dafny.sln
 

diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-go.dfy b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-go.dfy
@@ -6,10 +6,10 @@
 /*
  * Private API - these are intentionally not exported from the module and should not be used elsewhere
  */
-module 
+module
   {:compile false}
-  {:extern "DafnyStdLibs_FileIOInternalExterns"} 
-  {:dummyImportMember "INTERNAL__ReadBytesFromFile", false} 
+{:extern "DafnyStdLibs_FileIOInternalExterns"}
+{:dummyImportMember "INTERNAL__ReadBytesFromFile", false}
 DafnyStdLibs.FileIOInternalExterns {
   method
     {:extern}

diff --git a/...DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy b/...DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/FileIOInternalExterns-notarget.dfy
@@ -8,10 +8,10 @@
  */
 module DafnyStdLibs.FileIOInternalExterns {
   method
-  INTERNAL_ReadBytesFromFile(path: string)
+    INTERNAL_ReadBytesFromFile(path: string)
     returns (isError: bool, bytesRead: seq<bv8>, errorMsg: string)
 
   method
-  INTERNAL_WriteBytesToFile(path: string, bytes: seq<bv8>)
+    INTERNAL_WriteBytesToFile(path: string, bytes: seq<bv8>)
     returns (isError: bool, errorMsg: string)
 }
diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/Makefile b/Source/DafnyStandardLibraries/src/DafnyStdLibs/TargetSpecific/Makefile
@@ -19,9 +19,9 @@ build-binary:
 		--output:${DOO_FILE_SOURCE}
 
 check-binary: build-binary
-	unzip -o ${DOO_FILE_SOURCE} -d build/current
-	unzip -o ${DOO_FILE_TARGET} -d build/rebuilt
-	diff build/current build/rebuilt
+	unzip -o ${DOO_FILE_SOURCE} -d ../../../build/current
+	unzip -o ${DOO_FILE_TARGET} -d ../../../build/rebuilt
+	diff ../../../build/current ../../../build/rebuilt
 
 check-binary-all:
 	make check-binary TARGETLANG=notarget

diff --git a/Source/DafnyStandardLibraries/src/dfyconfig.toml b/Source/DafnyStandardLibraries/src/dfyconfig.toml
@@ -4,7 +4,7 @@ excludes = [
   # *Nonlinear.dfy in Arithmetic/Internals/ are subject to the options here
   "**/Arithmetic/*.dfy", "**/Arithmetic/**/*Internals.dfy",
   # Built per-target language instead
-  "**/TargetSpecfic/*.dfy"
+  "**/TargetSpecific/*.dfy"
 ]
 
 [options]