From a9db73d0beae9d1fa5b0be616c0aad2863ab106e Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 15 Aug 2025 17:10:17 +0000 Subject: [PATCH] CBOR.Spec.Constants -> CBOR.Spec.Const Pulse's DPE test is used in EverCDDL's DPE test, but I have not migrated CBOR in Pulse's DPE test to new EverCBOR/EverCDDL yet. This commit avoids name clashes in the respective CBOR modules. --- share/pulse/examples/dice/cbor/CBOR.Pulse.fst | 2 +- .../dice/cbor/{CBOR.Spec.Constants.fst => CBOR.Spec.Const.fst} | 2 +- share/pulse/examples/dice/cbor/CBOR.Spec.Type.fsti | 2 +- share/pulse/examples/dice/cbor/Makefile | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) rename share/pulse/examples/dice/cbor/{CBOR.Spec.Constants.fst => CBOR.Spec.Const.fst} (98%) diff --git a/share/pulse/examples/dice/cbor/CBOR.Pulse.fst b/share/pulse/examples/dice/cbor/CBOR.Pulse.fst index 9b1f20d35..5d6446fcc 100644 --- a/share/pulse/examples/dice/cbor/CBOR.Pulse.fst +++ b/share/pulse/examples/dice/cbor/CBOR.Pulse.fst @@ -16,7 +16,7 @@ module CBOR.Pulse #lang-pulse -include CBOR.Spec.Constants +include CBOR.Spec.Const include CBOR.Pulse.Extern open Pulse.Lib.Pervasives open Pulse.Lib.Trade diff --git a/share/pulse/examples/dice/cbor/CBOR.Spec.Constants.fst b/share/pulse/examples/dice/cbor/CBOR.Spec.Const.fst similarity index 98% rename from share/pulse/examples/dice/cbor/CBOR.Spec.Constants.fst rename to share/pulse/examples/dice/cbor/CBOR.Spec.Const.fst index 1c55a4cec..113e6f922 100644 --- a/share/pulse/examples/dice/cbor/CBOR.Spec.Constants.fst +++ b/share/pulse/examples/dice/cbor/CBOR.Spec.Const.fst @@ -14,7 +14,7 @@ limitations under the License. *) -module CBOR.Spec.Constants +module CBOR.Spec.Const module U8 = FStar.UInt8 diff --git a/share/pulse/examples/dice/cbor/CBOR.Spec.Type.fsti b/share/pulse/examples/dice/cbor/CBOR.Spec.Type.fsti index 5d33f6bc8..fe13a74b0 100644 --- a/share/pulse/examples/dice/cbor/CBOR.Spec.Type.fsti +++ b/share/pulse/examples/dice/cbor/CBOR.Spec.Type.fsti @@ -15,7 +15,7 @@ *) module CBOR.Spec.Type -include CBOR.Spec.Constants +include CBOR.Spec.Const module U8 = FStar.UInt8 module U64 = FStar.UInt64 diff --git a/share/pulse/examples/dice/cbor/Makefile b/share/pulse/examples/dice/cbor/Makefile index c8fc623ba..605b459b0 100644 --- a/share/pulse/examples/dice/cbor/Makefile +++ b/share/pulse/examples/dice/cbor/Makefile @@ -34,7 +34,7 @@ extract_all_ml: $(ALL_ML_FILES) extract_c: $(OUTPUT_DIR)/CBOR.h $(OUTPUT_DIR)/CBOR.h: $(ALL_KRML_FILES) - $(KRML) -bundle C -bundle CBOR.Spec.Constants+CBOR.Pulse.Type+CBOR.Pulse.Extern=[rename=CBOR] -no-prefix CBOR.Spec.Constants,CBOR.Pulse.Type,CBOR.Pulse.Extern -bundle CBOR.Pulse= -bundle CDDLExtractionTest.Assume+CDDLExtractionTest.Bytes+CDDLExtractionTest.BytesUnwrapped+CDDLExtractionTest.Choice=*[rename=CDDLExtractionTest] -skip-linking $^ -tmpdir $(OUTPUT_DIR) + $(KRML) -bundle C -bundle CBOR.Spec.Const+CBOR.Pulse.Type+CBOR.Pulse.Extern=[rename=CBOR] -no-prefix CBOR.Spec.Const,CBOR.Pulse.Type,CBOR.Pulse.Extern -bundle CBOR.Pulse= -bundle CDDLExtractionTest.Assume+CDDLExtractionTest.Bytes+CDDLExtractionTest.BytesUnwrapped+CDDLExtractionTest.Choice=*[rename=CDDLExtractionTest] -skip-linking $^ -tmpdir $(OUTPUT_DIR) .PHONY: extern