Move legacy probability theories to examples (#1185)

* Move legacy probability theories to examples * Minor cleanups * FTBFS RBDTheory depending also on legacy probability... * Fixed missing dependencies...
HOL-Theorem-Prover · Jan 23, 2024 · af77064 · af77064
1 parent 3a40bff
commit af77064
Show file tree

Hide file tree

Showing 10 changed files with 22 additions and 7 deletions.
diff --git a/examples/dependability/RBD/Holmakefile b/examples/dependability/RBD/Holmakefile
@@ -1,2 +1,2 @@
-INCDIRS = examples/miller/formalize src/probability src/real/analysis
+INCDIRS = examples/miller/formalize src/probability examples/probability/legacy src/real/analysis
 INCLUDES = $(patsubst %,$(dprot $(HOLDIR)/%),$(INCDIRS))
diff --git a/examples/diningcryptos/Holmakefile b/examples/diningcryptos/Holmakefile
@@ -1,2 +1,2 @@
-INCLUDES = ../miller/subtypes ../miller/formalize $(HOLDIR)/src/probability \
+INCLUDES = ../miller/subtypes ../miller/formalize $(HOLDIR)/examples/probability/legacy \
 	$(HOLDIR)/src/real/analysis
diff --git a/examples/miller/prob/Holmakefile b/examples/miller/prob/Holmakefile
@@ -1,2 +1,2 @@
 INCLUDES = ../formalize ../ho_prover ../subtypes ../../Crypto/RSA \
-	   $(HOLDIR)/src/real $(HOLDIR)/src/probability
+	   $(HOLDIR)/src/real $(HOLDIR)/examples/probability/legacy
diff --git a/examples/probability/legacy/Holmakefile b/examples/probability/legacy/Holmakefile
@@ -0,0 +1,8 @@
+INCLUDES = $(HOLDIR)/src/real $(HOLDIR)/src/res_quan/src $(HOLDIR)/src/real/analysis \
+	$(HOLDIR)/src/probability
+
+EXTRA_CLEANS = $(patsubst %Theory.uo,%Theory.html,$(DEFAULT_TARGETS))
+
+all: $(DEFAULT_TARGETS)
+
+.PHONY: all
diff --git a/examples/probability/legacy/README.md b/examples/probability/legacy/README.md
@@ -0,0 +1,7 @@
+# HOL's Legacy Probability Theory based on Finite Measure Theory
+
+The following theories in this directory was in `$(HOLDIR)/src/probability`:
+
+     real_measureScript.sml       * Finite Measure Theory (based on reals)
+     real_lebesgueScript.sml      * Lebesgue Integration based on Finite Measures
+     real_probabilityScript.sml   * Probability Theory based on Finite Measures
diff --git a/src/probability/real_lebesgueScript.sml → ...robability/legacy/real_lebesgueScript.sml b/src/probability/real_lebesgueScript.sml → ...robability/legacy/real_lebesgueScript.sml
diff --git a/src/probability/real_measureScript.sml → ...probability/legacy/real_measureScript.sml b/src/probability/real_measureScript.sml → ...probability/legacy/real_measureScript.sml
diff --git a/src/probability/real_probabilityScript.sml → ...ability/legacy/real_probabilityScript.sml b/src/probability/real_probabilityScript.sml → ...ability/legacy/real_probabilityScript.sml
diff --git a/src/parallel_builds/core/Holmakefile b/src/parallel_builds/core/Holmakefile
@@ -81,7 +81,7 @@ EX2DIRS = AKS algebra algorithms/boyer_moore \
             logic/ltl logic/temporal_deep \
             logic/ltl-transformations \
             l3-machine-code/decompilers \
-          miller \
+          probability/legacy miller \
           probability vector \
           separationLogic/src separationLogic/src/holfoot simple_complexity
 

diff --git a/src/probability/README.md b/src/probability/README.md
@@ -19,9 +19,9 @@ This directory contains HOL4's Measure, Lebesgue Integration and Probability the
 
 ## Measure, Integration and Probability Theory defined on reals (obsoleted)
 
-     real_measureScript.sml       * Measure Theory defined on reals
-     real_lebesgueScript.sml      * Lebesgue integration based on reals
-     real_probabilityScript.sml   * Probability Theory based on reals
+     NOTE: The legacy measure, integration and probability theories based on finite measures
+     are moved to `$(HOLDIR)/examples/probability/legacy`. They are needed when building the
+     two examples in `examples/miller` and `examples/diningcryptos`.
 
 ## Further extensions