History log of /seL4-l4v-10.1.1/l4v/spec/Makefile
Revision Date Author Comments
# 3abbdd74 18-Feb-2018 Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

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.


# 0b2cb85b 15-Feb-2018 Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

aspec: remove ARCH and git-id from specification document

This partially reverts a recent change which adds these.

Unfortunately, including the ARCH and git-id files in the ROOT file
causes frequent rebuilds during development. For example, adding a
commit that changes only CRefine would cause a change in the git-id
file, which would in turn trigger a rebuild of ASpec and everything that
depends on it. Because the git-id file also noted uncommitted changes,
these would also trigger an ASpec rebuild. Similarly, switching to a
different L4V_ARCH would cause the ARCH file to change, also triggering
an ASpec rebuild.

Since Isabelle makes it difficult to include this information in the
document without adding these files to the ROOT file, this commit is
removing this information until we find a better way.


# 07f4c601 25-Jan-2018 Gerwin Klein <gerwin.klein@data61.csiro.au>

abstract pdf: indicate additional/dirty files in hash


# e6c65356 25-Jan-2018 Gerwin Klein <gerwin.klein@data61.csiro.au>

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


# a5a9f100 22-Nov-2017 Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

dspec: add dependency on haskell-translator


# 8273ca81 12-Sep-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

cspec: Remove redundancy in build rules and theory files for c-kernel builds

Removes files that were duplicated in cspec/$L4V_ARCH directories to exist directly in
the cspec directory and contain $L4V_ARCH switches where needed. This allows for a single
Makefile for building the C kernel and the KernelInc_C theory, which is different between
architectures, to still exist per L4V_ARCH.

As the build location of the C kernel, and the resulting kernel_all.c_pp artifact, is
moved this change needs to be reflected in all the theory files that refer to it.


# ba941179 13-Sep-2017 Adrian Danis <Adrian.Danis@data61.csiro.au>

cspec: Use CMake for building the C kernel

The seL4 kernel now supports a CMake based build in addition to the original Make based
one. This changes the Makefile that previously included the kernel Makefile to instead
have rules for instantiating a sub CMake build

As the location of built files have changed the KernelInc_C theory also needs to be updated
to point to the new locations for the generated artifacts.


# 81e87e5e 07-Aug-2017 Gerwin Klein <gerwin.klein@data61.csiro.au>

Makefile: CSpec and CKernel depend on theories from design spec


# dba1b08c 20-Jul-2017 Alejandro Gomez-Londono <alejandro.gomez@data61.csiro.au>

c-parser: Removes automatically generated lexer and parser files


# ce748b75 22-Jun-2017 Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

x64: create arch-specific CKernel


# 0a31fa7f 09-May-2017 Alejandro Gomez-Londono <alejandro.gomez@data61.csiro.au>

Remove spec-check test and scripts


# 41f200d5 09-May-2017 Alejandro Gomez-Londono <alejandro.gomez@data61.csiro.au>

design: Update Makefiles + tests.xml to auto-generate the design spec

* It runs the haskell-translator as a dependency, eliminating the
need for "run haskell translator" commits.


# 7e13fb9e 29-Mar-2017 Rafal Kolanski <rafal.kolanski@nicta.com.au>

cspec: move to ARM subdirectory

Configure to build with L4V_ARCH=ARM


# c1574f1f 16-Feb-2016 Matthew Brecknell <Matthew.Brecknell@nicta.com.au>

cspec: build: avoid re-entering isabelle via dash-0.5.8


# fad2c6aa 11-Jan-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

paramatrised abstract and haskell specs over L4V_ARCH

Haskell translator was modified to support multiple translations
of the haskell, with different build parameters.


# d92666bc 10-Dec-2015 Japheth Lim <Japheth.Lim@nicta.com.au>

regression: remove forceful build options from CSpec makefiles. They don't seem to be needed.


# f1d808c9 13-Aug-2014 Gerwin Klein <gerwin.klein@nicta.com.au>

integrate separation kernel config proofs

Hooked up into build system and regression test; added READMEs


# 2a03e81d 14-Jul-2014 Gerwin Klein <gerwin.klein@nicta.com.au>

Import release snapshot.