equal
deleted
inserted
replaced
31 |
31 |
32 |
32 |
33 |
33 |
34 #### Tests and examples |
34 #### Tests and examples |
35 |
35 |
|
36 ## IMP |
|
37 |
|
38 IMP_THYS = IMP/Denotational.thy |
|
39 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML) |
|
40 |
|
41 IMP: $(OUT)/HOLCF $(IMP_FILES) |
|
42 @$(ISATOOL) testdir $(OUT)/HOLCF IMP |
|
43 |
36 ## Miscellaneous examples |
44 ## Miscellaneous examples |
37 |
45 |
38 EX_THYS = ex/Classlib.thy ex/Witness.thy\ |
46 EX_THYS = ex/Classlib.thy ex/Witness.thy\ |
39 ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\ |
47 ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\ |
40 ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\ |
48 ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\ |
41 ex/Hoare.thy ex/Loop.thy |
49 ex/Hoare.thy ex/Loop.thy |
42 |
50 |
43 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
51 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML) |
44 |
52 |
45 test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES) |
53 EX: ex/ROOT.ML $(EX_FILES) |
46 @$(ISATOOL) testdir $(OUT)/HOLCF ex |
54 @$(ISATOOL) testdir $(OUT)/HOLCF ex |
47 |
55 |
|
56 ## Full test |
|
57 |
|
58 test: $(OUT)/HOLCF IMP EX |
|
59 echo 'Test examples ran successfully' > test |
|
60 |
48 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |
61 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF |