From c54b95ebe066dfcf907e778f5965f6736d4338ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 17 Feb 2022 09:12:14 -0600 Subject: [PATCH 1/8] Try to download 5 times --- Scripts/package.py | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/Scripts/package.py b/Scripts/package.py index 78a9090c7f5..a8df31adb0c 100755 --- a/Scripts/package.py +++ b/Scripts/package.py @@ -106,9 +106,18 @@ def download(self): print("cached!") else: flush("downloading {:.2f}MB...".format(self.MB), end=' ') - with request.urlopen(self.url) as reader: - with open(self.z3_zip, mode="wb") as writer: - writer.write(reader.read()) + maxTries = 5 + while maxTries > 0: + try: + with request.urlopen(self.url) as reader: + with open(self.z3_zip, mode="wb") as writer: + writer.write(reader.read()) + break + except (http.client.IncompleteRead) as e: + maxTries -= 1 + if maxTries == 0: + throw e; + continue; flush("done!") @staticmethod From adec859149c6c1b7f01cc878d2eacab51b67ef74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 17 Feb 2022 09:16:50 -0600 Subject: [PATCH 2/8] Removed semicolons --- Scripts/package.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Scripts/package.py b/Scripts/package.py index a8df31adb0c..aefa2da57c7 100755 --- a/Scripts/package.py +++ b/Scripts/package.py @@ -116,8 +116,8 @@ def download(self): except (http.client.IncompleteRead) as e: maxTries -= 1 if maxTries == 0: - throw e; - continue; + throw e + continue flush("done!") @staticmethod From 4709a870e0ecc16d3bf552553c9f4f5ad6ba330d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 17 Feb 2022 09:17:49 -0600 Subject: [PATCH 3/8] raise instead of throw --- Scripts/package.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Scripts/package.py b/Scripts/package.py index aefa2da57c7..435527fde35 100755 --- a/Scripts/package.py +++ b/Scripts/package.py @@ -116,7 +116,7 @@ def download(self): except (http.client.IncompleteRead) as e: maxTries -= 1 if maxTries == 0: - throw e + raise continue flush("done!") From c343f4087dcfcd760b9ac809a137b4905beb921f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 17 Feb 2022 13:38:09 -0600 Subject: [PATCH 4/8] Review comments --- Scripts/package.py | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/Scripts/package.py b/Scripts/package.py index 435527fde35..b3e87393899 100755 --- a/Scripts/package.py +++ b/Scripts/package.py @@ -24,6 +24,8 @@ Z3_RELEASES_URL = "https://api.github.com/repos/Z3Prover/z3/releases/tags/Z3-4.8.5" ## How do we extract info from the name of a Z3 release file? Z3_RELEASE_REGEXP = re.compile(r"^(?Pz3-[0-9a-z\.]+-(?Px86|x64)-(?P[a-z0-9\.\-]+)).zip$", re.IGNORECASE) +## How many times we allow ourselves to try to download Z3 +Z3_MAX_DOWNLOAD_ATTEMPTS = 5 ## Allowed Dafny release names DAFNY_RELEASE_REGEX = re.compile("\\d+\\.\\d+\\.\\d+(-[\w\d_-]+)?$") @@ -106,19 +108,16 @@ def download(self): print("cached!") else: flush("downloading {:.2f}MB...".format(self.MB), end=' ') - maxTries = 5 - while maxTries > 0: + for currentAttempt in range(Z3_MAX_DOWNLOAD_ATTEMPTS): try: with request.urlopen(self.url) as reader: with open(self.z3_zip, mode="wb") as writer: writer.write(reader.read()) - break + flush("done!") except (http.client.IncompleteRead) as e: - maxTries -= 1 - if maxTries == 0: + if currentAttempt == Z3_MAX_DOWNLOAD_ATTEMPTS - 1: raise - continue - flush("done!") + @staticmethod def zipify_path(fpath): From a5f54b3e08807d4a83a879a1e35d33af00a5e40e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 17 Feb 2022 14:32:12 -0600 Subject: [PATCH 5/8] No parentheses --- Scripts/package.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Scripts/package.py b/Scripts/package.py index b3e87393899..142e8055162 100755 --- a/Scripts/package.py +++ b/Scripts/package.py @@ -114,7 +114,7 @@ def download(self): with open(self.z3_zip, mode="wb") as writer: writer.write(reader.read()) flush("done!") - except (http.client.IncompleteRead) as e: + except http.client.IncompleteRead as e: if currentAttempt == Z3_MAX_DOWNLOAD_ATTEMPTS - 1: raise From e2613ac2c9a776b39d6f5b89dd4ce3f82c774faa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 17 Feb 2022 14:34:27 -0600 Subject: [PATCH 6/8] Forgot the break... downloading Z3 too many times! --- Scripts/package.py | 1 + 1 file changed, 1 insertion(+) diff --git a/Scripts/package.py b/Scripts/package.py index 142e8055162..5e7545cafcb 100755 --- a/Scripts/package.py +++ b/Scripts/package.py @@ -114,6 +114,7 @@ def download(self): with open(self.z3_zip, mode="wb") as writer: writer.write(reader.read()) flush("done!") + break except http.client.IncompleteRead as e: if currentAttempt == Z3_MAX_DOWNLOAD_ATTEMPTS - 1: raise From 3defd21e48511183050bb77adcfb487607f2a003 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 17 Feb 2022 14:46:22 -0600 Subject: [PATCH 7/8] Update Release_notes for other PR --- RELEASE_NOTES.md | 1 + 1 file changed, 1 insertion(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 56f731e650f..92631fa1658 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,5 +1,6 @@ # Upcoming +- fix: Dafny with JavaScript target not producing any output on Windows (https://github.com/dafny-lang/dafny/pull/1824) # 3.4.1 From 8416b62669a66eabcf1c3478dc65d7be77319d16 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 17 Feb 2022 14:49:48 -0600 Subject: [PATCH 8/8] Update RELEASE_NOTES.md Co-authored-by: Fabio Madge --- RELEASE_NOTES.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 92631fa1658..a2adb000e58 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,6 +1,7 @@ # Upcoming -- fix: Dafny with JavaScript target not producing any output on Windows (https://github.com/dafny-lang/dafny/pull/1824) +- fix: No output when compiling to JavaScript on Windows (https://github.com/dafny-lang/dafny/pull/1824) + # 3.4.1