diff --git a/README.md b/README.md
index d9c5bddf95b47ec26894a9585d23aea9570ba5ce..2a303e357aa64e310702625237c2735898fe92f4 100644
--- a/README.md
+++ b/README.md
@@ -135,6 +135,7 @@ These include:
| `admit_proofs` | Boolean | Skip Coq's `Qed` check and instead run `Admitted` |
| `extra_specs` | Relative/absolute path | File whose contents will be inlined at the end of the generated specs file |
| `post_generation_hook` | Command | Run a command after code generation and before proof checking |
+| `generate_dune_project` | Boolean | Generate a dune-project file (on by default) |
| `lib_load_paths` | Array of relative/absolute paths to directories | Search these paths (recursively) for RefinedRust libraries |
The path to the config file can also be specified via the environment variable `RR_CONFIG`.
diff --git a/case_studies/minivec/RefinedRust.toml b/case_studies/minivec/RefinedRust.toml
index 6529c61f3f4697edcdcb4beb6493944627e2d3b2..5c4a0aca90708369b0235a67d7e4ffb037c87081 100644
--- a/case_studies/minivec/RefinedRust.toml
+++ b/case_studies/minivec/RefinedRust.toml
@@ -5,4 +5,5 @@ shims = "rr_shims.json"
run_check = false
extra_specs = "extra_specs.v"
lib_load_paths = ["../../stdlib"]
+generate_dune_project = false
post_generation_hook = "patch output/minivec/generated/generated_code_minivec.v annotation_patch.patch"
diff --git a/case_studies/paper-examples/RefinedRust.toml b/case_studies/paper-examples/RefinedRust.toml
index 45160d36311f197c41b8a44c507468d22b656e05..38ed5804769f887c6713f867065e7766e09e4529 100644
--- a/case_studies/paper-examples/RefinedRust.toml
+++ b/case_studies/paper-examples/RefinedRust.toml
@@ -1 +1,2 @@
output_dir="./output"
+generate_dune_project = false
diff --git a/case_studies/tests/RefinedRust.toml b/case_studies/tests/RefinedRust.toml
index 28d632c6d18a27376c26514e286b1709dcccaa60..d1c6347945f0bb0f79381fdd2d0ce5b3323547e0 100644
--- a/case_studies/tests/RefinedRust.toml
+++ b/case_studies/tests/RefinedRust.toml
@@ -1,3 +1,4 @@
output_dir="./output"
dump_borrowck_info=true
lib_load_paths=["../../stdlib/"]
+generate_dune_project = false
diff --git a/rr_frontend/rrconfig/src/lib.rs b/rr_frontend/rrconfig/src/lib.rs
index fb1e038b29048b5425a6f5d055ce17185865755e..3d3f8f1bdabc1db66952812fcff7f2636ce2b1e0 100644
--- a/rr_frontend/rrconfig/src/lib.rs
+++ b/rr_frontend/rrconfig/src/lib.rs
@@ -42,6 +42,7 @@ lazy_static! {
.set_default("cargo_path", "cargo")?
.set_default("cargo_command", "check")?
.set_default("admit_proofs", false)?
+ .set_default("generate_dune_project", true)?
.set_default("lib_load_paths", Vec::<String>::new())?
.set_default("work_dir", ".")?;
@@ -169,6 +170,11 @@ pub fn skip_unsupported_features() -> bool {
read_setting("skip_unsupported_features")
}
+/// Whether to generate a dune-project file for this project
+pub fn generate_dune_project() -> bool {
+ read_setting("generate_dune_project")
+}
+
/// Which attribute parser to use? Currently, only the "verbose" parser is supported.
pub fn attribute_parser() -> String {
read_setting("attribute_parser")
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index e08d688b7258dd0acb2824db55ad3fd67715c9a0..4a9f5a113b96e42973c73323d1cac4ef2b135f35 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -4,8 +4,6 @@
// If a copy of the BSD-3-clause license was not distributed with this
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
-// TODO: remove this
-#![allow(dead_code)]
#![feature(box_patterns)]
#![feature(let_chains)]
#![feature(rustc_private)]
@@ -648,13 +646,14 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
// write gitignore file
let gitignore_path = base_dir_path.as_path().join(format!(".gitignore"));
- if !gitignore_path.exists() {
+ {
let mut gitignore_file = io::BufWriter::new(fs::File::create(gitignore_path.as_path()).unwrap());
write!(
gitignore_file,
"\
generated\n\
- proofs/dune"
+ proofs/dune\n\
+ interface.rrlib"
)
.unwrap();
}
@@ -680,6 +679,29 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
base_dir_path.as_path(),
);
+ // write the dune-project file, if required
+ if rrconfig::generate_dune_project() {
+ base_dir_path.pop();
+ base_dir_path.push("dune-project");
+ let mut dune_project_file =
+ io::BufWriter::new(fs::File::create(base_dir_path.as_path()).unwrap());
+
+ let (project_name, dune_project_package) = if let Some(ref dune_package) = self.dune_package {
+ (dune_package.to_string(), format!("(package (name {dune_package}))\n"))
+ } else {
+ (stem.to_string(), format!(""))
+ };
+ write!(
+ dune_project_file,
+ "\
+ ; Generated by [refinedrust], do not edit.\n\
+ (lang dune 3.8)\n\
+ (using coq 0.8)\n\
+ (name {project_name})\n{dune_project_package}",
+ )
+ .unwrap();
+ }
+
// write generated (subdirectory "generated")
info!("outputting generated code to {}", generated_dir_path.to_str().unwrap());
if let Err(_) = fs::read_dir(generated_dir_path) {
diff --git a/stdlib/alloc/RefinedRust.toml b/stdlib/alloc/RefinedRust.toml
index 76583fb421f6f207aad4f007da32fa94d95e69bc..e23c3dc166514fee147a3e6b4ccfe50c4462e516 100644
--- a/stdlib/alloc/RefinedRust.toml
+++ b/stdlib/alloc/RefinedRust.toml
@@ -1 +1,2 @@
lib_load_paths = ["../"]
+generate_dune_project = false
diff --git a/stdlib/btreemap/RefinedRust.toml b/stdlib/btreemap/RefinedRust.toml
index 76583fb421f6f207aad4f007da32fa94d95e69bc..e23c3dc166514fee147a3e6b4ccfe50c4462e516 100644
--- a/stdlib/btreemap/RefinedRust.toml
+++ b/stdlib/btreemap/RefinedRust.toml
@@ -1 +1,2 @@
lib_load_paths = ["../"]
+generate_dune_project = false
diff --git a/stdlib/controlflow/RefinedRust.toml b/stdlib/controlflow/RefinedRust.toml
new file mode 100644
index 0000000000000000000000000000000000000000..e23c3dc166514fee147a3e6b4ccfe50c4462e516
--- /dev/null
+++ b/stdlib/controlflow/RefinedRust.toml
@@ -0,0 +1,2 @@
+lib_load_paths = ["../"]
+generate_dune_project = false
diff --git a/stdlib/iterator/RefinedRust.toml b/stdlib/iterator/RefinedRust.toml
new file mode 100644
index 0000000000000000000000000000000000000000..e23c3dc166514fee147a3e6b4ccfe50c4462e516
--- /dev/null
+++ b/stdlib/iterator/RefinedRust.toml
@@ -0,0 +1,2 @@
+lib_load_paths = ["../"]
+generate_dune_project = false
diff --git a/stdlib/option/RefinedRust.toml b/stdlib/option/RefinedRust.toml
index 9c549dca4e90ded929b63eb1d990669322a303f9..4975dd76ae51ffce58aa7a1d8cc838499384e1d3 100644
--- a/stdlib/option/RefinedRust.toml
+++ b/stdlib/option/RefinedRust.toml
@@ -1 +1,2 @@
extra_specs = "extra_specs.v"
+generate_dune_project = false
diff --git a/stdlib/range/RefinedRust.toml b/stdlib/range/RefinedRust.toml
new file mode 100644
index 0000000000000000000000000000000000000000..e23c3dc166514fee147a3e6b4ccfe50c4462e516
--- /dev/null
+++ b/stdlib/range/RefinedRust.toml
@@ -0,0 +1,2 @@
+lib_load_paths = ["../"]
+generate_dune_project = false
diff --git a/stdlib/result/RefinedRust.toml b/stdlib/result/RefinedRust.toml
index a9a69fe5c9b964c9127533e6242a3fe56830a8d4..4d9b4db5bf28e92641a24c12d07790b0fdada9b5 100644
--- a/stdlib/result/RefinedRust.toml
+++ b/stdlib/result/RefinedRust.toml
@@ -1 +1,3 @@
extra_specs = "./extra_specs.v"
+generate_dune_project = false
+lib_load_paths = ["../"]
diff --git a/stdlib/rwlock/RefinedRust.toml b/stdlib/rwlock/RefinedRust.toml
new file mode 100644
index 0000000000000000000000000000000000000000..e23c3dc166514fee147a3e6b4ccfe50c4462e516
--- /dev/null
+++ b/stdlib/rwlock/RefinedRust.toml
@@ -0,0 +1,2 @@
+lib_load_paths = ["../"]
+generate_dune_project = false
diff --git a/stdlib/spin/RefinedRust.toml b/stdlib/spin/RefinedRust.toml
index 631aec8559e8a568adc84d8f918de1741ed2d2cc..5efd5ae61bb32c211750d39984ac64832db69e7a 100644
--- a/stdlib/spin/RefinedRust.toml
+++ b/stdlib/spin/RefinedRust.toml
@@ -1 +1,2 @@
lib_load_paths=["../"]
+generate_dune_project = false
diff --git a/stdlib/vec/RefinedRust.toml b/stdlib/vec/RefinedRust.toml
index 76583fb421f6f207aad4f007da32fa94d95e69bc..e23c3dc166514fee147a3e6b4ccfe50c4462e516 100644
--- a/stdlib/vec/RefinedRust.toml
+++ b/stdlib/vec/RefinedRust.toml
@@ -1 +1,2 @@
lib_load_paths = ["../"]
+generate_dune_project = false