lib: make Lib session a test dependency

Also ensure that the C parser is built before Lib, because it depends
on generated grammar files that need `make'.
This commit is contained in:
Gerwin Klein 2018-06-13 18:10:46 +02:00
parent b5cdf4703f
commit 6486bad264
6 changed files with 31 additions and 5 deletions

View File

@ -17,7 +17,7 @@
format.
-->
<testsuite depends="isabelle" cpu-timeout="3600">
<testsuite depends="isabelle Lib" cpu-timeout="3600">
<test name="CamkesAdlSpec">make CamkesAdlSpec</test>
<test name="CamkesCdlRefine" depends="CamkesAdlSpec DPolicy">make CamkesCdlRefine</test>
<test name="CamkesGlueSpec">make CamkesGlueSpec</test>

View File

@ -19,7 +19,7 @@
-->
<testsuite cpu-timeout="600">
<set depends="isabelle">
<set depends="isabelle Lib">
<test name="Sep_Algebra">../../isabelle/bin/isabelle build -v -d ../.. Sep_Algebra</test>
</set>

26
lib/tests.xml Normal file
View File

@ -0,0 +1,26 @@
<?xml version="1.0"?>
<!--
Copyright 2018, Data61
This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
@TAG(DATA61_BSD)
-->
<!--
Regression Specification File
See "misc/regression/tests.xml" for a description of the file
format.
-->
<testsuite cpu-timeout="600">
<set depends="isabelle CParser">
<test name="Lib">../isabelle/bin/isabelle build -v -d .. Lib</test>
</set>
</testsuite>

View File

@ -18,7 +18,7 @@
-->
<testsuite cpu-timeout="3600" depends="isabelle">
<testsuite cpu-timeout="3600" depends="isabelle Lib">
<!-- Refine -->
<sequence depends="ASpec">
<test name="AInvs" cpu-timeout="7200">make AInvs</test>

View File

@ -24,7 +24,7 @@
<test name="haskell-translator" cwd="design" cpu-timeout="600">make design</test>
</set>
<set depends="isabelle">
<set depends="isabelle Lib">
<!-- Various seL4 specifications. -->
<test name="ASpec" depends="haskell-translator">make ASpec</test>
<test name="ASpecDoc" depends="ASpec">make ASpecDoc</test>

View File

@ -17,7 +17,7 @@
format.
-->
<testsuite cpu-timeout="3600" depends="isabelle">
<testsuite cpu-timeout="3600" depends="isabelle Lib">
<!-- Refine -->
<sequence depends="DSpecProofs">
<test name="SysInit">make SysInit</test>