Get Aarch64 exported to HOL4

Worked around problem with the model where it tries to use bound variables
in patterns

1 files changed, 9 insertions, 0 deletions

diff --git a/aarch64/mono/demo/mk.hol b/aarch64/mono/demo/mk.hol
new file mode 100755
index 00000000..ac20717f
--- /dev/null
+++ b/aarch64/mono/demo/mk.hol
@@ -0,0 +1,9 @@
+#!/bin/bash
+set -ex
+../../../sail ../../prelude.sail ../mono_rewrites.sail \
+     aarch64_no_vector/spec.sail aarch64_no_vector/decode_start.sail aarch64_no_vector/decode.sail aarch64_no_vector/decode_end.sail \
+     -no_lexp_bounds_check -memo_z3 -undefined_gen \
+     -auto_mono -mono_rewrites -dall_split_errors -dmono_continue \
+     -lem -lem_mwords -lem_sequential -lem_lib Aarch64_extras -o aarch64_mono
+lem -hol -outdir . -lib ../../../lib/hol -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem 
+Holmake