87 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP |
87 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP |
88 |
88 |
89 IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES) |
89 IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES) |
90 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP |
90 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP |
91 |
91 |
|
92 |
92 ## IMP |
93 ## IMP |
93 |
94 |
94 IMP_THYS = IMP/Denotational.thy |
95 IMP_THYS = IMP/Denotational.thy |
95 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) |
96 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) |
96 |
97 |
97 IMP: $(OUT)/HOLCF $(IMP_FILES) |
98 IMP: $(OUT)/HOLCF $(IMP_FILES) |
98 @$(ISATOOL) usedir $(OUT)/HOLCF IMP |
99 @$(ISATOOL) usedir $(OUT)/HOLCF IMP |
99 |
100 |
|
101 |
100 ## Miscellaneous examples |
102 ## Miscellaneous examples |
101 |
103 |
102 EX_THYS = ex/Dnat.thy ex/Dlist.thy ex/Stream.thy \ |
104 EX_THYS = ex/Dnat.thy ex/Stream.thy \ |
103 ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \ |
105 ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \ |
104 ex/Hoare.thy ex/Loop.thy |
106 ex/Hoare.thy ex/Loop.thy |
105 |
107 |
106 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
108 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
107 |
109 |
108 EX: ex/ROOT.ML $(EX_FILES) |
110 ex: ex/ROOT.ML $(EX_FILES) |
109 @$(ISATOOL) usedir $(OUT)/HOLCF ex |
111 @$(ISATOOL) usedir $(OUT)/HOLCF ex |
|
112 |
110 |
113 |
111 ## Full test |
114 ## Full test |
112 |
115 |
113 test: $(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP EX |
116 test: $(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP ex |
114 echo 'Test examples ran successfully' > test |
117 echo 'Test examples ran successfully' > test |
115 |
118 |
|
119 |
116 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |
120 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |