Skip to content
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

Jump to bottom

chore: Try to download Z3 5 times instead of just once #1835

Merged
merged 10 commits into from
Feb 17, 2022
Merged

chore: Try to download Z3 5 times instead of just once #1835

Changes from 4 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
c54b95e
Try to download 5 times
MikaelMayer Feb 17, 2022
adec859
Removed semicolons
MikaelMayer Feb 17, 2022
4709a87
raise instead of throw
MikaelMayer Feb 17, 2022
c343f40
Review comments
MikaelMayer Feb 17, 2022
a5f54b3
No parentheses
MikaelMayer Feb 17, 2022
e2613ac
Forgot the break... downloading Z3 too many times!
MikaelMayer Feb 17, 2022
5c24b5a
Merge branch 'master' into chore-robustness-in-installation
MikaelMayer Feb 17, 2022
3defd21
Update Release_notes for other PR
MikaelMayer Feb 17, 2022
8416b62
Update RELEASE_NOTES.md
MikaelMayer Feb 17, 2022
1bf3513
Merge branch 'master' into chore-robustness-in-installation
fabiomadge Feb 17, 2022
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
16 changes: 12 additions & 4 deletions Scripts/package.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"^(?P<directory>z3-[0-9a-z\.]+-(?P<platform>x86|x64)-(?P<os>[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_-]+)?$")
Expand Down Expand Up @@ -106,10 +108,16 @@ 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())
flush("done!")
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())
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

urllib.request.urlretrieve instead of write(read())

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The documentation says your particular method has been deprecated.
Moreover, I don't feel comfortable editing what already worked before - for example, it might work today, but if the cache is outdated tomorrow and it does not work, we might not see the error
If you feel comfortable, feel free to contribute to this PR.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The documentation says your particular method has been deprecated.

Not quite :) But I agree with you that it's fine to keep the current code if it's working (I wrote it, but I'm not sure why I didn't use shutil.copyfileobj or urlretrieve ^^)

flush("done!")
except (http.client.IncompleteRead) as e:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need for parentheses here

if currentAttempt == Z3_MAX_DOWNLOAD_ATTEMPTS - 1:
raise
fabiomadge marked this conversation as resolved.
Show resolved Hide resolved

Copy link
Member

@cpitclaudel cpitclaudel Feb 17, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FWIW, an alternative way to write this kind of loop in Python is something like this (for-else)

err = None
for _ in range(NRETRIES):
    try:
        do_something()
        break
    except SomeException as e:
        err = e
else:
    raise err


@staticmethod
def zipify_path(fpath):
Expand Down