Fixes for cpc proofs setup (cvc5#11111)

ajreynol · Jul 31, 2024 · beff2e4 · beff2e4
1 parent 11bd4d7
commit beff2e4
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 6 deletions.
diff --git a/contrib/get-ethos-checker b/contrib/get-ethos-checker
@@ -59,7 +59,7 @@ cat << EOF > $BASE_DIR/bin/cpc_gen.sh
 #!/usr/bin/env bash
 
 # call cvc5 and remove the first line of the output (should be "unsat")
-echo "(include \"$SIG_DIR/Cvc5.smt3\")"
+echo "(include \"$SIG_DIR/Cpc.eo\")"
 \$@ --dump-proofs --proof-format=cpc --proof-granularity=dsl-rewrite | tail -n +2
 EOF
 chmod +x $BASE_DIR/bin/cpc_gen.sh

diff --git a/docs/proofs/output_cpc.rst b/docs/proofs/output_cpc.rst
@@ -22,7 +22,7 @@ checking them with the Ethos proof checker.
 The Ethos checker is based on the logical framework Eunoia.
 The Cooperating Proof Calculus has been formalized in a Eunoia signature, which
 is contained within the cvc5 repository in this
-:cvc5repo:`file <proofs/eo/cpc/Cvc5.eo>`.
+:cvc5repo:`file <proofs/eo/cpc/Cpc.eo>`.
 Based on this signature, Ethos can check CPC proofs over all theories that are
 formalized in this signature.
 For more details on Eunoia and a comprehensive overview of the language

diff --git a/proofs/eo/cpc/Cvc5.eo → proofs/eo/cpc/Cpc.eo b/proofs/eo/cpc/Cvc5.eo → proofs/eo/cpc/Cpc.eo
@@ -1,7 +1,7 @@
 ; =============================================================================
 ;
-; This is the official development version of the Eunoia signature for cvc5's
-; internal proof calculus. It is a faithful formalization of cvc5's theory
+; This is the official development version of the Eunoia signature for the
+; Cooperating Proof Calculus. It is a faithful formalization of cvc5's theory
 ; signatures and proof rules.
 ;
 ; NOTE: cvc5 does not strictly follow the SMT-LIB version 2.6 standard. In

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
@@ -263,4 +263,4 @@ name   = "Proof"
   long       = "proof-allow-trust"
   type       = "bool"
   default    = "true"
-  help       = "Whether to allow trust in the ALF printer"
+  help       = "Whether to allow trust in the proof printer (when applicable)"
diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py
@@ -290,7 +290,7 @@ def run_internal(self, benchmark_info):
                 benchmark_info.timeout,
             )
             cpc_sig_dir = os.path.abspath(g_args.cpc_sig_dir)
-            tmpf.write(("(include \"" + cpc_sig_dir + "/cpc/Cvc5.eo\")").encode())
+            tmpf.write(("(include \"" + cpc_sig_dir + "/cpc/Cpc.eo\")").encode())
             tmpf.write(output.strip("unsat\n".encode()))
             tmpf.flush()
             output, error = output.decode(), error.decode()