summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--isabelle-lib/Makefile41
-rw-r--r--isabelle-lib/ROOT6
-rw-r--r--lib/isabelle/Makefile34
-rw-r--r--lib/isabelle/ROOT18
4 files changed, 52 insertions, 47 deletions
diff --git a/isabelle-lib/Makefile b/isabelle-lib/Makefile
deleted file mode 100644
index 11cdbc27..00000000
--- a/isabelle-lib/Makefile
+++ /dev/null
@@ -1,41 +0,0 @@
-THYS = Sail_impl_base.thy Sail_values.thy State.thy Prompt.thy
-LEMS = sail_impl_base.lem sail_values.lem state.lem prompt.lem
-
-.PHONY: all heap-img clean
-
-all: heap-img
-
-heap-img: $(THYS)
- @echo '*** To build a heap image with the Sail library, please'
- @echo '*** add the ROOT file in this directory to your ROOTS file'
- @echo '*** (e.g. $$HOME/.isabelle/Isabelle<version>/ROOTS)'
- @echo '*** and add the isabelle binary to your PATH.'
- isabelle build -b Sail
-
-Sail_impl_base.thy: sail_impl_base.lem
- lem -isa $<
-
-Sail_values.thy: sail_values.lem Sail_impl_base.thy
- lem -isa $<
-
-State.thy: state.lem Sail_values.thy
- lem -isa $<
-
-Prompt.thy: prompt.lem Sail_values.thy
- lem -isa $<
-
-sail_impl_base.lem: ../src/lem_interp/sail_impl_base.lem
- cp $< .
-
-sail_values.lem: ../src/gen_lib/sail_values.lem
- cp $< .
-
-state.lem: ../src/gen_lib/state.lem
- cp $< .
-
-prompt.lem: ../src/gen_lib/prompt.lem
- cp $< .
-
-clean:
- -rm $(THYS) $(LEMS)
- -rm *Auxiliary.thy
diff --git a/isabelle-lib/ROOT b/isabelle-lib/ROOT
deleted file mode 100644
index d79b99ba..00000000
--- a/isabelle-lib/ROOT
+++ /dev/null
@@ -1,6 +0,0 @@
-session "Sail" = "LEM" +
- options [document = false]
- theories
- Sail_values
- State
- Prompt
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
new file mode 100644
index 00000000..f340b81b
--- /dev/null
+++ b/lib/isabelle/Makefile
@@ -0,0 +1,34 @@
+THYS = Sail_impl_base.thy Sail_values.thy Sail_operators.thy Sail_operators_mwords.thy State.thy Prompt.thy
+
+.PHONY: all heap-img clean
+
+all: heap-img
+
+heap-img: $(THYS)
+ @echo '*** To build a heap image with the Sail library, please'
+ @echo '*** add the ROOT file in this directory to your ROOTS file'
+ @echo '*** (e.g. $$HOME/.isabelle/Isabelle<version>/ROOTS)'
+ @echo '*** and add the isabelle binary to your PATH.'
+ isabelle build -b Sail
+
+Sail_impl_base.thy: ../../src/lem_interp/sail_impl_base.lem
+ lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+
+Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_impl_base.thy
+ lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+
+Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy
+ lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+
+Sail_operators_mwords.thy: ../../src/gen_lib/sail_operators_mwords.lem Sail_values.thy
+ lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+
+State.thy: ../../src/gen_lib/state.lem Sail_values.thy
+ lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+
+Prompt.thy: ../../src/gen_lib/prompt.lem Sail_values.thy
+ lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
+
+clean:
+ -rm $(THYS)
+ -rm *Auxiliary.thy
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
new file mode 100644
index 00000000..7e90cdf0
--- /dev/null
+++ b/lib/isabelle/ROOT
@@ -0,0 +1,18 @@
+session "Sail" = "LEM" +
+ options [document = false]
+ theories
+ Sail_values
+ State
+ Prompt
+ Sail_operators
+ Sail_operators_mwords
+
+(*session "Sail" = "Sail_Base" +
+ options [document = false]
+ theories
+ Sail_operators
+
+session "Sail_Word" = "Sail_Base" +
+ options [document = false]
+ theories
+ Sail_operators_mwords*)