blob: 3aa142a3c40c3f1de4f129916d1b02a0cfe13522 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
#!/bin/bash
set -ex
../../../sail ../../prelude.sail ../../no_devices.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
# Explicitly include replacement prompt files, as Lem's choice of file depends
# on some internal dependency ordering
lem -hol -outdir . -lib ../../../lib/hol ../../../lib/hol/sail2_prompt_monad.lem ../../../lib/hol/sail2_prompt.lem -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem
Holmake
|
