OverviewCakeML:84be3269450a8eb815bcc20e0dd686f66ca21fea
Update backendComputeLib use of ThmSetData.
#630 (compute-thmset)
Merging into:dd8ca4fca024b5b629a7c3ed7d3d4b1844c82f3d
Merge pull request #628 from CakeML/ThmSetData-API-change
HOL:0cdc1c5e474153a12e74161f20eb8f5d88a3405f
mark local program variable
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Claimed job
Building HOL
Starting developers
Finished developers 2s 20MB
Starting developers/bin
Finished developers/bin 1m16s 918MB
Starting semantics/ffi
Finished semantics/ffi 37s 580MB
Starting semantics
Finished semantics 1m35s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m59s 1GB
Starting basis/pure
Finished basis/pure 3m34s 595MB
Starting translator
Finished translator 1m40s 1GB
Starting compiler/parsing
Finished compiler/parsing 57s 2GB
Starting characteristic
Finished characteristic 5m13s 1GB
Starting translator/monadic
Finished translator/monadic 1m27s 1GB
Starting basis
FAILED: basis
]0;Holmake: pure]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: pure]0;Holmake: ~/oven/regression/cakeml-788/misc]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-788/misc]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-0cdc1c5e474153a12e74161f20eb8f5d88a3405f/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-788/misc]0;Holmake: ~/oven/regression/cakeml-788/developers]0;Holmake: ~/oven/regression/cakeml-788/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-788/misc]0;Holmake: ~/oven/regression/cakeml-788/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-788/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-788/misc]0;Holmake: ~/oven/regression/cakeml-788/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: pure]0;Holmake: pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-788/characteristic]0;Holmake: ~/oven/regression/cakeml-788/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-788/semantics]0;Holmake: ~/oven/regression/cakeml-788/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-788/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-788/semantics]0;Holmake: ~/oven/regression/cakeml-788/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-788/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-788/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-788/characteristic]0;Holmake: ~/oven/regression/cakeml-788/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-788/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-788/characteristic]0;Holmake: ~/oven/regression/cakeml-788/translator]0;Holmake: ~/oven/regression/cakeml-788/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-788/characteristic]0;Holmake: ~/oven/regression/cakeml-788/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-788/translator/monadic]0;Holmake: ~/oven/regression/cakeml-788/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-788/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-788/translator/monadic]0;Holmake: ~/oven/regression/cakeml-788/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/basis
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on runtimeFFITheory
MarshallingTheory OK
Starting work on fsFFITheory
runtimeFFITheory OK
Starting work on README.md
README.md OK
Starting work on basis_ffi.o
basis_ffi.o OK
clFFITheory OK
RuntimeProgTheory OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory OK
Starting work on fsFFIPropsTheory
OptionProgTheory OK
Starting work on ListProgTheory
RuntimeProofTheory OK
fsFFIPropsTheory OK
ListProgTheory FAILED! <Signal F>
Adding nsLookup representation thms for [ListProg_env_33]
Saved theorem _____ "genlist_aux_v_thm"
Translating genlist
Saved theorem _____ "nsLookup_ListProg_env_34_pfun_eqs"
Saved theorem _____ "genlist_v_thm"
Translating tabulate_aux
Saved theorem _____ "nsLookup_ListProg_env_35_pfun_eqs"
Adding nsLookup representation thms for [ListProg_env_34]
Adding nsLookup representation thms for [ListProg_env_35]
Saved theorem _____ "tabulate_aux_v_thm"