/usr/share/hol88-2.02.19940316/contrib/UNITY/Makefile is in hol88-contrib-source 2.02.19940316-14.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 | # =====================================================================
#
# MAKEFILE FOR THE HOL LIBRARY: UNITY
#
# =====================================================================
# =====================================================================
#
# MAIN ENTRIES:
#
# make all : create theories and compile code
#
# make clean : remove only compiled code
#
# make clobber : remove both theories and compiled code
#
# For the moment no compilation files have been made
#
# ---------------------------------------------------------------------
#
# MACROS:
#
# Hol : the pathname of the version of hol used
# =====================================================================
Hol=../../hol
dummy:
@echo "*** UNITY library: make parameter missing ***"
# =====================================================================
# Cleaning functions.
# =====================================================================
clean:
rm -f *_ml.o
@echo "===> library UNITY: all object code deleted"
clobber:
rm -f *_ml.o *_ml.l *.th
@echo "===> library UNITY: all object code and theory files deleted"
# =====================================================================
# Entries for individual files.
# =====================================================================
state_logic.th: mk_state_logic.ml
echo 'set_flag(`abort_when_fail`,true);;'\
'loadf `aux_definitions`;;'\
'loadt `mk_state_logic`;;'\
'quit();;' | ${Hol}
unless.th: state_logic.th mk_unless.ml
echo 'set_flag(`abort_when_fail`,true);;'\
'loadf `aux_definitions`;;'\
'autoload_defs_and_thms `state_logic`;;'\
'loadt `mk_unless`;;'\
'quit();;' | ${Hol}
ensures.th: unless.th mk_ensures.ml
echo 'set_flag(`abort_when_fail`,true);;'\
'loadf `aux_definitions`;;'\
'autoload_defs_and_thms `state_logic`;;'\
'autoload_defs_and_thms `unless`;;'\
'loadt `mk_ensures`;;'\
'quit();;' | ${Hol}
gen_induct.th: ensures.th mk_gen_induct.ml
echo 'set_flag(`abort_when_fail`,true);;'\
'loadf `aux_definitions`;;'\
'autoload_defs_and_thms `state_logic`;;'\
'autoload_defs_and_thms `unless`;;'\
'autoload_defs_and_thms `ensures`;;'\
'loadt `mk_gen_induct`;;'\
'quit();;' | ${Hol}
leadsto.th: gen_induct.th mk_leadsto.ml
echo 'set_flag(`abort_when_fail`,true);;'\
'loadf `aux_definitions`;;'\
'autoload_defs_and_thms `state_logic`;;'\
'autoload_defs_and_thms `unless`;;'\
'autoload_defs_and_thms `ensures`;;'\
'autoload_defs_and_thms `gen_induct`;;'\
'loadt `mk_leadsto`;;'\
'quit();;' | ${Hol}
comp_unity.th: leadsto.th mk_comp_unity.ml
echo 'set_flag(`abort_when_fail`,true);;'\
'loadf `aux_definitions`;;'\
'autoload_defs_and_thms `state_logic`;;'\
'autoload_defs_and_thms `unless`;;'\
'autoload_defs_and_thms `ensures`;;'\
'autoload_defs_and_thms `gen_induct`;;'\
'autoload_defs_and_thms `leadsto`;;'\
'loadt `mk_comp_unity`;;'\
'quit();;' | ${Hol}
all: state_logic.th unless.th ensures.th gen_induct.th leadsto.th\
comp_unity.th
@echo "===> library UNITY rebuilt"
|