Job 2622

CakeML:cbad3080ab75bc72ce4ab37402cdfb36a8cd55e0
  Remove remaining _ = Define ... manually [Sep 28 07:58:40]
#1059 (new-define-_)
Merging into:06d5cf707aca7e50703c7e8b43e3a02dc37253e2
  Merge pull request #1058 from CakeML/dafny-ir-update [Sep 28 06:33:16]
HOL:72a01e7935ee7175f22527332d54ac58085668ed
  Add more primitive proof rules [Sep 23 23:08:36]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Sep 28 17:58:08 Claimed job
Sep 28 17:58:14 Building HOL
Sep 28 18:12:00 Starting developers
Sep 28 18:12:06 Finished developers                                               5s 173MB
Sep 28 18:12:06 Starting developers/bin
Sep 28 18:12:12 Finished developers/bin                                           5s   1GB
Sep 28 18:12:12 Starting compiler/proofs
Sep 28 20:10:57 Finished compiler/proofs                                    1h58m44s  14GB
Sep 28 20:10:57 Starting compiler/bootstrap/translation
Sep 29 05:09:49 Finished compiler/bootstrap/translation                     8h58m52s  37GB
Sep 29 05:09:49 Starting semantics/ffi
Sep 29 05:09:55 Finished semantics/ffi                                            5s 420MB
Sep 29 05:09:55 Starting semantics
Sep 29 05:09:56 Finished semantics                                                1s  18MB
Sep 29 05:09:56 Starting semantics/proofs
Sep 29 05:10:22 Finished semantics/proofs                                        25s 434MB
Sep 29 05:10:22 Starting semantics/alt_semantics
Sep 29 05:10:45 Finished semantics/alt_semantics                                 22s 524MB
Sep 29 05:10:45 Starting semantics/alt_semantics/proofs
Sep 29 05:11:13 FAILED: semantics/alt_semantics/proofs
Scanning [1m$(HOLDIR)/src/bag[0m
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)/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)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 20 directories
Starting work on README.md
Starting work on determTheory
Starting work on bigSmallInvariantsTheory
Starting work on bigStepPropsTheory
README.md                                                                                                   (0s)     OK
bigSmallInvariantsTheory                                                                                    (3s)     OK
determTheory                                                                                               (25s)FAIL<1>
 Saved theorem _______ "RTC_decl_step_confl"
 Saved theorem _______ "RTC_decl_step_determ"
 error in quse /home/cug/hk324/cml-regression/cakeml-2622/semantics/alt_semantics/proofs/determScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-2622/semantics/alt_semantics/proofs/determScript : Fail "Static Errors"
 Saved definition ____ "Rerr_to_decl_step_result_def"
 /home/cug/hk324/cml-regression/cakeml-2622/semantics/alt_semantics/proofs/determScript.sml:162: error: Value or constructor (small_eval_dec_def) has not been declared
 Found near [small_eval_dec_def]
 /home/cug/hk324/cml-regression/cakeml-2622/semantics/alt_semantics/proofs/determScript.sml:163: error: Value or constructor (small_eval_dec_def) has not been declared
 Found near [small_eval_dec_def, EXISTS_PROD]
 Uncaught exception at ./basis/FinalPolyML.sml:491: Fail "Static Errors"
bigStepPropsTheory                                                                                         (25s)MKILLED