Job 1787

CakeML:2894b0315f5585f5267c0f7b6bd3b54ddb2166e1
  Attempt a minimal fix to the translator [Feb 21 22:06:09]
HOL:b2236d1e8f18d389921766fcda06075975394e9f
  Fix ZIP_ind test case [Feb 23 03:12:26]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 23 09:46:55 Claimed job
Feb 23 09:47:00 Building HOL
Feb 23 09:56:26 Starting developers
Feb 23 09:56:30 Finished developers                                               4s 125MB
Feb 23 09:56:30 Starting developers/bin
Feb 23 09:56:35 Finished developers/bin                                           4s 675MB
Feb 23 09:56:35 Starting semantics/ffi
Feb 23 09:56:44 Finished semantics/ffi                                            9s 245MB
Feb 23 09:56:45 Starting semantics
Feb 23 09:58:59 Finished semantics                                             2m14s   1GB
Feb 23 09:58:59 Starting semantics/proofs
Feb 23 10:02:38 Finished semantics/proofs                                      3m39s   1GB
Feb 23 10:02:38 Starting semantics/alt_semantics
Feb 23 10:02:55 Finished semantics/alt_semantics                                 16s 513MB
Feb 23 10:02:55 Starting semantics/alt_semantics/proofs
Feb 23 10:05:25 Finished semantics/alt_semantics/proofs                        2m29s   1GB
Feb 23 10:05:25 Starting basis/pure
Feb 23 10:08:20 Finished basis/pure                                            2m53s 861MB
Feb 23 10:08:20 Starting translator
Feb 23 10:11:23 Finished translator                                            3m02s   1GB
Feb 23 10:11:23 Starting compiler/parsing
Feb 23 10:12:38 Finished compiler/parsing                                      1m15s   2GB
Feb 23 10:12:38 Starting characteristic
Feb 23 10:19:05 Finished characteristic                                        6m26s   1GB
Feb 23 10:19:05 Starting translator/monadic
Feb 23 10:21:02 Finished translator/monadic                                    1m57s   1GB
Feb 23 10:21:02 Starting basis
Feb 23 10:22:37 FAILED: basis
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)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanned 28 directories
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md                                                                                                                                                                         (0s)     OK
Starting work on runtimeFFITheory
MarshallingTheory                                                                                                                                                                (11s)     OK
Starting work on fsFFITheory
runtimeFFITheory                                                                                                                                                                 (12s)     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                                                                                       (0s)     OK
clFFITheory                                                                                                                                                                      (14s)     OK
RuntimeProgTheory                                                                                                                                                                (27s)     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                                                                                                                      (22s)     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                                                                                                                 (17s)     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                                                                                                                               (27s)     OK
fsFFIPropsTheory                                                                                                                                                                 (55s)     OK
ListProgTheory                                                                                                                                                                   (44s)FAIL<1>
 Updating front_v_thm
 Saved theorem _______ "front_v_thm"
 Updating last_v_thm
 Saved theorem _______ "last_v_thm"
 Updating nth_v_thm
 Saved theorem _______ "nth_v_thm"
 Failed translation: !
 error in quse /home/cug/hk324/cml-regression/cakeml-1787/basis/ListProgScript.sml : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
 error in load /home/cug/hk324/cml-regression/cakeml-1787/basis/ListProgScript : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
 Uncaught exception: HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}