diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index ea3a25405..90d3230f3 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -209,7 +209,7 @@ transpile_implementation: $(DAFNY_OTHER_FILES) \ $(TRANSPILE_MODULE_NAME) \ $(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ - $(if $(USE_DAFNY_STANDARD_LIBRARIES) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \ + $(if $(USE_DAFNY_STANDARD_LIBRARIES) , $(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ), ) \ $(TRANSLATION_RECORD) \ $(TRANSPILE_DEPENDENCIES) @@ -248,7 +248,7 @@ transpile_test: $(DAFNY_OPTIONS) \ $(DAFNY_OTHER_FILES) \ $(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ - $(if $(USE_DAFNY_STANDARD_LIBRARIES) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \ + $(if $(USE_DAFNY_STANDARD_LIBRARIES) , $(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ), ) \ $(TRANSLATION_RECORD) \ $(SOURCE_TRANSLATION_RECORD) \ $(TRANSPILE_MODULE_NAME) \ diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile index f3984ba7f..f4d1c2d32 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/Makefile +++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile @@ -107,7 +107,7 @@ transpile_implementation: --unicode-char:false \ --function-syntax:3 \ --output $(OUT) \ - $(if $(USE_DAFNY_STANDARD_LIBRARIES), bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \ + $(if $(USE_DAFNY_STANDARD_LIBRARIES), ./bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \ $(DAFNY_OPTIONS) \ $(DAFNY_OTHER_FILES) \ $(TRANSPILE_MODULE_NAME) diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py b/TestModels/dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py index 7a6eff36b..b2710c8cb 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py @@ -17,8 +17,10 @@ def __init__(self, dafny_byte_stream): self.dafny_byte_stream = dafny_byte_stream def read(self, size: int = -1) -> bytes: - # TODO: assert size is -1, buffer, - # or define a more specialized Action type for streams. + # We could define a more specialized Action type for streams + # if we wanted to support this level of control in all languages. + if size != -1: + raise ValueError(f"A read size other than -1 is not supported: {size}") next = self.dafny_byte_stream.Next() while next.is_Some and len(next.value) == 0: next = self.dafny_byte_stream.Next() diff --git a/TestModels/dafny-dependencies/dafny b/TestModels/dafny-dependencies/dafny index 70831a833..46e818a64 160000 --- a/TestModels/dafny-dependencies/dafny +++ b/TestModels/dafny-dependencies/dafny @@ -1 +1 @@ -Subproject commit 70831a8332ccbca883ac54b273db26d98cc06e48 +Subproject commit 46e818a64ae289b8d0ddb37249e66ae86b7348d6