Job 1439

CakeML:533a5e920e8f7e1dd77bd53a095fd49f35fb4afc
  Add `sptreeTheory.subspt_eq` to bootstrap translation [Jan 14 19:40:02]
#810 (master)
Merging into:3c6495906dc020e093e2f5cf101cea1cba2fc468
  Fix breakage caused by change to sorted_map in HOL [Jan 05 15:57:59]
HOL:07dca05c1eb441bb9b18556ae55f275d2518bade
  Fix bugs in Makefiles/lib files preventing Lassie from compiling [Jan 06 06:03:07]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 14 21:42:50 Claimed job
Jan 14 21:42:53 Reusing HOL
Jan 14 21:43:40 Starting developers
Jan 14 21:43:44 Finished developers                                               4s 117MB
Jan 14 21:43:44 Starting developers/bin
Jan 14 21:43:51 Finished developers/bin                                           7s   1GB
Jan 14 21:43:51 Starting semantics/ffi
Jan 14 21:44:04 Finished semantics/ffi                                           12s 261MB
Jan 14 21:44:04 Starting semantics
Jan 14 21:45:35 Finished semantics                                             1m31s   1GB
Jan 14 21:45:36 Starting semantics/proofs
Jan 14 21:49:16 Finished semantics/proofs                                      3m40s 800MB
Jan 14 21:49:16 Starting semantics/alt_semantics
Jan 14 21:49:25 Finished semantics/alt_semantics                                  8s 292MB
Jan 14 21:49:26 Starting semantics/alt_semantics/proofs
Jan 14 21:51:45 Finished semantics/alt_semantics/proofs                        2m19s 804MB
Jan 14 21:51:46 Starting basis/pure
Jan 14 21:52:39 Finished basis/pure                                              52s 708MB
Jan 14 21:52:39 Starting translator
Jan 14 21:55:33 Finished translator                                            2m53s   1GB
Jan 14 21:55:33 Starting compiler/parsing
Jan 14 21:56:50 Finished compiler/parsing                                      1m16s   2GB
Jan 14 21:56:50 Starting characteristic
Jan 14 22:03:11 Finished characteristic                                        6m21s   2GB
Jan 14 22:03:12 Starting translator/monadic
Jan 14 22:04:55 Finished translator/monadic                                    1m43s   1GB
Jan 14 22:04:56 Starting basis
Jan 14 22:42:44 Finished basis                                                37m47s  11GB
Jan 14 22:42:44 Starting compiler/inference
Jan 14 22:43:51 Finished compiler/inference                                    1m06s   1GB
Jan 14 22:43:51 Starting compiler/backend/reg_alloc
Jan 14 22:45:00 Finished compiler/backend/reg_alloc                            1m08s   1GB
Jan 14 22:45:00 Starting compiler/backend/gc
Jan 14 22:48:42 Finished compiler/backend/gc                                   3m41s   2GB
Jan 14 22:48:42 Starting compiler/backend
Jan 14 22:54:04 Finished compiler/backend                                      5m21s   3GB
Jan 14 22:54:04 Starting compiler/encoders/asm
Jan 14 22:54:27 Finished compiler/encoders/asm                                   23s 781MB
Jan 14 22:54:28 Starting compiler/encoders/x64
Jan 14 22:54:54 Finished compiler/encoders/x64                                   26s 769MB
Jan 14 22:54:55 Starting compiler/encoders/arm7
Jan 14 22:55:49 Finished compiler/encoders/arm7                                  54s 790MB
Jan 14 22:55:49 Starting compiler/encoders/arm8
Jan 14 22:56:03 Finished compiler/encoders/arm8                                  13s 936MB
Jan 14 22:56:03 Starting compiler/encoders/mips
Jan 14 22:56:22 Finished compiler/encoders/mips                                  18s   1GB
Jan 14 22:56:22 Starting compiler/encoders/riscv
Jan 14 22:56:38 Finished compiler/encoders/riscv                                 16s 729MB
Jan 14 22:56:39 Starting compiler/encoders/ag32
Jan 14 22:56:58 Finished compiler/encoders/ag32                                  19s 579MB
Jan 14 22:56:58 Starting compiler/backend/x64
Jan 14 22:57:18 Finished compiler/backend/x64                                    19s 995MB
Jan 14 22:57:18 Starting compiler/backend/arm7
Jan 14 22:57:38 Finished compiler/backend/arm7                                   19s   1GB
Jan 14 22:57:38 Starting compiler/backend/arm8
Jan 14 22:57:57 Finished compiler/backend/arm8                                   18s   1GB
Jan 14 22:57:57 Starting compiler/backend/mips
Jan 14 22:58:18 Finished compiler/backend/mips                                   20s   1GB
Jan 14 22:58:19 Starting compiler/backend/riscv
Jan 14 22:58:38 Finished compiler/backend/riscv                                  19s   1GB
Jan 14 22:58:38 Starting compiler/backend/ag32
Jan 14 22:59:53 Finished compiler/backend/ag32                                 1m15s   1GB
Jan 14 22:59:54 Starting compiler/parsing/proofs
Jan 14 23:05:50 Finished compiler/parsing/proofs                               5m56s   1GB
Jan 14 23:05:50 Starting compiler/inference/proofs
Jan 14 23:08:32 Finished compiler/inference/proofs                             2m40s 948MB
Jan 14 23:08:32 Starting compiler/backend/semantics
Jan 14 23:43:18 Finished compiler/backend/semantics                           34m45s   2GB
Jan 14 23:43:18 Starting compiler/backend/reg_alloc/proofs
Jan 14 23:47:16 Finished compiler/backend/reg_alloc/proofs                     3m57s 734MB
Jan 14 23:47:16 Starting compiler/backend/proofs
Jan 15 00:50:36 Finished compiler/backend/proofs                            1h03m19s  11GB
Jan 15 00:50:36 Starting compiler/encoders/x64/proofs
Jan 15 01:02:25 Finished compiler/encoders/x64/proofs                         11m48s   1GB
Jan 15 01:02:25 Starting compiler/encoders/arm7/proofs
Jan 15 01:16:39 Finished compiler/encoders/arm7/proofs                        14m13s   3GB
Jan 15 01:16:39 Starting compiler/encoders/arm8/proofs
Jan 15 01:23:54 Finished compiler/encoders/arm8/proofs                         7m15s   1GB
Jan 15 01:23:54 Starting compiler/encoders/mips/proofs
Jan 15 01:35:18 Finished compiler/encoders/mips/proofs                        11m23s   2GB
Jan 15 01:35:18 Starting compiler/encoders/riscv/proofs
Jan 15 01:45:09 Finished compiler/encoders/riscv/proofs                        9m51s   1GB
Jan 15 01:45:10 Starting compiler/encoders/ag32/proofs
Jan 15 01:48:03 Finished compiler/encoders/ag32/proofs                         2m53s 653MB
Jan 15 01:48:04 Starting compiler/backend/x64/proofs
Jan 15 01:48:26 Finished compiler/backend/x64/proofs                             22s   1GB
Jan 15 01:48:26 Starting compiler/backend/arm7/proofs
Jan 15 01:48:50 Finished compiler/backend/arm7/proofs                            23s   1GB
Jan 15 01:48:50 Starting compiler/backend/arm8/proofs
Jan 15 01:49:12 Finished compiler/backend/arm8/proofs                            20s   1GB
Jan 15 01:49:12 Starting compiler/backend/mips/proofs
Jan 15 01:49:34 Finished compiler/backend/mips/proofs                            21s   1GB
Jan 15 01:49:34 Starting compiler/backend/riscv/proofs
Jan 15 01:49:57 Finished compiler/backend/riscv/proofs                           22s   1GB
Jan 15 01:49:57 Starting compiler/backend/ag32/proofs
Jan 15 02:04:00 Finished compiler/backend/ag32/proofs                         14m02s   2GB
Jan 15 02:04:00 Starting compiler/proofs
Jan 15 02:05:41 Finished compiler/proofs                                       1m41s   2GB
Jan 15 02:05:41 Starting candle/set-theory
Jan 15 02:06:12 Finished candle/set-theory                                       30s 743MB
Jan 15 02:06:12 Starting candle/syntax-lib
Jan 15 02:06:23 Finished candle/syntax-lib                                       11s 456MB
Jan 15 02:06:23 Starting candle/standard/syntax
Jan 15 02:08:21 Finished candle/standard/syntax                                1m57s   1GB
Jan 15 02:08:21 Starting candle/standard/semantics
Jan 15 02:10:12 Finished candle/standard/semantics                             1m50s 987MB
Jan 15 02:10:13 Starting candle/standard/monadic
Jan 15 02:12:05 Finished candle/standard/monadic                               1m52s 983MB
Jan 15 02:12:05 Starting candle/standard/ml_kernel
Jan 15 02:18:11 Finished candle/standard/ml_kernel                             6m05s   3GB
Jan 15 02:18:12 Starting candle/overloading/syntax
Jan 15 02:21:35 Finished candle/overloading/syntax                             3m23s   1GB
Jan 15 02:21:35 Starting candle/overloading/semantics
Jan 15 02:35:01 Finished candle/overloading/semantics                         13m25s   4GB
Jan 15 02:35:01 Starting characteristic/examples
Jan 15 02:36:28 Finished characteristic/examples                               1m26s   2GB
Jan 15 02:36:28 Starting tutorial/solutions
Jan 15 02:52:41 Finished tutorial/solutions                                   16m12s   8GB
Jan 15 02:52:41 Starting translator/monadic/examples
Jan 15 02:56:22 Finished translator/monadic/examples                           3m41s   2GB
Jan 15 02:56:23 Starting examples
Jan 15 03:06:26 Finished examples                                             10m02s   3GB
Jan 15 03:06:26 Starting examples/compilation/x64
Jan 15 05:41:35 Finished examples/compilation/x64                           2h35m08s  13GB
Jan 15 05:41:35 Starting examples/compilation/x64/proofs
Jan 15 05:43:40 Finished examples/compilation/x64/proofs                       2m04s   3GB
Jan 15 05:43:40 Starting examples/compilation/ag32
Jan 15 06:18:58 Finished examples/compilation/ag32                            35m17s   8GB
Jan 15 06:18:58 Starting examples/compilation/ag32/proofs
Jan 15 06:19:45 Finished examples/compilation/ag32/proofs                        47s   2GB
Jan 15 06:19:46 Starting examples/cost
Jan 15 07:26:29 Finished examples/cost                                      1h06m42s   6GB
Jan 15 07:26:29 Starting examples/lpr_checker
Jan 15 07:30:51 Finished examples/lpr_checker                                  4m22s   2GB
Jan 15 07:30:52 Starting examples/lpr_checker/compilation
Jan 15 07:50:36 Finished examples/lpr_checker/compilation                     19m44s   9GB
Jan 15 07:50:37 Starting examples/lpr_checker/compilation/proofs
Jan 15 07:51:56 Finished examples/lpr_checker/compilation/proofs               1m19s   2GB
Jan 15 07:51:56 Starting examples/lpr_checker/array
Jan 15 08:08:08 Finished examples/lpr_checker/array                           16m11s   3GB
Jan 15 08:08:08 Starting examples/lpr_checker/array/compilation
Jan 15 08:29:08 Finished examples/lpr_checker/array/compilation               20m59s  12GB
Jan 15 08:29:08 Starting examples/lpr_checker/array/compilation/proofs
Jan 15 08:30:14 Finished examples/lpr_checker/array/compilation/proofs         1m06s   2GB
Jan 15 08:30:14 Starting examples/opentheory
Jan 15 08:30:47 FAILED: examples/opentheory
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)/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$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Starting work on README.md
Starting work on prettyTheory
README.md                                       real:    0s  user:    0s     OK
prettyTheory                                    real:   20s  user:   19s     OK
Starting work on readerTheory
readerTheory                                    real:   10s  user:    9sFAIL<1>
 Run out of store - interrupting threads
 error in quse /home/cake/oven/regression/cakeml-1439/candle/standard/ml_kernel/ml_hol_kernelProgTheory.sml : Interrupt
 error in load $(CAKEMLDIR)/candle/standard/ml_kernel/ml_hol_kernelProgTheory : Interrupt
 error in load /home/cake/oven/regression/cakeml-1439/examples/opentheory/readerScript : Interrupt
 Uncaught exception: Interrupt