From fb60f696c46d90a8412f7b2df967695af5ddf077 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <Lennard.Gaeher@ibm.com>
Date: Fri, 8 Dec 2023 12:20:48 +0100
Subject: [PATCH] allow to admit proofs for performance reasons
---
rr_frontend/Cargo.lock | 1 +
rr_frontend/radium/Cargo.toml | 2 ++
rr_frontend/radium/src/code.rs | 7 ++++++-
rr_frontend/radium/src/lib.rs | 1 +
rr_frontend/rrconfig/src/lib.rs | 8 +++++++-
5 files changed, 17 insertions(+), 2 deletions(-)
diff --git a/rr_frontend/Cargo.lock b/rr_frontend/Cargo.lock
index 6676e3aa..b7ab26eb 100644
--- a/rr_frontend/Cargo.lock
+++ b/rr_frontend/Cargo.lock
@@ -589,6 +589,7 @@ name = "radium"
version = "0.1.0"
dependencies = [
"log",
+ "rrconfig",
]
[[package]]
diff --git a/rr_frontend/radium/Cargo.toml b/rr_frontend/radium/Cargo.toml
index 98d62751..910c3c36 100644
--- a/rr_frontend/radium/Cargo.toml
+++ b/rr_frontend/radium/Cargo.toml
@@ -7,3 +7,5 @@ edition = "2021"
[dependencies]
log = "0.4"
+rrconfig = { path = "../rrconfig" }
+
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index c76eb566..33439e93 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/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
}
}
diff --git a/rr_frontend/radium/src/lib.rs b/rr_frontend/radium/src/lib.rs
index cf72485b..f296572e 100644
--- a/rr_frontend/radium/src/lib.rs
+++ b/rr_frontend/radium/src/lib.rs
@@ -1,5 +1,6 @@
#![feature(box_patterns)]
+use rrconfig;
pub mod code;
pub mod specs;
diff --git a/rr_frontend/rrconfig/src/lib.rs b/rr_frontend/rrconfig/src/lib.rs
index bf2d4a9c..3dfd6469 100644
--- a/rr_frontend/rrconfig/src/lib.rs
+++ b/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")
--
GitLab