Job 2700

CakeML:32a02d3fee1a1f74f39ebde9a9ea5dbf8507c0c8
  Remove non-working example [Nov 13 19:43:05]
#1092 (cost)
Merging into:6b2039e9c365bca1bb05f521e2c6060d6a901bdb
  Merge pull request #1094 from CakeML/tweak-root-dir [Nov 23 20:15:27]
HOL:2de6b3ccc36da9c19998787a835c3ef9c81466fe
  Add a cute problem to examples/misc [Oct 30 04:33:10]
Machine:pavlova

Nov 23 20:27:50 Claimed job
Nov 23 20:27:54 Reusing HOL
Nov 23 20:28:06 Starting developers
Nov 23 20:28:10 Finished developers                                               3s 201MB
Nov 23 20:28:11 Starting developers/bin
Nov 23 20:28:27 Finished developers/bin                                          15s   1GB
Nov 23 20:28:28 Starting compiler/proofs
Nov 23 22:09:52 Finished compiler/proofs                                    1h41m22s  41GB
Nov 23 22:09:53 Starting compiler/bootstrap/translation
Nov 25 19:12:37 Resuming compiler/bootstrap/translation
Nov 25 19:12:41 Finished compiler/bootstrap/translation                           3s 265MB
Nov 25 19:12:42 Starting semantics/ffi
Nov 25 19:12:59 Finished semantics/ffi                                           15s   1GB
Nov 25 19:13:00 Starting semantics
Nov 25 19:13:01 Finished semantics                                                0s  63MB
Nov 25 19:13:02 Starting semantics/proofs
Nov 25 19:13:26 Finished semantics/proofs                                        23s 777MB
Nov 25 19:13:27 Starting semantics/alt_semantics
Nov 25 19:13:50 Finished semantics/alt_semantics                                 22s 688MB
Nov 25 19:13:51 Starting semantics/alt_semantics/proofs
Nov 25 19:24:17 Finished semantics/alt_semantics/proofs                       10m25s   3GB
Nov 25 19:24:18 Starting basis/pure
Nov 25 19:24:20 Finished basis/pure                                               0s  69MB
Nov 25 19:24:21 Starting translator
Nov 25 19:25:59 Finished translator                                            1m37s   2GB
Nov 25 19:26:00 Starting compiler/parsing
Nov 25 19:26:01 Finished compiler/parsing                                         0s  71MB
Nov 25 19:26:02 Starting characteristic
Nov 25 19:26:04 Finished characteristic                                           0s  96MB
Nov 25 19:26:05 Starting translator/monadic
Nov 25 19:26:07 Finished translator/monadic                                       0s  95MB
Nov 25 19:26:07 Starting basis
Nov 25 19:28:32 Finished basis                                                 2m23s   4GB
Nov 25 19:28:33 Starting compiler/inference
Nov 25 19:28:35 Finished compiler/inference                                       0s  95MB
Nov 25 19:28:36 Starting compiler/backend/reg_alloc
Nov 25 19:28:37 Finished compiler/backend/reg_alloc                               0s  67MB
Nov 25 19:28:38 Starting compiler/backend/gc
Nov 25 19:28:40 Finished compiler/backend/gc                                      1s 140MB
Nov 25 19:28:41 Starting compiler/backend
Nov 25 19:28:46 Finished compiler/backend                                         4s 319MB
Nov 25 19:28:47 Starting compiler/encoders/asm
Nov 25 19:28:49 Finished compiler/encoders/asm                                    0s  99MB
Nov 25 19:28:50 Starting compiler/encoders/x64
Nov 25 19:28:51 Finished compiler/encoders/x64                                    0s  98MB
Nov 25 19:28:52 Starting compiler/encoders/arm7
Nov 25 19:28:54 Finished compiler/encoders/arm7                                   0s  98MB
Nov 25 19:28:55 Starting compiler/encoders/arm8
Nov 25 19:28:57 Finished compiler/encoders/arm8                                   0s  98MB
Nov 25 19:28:58 Starting compiler/encoders/arm8_asl
Nov 25 19:31:13 Finished compiler/encoders/arm8_asl                            2m14s   1GB
Nov 25 19:31:14 Starting compiler/encoders/mips
Nov 25 19:31:15 Finished compiler/encoders/mips                                   0s  99MB
Nov 25 19:31:16 Starting compiler/encoders/riscv
Nov 25 19:31:18 Finished compiler/encoders/riscv                                  0s  99MB
Nov 25 19:31:19 Starting compiler/encoders/ag32
Nov 25 19:31:20 Finished compiler/encoders/ag32                                   0s  99MB
Nov 25 19:31:21 Starting compiler/backend/x64
Nov 25 19:31:23 Finished compiler/backend/x64                                     1s 138MB
Nov 25 19:31:24 Starting compiler/backend/arm7
Nov 25 19:31:26 Finished compiler/backend/arm7                                    1s 138MB
Nov 25 19:31:27 Starting compiler/backend/arm8
Nov 25 19:31:29 Finished compiler/backend/arm8                                    1s 138MB
Nov 25 19:31:30 Starting compiler/backend/mips
Nov 25 19:31:32 Finished compiler/backend/mips                                    1s 138MB
Nov 25 19:31:33 Starting compiler/backend/riscv
Nov 25 19:31:35 Finished compiler/backend/riscv                                   1s 138MB
Nov 25 19:31:36 Starting compiler/backend/ag32
Nov 25 19:32:49 Finished compiler/backend/ag32                                 1m11s   2GB
Nov 25 19:32:49 Starting compiler/parsing/proofs
Nov 25 19:32:51 Finished compiler/parsing/proofs                                  0s  75MB
Nov 25 19:32:52 Starting compiler/inference/proofs
Nov 25 19:32:54 Finished compiler/inference/proofs                                0s 100MB
Nov 25 19:32:55 Starting compiler/backend/semantics
Nov 25 19:36:15 Finished compiler/backend/semantics                            3m19s   2GB
Nov 25 19:36:15 Starting compiler/backend/reg_alloc/proofs
Nov 25 19:36:17 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Nov 25 19:36:18 Starting compiler/backend/proofs
Nov 25 19:37:18 Finished compiler/backend/proofs                                 59s   5GB
Nov 25 19:37:19 Starting compiler/backend/serialiser
Nov 25 19:37:21 Finished compiler/backend/serialiser                              1s 139MB
Nov 25 19:37:22 Starting compiler/encoders/x64/proofs
Nov 25 19:47:43 Finished compiler/encoders/x64/proofs                         10m20s   5GB
Nov 25 19:47:44 Starting compiler/encoders/arm7/proofs
Nov 25 20:00:55 Finished compiler/encoders/arm7/proofs                        13m10s   8GB
Nov 25 20:00:56 Starting compiler/encoders/arm8/proofs
Nov 25 20:07:51 Finished compiler/encoders/arm8/proofs                         6m53s   5GB
Nov 25 20:07:52 Starting compiler/encoders/arm8_asl/proofs
Nov 25 20:23:22 Finished compiler/encoders/arm8_asl/proofs                    15m29s   4GB
Nov 25 20:23:23 Starting compiler/encoders/mips/proofs
Nov 25 20:33:46 Finished compiler/encoders/mips/proofs                        10m22s   8GB
Nov 25 20:33:47 Starting compiler/encoders/riscv/proofs
Nov 25 20:42:20 Finished compiler/encoders/riscv/proofs                        8m31s   5GB
Nov 25 20:42:21 Starting compiler/encoders/ag32/proofs
Nov 25 20:45:17 Finished compiler/encoders/ag32/proofs                         2m55s   2GB
Nov 25 20:45:18 Starting compiler/backend/x64/proofs
Nov 25 20:46:05 Finished compiler/backend/x64/proofs                             45s   2GB
Nov 25 20:46:06 Starting compiler/backend/arm7/proofs
Nov 25 20:46:53 Finished compiler/backend/arm7/proofs                            46s   3GB
Nov 25 20:46:54 Starting compiler/backend/arm8/proofs
Nov 25 20:47:41 Finished compiler/backend/arm8/proofs                            45s   3GB
Nov 25 20:47:42 Starting compiler/backend/arm8_asl
Nov 25 20:48:09 Finished compiler/backend/arm8_asl                               26s   1GB
Nov 25 20:48:10 Starting compiler/backend/mips/proofs
Nov 25 20:48:59 Finished compiler/backend/mips/proofs                            47s   3GB
Nov 25 20:49:00 Starting compiler/backend/riscv/proofs
Nov 25 20:49:56 Finished compiler/backend/riscv/proofs                           55s   3GB
Nov 25 20:49:57 Starting compiler/backend/ag32/proofs
Nov 25 21:04:27 Finished compiler/backend/ag32/proofs                         14m28s   6GB
Nov 25 21:04:28 Starting compiler/backend/cv_compute
Nov 25 21:06:21 Finished compiler/backend/cv_compute                           1m52s   3GB
Nov 25 21:06:22 Starting cv_translator
Nov 25 21:26:11 Finished cv_translator                                        19m48s  13GB
Nov 25 21:26:12 Starting candle/set-theory
Nov 25 21:27:00 Finished candle/set-theory                                       47s   1GB
Nov 25 21:27:01 Starting candle/syntax-lib
Nov 25 21:27:03 Finished candle/syntax-lib                                        0s  68MB
Nov 25 21:27:03 Starting candle/standard/syntax
Nov 25 21:27:24 Finished candle/standard/syntax                                  19s   1GB
Nov 25 21:27:25 Starting candle/standard/semantics
Nov 25 21:30:05 Finished candle/standard/semantics                             2m38s   2GB
Nov 25 21:30:05 Starting candle/standard/monadic
Nov 25 21:30:07 Finished candle/standard/monadic                                  0s 103MB
Nov 25 21:30:08 Starting candle/standard/ml_kernel
Nov 25 21:32:14 Finished candle/standard/ml_kernel                             2m05s   5GB
Nov 25 21:32:15 Starting candle/overloading/syntax
Nov 25 21:35:50 Finished candle/overloading/syntax                             3m33s   2GB
Nov 25 21:35:50 Starting candle/overloading/semantics
Nov 25 21:47:28 Finished candle/overloading/semantics                         11m36s   4GB
Nov 25 21:47:29 Starting candle/overloading/monadic
Nov 25 21:49:54 Finished candle/overloading/monadic                            2m24s   2GB
Nov 25 21:49:55 Starting candle/overloading/ml_kernel
Nov 25 21:57:51 Finished candle/overloading/ml_kernel                          7m55s   6GB
Nov 25 21:57:52 Starting candle/overloading/ml_checker
Nov 25 22:00:39 Finished candle/overloading/ml_checker                         2m46s   7GB
Nov 25 22:00:40 Starting candle/prover
Nov 25 22:11:06 Finished candle/prover                                        10m25s   5GB
Nov 25 22:11:07 Starting pancake
Nov 25 22:11:33 Finished pancake                                                 24s 949MB
Nov 25 22:11:34 Starting pancake/ffi
Nov 25 22:11:35 Finished pancake/ffi                                              0s  16MB
Nov 25 22:11:35 Starting pancake/semantics
Nov 25 22:13:44 Finished pancake/semantics                                     2m07s   1GB
Nov 25 22:13:45 Starting pancake/parser
Nov 25 22:14:09 Finished pancake/parser                                          23s 537MB
Nov 25 22:14:10 Starting pancake/proofs
Nov 25 22:30:23 Finished pancake/proofs                                       16m12s   7GB
Nov 25 22:30:24 Starting compiler/dafny
Nov 25 22:33:00 Finished compiler/dafny                                        2m35s  11GB
Nov 25 22:33:01 Starting compiler/dafny/translation
Nov 25 23:01:56 Finished compiler/dafny/translation                           28m53s  19GB
Nov 25 23:01:57 Starting compiler/dafny/compilation
Nov 25 23:04:30 Finished compiler/dafny/compilation                            2m32s   9GB
Nov 25 23:04:31 Starting compiler/dafny/semantics
Nov 25 23:05:06 Finished compiler/dafny/semantics                                33s   1GB
Nov 25 23:05:06 Starting characteristic/examples
Nov 25 23:06:39 Finished characteristic/examples                               1m31s   5GB
Nov 25 23:06:39 Starting tutorial/solutions
Nov 25 23:09:11 Finished tutorial/solutions                                    2m30s   3GB
Nov 25 23:09:12 Starting translator/monadic/examples
Nov 25 23:12:20 Finished translator/monadic/examples                           3m06s   4GB
Nov 25 23:12:21 Starting examples
Nov 25 23:24:39 Finished examples                                             12m17s   4GB
Nov 25 23:24:40 Starting examples/compilation/x64
Nov 25 23:32:35 Finished examples/compilation/x64                              7m53s   7GB
Nov 25 23:32:36 Starting examples/compilation/x64/proofs
Nov 25 23:37:40 Finished examples/compilation/x64/proofs                       5m02s   8GB
Nov 25 23:37:40 Starting examples/compilation/ag32
Nov 25 23:39:57 Finished examples/compilation/ag32                             2m15s   3GB
Nov 25 23:39:58 Starting examples/compilation/ag32/proofs
Nov 25 23:41:46 Finished examples/compilation/ag32/proofs                      1m47s   9GB
Nov 25 23:41:47 Starting examples/compilation/to_word
Nov 25 23:46:00 Finished examples/compilation/to_word                          4m12s  13GB
Nov 25 23:46:01 Starting examples/lpr_checker
Nov 25 23:46:32 Finished examples/lpr_checker                                    29s   1GB
Nov 25 23:46:32 Starting examples/lpr_checker/array
Nov 26 00:12:49 Finished examples/lpr_checker/array                           26m15s  18GB
Nov 26 00:12:50 Starting examples/lpr_checker/array/compilation
Nov 26 00:14:40 Finished examples/lpr_checker/array/compilation                1m49s   7GB
Nov 26 00:14:41 Starting examples/lpr_checker/array/compilation/proofs
Nov 26 00:16:42 Finished examples/lpr_checker/array/compilation/proofs         1m59s   7GB
Nov 26 00:16:42 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 26 00:18:38 Finished examples/lpr_checker/array/compilation/proofsARM8     1m54s   9GB
Nov 26 00:18:39 Starting .
Nov 26 00:18:42 Finished .                                                        2s 305MB
Nov 26 00:18:43 Starting examples/xlrup_checker
Nov 26 00:19:18 Finished examples/xlrup_checker                                  33s   1GB
Nov 26 00:19:19 Starting examples/xlrup_checker/array
Nov 26 00:32:26 Finished examples/xlrup_checker/array                         13m06s  10GB
Nov 26 00:32:27 Starting examples/xlrup_checker/array/compilation
Nov 26 00:33:29 Finished examples/xlrup_checker/array/compilation              1m01s   4GB
Nov 26 00:33:30 Starting examples/xlrup_checker/array/compilation/proofs
Nov 26 00:35:23 Finished examples/xlrup_checker/array/compilation/proofs       1m51s   7GB
Nov 26 00:35:23 Starting examples/pseudo_bool
Nov 26 00:36:55 Finished examples/pseudo_bool                                  1m30s   2GB
Nov 26 00:36:56 Starting examples/pseudo_bool/cnf_encoding
Nov 26 00:37:36 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
Nov 26 00:37:37 Starting examples/pseudo_bool/graph_encoding
Nov 26 00:38:32 Finished examples/pseudo_bool/graph_encoding                     53s   1GB
Nov 26 00:38:33 Starting examples/pseudo_bool/array
Nov 26 01:47:08 Finished examples/pseudo_bool/array                         1h08m33s  33GB
Nov 26 01:47:09 Starting examples/pseudo_bool/array/compilation
Nov 26 01:56:00 Finished examples/pseudo_bool/array/compilation                8m50s  16GB
Nov 26 01:56:01 Starting examples/pseudo_bool/array/compilation/proofs
Nov 26 02:00:20 Finished examples/pseudo_bool/array/compilation/proofs         4m17s   9GB
Nov 26 02:00:21 Starting examples/pseudo_bool/array/compilation/proofsARM8
Nov 26 02:02:20 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m58s   9GB
Nov 26 02:02:21 Starting examples/opentheory
Nov 26 02:11:08 Finished examples/opentheory                                   8m46s   5GB
Nov 26 02:11:09 Starting examples/opentheory
Nov 26 02:11:11 Finished examples/opentheory                                      1s 126MB
Nov 26 02:11:12 Starting examples/opentheory/compilation
Nov 26 02:11:15 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.)