adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

spec: factor out common `design-spec` task. 

`ASpec`, `ExecSpec`, and `DSpec` were identical tests which built the
`design-spec` make target. This means that when `./run_tests` runs tests
concurrently, multiple instances of the `design-spec` make target were
also run concurrently.

We address the issue by making a new "test" called `design-spec` which
builds the `design-spec` make target, and making `{A,Exec,D}Spec`
dependees on `design-spec`.
This commit is contained in:
Edward Pierzchalski 2020-01-20 15:40:29 +11:00
parent ff6c0d8a0a
commit 2fec23d646
1 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
spec/tests.xml
View File

@ -26,10 +26,11 @@
<set depends="isabelle Lib">
<!-- Various seL4 specifications. -->
<test name="ASpec" depends="haskell-translator">make ASpec</test>
<test name="design-spec" depends="haskell-translator">make design-spec</test>
<test name="ASpec" depends="design-spec">make ASpec</test>
<test name="ASpecDoc" depends="ASpec">make ASpecDoc</test>
<test name="ExecSpec" depends="haskell-translator">make ExecSpec</test>
<test name="DSpec" depends="haskell-translator">make DSpec</test>
<test name="ExecSpec" depends="design-spec">make ExecSpec</test>
<test name="DSpec" depends="design-spec">make DSpec</test>
<test name="TakeGrant">make TakeGrant</test>
<test name="ASepSpec" depends="ASpec">make ASepSpec</test>
</set>