Add support for Ubuntu 18.04 to installer #1231
Conversation
| include: | ||
| - os: macos-10.15 | ||
| artifact: kani-latest-x86_64-apple-darwin.tar.gz | ||
| - os: ubuntu-20.04 | ||
| - os: ubuntu-18.04 |
There was a problem hiding this comment.
Do we want to get rid of ubuntu-20? Or should we have it as a third option
There was a problem hiding this comment.
"get rid of" in what sense? Are you saying not building the regressions (currently 18, 20, and mac) there anymore?
I would sort of endorse that, in that I think we don't need the regressions running on two linux platforms... but what we DO need is "install/smoke testing" running on multiple linux platforms... which is sort of what this is simulating, but it's not good enough yet.
I spent an hour with a whiteboard yesterday trying to sketch out what I thought we'd ideally want to work towards in terms of CI flow and found it a bit frustratingly complicated. I might write up a doc/proposal soon...
There was a problem hiding this comment.
@danielsn Note that this is for building the release bundle, and we're building a single bundle for both Ubuntu 18.04 and Ubuntu 20.04.
| @@ -19,6 +19,7 @@ include = ["/src", "/build.rs", "/rust-toolchain.toml", "/LICENSE-*", "/README.m | |||
| [dependencies] | |||
| anyhow = "1" | |||
| home = "0.5" | |||
| os_info = { version = "3", default-features = false } | |||
There was a problem hiding this comment.
cargo uses os_info so probably a good choice :) https://crates.io/crates/os_info/reverse_dependencies
| let pkg_versions = &["cbmc-viewer==3.2", "colorama==0.4.3"]; | ||
|
|
||
| if os.os_type() == os_info::Type::Ubuntu | ||
| && *os.version() == os_info::Version::Semantic(18, 4, 0) |
There was a problem hiding this comment.
Is there a risk there will be an 18.4.1?
There was a problem hiding this comment.
I think there is not a risk of that because I think it's already running on "18.4.4" and not picking that up. I believe what's happening is it's parsing "18.04" as if it were a version number.
I agree this is seems fragile but this unit test seems to confirm this is the expected behavior: https://github.com/stanislav-tkach/os_info/blob/master/os_info/src/linux/lsb_release.rs#L317-L318
| include: | ||
| - os: macos-10.15 | ||
| artifact: kani-latest-x86_64-apple-darwin.tar.gz | ||
| - os: ubuntu-20.04 | ||
| - os: ubuntu-18.04 |
There was a problem hiding this comment.
@danielsn Note that this is for building the release bundle, and we're building a single bundle for both Ubuntu 18.04 and Ubuntu 20.04.
src/os_hacks.rs
Outdated
| mv_cmd.push("cp -r "); | ||
| mv_cmd.push(pyroot.as_os_str()); | ||
| mv_cmd.push("/lib/python*/site-packages/* "); | ||
| mv_cmd.push(pyroot.as_os_str()); |
There was a problem hiding this comment.
Is there a risk that the target directory is not writeable (or requires sudo)?
There was a problem hiding this comment.
Nope, pyroot here is ~/.kani/kani-VERSION/pyroot and we created it.
src/os_hacks.rs
Outdated
|
|
||
| // Step 2: move `pyroot/lib/python3.6/site-packages/*` up to `pyroot` | ||
| // This seems to successfully replicate the behavior of `--target` | ||
| // "mv" is not idempotent however so we need to do "cp -r" |
There was a problem hiding this comment.
If we're doing cp instead of mv, should we:
- Rename the variable
- Delete the source directory after copying it
?
I'm a bit unclear on the issue withmv.
There was a problem hiding this comment.
mv makes the setup procedure non-idempotent because it fails if the directory already exists (from a previous install).
I can rename the variable and delete the extra directory, that seems reasonable.
Description of changes:
Resolved issues:
Resolves #1184
Call-outs:
os_hackstokani-verifier, as a place to hopefully confine os-specific logic without making it harder to see the general case. I'll be adding a nixos one next.os_infocrate was just the first one I found for this purpose basically...Testing:
How is this change tested? docker test
Is this a refactor change? no
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.