Overview

Job 1825

CakeML:28887651686effa00fe898332ae96d47ac3b21a9
  Merge pull request #867 from CakeML/array-fixed
HOL:60adf92493ffff8c7ecacfd628f628af5c35f305
  Make some more arithmetic theorems (mostly about EXP) automatic
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               0s  36MB
 Starting developers/bin
 Finished developers/bin                                          47s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                            9s 276MB
 Starting semantics
 Finished semantics                                             2m09s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m53s   2GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 15s 541MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m21s   2GB
 Starting basis/pure
 Finished basis/pure                                            3m04s   1GB
 Starting translator
 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"}