#
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.
|