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

MikaelMayer · 2022-02-17T15:16:11Z

Problem
In one fo my last PR, the CI was not able to download Z3 in only 1 of the 15 instances.
This happens regularly (like, 1 time over 5) over an entire CI. Assuming that there are 10 runs every day, I don't want this problem to happen more than once a year.

Solution
With 5 tries, this problem will happen only 1 time every 3125, so that should get us covered.

Original exception

The date in version.cs does not agree with today's date: 40216 vs. 40215
12
The version number in version.cs does not agree with the given version: 0.0.0 vs. 3.4.1
13
Creating release files for release "0.0.0-CI" and internal version information: 3.4.1.40215
14
* Finding and downloading Z3 releases
15
  - Getting information about latest release
16
    + Selecting z3-4.8.5-x64-debian-8.11.zip (35.66MB, 35658053)
17
    + Selecting z3-4.8.5-x64-osx-10.14.2.zip (30.06MB, 30064624)
18
    + Selecting z3-4.8.5-x64-ubuntu-14.04.zip (34.44MB, 34441090)
19
    + Selecting z3-4.8.5-x64-ubuntu-16.04.zip (36.22MB, 36216249)
20
    + Selecting z3-4.8.5-x64-win.zip (14.11MB, 14112529)
21
    + Rejecting z3-4.8.5-x86-win.zip
22
  - Downloading 1 z3 archives
23
Traceback (most recent call last):
24
  File "/Users/runner/work/dafny/dafny/dafny/Scripts/package.py", line 302, in <module>
25
    main()
26
    + z3-4.8.5-x64-osx-10.14.2.zip: downloading 30.06MB... 
27
  File "/Users/runner/work/dafny/dafny/dafny/Scripts/package.py", line 296, in main
28
    download(releases)
29
  File "/Users/runner/work/dafny/dafny/dafny/Scripts/package.py", line 223, in download
30
    release.download()
31
  File "/Users/runner/work/dafny/dafny/dafny/Scripts/package.py", line 111, in download
32
    writer.write(reader.read())
33
  File "/Users/runner/hostedtoolcache/Python/3.10.2/x64/lib/python3.10/http/client.py", line 481, in read
34
    s = self._safe_read(self.length)
35
  File "/Users/runner/hostedtoolcache/Python/3.10.2/x64/lib/python3.10/http/client.py", line 632, in _safe_read
36
    raise IncompleteRead(data, amt-len(data))
37
http.client.IncompleteRead: IncompleteRead(8388608 bytes read, 21676016 more expected)
38

fabiomadge · 2022-02-17T15:21:58Z

Scripts/package.py

-            with request.urlopen(self.url) as reader:
-                with open(self.z3_zip, mode="wb") as writer:
-                    writer.write(reader.read())
+            maxTries = 5


At this point it might make sense to put this into a global constant. (With L132)

But I do see the argument that we are dealing with events of a different nature here.

Scripts/package.py

fabiomadge · 2022-02-17T15:28:47Z

Scripts/package.py

-                with open(self.z3_zip, mode="wb") as writer:
-                    writer.write(reader.read())
+            maxTries = 5
+            while maxTries > 0:


This might be cleaner in a for loop.

It still have to check for the last bound to reraise the exception, but I converted it to a for loop with a global constant

cpitclaudel · 2022-02-17T16:13:57Z

Scripts/package.py

+                    maxTries -= 1
+                    if maxTries == 0:
+                        raise
+                    continue


continue is not needed here

cpitclaudel · 2022-02-17T16:15:03Z

Scripts/package.py

+                try:
+                    with request.urlopen(self.url) as reader:
+                        with open(self.z3_zip, mode="wb") as writer:
+                            writer.write(reader.read())


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

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.

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 ^^)

atomb · 2022-02-17T18:26:00Z

I wonder whether it might make sense to maintain a mapping from OS name to release files directly in this script, rather than asking the GitHub API for it. Something like {"linux": "https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-debian-8.11.zip", ... }. It would mean a slightly larger chunk of data to keep up-to-date (rather than just a version number) but would reduce the number of round trips to GitHub which should speed it up and hopefully make it less likely to fail. Including that in addition to the retry logic you've already added could be even better.

fabiomadge · 2022-02-17T18:34:54Z

I wonder whether it might make sense to maintain a mapping from OS name to release files directly in this script, rather than asking the GitHub API for it. Something like {"linux": "https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-debian-8.11.zip", ... }. It would mean a slightly larger chunk of data to keep up-to-date (rather than just a version number) but would reduce the number of round trips to GitHub which should speed it up and hopefully make it less likely to fail. Including that in addition to the retry logic you've already added could be even better.

Let's try that in a separate PR if the issue persists.

robin-aws · 2022-02-17T18:46:48Z

Sanity check: we can't use the versions of Z3 in nuget can we? What if we eventually move to newer versions?

fabiomadge · 2022-02-17T18:53:38Z

Sanity check: we can't use the versions of Z3 in nuget can we? What if we eventually move to newer versions?

We're building the release for multiple platforms. I don't think that's a service nuget provides.

cpitclaudel · 2022-02-17T20:12:36Z

Scripts/package.py

+                        with open(self.z3_zip, mode="wb") as writer:
+                            writer.write(reader.read())
+                    flush("done!")
+                except (http.client.IncompleteRead) as e:


No need for parentheses here

cpitclaudel · 2022-02-17T20:13:50Z

Scripts/package.py

+                except (http.client.IncompleteRead) as e:
+                    if currentAttempt == Z3_MAX_DOWNLOAD_ATTEMPTS - 1:
+                        raise
+


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

RELEASE_NOTES.md

Co-authored-by: Fabio Madge <[email protected]>

keyboardDrummer · 2022-02-18T16:24:55Z

Sanity check: we can't use the versions of Z3 in nuget can we? What if we eventually move to newer versions?

We're building the release for multiple platforms. I don't think that's a service nuget provides.

I believe the Z3 NuGet package contains binaries for different platforms, but to use it you have to use a C# API instead of the textual SMTLib2 API that Boogie is using now, so that'd be significant updates to Boogie to support using that new API.

fabiomadge · 2022-02-18T16:55:20Z

Yes, looks like all you get is libz3, but for different architectures.

* returns, ifs, and blocks * fix the retry logic added a short while back in #1835

Try to download 5 times

c54b95e

MikaelMayer requested review from atomb and fabiomadge February 17, 2022 15:16

MikaelMayer self-assigned this Feb 17, 2022

MikaelMayer added 2 commits February 17, 2022 09:16

Removed semicolons

adec859

raise instead of throw

4709a87

fabiomadge reviewed Feb 17, 2022

View reviewed changes

fabiomadge changed the title ~~chore:Try to download 5 times Z3 instead of just once~~ chore: Try to download 5 times Z3 instead of just once Feb 17, 2022

fabiomadge changed the title ~~chore: Try to download 5 times Z3 instead of just once~~ chore: Try to download Z3 5 times instead of just once Feb 17, 2022

cpitclaudel reviewed Feb 17, 2022

View reviewed changes

Review comments

c343f40

MikaelMayer requested review from fabiomadge and cpitclaudel February 17, 2022 19:38

fabiomadge previously approved these changes Feb 17, 2022

View reviewed changes

cpitclaudel reviewed Feb 17, 2022

View reviewed changes

No parentheses

a5f54b3

MikaelMayer dismissed fabiomadge’s stale review via a5f54b3 February 17, 2022 20:32

MikaelMayer added 2 commits February 17, 2022 14:34

Forgot the break... downloading Z3 too many times!

e2613ac

Merge branch 'master' into chore-robustness-in-installation

5c24b5a

MikaelMayer enabled auto-merge (squash) February 17, 2022 20:35

MikaelMayer requested a review from fabiomadge February 17, 2022 20:35

fabiomadge previously approved these changes Feb 17, 2022

View reviewed changes

Update Release_notes for other PR

3defd21

MikaelMayer dismissed fabiomadge’s stale review via 3defd21 February 17, 2022 20:46

fabiomadge reviewed Feb 17, 2022

View reviewed changes

RELEASE_NOTES.md Outdated Show resolved Hide resolved

Update RELEASE_NOTES.md

8416b62

Co-authored-by: Fabio Madge <[email protected]>

fabiomadge approved these changes Feb 17, 2022

View reviewed changes

Merge branch 'master' into chore-robustness-in-installation

1bf3513

MikaelMayer merged commit 6252b08 into master Feb 17, 2022

MikaelMayer deleted the chore-robustness-in-installation branch February 17, 2022 22:18

fabiomadge mentioned this pull request Mar 5, 2022

feat: Add returns, ifs, and blocks to the python compiler #1886

Merged

fabiomadge added a commit that referenced this pull request Mar 7, 2022

feat: Add returns, ifs, and blocks to the python compiler (#1886)

87f757d

* returns, ifs, and blocks * fix the retry logic added a short while back in #1835

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

MikaelMayer commented Feb 17, 2022

fabiomadge Feb 17, 2022

fabiomadge Feb 17, 2022

fabiomadge Feb 17, 2022

MikaelMayer Feb 17, 2022

cpitclaudel Feb 17, 2022

cpitclaudel Feb 17, 2022

MikaelMayer Feb 17, 2022

cpitclaudel Feb 17, 2022

atomb commented Feb 17, 2022

fabiomadge commented Feb 17, 2022

robin-aws commented Feb 17, 2022

fabiomadge commented Feb 17, 2022

cpitclaudel Feb 17, 2022

cpitclaudel Feb 17, 2022 •

edited

Loading

keyboardDrummer commented Feb 18, 2022

fabiomadge commented Feb 18, 2022 •

edited

Loading

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

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

Conversation

MikaelMayer commented Feb 17, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb commented Feb 17, 2022

fabiomadge commented Feb 17, 2022

robin-aws commented Feb 17, 2022

fabiomadge commented Feb 17, 2022

Choose a reason for hiding this comment

cpitclaudel Feb 17, 2022 • edited Loading

Choose a reason for hiding this comment

keyboardDrummer commented Feb 18, 2022

fabiomadge commented Feb 18, 2022 • edited Loading

cpitclaudel Feb 17, 2022 •

edited

Loading

fabiomadge commented Feb 18, 2022 •

edited

Loading