Job 1767

CakeML:58ece1432c25bfca39de8a22e87decc09bc3516b
  Merge pull request #860 from arolle/cyclicity-check-rebase [Feb 11 10:57:07]
HOL:7d8123fd0cb1e8c2b7e3fffb337516da7cb7c9df
  Reinstate sptreeTheory.lrnext_def, which 8247e5e3a465 had deleted [Feb 10 23:16:16]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 11 11:15:04 Claimed job
Feb 11 11:15:16 Building HOL
Feb 11 11:25:15 Starting developers
Feb 11 11:25:20 Finished developers                                               4s 106MB
Feb 11 11:25:20 Starting developers/bin
Feb 11 11:25:26 Finished developers/bin                                           5s 670MB
Feb 11 11:25:26 Starting semantics/ffi
Feb 11 11:25:37 Finished semantics/ffi                                           10s 199MB
Feb 11 11:25:37 Starting semantics
Feb 11 11:27:17 Finished semantics                                             1m40s   1GB
Feb 11 11:27:18 Starting semantics/proofs
Feb 11 11:31:11 Finished semantics/proofs                                      3m53s   1GB
Feb 11 11:31:11 Starting semantics/alt_semantics
Feb 11 11:31:24 Finished semantics/alt_semantics                                 13s 407MB
Feb 11 11:31:25 Starting semantics/alt_semantics/proofs
Feb 11 11:34:05 Finished semantics/alt_semantics/proofs                        2m40s 845MB
Feb 11 11:34:05 Starting basis/pure
Feb 11 11:37:09 Finished basis/pure                                            3m03s 686MB
Feb 11 11:37:09 Starting translator
Feb 11 11:40:15 Finished translator                                            3m05s   1GB
Feb 11 11:40:15 Starting compiler/parsing
Feb 11 11:41:38 Finished compiler/parsing                                      1m22s   2GB
Feb 11 11:41:38 Starting characteristic
Feb 11 11:47:46 Finished characteristic                                        6m07s   1GB
Feb 11 11:47:46 Starting translator/monadic
Feb 11 11:49:39 Finished translator/monadic                                    1m52s   1GB
Feb 11 11:49:39 Starting basis
Feb 11 12:39:22 Finished basis                                                49m41s  21GB
Feb 11 12:39:22 Starting compiler/inference
Feb 11 12:40:42 Finished compiler/inference                                    1m19s   1GB
Feb 11 12:40:42 Starting compiler/backend/reg_alloc
Feb 11 12:41:54 Finished compiler/backend/reg_alloc                            1m11s   1GB
Feb 11 12:41:54 Starting compiler/backend/gc
Feb 11 12:45:57 Finished compiler/backend/gc                                   4m02s   1GB
Feb 11 12:45:57 Starting compiler/backend
Feb 11 12:51:32 Finished compiler/backend                                      5m35s   2GB
Feb 11 12:51:32 Starting compiler/encoders/asm
Feb 11 12:51:58 Finished compiler/encoders/asm                                   25s 696MB
Feb 11 12:51:58 Starting compiler/encoders/x64
Feb 11 12:53:05 Finished compiler/encoders/x64                                 1m07s 643MB
Feb 11 12:53:06 Starting compiler/encoders/arm7
Feb 11 12:55:19 Finished compiler/encoders/arm7                                2m13s   1GB
Feb 11 12:55:19 Starting compiler/encoders/arm8
Feb 11 12:56:01 Finished compiler/encoders/arm8                                  41s 944MB
Feb 11 12:56:01 Starting compiler/encoders/arm8_asl
Feb 11 14:30:24 Finished compiler/encoders/arm8_asl                         1h34m22s  34GB
Feb 11 14:30:25 Starting compiler/encoders/mips
Feb 11 14:32:05 Finished compiler/encoders/mips                                1m39s   1GB
Feb 11 14:32:05 Starting compiler/encoders/riscv
Feb 11 14:34:03 Finished compiler/encoders/riscv                               1m58s 879MB
Feb 11 14:34:03 Starting compiler/encoders/ag32
Feb 11 14:34:24 Finished compiler/encoders/ag32                                  20s 608MB
Feb 11 14:34:25 Starting compiler/backend/x64
Feb 11 14:34:48 Finished compiler/backend/x64                                    22s   1GB
Feb 11 14:34:48 Starting compiler/backend/arm7
Feb 11 14:35:10 Finished compiler/backend/arm7                                   22s   1GB
Feb 11 14:35:10 Starting compiler/backend/arm8
Feb 11 14:35:34 Finished compiler/backend/arm8                                   23s   1GB
Feb 11 14:35:34 Starting compiler/backend/mips
Feb 11 14:35:57 Finished compiler/backend/mips                                   22s   1GB
Feb 11 14:35:57 Starting compiler/backend/riscv
Feb 11 14:36:20 Finished compiler/backend/riscv                                  23s   1GB
Feb 11 14:36:21 Starting compiler/backend/ag32
Feb 11 14:37:35 Finished compiler/backend/ag32                                 1m14s   1GB
Feb 11 14:37:36 Starting compiler/parsing/proofs
Feb 11 14:41:40 Finished compiler/parsing/proofs                               4m04s   1GB
Feb 11 14:41:40 Starting compiler/inference/proofs
Feb 11 14:44:20 Finished compiler/inference/proofs                             2m39s   1GB
Feb 11 14:44:20 Starting compiler/backend/semantics
Feb 11 15:15:55 Finished compiler/backend/semantics                           31m34s   2GB
Feb 11 15:15:56 Starting compiler/backend/reg_alloc/proofs
Feb 11 15:19:46 Finished compiler/backend/reg_alloc/proofs                     3m49s 961MB
Feb 11 15:19:46 Starting compiler/backend/proofs
Feb 11 16:19:00 Finished compiler/backend/proofs                              59m12s  14GB
Feb 11 16:19:01 Starting compiler/backend/serialiser
Feb 11 16:20:32 Finished compiler/backend/serialiser                           1m30s   1GB
Feb 11 16:20:32 Starting compiler/encoders/x64/proofs
Feb 11 16:30:51 Finished compiler/encoders/x64/proofs                         10m19s   5GB
Feb 11 16:30:52 Starting compiler/encoders/arm7/proofs
Feb 11 16:45:03 Finished compiler/encoders/arm7/proofs                        14m10s   4GB
Feb 11 16:45:03 Starting compiler/encoders/arm8/proofs
Feb 11 16:52:25 Finished compiler/encoders/arm8/proofs                         7m22s   1GB
Feb 11 16:52:25 Starting compiler/encoders/arm8_asl/proofs
Feb 11 17:46:23 Finished compiler/encoders/arm8_asl/proofs                    53m56s   5GB
Feb 11 17:46:24 Starting compiler/encoders/mips/proofs
Feb 11 17:56:58 Finished compiler/encoders/mips/proofs                        10m34s   2GB
Feb 11 17:56:58 Starting compiler/encoders/riscv/proofs
Feb 11 18:06:31 Finished compiler/encoders/riscv/proofs                        9m32s   1GB
Feb 11 18:06:32 Starting compiler/encoders/ag32/proofs
Feb 11 18:09:21 Finished compiler/encoders/ag32/proofs                         2m48s 739MB
Feb 11 18:09:21 Starting compiler/backend/x64/proofs
Feb 11 18:09:49 Finished compiler/backend/x64/proofs                             28s   1GB
Feb 11 18:09:50 Starting compiler/backend/arm7/proofs
Feb 11 18:10:19 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 11 18:10:19 Starting compiler/backend/arm8/proofs
Feb 11 18:10:47 Finished compiler/backend/arm8/proofs                            28s   1GB
Feb 11 18:10:47 Starting compiler/backend/arm8_asl
Feb 11 18:11:11 Finished compiler/backend/arm8_asl                               23s   1GB
Feb 11 18:11:12 Starting compiler/backend/mips/proofs
Feb 11 18:11:41 Finished compiler/backend/mips/proofs                            29s   1GB
Feb 11 18:11:41 Starting compiler/backend/riscv/proofs
Feb 11 18:12:10 Finished compiler/backend/riscv/proofs                           28s   1GB
Feb 11 18:12:10 Starting compiler/backend/ag32/proofs
Feb 11 18:26:20 Finished compiler/backend/ag32/proofs                         14m09s   2GB
Feb 11 18:26:20 Starting compiler/proofs
Feb 11 18:28:36 Finished compiler/proofs                                       2m15s   3GB
Feb 11 18:28:37 Starting candle/set-theory
Feb 11 18:29:07 Finished candle/set-theory                                       30s 885MB
Feb 11 18:29:07 Starting candle/syntax-lib
Feb 11 18:29:20 Finished candle/syntax-lib                                       12s 455MB
Feb 11 18:29:20 Starting candle/standard/syntax
Feb 11 18:31:14 Finished candle/standard/syntax                                1m54s 860MB
Feb 11 18:31:14 Starting candle/standard/semantics
Feb 11 18:33:06 Finished candle/standard/semantics                             1m52s   1GB
Feb 11 18:33:07 Starting candle/standard/monadic
Feb 11 18:34:52 Finished candle/standard/monadic                               1m44s   1GB
Feb 11 18:34:52 Starting candle/standard/ml_kernel
Feb 11 18:42:06 Finished candle/standard/ml_kernel                             7m13s   3GB
Feb 11 18:42:06 Starting candle/overloading/syntax
Feb 11 18:45:28 Finished candle/overloading/syntax                             3m21s   1GB
Feb 11 18:45:28 Starting candle/overloading/semantics
Feb 11 18:58:06 Finished candle/overloading/semantics                         12m37s   2GB
Feb 11 18:58:06 Starting candle/overloading/monadic
Feb 11 19:00:32 Finished candle/overloading/monadic                            2m26s   1GB
Feb 11 19:00:32 Starting candle/overloading/ml_kernel
Feb 11 19:08:48 Finished candle/overloading/ml_kernel                          8m15s   3GB
Feb 11 19:08:48 Starting candle/overloading/ml_checker
Feb 11 19:11:21 Finished candle/overloading/ml_checker                         2m32s   3GB
Feb 11 19:11:21 Starting candle/prover
Feb 11 19:19:22 Finished candle/prover                                         8m01s   3GB
Feb 11 19:19:23 Starting pancake
Feb 11 19:22:16 Finished pancake                                               2m52s   2GB
Feb 11 19:22:16 Starting pancake/ffi
Feb 11 19:22:17 Finished pancake/ffi                                              0s  23MB
Feb 11 19:22:17 Starting pancake/semantics
Feb 11 19:24:57 Finished pancake/semantics                                     2m40s   1GB
Feb 11 19:24:57 Starting pancake/proofs
Feb 11 19:37:58 Finished pancake/proofs                                       13m00s   6GB
Feb 11 19:37:58 Starting characteristic/examples
Feb 11 19:39:27 Finished characteristic/examples                               1m28s   2GB
Feb 11 19:39:27 Starting tutorial/solutions
Feb 11 19:56:43 Finished tutorial/solutions                                   17m15s  10GB
Feb 11 19:56:43 Starting translator/monadic/examples
Feb 11 20:00:20 Finished translator/monadic/examples                           3m36s   2GB
Feb 11 20:00:21 Starting examples
Feb 11 20:10:58 Finished examples                                             10m37s   3GB
Feb 11 20:10:58 Starting examples/compilation/x64
Feb 11 22:44:43 Finished examples/compilation/x64                           2h33m44s  18GB
Feb 11 22:44:43 Starting examples/compilation/x64/proofs
Feb 11 22:47:20 Finished examples/compilation/x64/proofs                       2m36s   3GB
Feb 11 22:47:20 Starting examples/compilation/ag32
Feb 11 23:23:35 Finished examples/compilation/ag32                            36m14s  10GB
Feb 11 23:23:35 Starting examples/compilation/ag32/proofs
Feb 11 23:24:32 Finished examples/compilation/ag32/proofs                        56s   3GB
Feb 11 23:24:32 Starting examples/cost
Feb 12 00:26:16 Finished examples/cost                                      1h01m43s   9GB
Feb 12 00:26:16 Starting examples/lpr_checker
Feb 12 00:27:10 Finished examples/lpr_checker                                    54s 979MB
Feb 12 00:27:10 Starting examples/lpr_checker/array
Feb 12 00:58:28 Finished examples/lpr_checker/array                           31m17s   5GB
Feb 12 00:58:28 Starting examples/lpr_checker/array/compilation
Feb 12 02:26:47 Finished examples/lpr_checker/array/compilation             1h28m18s  54GB
Feb 12 02:26:48 Starting examples/lpr_checker/array/compilation/proofs
Feb 12 02:28:15 Finished examples/lpr_checker/array/compilation/proofs         1m27s   7GB
Feb 12 02:28:15 Starting examples/opentheory
Feb 12 02:38:51 Finished examples/opentheory                                  10m35s   6GB
Feb 12 02:38:51 Starting examples/opentheory
Feb 12 02:38:53 Finished examples/opentheory                                      1s  28MB
Feb 12 02:38:53 Starting examples/opentheory/compilation
Feb 12 03:20:34 Finished examples/opentheory/compilation                      41m40s  29GB
Feb 12 03:20:34 Starting examples/opentheory/compilation/proofs
Feb 12 03:21:54 Finished examples/opentheory/compilation/proofs                1m19s   3GB
Feb 12 03:21:54 Starting examples/opentheory/compilation/ag32
Feb 12 04:03:34 Finished examples/opentheory/compilation/ag32                 41m39s  25GB
Feb 12 04:03:34 Starting examples/opentheory/compilation/ag32/proofs
Feb 12 04:05:33 Finished examples/opentheory/compilation/ag32/proofs           1m59s   6GB
Feb 12 04:05:33 Starting examples/sat_encodings
Feb 12 04:07:40 Finished examples/sat_encodings                                2m06s 773MB
Feb 12 04:07:40 Starting examples/sat_encodings/case_studies
Feb 12 04:09:31 Finished examples/sat_encodings/case_studies                   1m50s 859MB
Feb 12 04:09:31 Starting examples/sat_encodings/translation
Feb 12 04:15:37 Finished examples/sat_encodings/translation                    6m05s   4GB
Feb 12 04:15:37 Starting examples/sat_encodings/translation/compilation
Feb 12 05:10:24 Finished examples/sat_encodings/translation/compilation       54m43s  18GB
Feb 12 05:10:25 Starting translator/okasaki-examples
Feb 12 05:15:24 Finished translator/okasaki-examples                           4m59s   1GB
Feb 12 05:15:24 Starting translator/other-examples
Feb 12 05:17:29 Finished translator/other-examples                             2m04s   1GB
Feb 12 05:17:29 Starting compiler/parsing/tests
Feb 12 05:18:00 Finished compiler/parsing/tests                                  30s 640MB
Feb 12 05:18:00 Starting compiler/inference/tests
Feb 12 05:26:20 Finished compiler/inference/tests                              8m19s   6GB
Feb 12 05:26:20 Starting compiler/bootstrap/translation
Feb 12 06:26:28 FAILED: compiler/bootstrap/translation
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/machine-code/hoare-triple
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanned 77 directories
Starting work on monadic_encTheory
Starting work on README.md
Starting work on to_flatProgTheory
README.md                           compiler/bootstrap/translation  (0s)     OK
monadic_encTheory                    compiler/encoders/monadic_enc (12s)     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                  compiler/encoders/monadic_enc (16s)     OK
monadic_enc64Theory                  compiler/encoders/monadic_enc (16s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]    (44.838s) 
to_flatProgTheory                   compiler/bootstrap/translation(285s)     OK
Starting work on to_closProgTheory
to_closProgTheory                   compiler/bootstrap/translation(445s)     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                    compiler/bootstrap/translation(414s)     OK
Starting work on to_bviProgTheory
to_bviProgTheory                    compiler/bootstrap/translation(337s)     OK
Starting work on to_dataProgTheory
to_dataProgTheory                   compiler/bootstrap/translation(199s)     OK
Starting work on lexerProgTheory
lexerProgTheory                     compiler/bootstrap/translation(178s)     OK
Starting work on parserProgTheory
parserProgTheory                    compiler/bootstrap/translation(505s)     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                 compiler/bootstrap/translation (17m)     OK
Starting work on inferProgTheory
inferProgTheory                     compiler/bootstrap/translation(112s)FAIL<1>
 Saved theorem _______ "recordtypeinf_envseldefinf_c_fupd_v_thm"
 Translating recordtypeinf_envseldefinf_t_fupd
 Adding nsLookup representation thms for [inferProg_env_61]
 Saved theorem _______ "nsLookup_inferProg_env_62_pfun_eqs"
 Saved theorem _______ "recordtypeinf_envseldefinf_t_fupd_v_thm"
 error in quse /home/cake/oven/regression/cakeml-1767/compiler/bootstrap/translation/inferProgScript.sml : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
 error in load /home/cake/oven/regression/cakeml-1767/compiler/bootstrap/translation/inferProgScript : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
 Failed translation: ns_nub
 Failed translation: inf_env_to_types_string
 Uncaught exception: HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}