abstract pdf: generate VERSION, ARCH, git-id information for PDF

spec/Makefile

@@ -9,6 +9,7 @@
 #
 
 SHELL=bash
+SEL4_VERSION=../../seL4/VERSION
 
 # default to primary verification platform
 L4V_ARCH?=ARM
@@ -34,7 +35,19 @@ CKernel CSpec: c-kernel design-spec
 
 # NOTE: The abstract spec imports Events from Haskell hence the dependency
 
-ExecSpec ASpec DSpec : design-spec
+ExecSpec DSpec : design-spec
+
+ASpec: design-spec abstract/document/VERSION \
+       abstract/document/git-id abstract/document/ARCH
+
+abstract/document/VERSION: $(SEL4_VERSION)
+	cp $< $@
+
+abstract/document/git-id: .FORCE
+	git rev-parse HEAD | cut -c -15 > $@
+
+abstract/document/ARCH: .FORCE
+	echo $(L4V_ARCH) | perl -pe "s/\\_/\\\\_/g" > $@
 
 # 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
@@ -50,7 +63,6 @@ design-spec: .FORCE
 	cd design/ && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) design
 .PHONY: design-spec
 
-
 # Sets up the c-parser grammar files
 c-parser: .FORCE
 	cd ../tools/c-parser && make c-parser-deps

spec/ROOT

@@ -47,7 +47,9 @@ session ASpec in "abstract" = Word_Lib +
     "Glossary_Doc"
     (* "KernelInit_A" *)
   document_files
-    "VERSION"
+    "VERSION" (* this file and the next 2 are generated by "make ASpec" *)
+    "ARCH"
+    "git-id"
     "root.tex"
     "root.bib"
     "defs.bib"

spec/abstract/document/.gitignore

@@ -0,0 +1,3 @@
+/ARCH
+/VERSION
+/git-id

spec/abstract/document/root.tex

@@ -46,6 +46,7 @@
 \usepackage{graphicx}
 \usepackage[draft]{fixme}
 \usepackage{cite}
+\usepackage{xspace}
 
 % this should be the last package used
 \usepackage{color}
@@ -56,10 +57,14 @@
 \urlstyle{rm}
 \isabellestyle{tt}
 
+\newcommand{\version}{\input{VERSION}\xspace}
+\newcommand{\arch}{\input{ARCH}\xspace}
+\newcommand{\gitid}{\input{git-id}\xspace}
+
 \hypersetup
 {
-    pdfauthor={NICTA SSRG Research Group},
-    pdftitle={Abstract Formal Specification of the seL4/ARMv6 API}
+    pdfauthor={Trustworthy Systems, Data61},
+    pdftitle={Abstract Formal Specification of the seL4/\arch API}
 }
 
 \renewcommand{\isamarkupchapter}[1]{\chapter{#1}}
@@ -86,11 +91,9 @@
 \newcommand{\meth}[1]{\texttt{#1()}}
 \newcommand{\obj}[1]{\textsf{\small #1}}
 
-\newcommand{\version}{\input{VERSION}}
-
 \begin{document}
 
-\title{Abstract Formal Specification of the seL4/ARMv6 API}
+\title{Abstract Formal Specification of the seL4/\arch API}
 
 \date{Version \version}
 
@@ -119,13 +122,19 @@
 
 \textsc{All rights reserved}.
 
+\bigskip
+
+Architecture: \arch\\
+Document build date: \today\\
+Produced from git change set: \gitid
+
 \clearpage
 
 \chapter*{Abstract}
 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 on the ARMv6 architecture.
+seL4 microkernel on the \arch architecture.
 The document contains a short overview, followed by
 text generated from the formal Isabelle/HOL definitions.