Job 1688

CakeML:d064a0d14db09e9f35c32cecf26c59e2ba46820c
  Insert a pointer to source_eval in a comment [Dec 17 13:05:23]
#850 (eval)
Merging into:ac6dd83f48ab211455fb85c60d3e20e212dc7b8a
  Remove some primes [Dec 12 21:27:55]
HOL:9511d2021f824ef967db312f1d1a41c58dbf7acb
  Fix a proof in face of automatic simp change in affbde85bd8 [Dec 16 05:35:31]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 17 15:45:02 Claimed job
Dec 17 15:45:08 Reusing HOL
Dec 17 15:45:46 Starting developers
Dec 17 15:45:51 Finished developers                                               4s 131MB
Dec 17 15:45:51 Starting developers/bin
Dec 17 15:45:57 Finished developers/bin                                           5s 670MB
Dec 17 15:45:57 Starting semantics/ffi
Dec 17 15:46:06 Finished semantics/ffi                                            8s 228MB
Dec 17 15:46:06 Starting semantics
Dec 17 15:47:42 Finished semantics                                             1m36s   1GB
Dec 17 15:47:42 Starting semantics/proofs
Dec 17 15:51:31 Finished semantics/proofs                                      3m48s   1GB
Dec 17 15:51:31 Starting semantics/alt_semantics
Dec 17 15:51:43 Finished semantics/alt_semantics                                 11s 399MB
Dec 17 15:51:43 Starting semantics/alt_semantics/proofs
Dec 17 15:54:19 Finished semantics/alt_semantics/proofs                        2m35s 807MB
Dec 17 15:54:19 Starting basis/pure
Dec 17 15:57:31 Finished basis/pure                                            3m11s 761MB
Dec 17 15:57:31 Starting translator
Dec 17 16:00:11 FAILED: translator
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Finished $(CAKEMLDIR)/misc                                             (0.000s) 
Starting work on README.md
Starting work on ml_progTheory
README.md                                               translator  (0s)     OK
ml_progTheory                                           translator (16s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory                                     translator (38s)     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_optimiseTheory                                       translator (15s)     OK
ml_pmatchTheory                                         translator (16s)     OK
Starting work on decProgTheory
Starting work on ml_module_demoTheory
Starting work on ml_pmatch_demoTheory
Starting work on ml_translator_demoTheory
ml_translator_demoTheory                                translator (12s)     OK
Starting work on ml_translator_testTheory
ml_module_demoTheory                                    translator (14s)     OK
ml_translator_testTheory                                translator (63s)     OK
decProgTheory                                           translator (81s)FAIL<1>
 Saved theorem _______ "FPSEM_FP_UOP_TYPE_eq_enc"
 Saved theorem _______ "FPSEM_FP_BOP_TYPE_eq_enc"
 Saved theorem _______ "FPSEM_FP_TOP_TYPE_eq_enc"
 Saved theorem _______ "FPSEM_FP_CMP_TYPE_eq_enc"
 error in quse /home/cake/oven/regression/cakeml-1688/translator/decProgScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1688/translator/decProgScript : Fail "Static Errors"
 Saved theorem _______ "AST_OP_TYPE_eq_enc"
 /home/cake/oven/regression/cakeml-1688/translator/decProgScript.sml:184: error: Value or constructor (enc_locn_def) has not been declared
 Found near [LOCATION_LOCN_TYPE_def, enc_locn_def, type_num_defs]
 Uncaught exception: Fail "Static Errors"
ml_pmatch_demoTheory                                    translator (82s)MKILLED