Job 1825

CakeML:28887651686effa00fe898332ae96d47ac3b21a9
  Merge pull request #867 from CakeML/array-fixed [Mar 16 07:52:53]
HOL:60adf92493ffff8c7ecacfd628f628af5c35f305
  Make some more arithmetic theorems (mostly about EXP) automatic [Mar 11 07:25:58]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Mar 16 07:53:34 Claimed job
Mar 16 07:53:38 Building HOL
Mar 16 08:02:55 Starting developers
Mar 16 08:02:55 Finished developers                                               0s  36MB
Mar 16 08:02:56 Starting developers/bin
Mar 16 08:03:43 Finished developers/bin                                          47s   1GB
Mar 16 08:03:43 Starting semantics/ffi
Mar 16 08:03:53 Finished semantics/ffi                                            9s 276MB
Mar 16 08:03:53 Starting semantics
Mar 16 08:06:03 Finished semantics                                             2m09s   1GB
Mar 16 08:06:03 Starting semantics/proofs
Mar 16 08:09:57 Finished semantics/proofs                                      3m53s   2GB
Mar 16 08:09:57 Starting semantics/alt_semantics
Mar 16 08:10:13 Finished semantics/alt_semantics                                 15s 541MB
Mar 16 08:10:13 Starting semantics/alt_semantics/proofs
Mar 16 08:12:35 Finished semantics/alt_semantics/proofs                        2m21s   2GB
Mar 16 08:12:35 Starting basis/pure
Mar 16 08:15:40 Finished basis/pure                                            3m04s   1GB
Mar 16 08:15:40 Starting translator
Mar 16 08:16:29 FAILED: translator
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)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 23 directories
Finished $(CAKEMLDIR)/misc                                                                                                                                                  (0.000s) 
Starting work on ml_progTheory
ml_progTheory                                                                                                                                                translator (21s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory                                                                                                                                          translator (23s)FAIL<1>
 
 dimindex (:)  k  n' < dimword (:) 
 (n * 2 ** (k  dimindex (:)) +
  (2 ** k  (n' * 2 ** (k  dimindex (:))) MOD 2 ** k) MOD 2 ** k) MOD 2 ** k =
 ((n + dimword (:)  n') * 2 ** (k  dimindex (:))) MOD 2 ** k
 
 failed.
 error in quse /home/myreen/regression/cakeml-1825/translator/ml_translatorScript.sml : HOL_ERR {message = "functions on lhs and rhs differ", origin_function = "AP_TERM_TAC", origin_structure = "Tactic"}
 error in load /home/myreen/regression/cakeml-1825/translator/ml_translatorScript : HOL_ERR {message = "functions on lhs and rhs differ", origin_function = "AP_TERM_TAC", origin_structure = "Tactic"}
 Uncaught exception: HOL_ERR {message = "functions on lhs and rhs differ", origin_function = "AP_TERM_TAC", origin_structure = "Tactic"}