Overview

Job 1988

CakeML:4cd953474ce72ae40ffdbb303741a04124d4fb2a
  prove word_to_word_compile_semantics
#909 (word_to_word_Pancake)
Merging into:5124cba7723d5cf97e6dad4abef67f2f91257971
  Remove now-redundant calls to diminish_srw_ss
HOL:893dead4b6f59a9be7fc251533d0a5ee77e12e56
  Add some simple test for bitArithLib and document in next-release.md
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               0s  37MB
 Starting developers/bin
 Finished developers/bin                                           6s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                            8s 273MB
 Starting semantics
 Finished semantics                                             2m33s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      6m48s   2GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 25s 567MB
 Starting semantics/alt_semantics/proofs
 FAILED: semantics/alt_semantics/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/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/formal-languages/context-free[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)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 20 directories
Starting work on determTheory
Starting work on bigSmallInvariantsTheory
Starting work on bigStepPropsTheory
bigSmallInvariantsTheory                                                                                            (4s)     OK
determTheory                                                                                                       (30s)     OK
Starting work on bigClockTheory
Starting work on smallStepPropsTheory
bigStepPropsTheory                                                                                                 (62s)     OK
bigClockTheory                                                                                                    (111s)     OK
Starting work on interpTheory
interpTheory                                                                                                       (22s)     OK
Starting work on funBigStepEquivTheory
funBigStepEquivTheory                                                                                              (32s)     OK
smallStepPropsTheory                                                                                              (287s)FAIL<1>
 Saved theorem _______ "small_eval_match_cases"
 Saved definition ____ "alt_small_eval_def"
 Saved induction _____ "alt_small_eval_ind"
 Saved theorem _______ "small_eval_match_thm"
 Saved theorem _______ "small_eval_opapp_err"
 Saved theorem _______ "small_eval_app_err"
 Saved theorem _______ "small_eval_app_err_more"
 error in quse /home/myreen/regression/cakeml-1988/semantics/alt_semantics/proofs/smallStepPropsScript.sml : UNCHANGED
 error in load /home/myreen/regression/cakeml-1988/semantics/alt_semantics/proofs/smallStepPropsScript : UNCHANGED
 Uncaught exception: UNCHANGED