Merge pull request #197 from kth-step/bir-ott

Improvements to BIR documentation
kth-step · Jan 7, 2025 · a8557a8 · a8557a8
2 parents 72c6787 + f0fe329
commit a8557a8
Show file tree

Hide file tree

Showing 18 changed files with 1,460 additions and 1,801 deletions.
diff --git a/examples/compute/Holmakefile b/examples/compute/Holmakefile
@@ -24,5 +24,6 @@ test-compute.exe: test-compute.uo
 
 test: test-compute.exe
 	./test-compute.exe
+.PHONY: test
 
 EXTRA_CLEANS = test-compute.exe
diff --git a/examples/compute/examples/Holmakefile b/examples/compute/examples/Holmakefile
@@ -6,13 +6,14 @@ INCLUDES = $(HOLBADIR)/examples/compute/examples/increment \
  $(HOLBADIR)/examples/compute/examples/sum_list \
  $(HOLBADIR)/examples/compute/examples/jump_chain
 
-all: $(DEFAULT_TARGETS) test-examples.exe
+all: $(DEFAULT_TARGETS) benchmark-examples.exe
 .PHONY: all
 
-test-examples.exe: test-examples.uo
+benchmark-examples.exe: benchmark-examples.uo
 	$(HOLMOSMLC) -o $@ $<
 
-test: test-examples.exe
-	./test-examples.exe
+benchmark: benchmark-examples.exe
+	./benchmark-examples.exe
+.PHONY: benchmark
 
-EXTRA_CLEANS = test-examples.exe
+EXTRA_CLEANS = benchmark-examples.exe
diff --git a/examples/compute/examples/test-examples.sml → ...s/compute/examples/benchmark-examples.sml b/examples/compute/examples/test-examples.sml → ...s/compute/examples/benchmark-examples.sml
diff --git a/examples/compute/examples/increment/ex_incrementScript.sml b/examples/compute/examples/increment/ex_incrementScript.sml
@@ -5,7 +5,7 @@
 open HolKernel Parse boolLib bossLib;
 open birTheory;
 open bir_computeTheory;
-
+open bir_metaTheory;
 
 val _ = new_theory "ex_increment";