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

Parallelise GraphRefine in its default run.

This commit is contained in:
Thomas Sewell 2015-12-08 17:35:34 +11:00
parent a918b41163
commit 15d09a093a
2 changed files with 8 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/asmrefine/SEL4GraphRefine.thy
View File

@ -83,8 +83,8 @@ ML {*
*)
ML {* ProveSimplToGraphGoals.test_all_graph_refine_proofs_after
funs (csenv ()) @{context} NONE *}
ML {* ProveSimplToGraphGoals.test_all_graph_refine_proofs_parallel
funs (csenv ()) @{context} *}
end

6
tools/asmrefine/ProveGraphRefine.thy
View File

@ -729,6 +729,12 @@ fun test_all_graph_refine_proofs_after funs csenv ctxt nm = let
handle TERM _ => err s | TYPE _ => err s | THM _ => err s) ss
in "success" end
fun test_all_graph_refine_proofs_parallel funs csenv ctxt = let
val ss = Symtab.keys funs
val _ = Par_List.map (test_graph_refine_proof_with_def funs csenv ctxt
#> writeln) ss
in "success" end
end
*}