From b5e7fa4e45334335def9979242c292debf9f01c5 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 28 Oct 2020 13:34:32 +1000 Subject: [PATCH] Makefiles: factor out ASpec doc file generation Make these a separate target so that other sessions that depend on ASpec can kick off generation of these files (necessary because some are mentioned in spec/ROOT, and the session structure will fail if they don't exist). This is only relevant in a fresh check-out when you've never built ASpec, but in test environments this can happen if only specific sessions are tested. Signed-off-by: Gerwin Klein --- proof/Makefile | 10 ++++++++-- spec/Makefile | 4 +++- 2 files changed, 11 insertions(+), 3 deletions(-) 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 $< $@