add work_dir config option

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:

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",

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"

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?

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();
         }