allow to admit proofs for performance reasons

rr_frontend/Cargo.lock

@@ -589,6 +589,7 @@ name = "radium"
 version = "0.1.0"
 dependencies = [
  "log",
+ "rrconfig",
 ]
 
 [[package]]

rr_frontend/radium/Cargo.toml

@@ -7,3 +7,5 @@ edition = "2021"
 
 [dependencies]
 log = "0.4"
+rrconfig = { path = "../rrconfig" }
+

rr_frontend/radium/src/code.rs

@@ -1123,7 +1123,12 @@ impl<'def> Function<'def> {
 
         out.push_str(format!("{}Unshelve. all: try done; try apply: inhabitant; print_remaining_shelved_goal \"{}\".\n", indent, self.name()).as_str());
 
-        out.push_str("Qed.\n");
+        if rrconfig::admit_proofs() {
+            out.push_str("Admitted. (* admitted due to admit_proofs config flag *)\n");
+        }
+        else {
+            out.push_str("Qed.\n");
+        }
         out
     }
 }

rr_frontend/radium/src/lib.rs

 #![feature(box_patterns)]
 
+use rrconfig;
 
 pub mod code;
 pub mod specs;

rr_frontend/rrconfig/src/lib.rs

@@ -33,7 +33,8 @@ lazy_static! {
                 .set_default("verify_deps", false)?
                 .set_default("no_verify", false)?
                 .set_default("cargo_path", "cargo")?
-                .set_default("cargo_command", "check")?;
+                .set_default("cargo_command", "check")?
+                .set_default("admit_proofs", false)?;
 
             // 2. Override with the optional TOML file "RefinedRust.toml" (if there is any)
             builder = builder.add_source(
@@ -126,6 +127,11 @@ pub fn output_dir() -> Option<String> {
     read_optional_setting("output_dir")
 }
 
+/// Whether to admit proofs of functions instead of running Qed. 
+pub fn admit_proofs() -> bool {
+    read_setting("admit_proofs")
+}
+
 /// Which file to read shims from?
 pub fn shim_file() -> Option<String> {
     read_optional_setting("shims")