1.1 --- a/src/HOL/IsaMakefile Sun Mar 04 00:29:19 2012 +0100
1.2 +++ b/src/HOL/IsaMakefile Sun Mar 04 10:33:47 2012 +0100
1.3 @@ -11,6 +11,10 @@
1.4 HOL-Library \
1.5 HOL-Algebra \
1.6 HOL-Boogie \
1.7 + HOL-HOL4 \
1.8 + HOL-HOL_Light \
1.9 + HOL-HOL4-Imported \
1.10 +# HOL-HOL_Light-Imported \ FIXME not operative at the moment \
1.11 HOL-IMP \
1.12 HOL-Multivariate_Analysis \
1.13 HOL-NSA \
1.14 @@ -19,10 +23,6 @@
1.15 HOL-SPARK \
1.16 HOL-Word \
1.17 HOLCF \
1.18 - Import-HOL4 \
1.19 - Import-HOL_Light \
1.20 - Import-HOL4-Imported \
1.21 -# Import-HOL_Light-Imported \ FIXME not operative at the moment \
1.22 IOA \
1.23 TLA \
1.24 HOL-Base \
1.25 @@ -83,8 +83,8 @@
1.26 # ^ this is the sort position
1.27
1.28 generate: \
1.29 - Import-HOL4-Generate \
1.30 - Import-HOL_Light-Generate
1.31 + HOL-HOL4-Generate \
1.32 + HOL-HOL_Light-Generate
1.33
1.34 benchmark: \
1.35 HOL-Datatype_Benchmark \
1.36 @@ -557,35 +557,44 @@
1.37
1.38 ## Import sessions
1.39
1.40 -Import-HOL4: $(OUT)/Import-HOL4
1.41 -
1.42 -BASIC_IMPORTER_DEPENDENCIES = Import/Importer.thy \
1.43 +IMPORTER_BASIC_DEPENDENCIES = \
1.44 + Import/Importer.thy \
1.45 Import/shuffler.ML \
1.46 Import/import_rews.ML \
1.47 Import/proof_kernel.ML \
1.48 Import/replay.ML \
1.49 Import/import.ML
1.50
1.51 -$(OUT)/Import-HOL4: $(OUT)/HOL \
1.52 - $(BASIC_IMPORTER_DEPENDENCIES) \
1.53 +IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES = \
1.54 Import/HOL4/ROOT.ML \
1.55 Import/HOL4/Compatibility.thy
1.56 - @cd Import/HOL4; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL Import-HOL4
1.57
1.58 -Import-HOL_Light: $(OUT)/Import-HOL_Light
1.59 -
1.60 -$(OUT)/Import-HOL_Light: $(OUT)/HOL \
1.61 - $(BASIC_IMPORTER_DEPENDENCIES) \
1.62 +IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES = \
1.63 Import/HOL_Light/ROOT.ML \
1.64 Import/HOL_Light/HOLLightInt.thy \
1.65 Import/HOL_Light/HOLLightList.thy \
1.66 Import/HOL_Light/HOLLightReal.thy \
1.67 Import/HOL_Light/Compatibility.thy
1.68 - @cd Import/HOL_Light; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL Import-HOL_Light
1.69
1.70 -Import-HOL4-Imported: $(OUT)/Import-HOL4-Imported
1.71 +HOL-HOL4: $(LOG)/HOL-HOL4.gz
1.72
1.73 -$(OUT)/Import-HOL4-Imported: $(OUT)/Import-HOL4 \
1.74 +$(LOG)/HOL-HOL4.gz: $(OUT)/HOL \
1.75 + $(IMPORTER_BASIC_DEPENDENCIES) \
1.76 + $(IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES)
1.77 + @$(ISABELLE_TOOL) usedir $(OUT)/HOL Import/HOL4
1.78 +
1.79 +HOL-HOL_Light: $(LOG)/HOL-HOL_Light.gz
1.80 +
1.81 +$(LOG)/HOL-HOL_Light.gz: $(OUT)/HOL \
1.82 + $(IMPORTER_BASIC_DEPENDENCIES) \
1.83 + $(IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES)
1.84 + @$(ISABELLE_TOOL) usedir $(OUT)/HOL Import/HOL_Light
1.85 +
1.86 +HOL-HOL4-Imported: $(LOG)/HOL-HOL4-Imported.gz
1.87 +
1.88 +$(LOG)/HOL-HOL4-Imported.gz: $(OUT)/HOL \
1.89 + $(IMPORTER_BASIC_DEPENDENCIES) \
1.90 + $(IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES) \
1.91 Import/HOL4/imported.ML \
1.92 Import/HOL4/Imported.thy \
1.93 Import/HOL4/Generated/HOL4Base.thy \
1.94 @@ -641,20 +650,24 @@
1.95 Import/HOL4/Generated/word_base.imp \
1.96 Import/HOL4/Generated/word_bitop.imp \
1.97 Import/HOL4/Generated/word_num.imp
1.98 - @cd Import/HOL4; $(ISABELLE_TOOL) usedir -b -f imported.ML -p 0 $(OUT)/Import-HOL4 Import-HOL4-Imported
1.99 + @$(ISABELLE_TOOL) usedir -f imported.ML -s HOL4-Imported -p 0 $(OUT)/HOL Import/HOL4
1.100
1.101 -Import-HOL_Light-Imported: $(OUT)/Import-HOL_Light-Imported
1.102 +HOL-HOL_Light-Imported: $(LOG)/HOL-HOL_Light-Imported.gz
1.103
1.104 -$(OUT)/Import-HOL_Light-Imported: $(OUT)/Import-HOL_Light \
1.105 +$(LOG)/HOL-HOL_Light-Imported.gz: $(OUT)/HOL \
1.106 + $(IMPORTER_BASIC_DEPENDENCIES) \
1.107 + $(IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES) \
1.108 Import/HOL_Light/imported.ML \
1.109 Import/HOL_Light/Imported.thy \
1.110 Import/HOL_Light/Generated/HOLLight.thy \
1.111 Import/HOL_Light/Generated/hollight.imp
1.112 - @cd Import/HOL_Light; $(ISABELLE_TOOL) usedir -b -f imported.ML -p 0 $(OUT)/Import-HOL_Light Import-HOL_Light-Imported
1.113 + @$(ISABELLE_TOOL) usedir -f imported.ML -s HOL_Light-Imported -p 0 $(OUT)/HOL Import/HOL_Light
1.114
1.115 -Import-HOL4-Generate: $(LOG)/Import-HOL4-Generate.gz
1.116 +HOL-HOL4-Generate: $(LOG)/Import-HOL4-Generate.gz
1.117
1.118 -$(LOG)/Import-HOL4-Generate.gz: $(OUT)/Import-HOL4 \
1.119 +$(LOG)/Import-HOL4-Generate.gz: $(OUT)/HOL \
1.120 + $(IMPORTER_BASIC_DEPENDENCIES) \
1.121 + $(IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES) \
1.122 Import/HOL4/generate.ML \
1.123 Import/HOL4/Generate.thy \
1.124 Import/HOL4/Template/GenHOL4Base.thy \
1.125 @@ -662,15 +675,17 @@
1.126 Import/HOL4/Template/GenHOL4Real.thy \
1.127 Import/HOL4/Template/GenHOL4Vec.thy \
1.128 Import/HOL4/Template/GenHOL4Word32.thy
1.129 - @cd Import; $(ISABELLE_TOOL) usedir -f generate.ML -s Generate -p 0 $(OUT)/Import-HOL4 HOL4
1.130 + @$(ISABELLE_TOOL) usedir -f generate.ML -s HOL4-Generate -p 0 $(OUT)/HOL Import/HOL4
1.131
1.132 -Import-HOL_Light-Generate: $(LOG)/Import-HOL_Light-Generate.gz
1.133 +HOL-HOL_Light-Generate: $(LOG)/Import-HOL_Light-Generate.gz
1.134
1.135 -$(LOG)/Import-HOL_Light-Generate.gz: $(OUT)/Import-HOL_Light \
1.136 +$(LOG)/Import-HOL_Light-Generate.gz: $(OUT)/HOL \
1.137 + $(IMPORTER_BASIC_DEPENDENCIES) \
1.138 + $(IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES) \
1.139 Import/HOL_Light/generate.ML \
1.140 Import/HOL_Light/Generate.thy \
1.141 Import/HOL_Light/Template/GenHOLLight.thy
1.142 - @cd Import; $(ISABELLE_TOOL) usedir -f generate.ML -s Generate -p 0 $(OUT)/Import-HOL_Light HOL_Light
1.143 + @$(ISABELLE_TOOL) usedir -f generate.ML -s HOL_Light-Generate -p 0 $(OUT)/HOL Import/HOL_Light
1.144
1.145
1.146 ## HOL-Number_Theory