Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-RC2: Problems downloading


view this post on Zulip Email Gateway (Jan 19 2021 at 13:16):

From: Dominique Unruh <unruh@ut.ee>
Hello,

I am trying to download RC2 and cannot unpack the result. Are there any
hashes of the files so that I could narrow down where things fail? (I
downloaded
https://isabelle.in.tum.de/website-Isabelle2021-RC2/dist/Isabelle2021-RC2_linux.tar.gz,
and I get sha1 hash f3cb2849faa3ae923e4392c4628520e838102e86.) I get the
following error:

15:10 unruh@unruh-work:/opt$ tar xf Isabelle2021-RC2_linux.tar.gz
tar: Skipping to next header
tar: Exiting with failure status due to previous errors

(Maybe related: I also noticed that
https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020_linux.tar.gz
and https://isabelle.in.tum.de/dist/Isabelle2020_linux.tar.gz give
different files while my understanding is that they should give the same
file (and the first link is going to stay after 2021 is released).)

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Jan 19 2021 at 13:33):

From: Manuel Eberl <eberlm@in.tum.de>
cf. this thread:
https://www.mail-archive.com/isabelle-dev@mailman46.in.tum.de/msg00564.html

Apparently, the TUM servers are up to no good again. Our admins assured
us this was being looked into.

Manuel
smime.p7s

view this post on Zulip Email Gateway (Jan 19 2021 at 13:41):

From: Dominique Unruh <unruh@ut.ee>
Oh, I missed that one. Thanks. I guess there is currently no way to get
the RC then.

Re Denis: GNU tar does the gunzip itself automatically (and it
recognizes the need for it from the file extension).

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Jan 19 2021 at 14:04):

From: marco caminati via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>

(I downloaded https://isabelle.in.tum.de/website-Isabelle2021-RC2/dist/Isabelle2021-RC2_linux.tar.gz, and I get sha1 hash f3cb2849faa3ae923e4392c4628520e838102e86.)

Similar problem, here, but different hash :)

$ ls Isabelle2021-RC2_linux.tar.gz* -lh
-rw-rw-r-- 1 458M Jan 19 13:46 Isabelle2021-RC2_linux.tar.gz
-rw-rw-r-- 1 458M Jan 19 13:51 Isabelle2021-RC2_linux.tar.gz.1

$ sha256sum Isabelle2021-RC2_linux.tar.gz*
d218bb38d2e2b93fdbfd068329a6d95caa2d9d9c6531827cdb791bc3a14a22cc Isabelle2021-RC2_linux.tar.gz
d218bb38d2e2b93fdbfd068329a6d95caa2d9d9c6531827cdb791bc3a14a22cc Isabelle2021-RC2_linux.tar.gz.1

So I downloaded it twice and got a consistent hash. But consistency seems to be lost across different people downloading (assuming the file wasn't changed server side in the meantime).
Two more things: the downloads above were done using wget --compression=none; the error is already at the gunzip level: gunzip < Isabelle2021-RC2_linux.tar.gz > /dev/null fails (invalid compressed data--crc error).

Cheers,
Marco

view this post on Zulip Email Gateway (Jan 19 2021 at 14:16):

From: Dominique Unruh <unruh@ut.ee>
I used a sha1 hash, and you used a sha256 hash. :)

But my sha256 is also different from yours.
(af14edfadf6fbf8625e73c78016faa7435b9b322f13fbf23d45d064670d15f27)

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Jan 19 2021 at 14:21):

From: marco caminati via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>

I used a sha1 hash, and you used a sha256 hash. :)

You're right!

But my sha256 is also different from yours.
(af14edfadf6fbf8625e73c78016faa7435b9b322f13fbf23d45d064670d15f27)

Ah. Well :)

view this post on Zulip Email Gateway (Jan 19 2021 at 15:36):

From: Makarius <makarius@sketis.net>
Do you refer to my contact with them (from the above mail thread), or did you
communicate separately?

Anyway, I have now made an rsync clone of the whole thing here:

https://isabelle.sketis.net/website-Isabelle2021-RC2

(That is a rock-solid vServer for 11 EUR per month:
https://www.netcup.de/bestellen/produkt.php?produkt=2556 --- I have saved so
much time in the past 3 years to have it available at my own fingertips.)

Makarius

view this post on Zulip Email Gateway (Jan 19 2021 at 15:56):

From: Manuel Eberl <eberlm@in.tum.de>
Both what you said and what Tobias told me. He also poked them again a
week or so ago at my behest, but I don't think he heard back from them yet.

Our lecture materials for over 1000 students are also hosted there, so
we are not happy about this state of affairs.

Manuel
smime.p7s

view this post on Zulip Email Gateway (Jan 26 2021 at 17:50):

From: Manuel Eberl <eberlm@in.tum.de>
The server was moved today, so hopefully things will go more smoothly now.

Manuel
smime.p7s


Last updated: Jul 15 2022 at 23:21 UTC