OverviewCakeML:42596dd3aaa8b5ce1a7b27086d9b979fe5f7838a
Fixes following changes to Define in HOL
HOL:56dc1e0e615822dd6a135a511531a138bae2688c
Refine definition of what it is to be a vacuous pattern
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 4s 149MB
Starting developers/bin
Finished developers/bin 4s 674MB
Starting semantics/ffi
Finished semantics/ffi 9s 240MB
Starting semantics
Finished semantics 2m14s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m40s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 16s 496MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m29s 1GB
Starting basis/pure
Finished basis/pure 2m53s 923MB
Starting translator
Finished translator 3m02s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m14s 1GB
Starting characteristic
Finished characteristic 6m25s 1GB
Starting translator/monadic
Finished translator/monadic 1m55s 1GB
Starting basis
FAILED: basis
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanned 28 directories
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md (0s) OK
Starting work on runtimeFFITheory
MarshallingTheory (11s) OK
Starting work on fsFFITheory
runtimeFFITheory (12s) OK
Starting work on basis_ffi.o
basis_ffi.o (0s) OK
clFFITheory (13s) OK
RuntimeProgTheory (28s) OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory (22s) OK
Starting work on fsFFIPropsTheory
OptionProgTheory (17s) OK
Starting work on ListProgTheory
RuntimeProofTheory (26s) OK
fsFFIPropsTheory (55s) OK
ListProgTheory (56m)FAIL<Signal 9>
Saved theorem _______ "nsLookup_ListProg_env_37_pfun_eqs"
Adding nsLookup representation thms for [ListProg_env_37]
Saved theorem _______ "collate_v_thm"
Saved theorem _______ "ZIP_ind"
Translating zip
Saved theorem _______ "zip_side_rules"
Saved theorem _______ "zip_side_ind"
Saved theorem _______ "zip_side_strongind"
Saved theorem _______ "zip_side_cases"
Saved theorem _______ "zip_side_def"