diff --git a/proof/Makefile b/proof/Makefile index 16da22797..3667ca3e3 100644 --- a/proof/Makefile +++ b/proof/Makefile @@ -19,7 +19,7 @@ report-regression: # # Refine heaps. -HEAPS += AInvs BaseRefine BaseRefine2 Refine RefineOrphanage +HEAPS += AInvs BaseRefine Refine RefineOrphanage # CRefine heaps. HEAPS += CKernel CSpec CBaseRefine CRefine @@ -45,7 +45,9 @@ BaseRefine Refine DBaseRefine DRefine: design-spec # CKernel uses the `machinety=machine_state` option for `install_C_file`, # and therefore depends on `design-spec`. -CKernel CSpec CBaseRefine CRefine SimplExportAndRefine: c-kernel design-spec +CKernel CSpec : c-kernel design-spec + +CBaseRefine CRefine SimplExportAndRefine : c-kernel design-spec ASpec-files # Preprocess the kernel's source code and bitfield theory files. c-kernel: .FORCE @@ -57,6 +59,10 @@ design-spec: .FORCE cd ../spec && $(ISABELLE_TOOL) env make design-spec .PHONY: design-spec +ASpec-files: .FORCE + cd ../spec && make ASpec-files +.PHONY: ASpec-files + include ../misc/isa-common.mk # SimplExportOnly is treated specially, to not save an image. diff --git a/spec/Makefile b/spec/Makefile index 26fedc01c..3b4a42d37 100644 --- a/spec/Makefile +++ b/spec/Makefile @@ -38,7 +38,9 @@ ASPEC_GITREV_FILE=abstract/document/gitrev.tex GIT_ROOT_FILE=abstract/document/git-root.tex # NOTE: The abstract spec imports Events from Haskell hence the dependency -ASpec: $(ASPEC_VERSION_FILE) $(GIT_ROOT_FILE) $(ASPEC_GITREV_FILE) design-spec +ASpec: ASpec-files design-spec + +ASpec-files: $(ASPEC_VERSION_FILE) $(GIT_ROOT_FILE) $(ASPEC_GITREV_FILE) $(ASPEC_VERSION_FILE): $(SEL4_VERSION) cp $< $@