portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

proof: Defer theory dependencies to isabelle

Browse source 
Instead of explicitly depending on Kernel_C.thy prior to generating proofs, this removes
the dependency check and leaves isabelle to check the dependency upon import.
This commit is contained in:
Adrian Danis 2017-09-20 14:22:13 +10:00
parent 567127defe
commit eac4f6bfa2
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tools/helpers.cmake
View file

@ -133,7 +133,6 @@ function(GenThyBFTarget args target_name target_file pbf_path pbf_target prunes
foreach(prune IN LISTS prunes)
list(APPEND args "--prune" "${prune}")
endforeach()
list(APPEND deps "${CSPEC_DIR}/Kernel_C.thy" ${prunes})
GenBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${deps}")
endfunction(GenThyBFTarget)