diff --git a/README.md b/README.md
index 37072f76f4e7a33ed128010715d9e58697ce3ab0..9fe23a16aa8c10314bd7872d781d9439a01db2bd 100644
--- a/README.md
+++ b/README.md
@@ -74,13 +74,19 @@ These include:
| Option | Type | Configures |
|--------|------|------------|
+| `work_dir` | Relative/absolue path | Determines the working directory. Other relative paths are interpreted relative to this one. |
| `dump_borrowck_info` | Boolean | Dumps borrowck debug output in the log directory |
-| `output_dir` | Relative path | Determines the directory where the generated output files will be placed |
-| `log_dir` | Relative path | Determines the directory where logs and debug dumps will be placed if enabled |
+| `output_dir` | Relative/absolute path | Determines the directory where the generated output files will be placed |
+| `log_dir` | Relative/absolute path | Determines the directory where logs and debug dumps will be placed if enabled |
| `shims` | Relative path | Determines the JSON file storing information about shims that RefinedRust uses |
| `run_check` | Boolean | Automatically call the Coq type checker on the generated files |
+| `verify_deps` | Boolean | Verify dependencies or not |
+| `admit_proofs` | Boolean | Skip Coq's `Qed` check and instead run `Admitted` |
+The path to the config file can also be specified via the environment variable `RR_CONFIG`.
+Setting this variable will also change the `work_dir` (relative to which paths are interpreted) to the path of `RR_CONFIG`.
+Overrides for all settings can be specified in the environment via variables with the prefix `RR_`, e.g. `RR_SHIMS`, `RR_DUMP_BORROWCK_INFO`, etc.
## License
We currently re-use code from the following projects:
diff --git a/rr_frontend/Cargo.lock b/rr_frontend/Cargo.lock
index b7ab26ebddd6e89f46b07d6e65307513afb5d401..a022e21897978b432315bb8eae9a43cd1fbd16af 100644
--- a/rr_frontend/Cargo.lock
+++ b/rr_frontend/Cargo.lock
@@ -509,6 +509,12 @@ dependencies = [
name = "paper-examples"
version = "0.1.0"
+[[package]]
+name = "path-clean"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "17359afc20d7ab31fdb42bb844c8b3bb1dabd7dcf7e68428492da7f16966fcef"
+
[[package]]
name = "pathdiff"
version = "0.2.1"
@@ -668,6 +674,8 @@ version = "0.1.0"
dependencies = [
"config",
"lazy_static",
+ "log",
+ "path-clean",
"serde",
"serde_json",
"toml 0.8.8",
diff --git a/rr_frontend/rrconfig/Cargo.toml b/rr_frontend/rrconfig/Cargo.toml
index fb1a50dce4a7b6b655ea0e1a446f9283a023884e..1019ffeb8687f9256f9ce492c525fdfb92faf3bc 100644
--- a/rr_frontend/rrconfig/Cargo.toml
+++ b/rr_frontend/rrconfig/Cargo.toml
@@ -6,9 +6,11 @@ edition = "2021"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
+log = "0.4"
config = "0.13.4"
serde = {version = "1.0.130", features = ["derive"]}
lazy_static = "1.4.0"
serde_json = "1.0"
toml = "0.8.8"
+path-clean = "1.0.1"
diff --git a/rr_frontend/rrconfig/src/lib.rs b/rr_frontend/rrconfig/src/lib.rs
index 3dfd6469fa7f6c4e706e2173c944d841129eca69..d544ea21f26ee93ed9efd7963b08b93d5b0d031a 100644
--- a/rr_frontend/rrconfig/src/lib.rs
+++ b/rr_frontend/rrconfig/src/lib.rs
@@ -9,6 +9,9 @@ use std::env;
use std::{sync::RwLock, path::PathBuf};
use serde::Deserialize;
use lazy_static::lazy_static;
+use path_clean::PathClean;
+
+use log::info;
pub mod launch;
pub mod arg_value;
@@ -19,6 +22,10 @@ lazy_static! {
let mk_config = || {
let mut builder = Config::builder();
+ // determine working dir
+ //let work_dir = std::env::current_dir().unwrap();
+ //let work_dir = work_dir.to_str().unwrap();
+
// 1. Default values
builder = builder.set_default("be_rustc", false)?
.set_default("log_dir", "./log/")?
@@ -34,7 +41,8 @@ lazy_static! {
.set_default("no_verify", false)?
.set_default("cargo_path", "cargo")?
.set_default("cargo_command", "check")?
- .set_default("admit_proofs", false)?;
+ .set_default("admit_proofs", false)?
+ .set_default("work_dir", ".")?;
// 2. Override with the optional TOML file "RefinedRust.toml" (if there is any)
builder = builder.add_source(
@@ -46,6 +54,12 @@ lazy_static! {
// Since this file is explicitly specified by the user, it would be
// nice to tell them if we cannot open it.
builder = builder.add_source(File::with_name(&file));
+
+ // set override for workdir to the config file path
+ let path_to_file = std::path::PathBuf::from(file);
+ let parent = path_to_file.parent().unwrap();
+ let filepath = parent.to_str().unwrap();
+ builder = builder.set_default("work_dir", filepath)?;
}
// 4. Override with env variables (`RR_QUIET`, ...)
@@ -65,6 +79,21 @@ pub fn dump() -> String {
format!("{:#?}", SETTINGS.read().unwrap())
}
+/// Makes the path absolute with respect to the work_dir.
+fn make_path_absolute(path: &str) -> PathBuf {
+ // read the base path we set
+ let base_path: String = work_dir();
+
+ let path_buf = std::path::PathBuf::from(path);
+ if path_buf.is_absolute() {
+ path_buf
+ }
+ else {
+ let base_path_buf = std::path::PathBuf::from(base_path);
+ base_path_buf.join(path_buf).clean()
+ }
+}
+
fn read_optional_setting<T>(name: &'static str) -> Option<T>
where
T: Deserialize<'static>,
@@ -87,6 +116,10 @@ fn write_setting<T: Into<config::Value>>(key: &'static str, value: T) {
.unwrap_or_else(|e| panic!("Failed to write setting {key} due to {e}"));
}
+pub fn work_dir() -> String {
+ read_setting("work_dir")
+}
+
/// Should we dump debug files?
pub fn dump_debug_info() -> bool {
read_setting("dump_debug_info")
@@ -99,7 +132,7 @@ pub fn dump_borrowck_info() -> bool {
/// In which folder should we store log/dumps?
pub fn log_dir() -> PathBuf {
- PathBuf::from(read_setting::<String>("log_dir"))
+ make_path_absolute(&read_setting::<String>("log_dir"))
}
/// The hotword with which specification attributes should begin.
@@ -123,8 +156,8 @@ pub fn attribute_parser() -> String {
}
/// Which directory to write the generated Coq files to?
-pub fn output_dir() -> Option<String> {
- read_optional_setting("output_dir")
+pub fn output_dir() -> Option<PathBuf> {
+ read_optional_setting("output_dir").map(|s: String| make_path_absolute(&s))
}
/// Whether to admit proofs of functions instead of running Qed.
@@ -133,8 +166,8 @@ pub fn admit_proofs() -> bool {
}
/// Which file to read shims from?
-pub fn shim_file() -> Option<String> {
- read_optional_setting("shims")
+pub fn shim_file() -> Option<PathBuf> {
+ read_optional_setting("shims").map(|s: String| make_path_absolute(&s))
}
/// Run the proof checker after generating the Coq code?
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 5bafd3e6dd9b259a9ab985c0fb503e80dee6db9e..8b5ae5cb8e8fa2f2d7299368d93cdbd0878a50b6 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -308,19 +308,19 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
}
// create output directory
- let dir_str: String = if let Some(output) = rrconfig::output_dir() {
+ let base_dir_path: std::path::PathBuf = if let Some(output) = rrconfig::output_dir() {
output
} else {
info!("No output directory specified, not writing files");
return;
};
- let mut dir_path = std::path::PathBuf::from(&dir_str);
+ let mut dir_path = base_dir_path.clone();
dir_path.push(&stem);
let dir_path = dir_path.as_path();
info!("outputting generated code to {}", dir_path.to_str().unwrap());
if let Err(_) = fs::read_dir(dir_path) {
- warn!("Output directory {} does not exist, creating directory", dir_str);
+ warn!("Output directory {:?} does not exist, creating directory", base_dir_path);
fs::create_dir_all(dir_path).unwrap();
}