Back to downloading of jars

[vitorenesduarte]

Closes: #41

This PR essentially reverts #25. Differences:

• use ureq instead reqwest as ureq is more lightweight
• download jars from our repository instead of downloading them from the releases page of their repositories; this prevents situations where a GitHub release is deleted, which would result in modelator not working
• ensure that jars were not corrupted by embedding their SHA256 hash in the Rust code and checking that hashes match after the jars are written to disk

[andrey-kuprianov]

Nice Vitor! I think it is really good that way -- I like the minimal dependency introduced, as well that it's now downloaded from our repo.

Feel free to merge:)

[andrey-kuprianov]

Just an afterthought: I think it would be nice when the JARs are downloaded to display to the user the information like

Downloading model-checkers:
  downloading Apalache ... done
  downloading TLC ... done

This way the user will understand where the initial delay comes from.

[romac]

May I suggest embedding the SHA-256 hashes of each JAR file in the Rust code, and checking them after the download to ensure they were not corrupted or tempered with during transfer.

[andrey-kuprianov]

May I suggest embedding the SHA-256 hashes of each JAR file in the Rust code, and checking them after the download to ensure they were not corrupted or tempered with during transfer.

that is a very good idea!

[vitorenesduarte]

May I suggest embedding the SHA-256 hashes of each JAR file in the Rust code, and checking them after the download to ensure they were not corrupted or tempered with during transfer.

ureq uses TLS by default: https://github.com/algesten/ureq/blob/main/Cargo.toml#L18
Doesn't this prevent that situation?

[romac]

Doesn't this prevent that situation?

It does prevent against tampering during transfer but not corruption when writing to disk for example. I would therefore still advise checking the hash to ensure the file that's been downloaded and written to disk is intact.

[vitorenesduarte]

Doesn't this prevent that situation?

It does prevent against tampering during transfer but not corruption when writing to disk for example. I would therefore still advise checking the hash to ensure the file that's been downloaded and written to disk is intact.

That makes sense, thanks! Done in 4b27208. I'll update the top-level comment accordingly.

[vitorenesduarte]

Just an afterthought: I think it would be nice when the JARs are downloaded to display to the user the information like

Downloading model-checkers:
  downloading Apalache ... done
  downloading TLC ... done

This way the user will understand where the initial delay comes from.

Done in 7562461.

[andrey-kuprianov]

Looks good to me:)