Job 1375

CakeML:14fe6b7c71601ecef7aa8dd9d4716cbe0ea9e375
  Merge remote-tracking branch 'origin/master' into data-cost [Oct 16 13:03:09]
#802 (data-cost)
Merging into:bc1d24030a96270694c72cff1c37f656c1e85a9f
  Disambiguate some terms [Oct 16 13:02:29]
HOL:d4432472eed4748a30cac85026440e3a4fa77c0a
  Give finite maps their size function without an adjoin_to_theory call [Oct 17 10:04:49]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Oct 17 13:29:12 Claimed job
Oct 17 13:29:20 Building HOL
Oct 17 13:42:13 Starting developers
Oct 17 13:42:13 Finished developers                                               0s  33MB
Oct 17 13:42:14 Starting developers/bin
Oct 17 13:42:20 Finished developers/bin                                           5s   1GB
Oct 17 13:42:20 Starting semantics/ffi
Oct 17 13:42:30 Finished semantics/ffi                                            9s 298MB
Oct 17 13:42:30 Starting semantics
Oct 17 13:44:04 Finished semantics                                             1m33s   1GB
Oct 17 13:44:04 Starting semantics/proofs
Oct 17 13:47:20 Finished semantics/proofs                                      3m16s   1GB
Oct 17 13:47:20 Starting semantics/alt_semantics
Oct 17 13:47:28 Finished semantics/alt_semantics                                  7s 428MB
Oct 17 13:47:28 Starting semantics/alt_semantics/proofs
Oct 17 13:49:29 Finished semantics/alt_semantics/proofs                        1m59s   1GB
Oct 17 13:49:29 Starting basis/pure
Oct 17 13:52:16 Finished basis/pure                                            2m47s   1GB
Oct 17 13:52:17 Starting translator
Oct 17 13:54:56 Finished translator                                            2m38s   2GB
Oct 17 13:54:56 Starting compiler/parsing
Oct 17 13:56:05 Finished compiler/parsing                                      1m08s   4GB
Oct 17 13:56:05 Starting characteristic
Oct 17 14:01:48 Finished characteristic                                        5m42s   3GB
Oct 17 14:01:48 Starting translator/monadic
Oct 17 14:03:25 Finished translator/monadic                                    1m36s   2GB
Oct 17 14:03:25 Starting basis
Oct 17 14:36:08 Finished basis                                                32m42s  40GB
Oct 17 14:36:08 Starting compiler/inference
Oct 17 14:37:17 Finished compiler/inference                                    1m08s   1GB
Oct 17 14:37:17 Starting compiler/backend/reg_alloc
Oct 17 14:38:24 Finished compiler/backend/reg_alloc                            1m07s   1GB
Oct 17 14:38:25 Starting compiler/backend/gc
Oct 17 14:41:53 Finished compiler/backend/gc                                   3m27s   3GB
Oct 17 14:41:53 Starting compiler/backend
Oct 17 14:46:39 Finished compiler/backend                                      4m45s   5GB
Oct 17 14:46:39 Starting compiler/encoders/asm
Oct 17 14:47:01 Finished compiler/encoders/asm                                   21s 949MB
Oct 17 14:47:01 Starting compiler/encoders/x64
Oct 17 14:48:00 Finished compiler/encoders/x64                                   59s   1GB
Oct 17 14:48:01 Starting compiler/encoders/arm7
Oct 17 14:49:47 Finished compiler/encoders/arm7                                1m46s   1GB
Oct 17 14:49:47 Starting compiler/encoders/arm8
Oct 17 14:50:25 Finished compiler/encoders/arm8                                  37s   1GB
Oct 17 14:50:25 Starting compiler/encoders/mips
Oct 17 14:51:38 Finished compiler/encoders/mips                                1m13s   1GB
Oct 17 14:51:39 Starting compiler/encoders/riscv
Oct 17 14:53:06 Finished compiler/encoders/riscv                               1m27s   1GB
Oct 17 14:53:07 Starting compiler/encoders/ag32
Oct 17 14:53:25 Finished compiler/encoders/ag32                                  18s 951MB
Oct 17 14:53:25 Starting compiler/backend/x64
Oct 17 14:53:44 Finished compiler/backend/x64                                    18s   1GB
Oct 17 14:53:44 Starting compiler/backend/arm7
Oct 17 14:54:04 Finished compiler/backend/arm7                                   20s   1GB
Oct 17 14:54:05 Starting compiler/backend/arm8
Oct 17 14:54:24 Finished compiler/backend/arm8                                   18s   1GB
Oct 17 14:54:24 Starting compiler/backend/mips
Oct 17 14:54:43 Finished compiler/backend/mips                                   19s   1GB
Oct 17 14:54:43 Starting compiler/backend/riscv
Oct 17 14:55:04 Finished compiler/backend/riscv                                  20s   1GB
Oct 17 14:55:04 Starting compiler/backend/ag32
Oct 17 14:56:15 Finished compiler/backend/ag32                                 1m10s   1GB
Oct 17 14:56:15 Starting compiler/parsing/proofs
Oct 17 14:58:26 Finished compiler/parsing/proofs                               2m11s   2GB
Oct 17 14:58:26 Starting compiler/inference/proofs
Oct 17 15:00:42 Finished compiler/inference/proofs                             2m15s   1GB
Oct 17 15:00:42 Starting compiler/backend/semantics
Oct 17 15:27:12 Finished compiler/backend/semantics                           26m29s   4GB
Oct 17 15:27:12 Starting compiler/backend/reg_alloc/proofs
Oct 17 15:30:28 Finished compiler/backend/reg_alloc/proofs                     3m15s   1GB
Oct 17 15:30:28 Starting compiler/backend/proofs
Oct 17 16:21:29 Finished compiler/backend/proofs                              51m00s  15GB
Oct 17 16:21:29 Starting compiler/encoders/x64/proofs
Oct 17 16:31:14 Finished compiler/encoders/x64/proofs                          9m44s   5GB
Oct 17 16:31:14 Starting compiler/encoders/arm7/proofs
Oct 17 16:44:00 Finished compiler/encoders/arm7/proofs                        12m46s   3GB
Oct 17 16:44:00 Starting compiler/encoders/arm8/proofs
Oct 17 16:50:36 Finished compiler/encoders/arm8/proofs                         6m35s   2GB
Oct 17 16:50:36 Starting compiler/encoders/mips/proofs
Oct 17 17:00:18 Finished compiler/encoders/mips/proofs                         9m42s   4GB
Oct 17 17:00:18 Starting compiler/encoders/riscv/proofs
Oct 17 17:08:29 Finished compiler/encoders/riscv/proofs                        8m10s   3GB
Oct 17 17:08:29 Starting compiler/encoders/ag32/proofs
Oct 17 17:10:49 Finished compiler/encoders/ag32/proofs                         2m19s   1GB
Oct 17 17:10:49 Starting compiler/backend/x64/proofs
Oct 17 17:11:08 Finished compiler/backend/x64/proofs                             19s   1GB
Oct 17 17:11:09 Starting compiler/backend/arm7/proofs
Oct 17 17:11:30 Finished compiler/backend/arm7/proofs                            21s   1GB
Oct 17 17:11:31 Starting compiler/backend/arm8/proofs
Oct 17 17:11:49 Finished compiler/backend/arm8/proofs                            18s   1GB
Oct 17 17:11:49 Starting compiler/backend/mips/proofs
Oct 17 17:12:09 Finished compiler/backend/mips/proofs                            19s   1GB
Oct 17 17:12:10 Starting compiler/backend/riscv/proofs
Oct 17 17:12:30 Finished compiler/backend/riscv/proofs                           20s   1GB
Oct 17 17:12:31 Starting compiler/backend/ag32/proofs
Oct 17 17:24:27 Finished compiler/backend/ag32/proofs                         11m55s   3GB
Oct 17 17:24:27 Starting compiler/proofs
Oct 17 17:26:19 Finished compiler/proofs                                       1m51s   5GB
Oct 17 17:26:19 Starting candle/set-theory
Oct 17 17:26:48 Finished candle/set-theory                                       29s   1GB
Oct 17 17:26:49 Starting candle/syntax-lib
Oct 17 17:27:00 Finished candle/syntax-lib                                       11s 823MB
Oct 17 17:27:00 Starting candle/standard/syntax
Oct 17 17:28:48 Finished candle/standard/syntax                                1m48s   1GB
Oct 17 17:28:49 Starting candle/standard/semantics
Oct 17 17:30:31 Finished candle/standard/semantics                             1m42s   1GB
Oct 17 17:30:32 Starting candle/standard/monadic
Oct 17 17:32:14 Finished candle/standard/monadic                               1m42s   2GB
Oct 17 17:32:14 Starting candle/standard/ml_kernel
Oct 17 17:37:20 Finished candle/standard/ml_kernel                             5m05s   6GB
Oct 17 17:37:20 Starting candle/overloading/syntax
Oct 17 17:40:31 Finished candle/overloading/syntax                             3m09s   1GB
Oct 17 17:40:31 Starting candle/overloading/semantics
Oct 17 17:50:57 Finished candle/overloading/semantics                         10m25s   5GB
Oct 17 17:50:57 Starting characteristic/examples
Oct 17 17:52:13 Finished characteristic/examples                               1m15s   4GB
Oct 17 17:52:13 Starting tutorial/solutions
Oct 17 18:06:43 Finished tutorial/solutions                                   14m30s   7GB
Oct 17 18:06:44 Starting translator/monadic/examples
Oct 17 18:09:59 Finished translator/monadic/examples                           3m15s   3GB
Oct 17 18:09:59 Starting examples
Oct 17 18:18:23 Finished examples                                              8m23s   6GB
Oct 17 18:18:23 Starting examples/compilation/x64
Oct 17 20:30:16 Finished examples/compilation/x64                           2h11m52s  21GB
Oct 17 20:30:16 Starting examples/compilation/x64/proofs
Oct 17 20:32:02 Finished examples/compilation/x64/proofs                       1m45s   3GB
Oct 17 20:32:02 Starting examples/compilation/ag32
Oct 17 21:03:38 Finished examples/compilation/ag32                            31m36s   9GB
Oct 17 21:03:39 Starting examples/compilation/ag32/proofs
Oct 17 21:04:24 Finished examples/compilation/ag32/proofs                        45s   4GB
Oct 17 21:04:25 Starting examples/cost
Oct 17 21:58:56 Finished examples/cost                                        54m31s  21GB
Oct 17 21:58:56 Starting examples/lpr_checker
Oct 17 22:02:35 Finished examples/lpr_checker                                  3m38s   5GB
Oct 17 22:02:35 Starting examples/lpr_checker/compilation
Oct 17 22:20:09 Finished examples/lpr_checker/compilation                     17m33s  11GB
Oct 17 22:20:09 Starting examples/lpr_checker/compilation/proofs
Oct 17 22:20:49 Finished examples/lpr_checker/compilation/proofs                 40s   3GB
Oct 17 22:20:50 Starting examples/lpr_checker/array
Oct 17 22:34:24 Finished examples/lpr_checker/array                           13m33s   5GB
Oct 17 22:34:24 Starting examples/lpr_checker/array/compilation
Oct 17 22:52:56 Finished examples/lpr_checker/array/compilation               18m32s  18GB
Oct 17 22:52:57 Starting examples/lpr_checker/array/compilation/proofs
Oct 17 22:53:43 Finished examples/lpr_checker/array/compilation/proofs           46s   4GB
Oct 17 22:53:43 Starting examples/opentheory
Oct 17 23:02:49 Finished examples/opentheory                                   9m05s   9GB
Oct 17 23:02:49 Starting examples/opentheory
Oct 17 23:02:50 Finished examples/opentheory                                      0s  93MB
Oct 17 23:02:50 Starting examples/opentheory/compilation
Oct 17 23:34:41 Finished examples/opentheory/compilation                      31m50s  19GB
Oct 17 23:34:42 Starting examples/opentheory/compilation/proofs
Oct 17 23:35:21 Finished examples/opentheory/compilation/proofs                  39s   3GB
Oct 17 23:35:21 Starting examples/opentheory/compilation/ag32
Oct 18 00:12:46 FAILED: examples/opentheory/compilation/ag32
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$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[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/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[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
Scanning [1m$(CAKEMLDIR)/examples/opentheory[0m
Starting work on readerCompileTheory
readerCompileTheory                                                                                                                   real: 2243s  user: 3796sFAIL<1>
           lab_to_target real: 15m34s
           lab_to_target size: 6679753
                       export: runtime: 0.99159s,    gctime: 0.00000s,     systime: 0.00001s.
 Saved theorem _____ "reader_compiled"
 Exporting theory "readerCompile" ... Run out of store - interrupting threads
 
 Failure while writing theory!
 error in quse /home/myreen/regression/cakeml-1375/examples/opentheory/compilation/ag32/readerCompileScript.sml : Interrupt
 error in load /home/myreen/regression/cakeml-1375/examples/opentheory/compilation/ag32/readerCompileScript : Interrupt
 Uncaught exception: Interrupt