Job 1958

CakeML:42712c3f0757b8330cf98aaa30c0f4ed2800a50c
  Make bootstrap test ./cake --types output of basis [Jul 04 20:44:29]
#895 (issue894)
Merging into:939c98b120105252f0e1ee40b7fe9d6d0d028e12
  Fix proof broken by recent HOL change [Jul 06 08:39:40]
HOL:8b0248d705162f895cc7228fd638fe1c7d74b600
  Fix Unicode violation from 5184a58dae1 [Jul 04 06:34:10]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jul 07 20:46:09 Claimed job
Jul 07 20:46:15 Building HOL
Jul 07 21:06:05 Starting developers
Jul 07 21:06:10 Finished developers                                               4s 109MB
Jul 07 21:06:10 Starting developers/bin
Jul 07 21:06:21 Finished developers/bin                                          10s   1GB
Jul 07 21:06:21 Starting semantics/ffi
Jul 07 21:06:39 Finished semantics/ffi                                           17s 274MB
Jul 07 21:06:39 Starting semantics
Jul 07 21:10:33 Finished semantics                                             3m53s   2GB
Jul 07 21:10:33 Starting semantics/proofs
Jul 07 21:17:38 Finished semantics/proofs                                      7m05s   2GB
Jul 07 21:17:39 Starting semantics/alt_semantics
Jul 07 21:18:05 Finished semantics/alt_semantics                                 25s 637MB
Jul 07 21:18:05 Starting semantics/alt_semantics/proofs
Jul 07 21:29:07 Finished semantics/alt_semantics/proofs                       11m02s   2GB
Jul 07 21:29:07 Starting basis/pure
Jul 07 21:32:41 Finished basis/pure                                            3m33s   1GB
Jul 07 21:32:41 Starting translator
Jul 07 21:36:23 Finished translator                                            3m41s   2GB
Jul 07 21:36:23 Starting compiler/parsing
Jul 07 21:38:01 Finished compiler/parsing                                      1m37s   6GB
Jul 07 21:38:01 Starting characteristic
Jul 07 21:44:59 Finished characteristic                                        6m57s   3GB
Jul 07 21:44:59 Starting translator/monadic
Jul 07 21:47:06 Finished translator/monadic                                    2m06s   2GB
Jul 07 21:47:06 Starting basis
Jul 07 22:39:58 Finished basis                                                52m51s  43GB
Jul 07 22:39:58 Starting compiler/inference
Jul 07 22:41:35 Finished compiler/inference                                    1m36s   1GB
Jul 07 22:41:35 Starting compiler/backend/reg_alloc
Jul 07 22:43:17 Finished compiler/backend/reg_alloc                            1m42s   2GB
Jul 07 22:43:17 Starting compiler/backend/gc
Jul 07 22:47:57 Finished compiler/backend/gc                                   4m39s   3GB
Jul 07 22:47:58 Starting compiler/backend
Jul 07 22:54:38 Finished compiler/backend                                      6m40s   4GB
Jul 07 22:54:38 Starting compiler/encoders/asm
Jul 07 22:55:10 Finished compiler/encoders/asm                                   31s   1GB
Jul 07 22:55:10 Starting compiler/encoders/x64
Jul 07 22:56:22 Finished compiler/encoders/x64                                 1m11s   1GB
Jul 07 22:56:22 Starting compiler/encoders/arm7
Jul 07 22:58:36 Finished compiler/encoders/arm7                                2m14s   1GB
Jul 07 22:58:36 Starting compiler/encoders/arm8
Jul 07 22:59:22 Finished compiler/encoders/arm8                                  45s   1GB
Jul 07 22:59:22 Starting compiler/encoders/arm8_asl
Jul 08 01:48:26 Finished compiler/encoders/arm8_asl                         2h49m03s  33GB
Jul 08 01:48:26 Starting compiler/encoders/mips
Jul 08 01:50:01 Finished compiler/encoders/mips                                1m35s   1GB
Jul 08 01:50:01 Starting compiler/encoders/riscv
Jul 08 01:51:50 Finished compiler/encoders/riscv                               1m48s   1GB
Jul 08 01:51:50 Starting compiler/encoders/ag32
Jul 08 01:52:14 Finished compiler/encoders/ag32                                  23s   1GB
Jul 08 01:52:15 Starting compiler/backend/x64
Jul 08 01:52:38 Finished compiler/backend/x64                                    23s   1GB
Jul 08 01:52:39 Starting compiler/backend/arm7
Jul 08 01:53:05 Finished compiler/backend/arm7                                   25s   1GB
Jul 08 01:53:05 Starting compiler/backend/arm8
Jul 08 01:53:29 Finished compiler/backend/arm8                                   23s   1GB
Jul 08 01:53:29 Starting compiler/backend/mips
Jul 08 01:53:54 Finished compiler/backend/mips                                   24s   1GB
Jul 08 01:53:54 Starting compiler/backend/riscv
Jul 08 01:54:19 Finished compiler/backend/riscv                                  25s   1GB
Jul 08 01:54:20 Starting compiler/backend/ag32
Jul 08 01:55:47 Finished compiler/backend/ag32                                 1m27s   1GB
Jul 08 01:55:47 Starting compiler/parsing/proofs
Jul 08 01:58:34 Finished compiler/parsing/proofs                               2m46s   1GB
Jul 08 01:58:34 Starting compiler/inference/proofs
Jul 08 02:01:18 Finished compiler/inference/proofs                             2m44s   1GB
Jul 08 02:01:19 Starting compiler/backend/semantics
Jul 08 02:26:50 Finished compiler/backend/semantics                           25m31s   4GB
Jul 08 02:26:51 Starting compiler/backend/reg_alloc/proofs
Jul 08 02:30:18 Finished compiler/backend/reg_alloc/proofs                     3m27s   1GB
Jul 08 02:30:18 Starting compiler/backend/proofs
Jul 08 03:26:32 Finished compiler/backend/proofs                              56m12s  13GB
Jul 08 03:26:32 Starting compiler/backend/serialiser
Jul 08 03:28:15 Finished compiler/backend/serialiser                           1m42s   2GB
Jul 08 03:28:15 Starting compiler/encoders/x64/proofs
Jul 08 03:38:09 Finished compiler/encoders/x64/proofs                          9m54s   4GB
Jul 08 03:38:09 Starting compiler/encoders/arm7/proofs
Jul 08 03:51:37 Finished compiler/encoders/arm7/proofs                        13m27s   7GB
Jul 08 03:51:37 Starting compiler/encoders/arm8/proofs
Jul 08 03:58:28 Finished compiler/encoders/arm8/proofs                         6m50s   4GB
Jul 08 03:58:28 Starting compiler/encoders/arm8_asl/proofs
Jul 08 04:49:10 Finished compiler/encoders/arm8_asl/proofs                    50m41s  10GB
Jul 08 04:49:10 Starting compiler/encoders/mips/proofs
Jul 08 04:59:43 Finished compiler/encoders/mips/proofs                        10m33s   5GB
Jul 08 04:59:43 Starting compiler/encoders/riscv/proofs
Jul 08 05:08:23 Finished compiler/encoders/riscv/proofs                        8m39s   4GB
Jul 08 05:08:23 Starting compiler/encoders/ag32/proofs
Jul 08 05:10:52 Finished compiler/encoders/ag32/proofs                         2m28s   1GB
Jul 08 05:10:52 Starting compiler/backend/x64/proofs
Jul 08 05:11:21 Finished compiler/backend/x64/proofs                             28s   1GB
Jul 08 05:11:21 Starting compiler/backend/arm7/proofs
Jul 08 05:11:52 Finished compiler/backend/arm7/proofs                            30s   2GB
Jul 08 05:11:52 Starting compiler/backend/arm8/proofs
Jul 08 05:12:20 Finished compiler/backend/arm8/proofs                            28s   1GB
Jul 08 05:12:21 Starting compiler/backend/arm8_asl
Jul 08 05:12:44 Finished compiler/backend/arm8_asl                               23s   1GB
Jul 08 05:12:45 Starting compiler/backend/mips/proofs
Jul 08 05:13:16 Finished compiler/backend/mips/proofs                            30s   2GB
Jul 08 05:13:16 Starting compiler/backend/riscv/proofs
Jul 08 05:13:45 Finished compiler/backend/riscv/proofs                           29s   2GB
Jul 08 05:13:46 Starting compiler/backend/ag32/proofs
Jul 08 05:26:47 Finished compiler/backend/ag32/proofs                         13m01s   3GB
Jul 08 05:26:48 Starting compiler/proofs
Jul 08 05:29:24 Finished compiler/proofs                                       2m35s   6GB
Jul 08 05:29:24 Starting candle/set-theory
Jul 08 05:30:00 Finished candle/set-theory                                       36s   1GB
Jul 08 05:30:01 Starting candle/syntax-lib
Jul 08 05:30:16 Finished candle/syntax-lib                                       15s 851MB
Jul 08 05:30:16 Starting candle/standard/syntax
Jul 08 05:32:20 Finished candle/standard/syntax                                2m04s   1GB
Jul 08 05:32:21 Starting candle/standard/semantics
Jul 08 05:34:13 Finished candle/standard/semantics                             1m51s   1GB
Jul 08 05:34:13 Starting candle/standard/monadic
Jul 08 05:36:09 Finished candle/standard/monadic                               1m55s   2GB
Jul 08 05:36:09 Starting candle/standard/ml_kernel
Jul 08 05:42:29 Finished candle/standard/ml_kernel                             6m20s   4GB
Jul 08 05:42:30 Starting candle/overloading/syntax
Jul 08 05:45:44 Finished candle/overloading/syntax                             3m14s   1GB
Jul 08 05:45:44 Starting candle/overloading/semantics
Jul 08 05:56:53 Finished candle/overloading/semantics                         11m08s   4GB
Jul 08 05:56:54 Starting candle/overloading/monadic
Jul 08 05:59:25 Finished candle/overloading/monadic                            2m31s   2GB
Jul 08 05:59:25 Starting candle/overloading/ml_kernel
Jul 08 06:06:40 Finished candle/overloading/ml_kernel                          7m14s   5GB
Jul 08 06:06:40 Starting candle/overloading/ml_checker
Jul 08 06:09:06 Finished candle/overloading/ml_checker                         2m25s   5GB
Jul 08 06:09:06 Starting candle/prover
Jul 08 06:19:16 Finished candle/prover                                        10m09s   4GB
Jul 08 06:19:17 Starting pancake
Jul 08 06:23:13 Finished pancake                                               3m55s   5GB
Jul 08 06:23:13 Starting pancake/ffi
Jul 08 06:23:13 Finished pancake/ffi                                              0s  35MB
Jul 08 06:23:13 Starting pancake/semantics
Jul 08 06:25:48 Finished pancake/semantics                                     2m34s   1GB
Jul 08 06:25:48 Starting pancake/proofs
Jul 08 06:37:58 Finished pancake/proofs                                       12m09s   5GB
Jul 08 06:37:58 Starting characteristic/examples
Jul 08 06:39:26 Finished characteristic/examples                               1m27s   4GB
Jul 08 06:39:26 Starting tutorial/solutions
Jul 08 06:55:31 Finished tutorial/solutions                                   16m04s  13GB
Jul 08 06:55:32 Starting translator/monadic/examples
Jul 08 06:59:43 Finished translator/monadic/examples                           4m10s   3GB
Jul 08 06:59:43 Starting examples
Jul 08 07:10:47 Finished examples                                             11m03s   6GB
Jul 08 07:10:47 Starting examples/compilation/x64
Jul 08 09:18:08 Finished examples/compilation/x64                           2h07m20s  18GB
Jul 08 09:18:08 Starting examples/compilation/x64/proofs
Jul 08 09:20:44 Finished examples/compilation/x64/proofs                       2m35s   3GB
Jul 08 09:20:44 Starting examples/compilation/ag32
Jul 08 09:55:19 Finished examples/compilation/ag32                            34m34s  13GB
Jul 08 09:55:19 Starting examples/compilation/ag32/proofs
Jul 08 09:56:23 Finished examples/compilation/ag32/proofs                      1m03s   5GB
Jul 08 09:56:24 Starting examples/lpr_checker
Jul 08 09:57:30 Finished examples/lpr_checker                                  1m05s   1GB
Jul 08 09:57:30 Starting examples/lpr_checker/array
Jul 08 10:31:03 Finished examples/lpr_checker/array                           33m32s  28GB
Jul 08 10:31:03 Starting examples/lpr_checker/array/compilation
Jul 08 11:13:02 Finished examples/lpr_checker/array/compilation               41m58s  29GB
Jul 08 11:13:02 Starting examples/lpr_checker/array/compilation/proofs
Jul 08 11:14:27 Finished examples/lpr_checker/array/compilation/proofs         1m24s   6GB
Jul 08 11:14:27 Starting examples/opentheory
Jul 08 11:24:57 Finished examples/opentheory                                  10m30s   6GB
Jul 08 11:24:58 Starting examples/opentheory
Jul 08 11:24:59 Finished examples/opentheory                                      1s 140MB
Jul 08 11:24:59 Starting examples/opentheory/compilation
Jul 08 12:03:48 Finished examples/opentheory/compilation                      38m48s  27GB
Jul 08 12:03:48 Starting examples/opentheory/compilation/proofs
Jul 08 12:04:44 Finished examples/opentheory/compilation/proofs                  55s   4GB
Jul 08 12:04:44 Starting examples/opentheory/compilation/ag32
Jul 08 12:41:23 Finished examples/opentheory/compilation/ag32                 36m38s  29GB
Jul 08 12:41:23 Starting examples/opentheory/compilation/ag32/proofs
Jul 08 12:43:15 Finished examples/opentheory/compilation/ag32/proofs           1m52s   7GB
Jul 08 12:43:16 Starting examples/sat_encodings
Jul 08 12:45:27 Finished examples/sat_encodings                                2m11s   1GB
Jul 08 12:45:27 Starting examples/sat_encodings/case_studies
Jul 08 12:47:18 Finished examples/sat_encodings/case_studies                   1m51s   1GB
Jul 08 12:47:19 Starting examples/sat_encodings/translation
Jul 08 12:53:14 Finished examples/sat_encodings/translation                    5m55s   4GB
Jul 08 12:53:14 Starting examples/sat_encodings/translation/compilation
Jul 08 13:33:50 FAILED: examples/sat_encodings/translation/compilation
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/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[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
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
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/examples/sat_encodings[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/examples/sat_encodings/case_studies[0m
Scanning [1m$(CAKEMLDIR)/examples/sat_encodings/translation[0m
Scanned 78 directories
Starting work on README.md
Starting work on graphColoringEncoderCompileTheory
Starting work on killerSudokuEncoderCompileTheory
Starting work on nQueensEncoderCompileTheory
README.md                                                                                         (0s)     OK
Starting work on numBoolRangeEncoderCompileTheory
nQueensEncoderCompileTheory                                                                      (42m)     OK
Starting work on nQueens_encoder
nQueens_encoder                                                                                   (0s)     OK
Starting work on sudokuEncoderCompileTheory
killerSudokuEncoderCompileTheory                                                                 (51m)     OK
Starting work on killerSudoku_encoder
killerSudoku_encoder                                                                              (0s)     OK
graphColoringEncoderCompileTheory                                                                (51m)     OK
Starting work on graphColoring_encoder
graphColoring_encoder                                                                             (0s)     OK
numBoolRangeEncoderCompileTheory                                                                 (53m)FAIL<1>
           lab_to_target real: 12m10s
           lab_to_target size: 3398222
                       export: runtime: 1.6s,    gctime: 0.00000s,     systime: 0.00007s.
 Saved theorem _______ "numBoolRange_encoder_compiled"
 Exporting theory "numBoolRangeEncoderCompile" ... 
 Failure while writing theory!
 Run out of store - interrupting threads
 error in quse /home/myreen/regression/cakeml-1958/examples/sat_encodings/translation/compilation/numBoolRangeEncoderCompileScript.sml : Interrupt
 error in load /home/myreen/regression/cakeml-1958/examples/sat_encodings/translation/compilation/numBoolRangeEncoderCompileScript : Interrupt
 Uncaught exception: Interrupt
sudokuEncoderCompileTheory                                                                      (472s)MKILLED