Overview

Job 2146

CakeML:d2fedc4e90f1db37403de108a25fbda21f2f745f
  Merge pull request #955 from CakeML/vipr
HOL:990630ae2199b660ef33ad0f27944e48b2d2a7c4
  Two more fixes given core simpset changes
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               5s 101MB
 Starting developers/bin
 Finished developers/bin                                           6s   1GB
 Starting compiler/proofs
 FAILED: compiler/proofs
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/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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/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)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/proofs[0m
Scanned 83 directories
Starting work on locationTheory
Starting work on balanced_mapTheory
Starting work on FormalLangTheory
Starting work on charsetTheory
FormalLangTheory                                                                                                                                     examples/formal-languages  (1s)     OK
Finished $(HOLDIR)/examples/formal-languages [#theories: 1]                                                                                                                        (1.311s) 
Starting work on vec_mapTheory
locationTheory                                                                                                                          examples/formal-languages/context-free  (1s)     OK
Starting work on grammarTheory
vec_mapTheory                                                                                                                                examples/formal-languages/regular  (1s)     OK
Starting work on lprefix_lubTheory
grammarTheory                                                                                                                           examples/formal-languages/context-free  (2s)     OK
Starting work on NTpropertiesTheory
lprefix_lubTheory                                                                                                                              examples/fun-op-sem/lprefix_lub  (3s)     OK
Starting work on pegTheory
charsetTheory                                                                                                                                examples/formal-languages/regular  (9s)     OK
Starting work on regexpTheory
NTpropertiesTheory                                                                                                                      examples/formal-languages/context-free  (5s)     OK
Finished $(HOLDIR)/examples/fun-op-sem/lprefix_lub [#theories: 1]                                                                                                                  (3.429s) 
Starting work on set_sepTheory
pegTheory                                                                                                                               examples/formal-languages/context-free  (6s)     OK
Starting work on pegexecTheory
set_sepTheory                                                                                                                               examples/machine-code/hoare-triple  (5s)     OK
Starting work on simpleSexpTheory
pegexecTheory                                                                                                                           examples/formal-languages/context-free  (3s)     OK
Starting work on tailrecTheory
tailrecTheory                                                                                                                               examples/machine-code/hoare-triple  (0s)     OK
Starting work on progTheory
progTheory                                                                                                                                  examples/machine-code/hoare-triple  (3s)     OK
Starting work on addressTheory
simpleSexpTheory                                                                                                                        examples/formal-languages/context-free  (5s)     OK
Starting work on simpleSexpPEGTheory
regexpTheory                                                                                                                                 examples/formal-languages/regular (17s)     OK
Starting work on temporalTheory
simpleSexpPEGTheory                                                                                                                     examples/formal-languages/context-free  (3s)     OK
Starting work on simpleSexpParseTheory
addressTheory                                                                                                                               examples/machine-code/hoare-triple  (7s)     OK
Starting work on byteTheory
temporalTheory                                                                                                                              examples/machine-code/hoare-triple  (3s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 5]                                                                                                              (20.818s) 
Starting work on libTheory
libTheory                                                                                                                                                                 misc  (3s)     OK
Starting work on ffiTheory
byteTheory                                                                                                                                                                misc  (6s)     OK
Starting work on miscTheory
ffiTheory                                                                                                                                                        semantics/ffi  (3s)     OK
Finished $(CAKEMLDIR)/semantics/ffi [#theories: 1]                                                                                                                                 (3.520s) 
Starting work on spt_closureTheory
simpleSexpParseTheory                                                                                                                   examples/formal-languages/context-free (12s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 8]                                                                                                          (42.029s) 
Starting work on multiwordTheory
spt_closureTheory                                                                                                                                          examples/algorithms  (2s)     OK
Finished $(HOLDIR)/examples/algorithms [#theories: 1]                                                                                                                              (2.291s) 
Finished $(HOLDIR)/examples/l3-machine-code/common                                                                                                                                 (0.000s) 
Starting work on ag32Theory
ag32Theory                                                                                                                                              compiler/encoders/ag32  (6s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/lib                                                                                                                                    (0.000s) 
Starting work on armTheory
multiwordTheory                                                                                                                                examples/machine-code/multiword (30s)     OK
Starting work on mc_multiwordTheory
miscTheory                                                                                                                                                                misc (36s)     OK
Starting work on cakeml-heap
cakeml-heap                                                                                                                                                               misc (11s)     OK
Finished $(CAKEMLDIR)/misc [#theories: 3]                                                                                                                                         (57.612s) 
Starting work on fpValTreeTheory
fpValTreeTheory                                                                                                                                                      semantics  (1s)     OK
Starting work on fpOptTheory
fpOptTheory                                                                                                                                                          semantics  (5s)     OK
Starting work on fpSemTheory
fpSemTheory                                                                                                                                                          semantics  (2s)     OK
Starting work on namespaceTheory
armTheory                                                                                                                                   examples/l3-machine-code/arm/model (46s)     OK
Starting work on realOpsTheory
realOpsTheory                                                                                                                                                        semantics  (1s)     OK
Starting work on tokensTheory
namespaceTheory                                                                                                                                                      semantics  (2s)     OK
Starting work on astTheory
tokensTheory                                                                                                                                                         semantics  (3s)     OK
Starting work on gramTheory
astTheory                                                                                                                                                            semantics  (8s)     OK
Starting work on semanticPrimitivesTheory
gramTheory                                                                                                                                                           semantics  (7s)     OK
Starting work on tokenUtilsTheory
mc_multiwordTheory                                                                                                                             examples/machine-code/multiword (41s)     OK
Starting work on lexer_funTheory
tokenUtilsTheory                                                                                                                                                     semantics (10s)     OK
Starting work on cmlPtreeConversionTheory
lexer_funTheory                                                                                                                                                      semantics  (9s)     OK
Starting work on mllistTheory
mllistTheory                                                                                                                                                        basis/pure (10s)     OK
Starting work on mlstringTheory
cmlPtreeConversionTheory                                                                                                                                             semantics (22s)     OK
Starting work on mloptionTheory
semanticPrimitivesTheory                                                                                                                                             semantics (48s)     OK
Starting work on evaluateTheory
mloptionTheory                                                                                                                                                      basis/pure (10s)     OK
Starting work on typeSystemTheory
mlstringTheory                                                                                                                                                      basis/pure (26s)     OK
Starting work on mlintTheory
evaluateTheory                                                                                                                                                       semantics  (5s)     OK
Starting work on astPropsTheory
balanced_mapTheory                                                                                                                                       examples/balanced_bst(166s)     OK
Starting work on osetTheory
osetTheory                                                                                                                                               examples/balanced_bst  (5s)     OK
Finished $(HOLDIR)/examples/balanced_bst [#theories: 2]                                                                                                                          (172.062s) 
Starting work on regexp_mapTheory
astPropsTheory                                                                                                                                                semantics/proofs  (9s)     OK
Starting work on mlmapTheory
regexp_mapTheory                                                                                                                             examples/formal-languages/regular  (4s)     OK
Starting work on regexp_compilerTheory
mlintTheory                                                                                                                                                         basis/pure (17s)     OK
Starting work on mlratTheory
typeSystemTheory                                                                                                                                                     semantics (24s)     OK
Starting work on primTypesTheory
mlmapTheory                                                                                                                                                         basis/pure (11s)     OK
Starting work on typeDecToPPTheory
primTypesTheory                                                                                                                                                      semantics  (2s)     OK
Starting work on semanticsTheory
semanticsTheory                                                                                                                                                      semantics  (5s)     OK
Finished $(CAKEMLDIR)/semantics [#theories: 16]                                                                                                                                  (163.313s) 
Starting work on gramPropsTheory
typeDecToPPTheory                                                                                                                                                   basis/pure  (6s)     OK
Starting work on namespacePropsTheory
mlratTheory                                                                                                                                                         basis/pure (12s)     OK
Starting work on fpOptPropsTheory
regexp_compilerTheory                                                                                                                        examples/formal-languages/regular (17s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 5]                                                                                                               (49.631s) 
Starting work on mlvectorTheory
namespacePropsTheory                                                                                                                                          semantics/proofs (13s)     OK
Starting work on semanticPrimitivesPropsTheory
fpOptPropsTheory                                                                                                                                              semantics/proofs (13s)     OK
Starting work on fpSemPropsTheory
mlvectorTheory                                                                                                                                                      basis/pure (16s)     OK
Starting work on mlprettyprinterTheory
gramPropsTheory                                                                                                                                               semantics/proofs (23s)     OK
Starting work on typeSoundInvariantsTheory
mlprettyprinterTheory                                                                                                                                               basis/pure (16s)     OK
Finished $(CAKEMLDIR)/basis/pure [#theories: 9]                                                                                                                                  (128.426s) 
Starting work on cmlPEGTheory
typeSoundInvariantsTheory                                                                                                                                     semantics/proofs (12s)     OK
Starting work on fromSexpTheory
semanticPrimitivesPropsTheory                                                                                                                                 semantics/proofs (58s)     OK
Starting work on typeSysPropsTheory
typeSysPropsTheory                                                                                                                                            semantics/proofs (32s)     OK
Starting work on primSemEnvTheory
cmlPEGTheory                                                                                                                                                  compiler/parsing (72s)     OK
Starting work on weakeningTheory
weakeningTheory                                                                                                                                               semantics/proofs (14s)     OK
Starting work on cmlParseTheory
primSemEnvTheory                                                                                                                                              semantics/proofs (16s)     OK
Starting work on lexer_implTheory
fromSexpTheory                                                                                                                                                compiler/parsing (88s)     OK
Starting work on cfFFITypeTheory
fpSemPropsTheory                                                                                                                                              semantics/proofs(113s)     OK
Starting work on evaluatePropsTheory
cmlParseTheory                                                                                                                                                compiler/parsing  (7s)     OK
Starting work on ml_monadBaseTheory
cfFFITypeTheory                                                                                                                                                 characteristic (14s)     OK
Starting work on MarshallingTheory
MarshallingTheory                                                                                                                                                        basis (11s)     OK
Finished $(HOLDIR)/examples/machine-code/multiword [#theories: 2]                                                                                                                 (72.484s) 
Starting work on pattern_commonTheory
ml_monadBaseTheory                                                                                                                               translator/monadic/monad_base (23s)     OK
Finished $(CAKEMLDIR)/translator/monadic/monad_base [#theories: 1]                                                                                                                (23.658s) 
Starting work on reg_allocTheory
pattern_commonTheory                                                                                                                         compiler/backend/pattern_matching  (9s)     OK
Starting work on pattern_semanticsTheory
lexer_implTheory                                                                                                                                              compiler/parsing (50s)     OK
Finished $(CAKEMLDIR)/compiler/parsing [#theories: 4]                                                                                                                            (218.449s) 
Starting work on parmoveTheory
pattern_semanticsTheory                                                                                                                      compiler/backend/pattern_matching (13s)     OK
Starting work on pattern_compTheory
pattern_compTheory                                                                                                                           compiler/backend/pattern_matching (16s)     OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3]                                                                                                            (38.846s) 
Starting work on asmTheory
parmoveTheory                                                                                                                                       compiler/backend/reg_alloc (25s)     OK
Starting work on backend_commonTheory
asmTheory                                                                                                                                                compiler/encoders/asm (11s)     OK
Starting work on asmSemTheory
backend_commonTheory                                                                                                                                          compiler/backend (14s)     OK
Starting work on closLangTheory
reg_allocTheory                                                                                                                                     compiler/backend/reg_alloc (61s)     OK
Starting work on linear_scanTheory
asmSemTheory                                                                                                                                             compiler/encoders/asm (14s)     OK
Starting work on asmPropsTheory
evaluatePropsTheory                                                                                                                                           semantics/proofs(101s)     OK
Starting work on typeSoundTheory
closLangTheory                                                                                                                                                compiler/backend (16s)     OK
Starting work on ml_progTheory
asmPropsTheory                                                                                                                                           compiler/encoders/asm (12s)FAIL<1>
 <<HOL message: Defined type: "target">>
 Saved definition ____ "target_state_rel_def"
 Saved definition ____ "target_ok_def"
 Saved definition ____ "interference_ok_def"
 Initial goal:
 
 R. WF R  a k v2. R (SUC v2  2 ** k,a + n2w (2 ** k),k) (SUC v2,a,k)
 error in quse /home/cug/hk324/cml-regression/cakeml-2146/compiler/encoders/asm/asmPropsScript.sml : HOL_ERR {message = "\nUnable to prove termination!\n\nTry using \"TotalDefn.tDefine <name> <quotation> <tac>\".\n", origin_function = "defnDefine", origin_structure = "TotalDefn"}
 error in load /home/cug/hk324/cml-regression/cakeml-2146/compiler/encoders/asm/asmPropsScript : HOL_ERR {message = "\nUnable to prove termination!\n\nTry using \"TotalDefn.tDefine <name> <quotation> <tac>\".\n", origin_function = "defnDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "\nUnable to prove termination!\n\nTry using \"TotalDefn.tDefine <name> <quotation> <tac>\".\n", origin_function = "defnDefine", origin_structure = "TotalDefn"}
linear_scanTheory                                                                                                                                   compiler/backend/reg_alloc (18s)MKILLED
typeSoundTheory                                                                                                                                               semantics/proofs  (7s)MKILLED
ml_progTheory                                                                                                                                                       translator  (2s)MKILLED