CakeML Regression Test

Job 1614

CakeML:e7a5c005596708fcf02ba333f849a5ae1eefdf8a
  Merge pull request #839 from CakeML/lpr_transform [Oct 03 11:04:50]
HOL:cada10ccbffc01a09a20b813f3049b3b88b33d4b
  Fix problems to with lexing of string literals inside HOL terms [Oct 28 23:50:37]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Oct 29 06:18:13 Claimed job
Oct 29 06:18:18 Building HOL
Oct 29 06:29:21 Starting developers
Oct 29 06:29:24 Finished developers                                               2s 113MB
Oct 29 06:29:24 Starting developers/bin
Oct 29 06:29:31 Finished developers/bin                                           6s   1GB
Oct 29 06:29:31 Starting semantics/ffi
Oct 29 06:29:42 Finished semantics/ffi                                           10s 299MB
Oct 29 06:29:42 Starting semantics
Oct 29 06:31:18 Finished semantics                                             1m35s   1GB
Oct 29 06:31:18 Starting semantics/proofs
Oct 29 06:34:51 Finished semantics/proofs                                      3m33s   2GB
Oct 29 06:34:52 Starting semantics/alt_semantics
Oct 29 06:35:02 Finished semantics/alt_semantics                                 10s 453MB
Oct 29 06:35:03 Starting semantics/alt_semantics/proofs
Oct 29 06:37:23 Finished semantics/alt_semantics/proofs                        2m20s   2GB
Oct 29 06:37:24 Starting basis/pure
Oct 29 06:40:09 Finished basis/pure                                            2m44s   1GB
Oct 29 06:40:09 Starting translator
Oct 29 06:43:27 Finished translator                                            3m17s   2GB
Oct 29 06:43:27 Starting compiler/parsing
Oct 29 06:44:38 Finished compiler/parsing                                      1m10s   4GB
Oct 29 06:44:38 Starting characteristic
Oct 29 06:50:21 Finished characteristic                                        5m42s   3GB
Oct 29 06:50:21 Starting translator/monadic
Oct 29 06:52:21 Finished translator/monadic                                    1m59s   3GB
Oct 29 06:52:21 Starting basis
Oct 29 07:46:19 Finished basis                                                53m57s  33GB
Oct 29 07:46:20 Starting compiler/inference
Oct 29 07:47:39 Finished compiler/inference                                    1m19s   2GB
Oct 29 07:47:40 Starting compiler/backend/reg_alloc
Oct 29 07:48:54 Finished compiler/backend/reg_alloc                            1m14s   1GB
Oct 29 07:48:54 Starting compiler/backend/gc
Oct 29 07:53:12 Finished compiler/backend/gc                                   4m17s   4GB
Oct 29 07:53:12 Starting compiler/backend
Oct 29 07:59:47 Finished compiler/backend                                      6m34s   5GB
Oct 29 07:59:48 Starting compiler/encoders/asm
Oct 29 08:00:14 Finished compiler/encoders/asm                                   26s   1GB
Oct 29 08:00:14 Starting compiler/encoders/x64
Oct 29 08:01:34 Finished compiler/encoders/x64                                 1m19s   1GB
Oct 29 08:01:34 Starting compiler/encoders/arm7
Oct 29 08:04:01 Finished compiler/encoders/arm7                                2m27s   1GB
Oct 29 08:04:02 Starting compiler/encoders/arm8
Oct 29 08:04:47 Finished compiler/encoders/arm8                                  45s   1GB
Oct 29 08:04:47 Starting compiler/encoders/mips
Oct 29 08:06:24 Finished compiler/encoders/mips                                1m36s   1GB
Oct 29 08:06:24 Starting compiler/encoders/riscv
Oct 29 08:08:24 Finished compiler/encoders/riscv                               1m59s   1GB
Oct 29 08:08:24 Starting compiler/encoders/ag32
Oct 29 08:08:50 Finished compiler/encoders/ag32                                  25s 977MB
Oct 29 08:08:50 Starting compiler/backend/x64
Oct 29 08:09:15 Finished compiler/backend/x64                                    24s   1GB
Oct 29 08:09:15 Starting compiler/backend/arm7
Oct 29 08:09:39 Finished compiler/backend/arm7                                   24s   1GB
Oct 29 08:09:39 Starting compiler/backend/arm8
Oct 29 08:10:02 Finished compiler/backend/arm8                                   22s   1GB
Oct 29 08:10:02 Starting compiler/backend/mips
Oct 29 08:10:26 Finished compiler/backend/mips                                   23s   1GB
Oct 29 08:10:26 Starting compiler/backend/riscv
Oct 29 08:10:50 Finished compiler/backend/riscv                                  23s   1GB
Oct 29 08:10:50 Starting compiler/backend/ag32
Oct 29 08:12:07 Finished compiler/backend/ag32                                 1m16s   2GB
Oct 29 08:12:07 Starting compiler/parsing/proofs
Oct 29 08:14:51 Finished compiler/parsing/proofs                               2m43s   1GB
Oct 29 08:14:51 Starting compiler/inference/proofs
Oct 29 08:17:59 Finished compiler/inference/proofs                             3m07s   2GB
Oct 29 08:17:59 Starting compiler/backend/semantics
Oct 29 09:39:02 Finished compiler/backend/semantics                         1h21m02s   4GB
Oct 29 09:39:02 Starting compiler/backend/reg_alloc/proofs
Oct 29 09:45:42 Finished compiler/backend/reg_alloc/proofs                     6m39s   1GB
Oct 29 09:45:42 Starting compiler/backend/proofs
Oct 29 11:04:09 Finished compiler/backend/proofs                            1h18m26s  19GB
Oct 29 11:04:09 Starting compiler/backend/serialiser
Oct 29 11:05:18 Finished compiler/backend/serialiser                           1m08s   2GB
Oct 29 11:05:18 Starting compiler/encoders/x64/proofs
Oct 29 11:14:35 Finished compiler/encoders/x64/proofs                          9m16s   5GB
Oct 29 11:14:36 Starting compiler/encoders/arm7/proofs
Oct 29 11:27:19 Finished compiler/encoders/arm7/proofs                        12m43s   7GB
Oct 29 11:27:19 Starting compiler/encoders/arm8/proofs
Oct 29 11:33:58 Finished compiler/encoders/arm8/proofs                         6m38s   3GB
Oct 29 11:33:58 Starting compiler/encoders/mips/proofs
Oct 29 11:43:49 Finished compiler/encoders/mips/proofs                         9m50s   3GB
Oct 29 11:43:49 Starting compiler/encoders/riscv/proofs
Oct 29 11:52:13 Finished compiler/encoders/riscv/proofs                        8m23s   3GB
Oct 29 11:52:13 Starting compiler/encoders/ag32/proofs
Oct 29 11:54:34 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Oct 29 11:54:34 Starting compiler/backend/x64/proofs
Oct 29 11:54:57 Finished compiler/backend/x64/proofs                             22s   1GB
Oct 29 11:54:57 Starting compiler/backend/arm7/proofs
Oct 29 11:55:22 Finished compiler/backend/arm7/proofs                            24s   1GB
Oct 29 11:55:22 Starting compiler/backend/arm8/proofs
Oct 29 11:55:46 Finished compiler/backend/arm8/proofs                            24s   2GB
Oct 29 11:55:46 Starting compiler/backend/mips/proofs
Oct 29 11:56:10 Finished compiler/backend/mips/proofs                            23s   1GB
Oct 29 11:56:11 Starting compiler/backend/riscv/proofs
Oct 29 11:56:35 Finished compiler/backend/riscv/proofs                           24s   2GB
Oct 29 11:56:35 Starting compiler/backend/ag32/proofs
Oct 29 12:08:37 Finished compiler/backend/ag32/proofs                         12m01s   4GB
Oct 29 12:08:37 Starting compiler/proofs
Oct 29 12:10:44 Finished compiler/proofs                                       2m06s   6GB
Oct 29 12:10:44 Starting candle/set-theory
Oct 29 12:11:15 Finished candle/set-theory                                       30s   1GB
Oct 29 12:11:15 Starting candle/syntax-lib
Oct 29 12:11:27 Finished candle/syntax-lib                                       11s 823MB
Oct 29 12:11:27 Starting candle/standard/syntax
Oct 29 12:13:19 Finished candle/standard/syntax                                1m51s   1GB
Oct 29 12:13:19 Starting candle/standard/semantics
Oct 29 12:15:06 Finished candle/standard/semantics                             1m46s   2GB
Oct 29 12:15:06 Starting candle/standard/monadic
Oct 29 12:16:50 Finished candle/standard/monadic                               1m43s   1GB
Oct 29 12:16:50 Starting candle/standard/ml_kernel
Oct 29 12:22:21 Finished candle/standard/ml_kernel                             5m29s   5GB
Oct 29 12:22:21 Starting candle/overloading/syntax
Oct 29 12:25:39 Finished candle/overloading/syntax                             3m18s   2GB
Oct 29 12:25:40 Starting candle/overloading/semantics
Oct 29 12:40:35 Finished candle/overloading/semantics                         14m55s   6GB
Oct 29 12:40:35 Starting pancake
Oct 29 12:42:55 Finished pancake                                               2m19s   3GB
Oct 29 12:42:55 Starting pancake/ffi
Oct 29 12:42:55 Finished pancake/ffi                                              0s   6MB
Oct 29 12:42:55 Starting pancake/semantics
Oct 29 12:45:33 Finished pancake/semantics                                     2m36s   1GB
Oct 29 12:45:33 Starting pancake/proofs
Oct 29 12:58:27 Finished pancake/proofs                                       12m54s   8GB
Oct 29 12:58:27 Starting characteristic/examples
Oct 29 13:00:24 Finished characteristic/examples                               1m56s   5GB
Oct 29 13:00:24 Starting tutorial/solutions
Oct 29 13:17:50 Finished tutorial/solutions                                   17m25s  20GB
Oct 29 13:17:50 Starting translator/monadic/examples
Oct 29 13:22:28 Finished translator/monadic/examples                           4m37s   4GB
Oct 29 13:22:28 Starting examples
Oct 29 13:36:25 Finished examples                                             13m56s   6GB
Oct 29 13:36:25 Starting examples/compilation/x64
Oct 29 16:09:22 Finished examples/compilation/x64                           2h32m56s  46GB
Oct 29 16:09:22 Starting examples/compilation/x64/proofs
Oct 29 16:11:26 Finished examples/compilation/x64/proofs                       2m03s   3GB
Oct 29 16:11:26 Starting examples/compilation/ag32
Oct 29 16:46:37 Finished examples/compilation/ag32                            35m10s  15GB
Oct 29 16:46:38 Starting examples/compilation/ag32/proofs
Oct 29 16:47:35 Finished examples/compilation/ag32/proofs                        56s   5GB
Oct 29 16:47:35 Starting examples/cost
Oct 29 17:42:58 Finished examples/cost                                        55m22s  15GB
Oct 29 17:42:58 Starting examples/lpr_checker
Oct 29 17:43:50 Finished examples/lpr_checker                                    51s   2GB
Oct 29 17:43:50 Starting examples/lpr_checker/array
Oct 29 18:10:30 Finished examples/lpr_checker/array                           26m38s   8GB
Oct 29 18:10:30 Starting examples/lpr_checker/array/compilation
Oct 29 19:32:52 Finished examples/lpr_checker/array/compilation             1h22m21s  34GB
Oct 29 19:32:52 Starting examples/lpr_checker/array/compilation/proofs
Oct 29 19:34:08 Finished examples/lpr_checker/array/compilation/proofs         1m15s   7GB
Oct 29 19:34:08 Starting examples/opentheory
Oct 29 19:43:45 Finished examples/opentheory                                   9m36s   6GB
Oct 29 19:43:45 Starting examples/opentheory
Oct 29 19:43:46 Finished examples/opentheory                                      0s 124MB
Oct 29 19:43:46 Starting examples/opentheory/compilation
Oct 29 20:19:35 Finished examples/opentheory/compilation                      35m48s  35GB
Oct 29 20:19:35 Starting examples/opentheory/compilation/proofs
Oct 29 20:20:22 Finished examples/opentheory/compilation/proofs                  46s   4GB
Oct 29 20:20:22 Starting examples/opentheory/compilation/ag32
Oct 29 20:59:09 Finished examples/opentheory/compilation/ag32                 38m45s  53GB
Oct 29 20:59:09 Starting examples/opentheory/compilation/ag32/proofs
Oct 29 21:00:48 Finished examples/opentheory/compilation/ag32/proofs           1m38s   6GB
Oct 29 21:00:48 Starting examples/sat_encodings
Oct 29 21:02:43 Finished examples/sat_encodings                                1m54s   1GB
Oct 29 21:02:43 Starting examples/sat_encodings/case_studies
Oct 29 21:04:17 Finished examples/sat_encodings/case_studies                   1m34s   1GB
Oct 29 21:04:18 Starting examples/sat_encodings/translation
Oct 29 21:10:00 Finished examples/sat_encodings/translation                    5m42s   6GB
Oct 29 21:10:00 Starting examples/sat_encodings/translation/compilation
Oct 29 21:45:03 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/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/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[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/lem_lib_stub[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
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[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/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/topology[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
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                                                                                                                                              (40m)     OK
Starting work on nQueens_encoder
nQueens_encoder                                                                                                                                                           (0s)     OK
Starting work on sudokuEncoderCompileTheory
killerSudokuEncoderCompileTheory                                                                                                                                         (50m)     OK
Starting work on killerSudoku_encoder
killerSudoku_encoder                                                                                                                                                      (0s)     OK
graphColoringEncoderCompileTheory                                                                                                                                        (51m)FAIL<1>
           lab_to_target real: 9m13s
           lab_to_target size: 3639135
                       export: runtime: 0.79793s,    gctime: 0.00000s,     systime: 0.00000s.
 Saved theorem _____ "graphColoring_encoder_compiled"
 Exporting theory "graphColoringEncoderCompile" ...
 Failure while writing theory!
 Run out of store - interrupting threads
 error in quse /home/myreen/regression/cakeml-1614/examples/sat_encodings/translation/compilation/graphColoringEncoderCompileScript.sml : Interrupt
 error in load /home/myreen/regression/cakeml-1614/examples/sat_encodings/translation/compilation/graphColoringEncoderCompileScript : Interrupt
 Uncaught exception: Interrupt
numBoolRangeEncoderCompileTheory                                                                                                                                         (51m)MKILLED
sudokuEncoderCompileTheory                                                                                                                                              (287s)MKILLED