Job 324

CakeML:1337e803f1a56b2cfa209982d510332e3e14999d
  Correct proof failure caused by change to irule in HOL [May 29 01:48:22]
HOL:1c2f967871ae1f61f75a30d037a4100413700554
  Fix pretty-printing bug for large-if-exprs in rator position [May 28 08:02:00]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

May 29 02:55:42 Claimed job
May 29 02:55:52 Building HOL
May 29 03:07:15 Starting developers/bin
May 29 03:07:26 Finished developers/bin                                           8s 224MB
May 29 03:07:28 Starting semantics/ffi
May 29 03:08:27 Finished semantics/ffi                                           57s 273MB
May 29 03:08:29 Starting semantics
May 29 03:10:52 Finished semantics                                             2m20s 958MB
May 29 03:10:54 Starting semantics/proofs
May 29 03:12:47 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ../../misc]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../misc]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developersWorking in ../../developers
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../misc]0;Holmake: ../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../ffi]0;Holmake: ../ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/semantics/proofs
Starting work on heap
heap                                                                                            OK
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
astPropsTheory                                                                                  OK
typeSoundInvariantsTheory                                                                       OK
gramPropsTheory                                                                                 OK
Starting work on cmlPtreeConversionPropsTheory
semanticPrimitivesPropsTheory                                                                   OK
Starting work on evaluatePropsTheory
Starting work on primSemEnvTheory
Starting work on typeSysPropsTheory
primSemEnvTheory                                                                                OK
cmlPtreeConversionPropsTheory                                                                   OK
typeSysPropsTheory                                                                              OK
Starting work on weakeningTheory
evaluatePropsTheory                                                                             OK
weakeningTheory                                                                        FAILED! <1>
 uniq mn decls tenv ds decls' tenv'.
     type_ds uniq mn decls tenv ds decls' tenv' 
     decls'' tenv''.
         (uniq  F)  weak_decls decls'' decls 
         weak_decls_other_mods mn decls'' decls  tenv_ok tenv'' 
         weak tenv'' tenv 
         type_ds F mn decls'' tenv'' ds decls' tenv'
 
 failed.
 Failed to prove theorem type_ds_weakening.