From 3abbdd74a33ac50414e5ef495ee5847bbf6436f7 Mon Sep 17 00:00:00 2001 From: Matthew Brecknell Date: Mon, 19 Feb 2018 14:49:17 +1100 Subject: [PATCH] aspec: reintroduce spec document version information Including version information in the spec document is tricky, because Isabelle will rebuild the session whenever it sees that session inputs (including document sources) have changed. Since ASpec is close to the root of our session hierarchy, frequently changing version information causes excessive rebuilds during development. This commit avoids excessive rebuilding by building the document (with version information) in a separate ASpecDoc session. The ASpecDoc session is identical to the previous version of the ASpec session, but is not the parent of any other sessions. The ASpec session is used as the basis for other sessions, but has document-only inputs removed, and also has document builds disabled. --- .licenseignore | 2 ++ spec/Makefile | 17 +++++++++++++---- spec/ROOT | 14 +++++++++++++- spec/abstract/document/.gitignore | 1 + spec/abstract/document/ARM/ARCH.tex | 1 + spec/abstract/document/ARM_HYP/ARCH.tex | 1 + spec/abstract/document/X64/ARCH.tex | 1 + spec/abstract/document/root.tex | 12 ++++++++---- spec/tests.xml | 1 + 9 files changed, 41 insertions(+), 9 deletions(-) create mode 100644 spec/abstract/document/ARM/ARCH.tex create mode 100644 spec/abstract/document/ARM_HYP/ARCH.tex create mode 100644 spec/abstract/document/X64/ARCH.tex diff --git a/.licenseignore b/.licenseignore index 5958551ed..3ce3ef7d8 100644 --- a/.licenseignore +++ b/.licenseignore @@ -48,6 +48,8 @@ internal/* **/licenses **/CONTRIBUTORS +spec/abstract/document/*/ARCH.tex +spec/abstract/document/gitrev.tex spec/haskell/cabal.sandbox.config spec/haskell/.cabal-sandbox/* diff --git a/spec/Makefile b/spec/Makefile index d0ffc73e4..c5f10d029 100644 --- a/spec/Makefile +++ b/spec/Makefile @@ -27,7 +27,7 @@ report-regression: # # Spec heaps. -HEAPS += ASpec ExecSpec DSpec CKernel CSpec TakeGrant ASepSpec +HEAPS += ASpec ASpecDoc ExecSpec DSpec CKernel CSpec TakeGrant ASepSpec # Additional dependencies @@ -35,13 +35,22 @@ CKernel CSpec: c-kernel design-spec # NOTE: The abstract spec imports Events from Haskell hence the dependency -ExecSpec DSpec : design-spec +ASpec ExecSpec DSpec : design-spec -ASpec: design-spec abstract/document/VERSION +ASPEC_DOC_GITREV_FILE=abstract/document/gitrev.tex +ASPEC_DOC_VERSION_FILE=abstract/document/VERSION -abstract/document/VERSION: $(SEL4_VERSION) +ASpecDoc: design-spec $(ASPEC_DOC_VERSION_FILE) $(ASPEC_DOC_GITREV_FILE) + +$(ASPEC_DOC_VERSION_FILE): $(SEL4_VERSION) cp $< $@ +$(ASPEC_DOC_GITREV_FILE): .FORCE + git rev-parse --short=15 HEAD > $@ || echo unknown > $@ + git diff --no-ext-diff --quiet || echo "*" >> $@ + git diff --no-ext-diff --quiet --cached || echo "+" >> $@ + perl -p -i -e "s/\n//" $@ + # NOTE: the install_C_file in Kernel_C.thy invocation generates a spurious # umm_types.txt file in this folder. This file is never used nor # depended on. diff --git a/spec/ROOT b/spec/ROOT index dca6e0d71..092dbac5a 100644 --- a/spec/ROOT +++ b/spec/ROOT @@ -30,7 +30,16 @@ chapter "Specifications" * Abstract Specification *) +(* Session on which most other sessions build. *) session ASpec in "abstract" = Word_Lib + + options [document=false] + theories + "Syscall_A" + +(* We build the abstract specification document in a separate session, + to avoid rebuilding ASpec (and every session that depends on it) + whenever the git commit ID changes. *) +session ASpecDoc in "abstract" = Word_Lib + options [document=pdf] theories [document = false] "../../lib/Lib" @@ -47,7 +56,8 @@ session ASpec in "abstract" = Word_Lib + "Glossary_Doc" (* "KernelInit_A" *) document_files - "VERSION" (* generated by `make ASpec` *) + "VERSION" (* generated by `make ASpec` *) + "gitrev.tex" (* generated by `make ASpec` *) "root.tex" "root.bib" "defs.bib" @@ -58,6 +68,8 @@ session ASpec in "abstract" = Word_Lib + "imgs/sel4objects_01.pdf" "imgs/sel4objects_05.pdf" "imgs/sel4_internals_01.pdf" + document_files (in "document/$L4V_ARCH") + "ARCH.tex" (* * Executable/Design Specification diff --git a/spec/abstract/document/.gitignore b/spec/abstract/document/.gitignore index 5a9f50bf9..cce7565e4 100644 --- a/spec/abstract/document/.gitignore +++ b/spec/abstract/document/.gitignore @@ -1 +1,2 @@ /VERSION +/gitrev.tex diff --git a/spec/abstract/document/ARM/ARCH.tex b/spec/abstract/document/ARM/ARCH.tex new file mode 100644 index 000000000..74f9acfff --- /dev/null +++ b/spec/abstract/document/ARM/ARCH.tex @@ -0,0 +1 @@ +ARM diff --git a/spec/abstract/document/ARM_HYP/ARCH.tex b/spec/abstract/document/ARM_HYP/ARCH.tex new file mode 100644 index 000000000..e032cf0bd --- /dev/null +++ b/spec/abstract/document/ARM_HYP/ARCH.tex @@ -0,0 +1 @@ +ARM\_HYP diff --git a/spec/abstract/document/X64/ARCH.tex b/spec/abstract/document/X64/ARCH.tex new file mode 100644 index 000000000..8b22261ec --- /dev/null +++ b/spec/abstract/document/X64/ARCH.tex @@ -0,0 +1 @@ +X64 diff --git a/spec/abstract/document/root.tex b/spec/abstract/document/root.tex index 03e6c3796..7ce06c13f 100644 --- a/spec/abstract/document/root.tex +++ b/spec/abstract/document/root.tex @@ -58,11 +58,13 @@ \isabellestyle{tt} \newcommand{\version}{\input{VERSION}\xspace} +\newcommand{\arch}{\input{ARCH}\xspace} +\newcommand{\gitrev}{\input{gitrev}\xspace} \hypersetup { pdfauthor={Trustworthy Systems, Data61}, - pdftitle={Abstract Formal Specification of the seL4 API} + pdftitle={Abstract Formal Specification of the seL4/\arch API} } \renewcommand{\isamarkupchapter}[1]{\chapter{#1}} @@ -91,7 +93,7 @@ \begin{document} -\title{Abstract Formal Specification of the seL4 API} +\title{Abstract Formal Specification of the seL4/\arch API} \date{Version \version} @@ -130,7 +132,9 @@ Simon Winwood \bigskip -Document build date: \today +Architecture: \arch\\ +Document build date: \today\\ +Produced from git change set: \gitrev \clearpage @@ -138,7 +142,7 @@ Document build date: \today This document is the text version of the abstract, formal Isabelle/HOL specification of the seL4 microkernel. It is intended to give a precise, operational definition of the -seL4 microkernel. +seL4 microkernel on the \arch architecture. The document contains a short overview, followed by text generated from the formal Isabelle/HOL definitions. diff --git a/spec/tests.xml b/spec/tests.xml index 116d2f7fd..7ca318bfc 100644 --- a/spec/tests.xml +++ b/spec/tests.xml @@ -27,6 +27,7 @@ make ASpec + make ASpecDoc make ExecSpec make DSpec make TakeGrant