Skip to content

Commit

Permalink
Fix get_target_dir and build.py to make packaging work properly wit…
Browse files Browse the repository at this point in the history
…h new prusti_contracts dir (#1479)

* Fix `get_target_dir` and deploy.yml to make packaging work properly

* Add some comments, also reduce parallelism for carbon tests
  • Loading branch information
zgrannan authored Dec 6, 2023
1 parent a59d989 commit 01539d2
Show file tree
Hide file tree
Showing 4 changed files with 33 additions and 26 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/deploy.yml
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
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
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
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

0 comments on commit 01539d2

Please sign in to comment.