Job 2698

CakeML:32a02d3fee1a1f74f39ebde9a9ea5dbf8507c0c8
  Remove non-working example [Nov 13 19:43:05]
#1092 (cost)
Merging into:d8b47adcad1fba86c8f0ae0ce9d1da925b080c63
  Merge pull request #1085 from CakeML/parse_err [Nov 12 20:21:29]
HOL:2de6b3ccc36da9c19998787a835c3ef9c81466fe
  Add a cute problem to examples/misc [Oct 30 04:33:10]
Machine:lammmington

Nov 14 08:19:14 Claimed job
Nov 14 08:19:19 Reusing HOL
Nov 14 08:19:30 Starting developers
Nov 14 08:19:34 Finished developers                                               3s 207MB
Nov 14 08:19:35 Starting developers/bin
Nov 14 08:20:00 Finished developers/bin                                          23s   1GB
Nov 14 08:20:01 Starting compiler/proofs
Nov 14 10:02:47 Finished compiler/proofs                                    1h42m45s  34GB
Nov 14 10:02:47 Starting compiler/bootstrap/translation
Nov 14 19:12:17 Finished compiler/bootstrap/translation                     9h09m28s  85GB
Nov 14 19:12:17 Starting semantics/ffi
Nov 14 19:12:34 Finished semantics/ffi                                           15s   1GB
Nov 14 19:12:35 Starting semantics
Nov 14 19:12:36 Finished semantics                                                0s  62MB
Nov 14 19:12:37 Starting semantics/proofs
Nov 14 19:13:01 Finished semantics/proofs                                        22s 635MB
Nov 14 19:13:02 Starting semantics/alt_semantics
Nov 14 19:13:24 Finished semantics/alt_semantics                                 21s 645MB
Nov 14 19:13:25 Starting semantics/alt_semantics/proofs
Nov 14 19:23:26 Finished semantics/alt_semantics/proofs                       10m00s   2GB
Nov 14 19:23:27 Starting basis/pure
Nov 14 19:23:29 Finished basis/pure                                               0s  74MB
Nov 14 19:23:30 Starting translator
Nov 14 19:25:01 Finished translator                                            1m30s   2GB
Nov 14 19:25:02 Starting compiler/parsing
Nov 14 19:25:04 Finished compiler/parsing                                         0s  72MB
Nov 14 19:25:05 Starting characteristic
Nov 14 19:25:06 Finished characteristic                                           0s  93MB
Nov 14 19:25:07 Starting translator/monadic
Nov 14 19:25:09 Finished translator/monadic                                       0s 101MB
Nov 14 19:25:10 Starting basis
Nov 14 19:27:33 Finished basis                                                 2m21s   3GB
Nov 14 19:27:34 Starting compiler/inference
Nov 14 19:27:36 Finished compiler/inference                                       0s  92MB
Nov 14 19:27:37 Starting compiler/backend/reg_alloc
Nov 14 19:27:38 Finished compiler/backend/reg_alloc                               0s  65MB
Nov 14 19:27:39 Starting compiler/backend/gc
Nov 14 19:27:41 Finished compiler/backend/gc                                      1s 138MB
Nov 14 19:27:42 Starting compiler/backend
Nov 14 19:27:47 Finished compiler/backend                                         4s 325MB
Nov 14 19:27:48 Starting compiler/encoders/asm
Nov 14 19:27:50 Finished compiler/encoders/asm                                    0s  89MB
Nov 14 19:27:51 Starting compiler/encoders/x64
Nov 14 19:27:52 Finished compiler/encoders/x64                                    0s 102MB
Nov 14 19:27:53 Starting compiler/encoders/arm7
Nov 14 19:27:55 Finished compiler/encoders/arm7                                   0s 102MB
Nov 14 19:27:56 Starting compiler/encoders/arm8
Nov 14 19:27:58 Finished compiler/encoders/arm8                                   0s  98MB
Nov 14 19:27:59 Starting compiler/encoders/arm8_asl
Nov 14 19:30:11 Finished compiler/encoders/arm8_asl                            2m11s   1GB
Nov 14 19:30:12 Starting compiler/encoders/mips
Nov 14 19:30:13 Finished compiler/encoders/mips                                   0s  99MB
Nov 14 19:30:14 Starting compiler/encoders/riscv
Nov 14 19:30:16 Finished compiler/encoders/riscv                                  0s  99MB
Nov 14 19:30:17 Starting compiler/encoders/ag32
Nov 14 19:30:19 Finished compiler/encoders/ag32                                   0s  97MB
Nov 14 19:30:20 Starting compiler/backend/x64
Nov 14 19:30:22 Finished compiler/backend/x64                                     1s 139MB
Nov 14 19:30:23 Starting compiler/backend/arm7
Nov 14 19:30:25 Finished compiler/backend/arm7                                    1s 138MB
Nov 14 19:30:25 Starting compiler/backend/arm8
Nov 14 19:30:27 Finished compiler/backend/arm8                                    1s 138MB
Nov 14 19:30:28 Starting compiler/backend/mips
Nov 14 19:30:30 Finished compiler/backend/mips                                    1s 138MB
Nov 14 19:30:31 Starting compiler/backend/riscv
Nov 14 19:30:33 Finished compiler/backend/riscv                                   1s 138MB
Nov 14 19:30:34 Starting compiler/backend/ag32
Nov 14 19:31:45 Finished compiler/backend/ag32                                 1m09s   2GB
Nov 14 19:31:46 Starting compiler/parsing/proofs
Nov 14 19:31:48 Finished compiler/parsing/proofs                                  0s  75MB
Nov 14 19:31:49 Starting compiler/inference/proofs
Nov 14 19:31:50 Finished compiler/inference/proofs                                0s  99MB
Nov 14 19:31:51 Starting compiler/backend/semantics
Nov 14 19:35:01 Finished compiler/backend/semantics                            3m08s   3GB
Nov 14 19:35:02 Starting compiler/backend/reg_alloc/proofs
Nov 14 19:35:03 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Nov 14 19:35:04 Starting compiler/backend/proofs
Nov 14 19:35:59 Finished compiler/backend/proofs                                 53s   2GB
Nov 14 19:35:59 Starting compiler/backend/serialiser
Nov 14 19:36:02 Finished compiler/backend/serialiser                              1s 140MB
Nov 14 19:36:03 Starting compiler/encoders/x64/proofs
Nov 14 19:46:05 Finished compiler/encoders/x64/proofs                         10m01s   5GB
Nov 14 19:46:06 Starting compiler/encoders/arm7/proofs
Nov 14 19:59:02 Finished compiler/encoders/arm7/proofs                        12m55s   7GB
Nov 14 19:59:03 Starting compiler/encoders/arm8/proofs
Nov 14 20:06:09 Finished compiler/encoders/arm8/proofs                         7m04s   5GB
Nov 14 20:06:10 Starting compiler/encoders/arm8_asl/proofs
Nov 14 20:21:07 Finished compiler/encoders/arm8_asl/proofs                    14m55s   4GB
Nov 14 20:21:08 Starting compiler/encoders/mips/proofs
Nov 14 20:31:12 Finished compiler/encoders/mips/proofs                        10m02s   6GB
Nov 14 20:31:13 Starting compiler/encoders/riscv/proofs
Nov 14 20:39:17 Finished compiler/encoders/riscv/proofs                        8m03s   3GB
Nov 14 20:39:18 Starting compiler/encoders/ag32/proofs
Nov 14 20:42:11 Finished compiler/encoders/ag32/proofs                         2m51s   2GB
Nov 14 20:42:12 Starting compiler/backend/x64/proofs
Nov 14 20:42:58 Finished compiler/backend/x64/proofs                             45s   2GB
Nov 14 20:42:59 Starting compiler/backend/arm7/proofs
Nov 14 20:43:45 Finished compiler/backend/arm7/proofs                            44s   2GB
Nov 14 20:43:46 Starting compiler/backend/arm8/proofs
Nov 14 20:44:31 Finished compiler/backend/arm8/proofs                            44s   3GB
Nov 14 20:44:32 Starting compiler/backend/arm8_asl
Nov 14 20:45:04 Finished compiler/backend/arm8_asl                               30s   2GB
Nov 14 20:45:04 Starting compiler/backend/mips/proofs
Nov 14 20:45:53 Finished compiler/backend/mips/proofs                            47s   3GB
Nov 14 20:45:54 Starting compiler/backend/riscv/proofs
Nov 14 20:46:49 Finished compiler/backend/riscv/proofs                           54s   3GB
Nov 14 20:46:50 Starting compiler/backend/ag32/proofs
Nov 14 21:01:12 Finished compiler/backend/ag32/proofs                         14m21s   6GB
Nov 14 21:01:13 Starting compiler/backend/cv_compute
Nov 14 21:03:09 Finished compiler/backend/cv_compute                           1m55s   3GB
Nov 14 21:03:10 Starting cv_translator
Nov 14 21:22:40 Finished cv_translator                                        19m28s  13GB
Nov 14 21:22:41 Starting candle/set-theory
Nov 14 21:23:26 Finished candle/set-theory                                       43s   1GB
Nov 14 21:23:27 Starting candle/syntax-lib
Nov 14 21:23:28 Finished candle/syntax-lib                                        0s  69MB
Nov 14 21:23:29 Starting candle/standard/syntax
Nov 14 21:23:48 Finished candle/standard/syntax                                  18s   1GB
Nov 14 21:23:49 Starting candle/standard/semantics
Nov 14 21:26:33 Finished candle/standard/semantics                             2m43s   3GB
Nov 14 21:26:34 Starting candle/standard/monadic
Nov 14 21:26:36 Finished candle/standard/monadic                                  0s 102MB
Nov 14 21:26:37 Starting candle/standard/ml_kernel
Nov 14 21:28:40 Finished candle/standard/ml_kernel                             2m01s   5GB
Nov 14 21:28:41 Starting candle/overloading/syntax
Nov 14 21:32:15 Finished candle/overloading/syntax                             3m33s   2GB
Nov 14 21:32:16 Starting candle/overloading/semantics
Nov 14 21:43:45 Finished candle/overloading/semantics                         11m28s   4GB
Nov 14 21:43:46 Starting candle/overloading/monadic
Nov 14 21:46:10 Finished candle/overloading/monadic                            2m23s   2GB
Nov 14 21:46:11 Starting candle/overloading/ml_kernel
Nov 14 21:54:08 Finished candle/overloading/ml_kernel                          7m55s   7GB
Nov 14 21:54:09 Starting candle/overloading/ml_checker
Nov 14 21:56:55 Finished candle/overloading/ml_checker                         2m45s   7GB
Nov 14 21:56:56 Starting candle/prover
Nov 14 22:07:24 Finished candle/prover                                        10m27s   5GB
Nov 14 22:07:25 Starting pancake
Nov 14 22:07:51 Finished pancake                                                 25s 981MB
Nov 14 22:07:52 Starting pancake/ffi
Nov 14 22:07:54 Finished pancake/ffi                                              0s  22MB
Nov 14 22:07:55 Starting pancake/semantics
Nov 14 22:09:58 Finished pancake/semantics                                     2m02s   2GB
Nov 14 22:09:59 Starting pancake/parser
Nov 14 22:10:23 Finished pancake/parser                                          23s 520MB
Nov 14 22:10:23 Starting pancake/proofs
Nov 14 22:26:13 Finished pancake/proofs                                       15m48s   7GB
Nov 14 22:26:13 Starting compiler/dafny
Nov 14 22:28:51 Finished compiler/dafny                                        2m36s   8GB
Nov 14 22:28:52 Starting compiler/dafny/translation
Nov 14 22:57:19 Finished compiler/dafny/translation                           28m25s  15GB
Nov 14 22:57:20 Starting compiler/dafny/compilation
Nov 14 22:59:55 Finished compiler/dafny/compilation                            2m34s  10GB
Nov 14 22:59:56 Starting compiler/dafny/semantics
Nov 14 23:00:31 Finished compiler/dafny/semantics                                34s   1GB
Nov 14 23:00:32 Starting characteristic/examples
Nov 14 23:02:02 Finished characteristic/examples                               1m28s   5GB
Nov 14 23:02:03 Starting tutorial/solutions
Nov 14 23:04:38 Finished tutorial/solutions                                    2m34s   4GB
Nov 14 23:04:39 Starting translator/monadic/examples
Nov 14 23:07:42 Finished translator/monadic/examples                           3m02s   4GB
Nov 14 23:07:43 Starting examples
Nov 14 23:19:51 Finished examples                                             12m07s   3GB
Nov 14 23:19:52 Starting examples/compilation/x64
Nov 14 23:27:46 Finished examples/compilation/x64                              7m53s   7GB
Nov 14 23:27:47 Starting examples/compilation/x64/proofs
Nov 14 23:32:45 Finished examples/compilation/x64/proofs                       4m56s   7GB
Nov 14 23:32:46 Starting examples/compilation/ag32
Nov 14 23:35:02 Finished examples/compilation/ag32                             2m15s   3GB
Nov 14 23:35:03 Starting examples/compilation/ag32/proofs
Nov 14 23:36:50 Finished examples/compilation/ag32/proofs                      1m46s   8GB
Nov 14 23:36:51 Starting examples/compilation/to_word
Nov 14 23:41:14 Finished examples/compilation/to_word                          4m22s  12GB
Nov 14 23:41:15 Starting examples/lpr_checker
Nov 14 23:41:45 Finished examples/lpr_checker                                    29s   1GB
Nov 14 23:41:46 Starting examples/lpr_checker/array
Nov 15 00:07:56 Finished examples/lpr_checker/array                           26m08s  26GB
Nov 15 00:07:57 Starting examples/lpr_checker/array/compilation
Nov 15 00:09:47 Finished examples/lpr_checker/array/compilation                1m49s   7GB
Nov 15 00:09:48 Starting examples/lpr_checker/array/compilation/proofs
Nov 15 00:11:58 Finished examples/lpr_checker/array/compilation/proofs         2m09s   7GB
Nov 15 00:11:59 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 15 00:13:57 Finished examples/lpr_checker/array/compilation/proofsARM8     1m57s  10GB
Nov 15 00:13:58 Starting examples/xlrup_checker
Nov 15 00:14:33 Finished examples/xlrup_checker                                  33s   1GB
Nov 15 00:14:34 Starting examples/xlrup_checker/array
Nov 15 00:27:35 Finished examples/xlrup_checker/array                         13m00s  10GB
Nov 15 00:27:36 Starting examples/xlrup_checker/array/compilation
Nov 15 00:28:38 Finished examples/xlrup_checker/array/compilation              1m01s   4GB
Nov 15 00:28:39 Starting examples/xlrup_checker/array/compilation/proofs
Nov 15 00:30:32 Finished examples/xlrup_checker/array/compilation/proofs       1m51s   7GB
Nov 15 00:30:33 Starting examples/pseudo_bool
Nov 15 00:32:04 Finished examples/pseudo_bool                                  1m30s   2GB
Nov 15 00:32:05 Starting examples/pseudo_bool/cnf_encoding
Nov 15 00:32:46 Finished examples/pseudo_bool/cnf_encoding                       40s   1GB
Nov 15 00:32:47 Starting examples/pseudo_bool/graph_encoding
Nov 15 00:33:43 Finished examples/pseudo_bool/graph_encoding                     54s   2GB
Nov 15 00:33:43 Starting examples/pseudo_bool/array
Nov 15 01:41:46 Finished examples/pseudo_bool/array                         1h08m01s  40GB
Nov 15 01:41:47 Starting examples/pseudo_bool/array/compilation
Nov 15 01:50:45 Finished examples/pseudo_bool/array/compilation                8m57s  16GB
Nov 15 01:50:46 Starting examples/pseudo_bool/array/compilation/proofs
Nov 15 01:55:10 Finished examples/pseudo_bool/array/compilation/proofs         4m22s  10GB
Nov 15 01:55:11 Starting examples/pseudo_bool/array/compilation/proofsARM8
Nov 15 01:57:10 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m58s   9GB
Nov 15 01:57:11 Starting examples/opentheory
Nov 15 02:05:48 Finished examples/opentheory                                   8m35s   5GB
Nov 15 02:05:49 Starting examples/opentheory
Nov 15 02:05:51 Finished examples/opentheory                                      1s 135MB
Nov 15 02:05:52 Starting examples/opentheory/compilation
Nov 15 02:05:55 FAILED: examples/opentheory/compilation
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
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)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
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 $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
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/model
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/model
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/model
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/model
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)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/cv_translator
Holmake: Attempt to recurse into non-existent directory: $(CAKEMLDIR)/examples/cost
  (Probably a result of bad INCLUDES spec.)