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

Fix get_target_dir and build.py to make packaging work properly with new prusti_contracts dir #1479

Merged
merged 2 commits into from
Dec 6, 2023
Merged

Fix get_target_dir and build.py to make packaging work properly with new prusti_contracts dir #1479

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d5fd7b3
Fix `get_target_dir` and deploy.yml to make packaging work properly
zgrannan Dec 5, 2023
f56dbe1
Add some comments, also reduce parallelism for carbon tests
zgrannan Dec 5, 2023
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
4 changes: 2 additions & 2 deletions .github/workflows/deploy.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,10 +36,10 @@ jobs:
run: python x.py setup

- name: Build with cargo --release
run: python x.py build --release --all
run: python x.py build --release --all --jobs 1

- name: Run cargo tests --release
run: python x.py test --release --all
run: python x.py test --release --all --jobs 1

- name: Package Prusti artifact
run: python x.py package release prusti_artifact
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/test.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -255,7 +255,7 @@ jobs:
run: python x.py test --all --jobs 1
- name: Run a subset of tests with Carbon
run: |
python x.py test pass/no-annotation --all --verbose
python x.py test pass/no-annotation --all --verbose --jobs 1
env:
PRUSTI_VIPER_BACKEND: carbon
- name: Check prusti-contracts
Expand Down
37 changes: 22 additions & 15 deletions prusti-utils/src/launch/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,12 +35,17 @@ pub fn get_current_executable_dir() -> PathBuf {
/// Finds the closest `target` directory in the current path.
/// This should be the target directory at the root of the repository,
/// i.e. `prusti-dev/target`.
pub fn get_target_dir(exe_dir: &Path) -> PathBuf {
fn get_target_dir(exe_dir: &Path) -> Option<PathBuf> {
let mut root_dir = exe_dir;
while root_dir.file_name().unwrap() != "target" {
root_dir = root_dir.parent().unwrap();
loop {
if root_dir.file_name().unwrap() == "target" {
return Some(root_dir.to_path_buf());
}
match root_dir.parent() {
Some(parent) => root_dir = parent,
None => return None,
}
}
root_dir.to_path_buf()
}

pub fn get_prusti_contracts_build_target_dir(target_dir: &Path) -> PathBuf {
Expand All @@ -50,17 +55,19 @@ pub fn get_prusti_contracts_build_target_dir(target_dir: &Path) -> PathBuf {
pub fn get_prusti_contracts_dir(exe_dir: &Path) -> Option<PathBuf> {
let a_prusti_contracts_file = format!("lib{}.rlib", PRUSTI_LIBS[0].replace('-', "_"));

let target_dir = get_target_dir(exe_dir);
let candidates = [
// Libraries in the Prusti artifact will show up here
get_prusti_contracts_build_target_dir(&target_dir),
// Libraries when building Prusti will show up here
target_dir,
]
.map(|path| path.join("verify").join(BUILD_MODE));
candidates
.into_iter()
.find(|candidate| candidate.join(&a_prusti_contracts_file).exists())
if exe_dir.join(&a_prusti_contracts_file).exists() {
// If this branch is entered, then this is the Prusti Artifact
return Some(exe_dir.to_path_buf());
} else if let Some(target_dir) = get_target_dir(exe_dir) {
// If this branch is entered, then we're building Prusti
let candidate = get_prusti_contracts_build_target_dir(&target_dir)
.join("verify")
.join(BUILD_MODE);
if candidate.join(&a_prusti_contracts_file).exists() {
return Some(candidate);
}
}
None
}

/// Append paths to the loader environment variable
Expand Down
16 changes: 8 additions & 8 deletions x.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,17 +233,17 @@ def package(mode: str, package_path: str):
(f"target/{mode}/prusti-server*", "."),
(f"target/{mode}/prusti-rustc*", "."),
(f"target/{mode}/cargo-prusti*", "."),
(f"target/verify/{mode}/libprusti_contracts.*", "."),
(f"target/verify/{mode}/deps/libprusti_contracts_proc_macros-*", "deps"),
(f"target/verify/{mode}/deps/prusti_contracts_proc_macros-*.dll", "deps"),
(f"target/verify/{mode}/libprusti_std.*", "."),
(f"target/verify/{mode}/deps/libprusti_contracts-*", "deps"),
(f"target/verify/{mode}/deps/prusti_contracts-*.dll", "deps"),
(f"target/prusti-contracts/{mode}/verify/{mode}/libprusti_contracts.*", "."),
(f"target/prusti-contracts/{mode}/verify/{mode}/deps/libprusti_contracts_proc_macros-*", "deps"),
(f"target/prusti-contracts/{mode}/verify/{mode}/deps/prusti_contracts_proc_macros-*.dll", "deps"),
(f"target/prusti-contracts/{mode}/verify/{mode}/libprusti_std.*", "."),
(f"target/prusti-contracts/{mode}/verify/{mode}/deps/libprusti_contracts-*", "deps"),
(f"target/prusti-contracts/{mode}/verify/{mode}/deps/prusti_contracts-*.dll", "deps"),
]
exclude_paths = [
f"target/{mode}/*.d",
f"target/verify/{mode}/*.d",
f"target/verify/{mode}/deps/*.d",
f"target/prusti-contracts/{mode}/verify/{mode}/*.d",
f"target/prusti-contracts/{mode}/verify/{mode}/deps/*.d",
]
actual_exclude_set = set(path for pattern in exclude_paths for path in glob.glob(pattern))
logging.debug(f"The number of excluded paths is: {len(actual_exclude_set)}")
Expand Down
Loading