Job 2782

CakeML:34d3cdee4e7807003f08e8f9d19cb70a9076dff9
  Streamline license [Mar 10 14:42:51]
#1141 (dnezam-patch-1)
Merging into:07721cefa5b73bcac8da63d63b20ed0079564b51
  Merge pull request #1140 from CakeML/discord-to-zulip [Mar 10 12:11:14]
HOL:cfe1cccd3fc0aa4459e8cc8312f9ec0c959e3678
  Modify emacs mode to make it fall into line with new open behaviours [Mar 08 02:37:25]
Machine:pavlova

Mar 11 23:29:25 Claimed job
Mar 11 23:29:33 Building HOL
Mar 11 23:40:29 Starting developers
Mar 11 23:40:33 Finished developers                                               3s 204MB
Mar 11 23:40:34 Starting developers/bin
Mar 11 23:40:40 Finished developers/bin                                           5s 746MB
Mar 11 23:40:41 Starting misc
Mar 11 23:41:41 Finished misc                                                    58s   2GB
Mar 11 23:41:42 Starting compiler/proofs
Mar 12 01:22:25 Finished compiler/proofs                                    1h40m41s  25GB
Mar 12 01:22:26 Starting compiler/bootstrap/translation
Mar 12 07:09:18 Finished compiler/bootstrap/translation                     5h46m50s  62GB
Mar 12 07:09:19 Starting semantics/ffi
Mar 12 07:09:29 Finished semantics/ffi                                            9s 596MB
Mar 12 07:09:30 Starting semantics
Mar 12 07:09:31 Finished semantics                                                0s  54MB
Mar 12 07:09:32 Starting semantics/proofs
Mar 12 07:09:55 Finished semantics/proofs                                        22s 727MB
Mar 12 07:09:56 Starting semantics/alt_semantics
Mar 12 07:10:17 Finished semantics/alt_semantics                                 19s 899MB
Mar 12 07:10:18 Starting semantics/alt_semantics/proofs
Mar 12 07:20:33 Finished semantics/alt_semantics/proofs                       10m13s   2GB
Mar 12 07:20:34 Starting basis/pure
Mar 12 07:20:35 Finished basis/pure                                               0s  94MB
Mar 12 07:20:36 Starting translator
Mar 12 07:22:09 Finished translator                                            1m31s   2GB
Mar 12 07:22:10 Starting compiler/parsing
Mar 12 07:22:11 Finished compiler/parsing                                         0s  61MB
Mar 12 07:22:12 Starting characteristic
Mar 12 07:22:14 Finished characteristic                                           1s 119MB
Mar 12 07:22:15 Starting translator/monadic
Mar 12 07:22:17 Finished translator/monadic                                       1s 117MB
Mar 12 07:22:18 Starting translator/monadic/monad_base
Mar 12 07:22:19 Finished translator/monadic/monad_base                            0s  54MB
Mar 12 07:22:20 Starting basis
Mar 12 07:24:40 Finished basis                                                 2m18s   3GB
Mar 12 07:24:41 Starting compiler
Mar 12 07:24:44 Finished compiler                                                 1s 217MB
Mar 12 07:24:45 Starting compiler/inference
Mar 12 07:24:47 Finished compiler/inference                                       1s 112MB
Mar 12 07:24:47 Starting compiler/backend/reg_alloc
Mar 12 07:24:49 Finished compiler/backend/reg_alloc                               0s  58MB
Mar 12 07:24:50 Starting compiler/backend/gc
Mar 12 07:24:52 Finished compiler/backend/gc                                      1s 144MB
Mar 12 07:24:53 Starting compiler/backend
Mar 12 07:24:58 Finished compiler/backend                                         4s 244MB
Mar 12 07:24:59 Starting compiler/encoders/asm
Mar 12 07:25:00 Finished compiler/encoders/asm                                    0s  84MB
Mar 12 07:25:01 Starting compiler/encoders/x64
Mar 12 07:25:03 Finished compiler/encoders/x64                                    0s  89MB
Mar 12 07:25:04 Starting compiler/encoders/arm7
Mar 12 07:25:05 Finished compiler/encoders/arm7                                   0s  90MB
Mar 12 07:25:06 Starting compiler/encoders/arm8
Mar 12 07:25:08 Finished compiler/encoders/arm8                                   0s  89MB
Mar 12 07:25:09 Starting compiler/encoders/arm8_asl
Mar 12 09:25:17 Finished compiler/encoders/arm8_asl                         2h00m06s  28GB
Mar 12 09:25:18 Starting compiler/encoders/mips
Mar 12 09:25:19 Finished compiler/encoders/mips                                   0s  83MB
Mar 12 09:25:20 Starting compiler/encoders/riscv
Mar 12 09:25:22 Finished compiler/encoders/riscv                                  0s  87MB
Mar 12 09:25:23 Starting compiler/encoders/ag32
Mar 12 09:25:24 Finished compiler/encoders/ag32                                   0s  80MB
Mar 12 09:25:25 Starting compiler/encoders/tests
Mar 12 09:25:27 Finished compiler/encoders/tests                                  1s 115MB
Mar 12 09:25:28 Starting compiler/encoders/monadic_enc
Mar 12 09:25:30 Finished compiler/encoders/monadic_enc                            1s 139MB
Mar 12 09:25:31 Starting compiler/backend/x64
Mar 12 09:25:33 Finished compiler/backend/x64                                     1s 137MB
Mar 12 09:25:34 Starting compiler/backend/arm7
Mar 12 09:25:36 Finished compiler/backend/arm7                                    1s 142MB
Mar 12 09:25:37 Starting compiler/backend/arm8
Mar 12 09:25:39 Finished compiler/backend/arm8                                    1s 143MB
Mar 12 09:25:40 Starting compiler/backend/mips
Mar 12 09:25:42 Finished compiler/backend/mips                                    1s 143MB
Mar 12 09:25:43 Starting compiler/backend/riscv
Mar 12 09:25:45 Finished compiler/backend/riscv                                   1s 138MB
Mar 12 09:25:46 Starting compiler/backend/ag32
Mar 12 09:26:53 Finished compiler/backend/ag32                                 1m05s   2GB
Mar 12 09:26:54 Starting compiler/backend/pattern_matching
Mar 12 09:26:55 Finished compiler/backend/pattern_matching                        0s  52MB
Mar 12 09:26:56 Starting compiler/parsing/ocaml
Mar 12 09:28:38 Finished compiler/parsing/ocaml                                1m41s   1GB
Mar 12 09:28:39 Starting compiler/printing
Mar 12 09:28:41 Finished compiler/printing                                        1s 116MB
Mar 12 09:28:42 Starting compiler/parsing/proofs
Mar 12 09:28:43 Finished compiler/parsing/proofs                                  0s  63MB
Mar 12 09:28:44 Starting compiler/inference/proofs
Mar 12 09:28:46 Finished compiler/inference/proofs                                1s 113MB
Mar 12 09:28:47 Starting compiler/backend/semantics
Mar 12 09:31:51 Finished compiler/backend/semantics                            3m02s   3GB
Mar 12 09:31:52 Starting compiler/backend/reg_alloc/proofs
Mar 12 09:31:54 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Mar 12 09:31:55 Starting compiler/backend/proofs
Mar 12 09:32:43 Finished compiler/backend/proofs                                 47s   2GB
Mar 12 09:32:44 Starting compiler/backend/serialiser
Mar 12 09:32:46 Finished compiler/backend/serialiser                              1s 143MB
Mar 12 09:32:47 Starting compiler/encoders/x64/proofs
Mar 12 09:42:53 Finished compiler/encoders/x64/proofs                         10m04s   4GB
Mar 12 09:42:54 Starting compiler/encoders/arm7/proofs
Mar 12 09:56:16 Finished compiler/encoders/arm7/proofs                        13m21s  11GB
Mar 12 09:56:17 Starting compiler/encoders/arm8/proofs
Mar 12 10:03:28 Finished compiler/encoders/arm8/proofs                         7m09s   4GB
Mar 12 10:03:29 Starting compiler/encoders/arm8_asl/proofs
Mar 12 10:52:25 Finished compiler/encoders/arm8_asl/proofs                    48m54s  20GB
Mar 12 10:52:26 Starting compiler/encoders/mips/proofs
Mar 12 11:02:47 Finished compiler/encoders/mips/proofs                        10m19s   5GB
Mar 12 11:02:47 Starting compiler/encoders/riscv/proofs
Mar 12 11:10:52 Finished compiler/encoders/riscv/proofs                        8m03s   4GB
Mar 12 11:10:53 Starting compiler/encoders/ag32/proofs
Mar 12 11:13:44 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
Mar 12 11:13:44 Starting compiler/backend/x64/proofs
Mar 12 11:14:15 Finished compiler/backend/x64/proofs                             29s   2GB
Mar 12 11:14:16 Starting compiler/backend/arm7/proofs
Mar 12 11:14:46 Finished compiler/backend/arm7/proofs                            29s   1GB
Mar 12 11:14:47 Starting compiler/backend/arm8/proofs
Mar 12 11:15:20 Finished compiler/backend/arm8/proofs                            32s   2GB
Mar 12 11:15:21 Starting compiler/backend/arm8_asl
Mar 12 11:15:42 Finished compiler/backend/arm8_asl                               19s   1GB
Mar 12 11:15:43 Starting compiler/backend/mips/proofs
Mar 12 11:16:13 Finished compiler/backend/mips/proofs                            29s   2GB
Mar 12 11:16:14 Starting compiler/backend/riscv/proofs
Mar 12 11:16:48 Finished compiler/backend/riscv/proofs                           33s   2GB
Mar 12 11:16:49 Starting compiler/backend/ag32/proofs
Mar 12 11:30:44 Finished compiler/backend/ag32/proofs                         13m53s   3GB
Mar 12 11:30:45 Starting compiler/backend/cv_compute
Mar 12 11:31:56 Finished compiler/backend/cv_compute                           1m09s   2GB
Mar 12 11:31:57 Starting cv_translator
Mar 12 11:52:50 Finished cv_translator                                        20m51s   7GB
Mar 12 11:52:51 Starting candle
Mar 12 11:52:52 Finished candle                                                   0s  11MB
Mar 12 11:52:53 Starting candle/set-theory
Mar 12 11:53:28 Finished candle/set-theory                                       33s   1GB
Mar 12 11:53:29 Starting candle/syntax-lib
Mar 12 11:53:31 Finished candle/syntax-lib                                        0s  90MB
Mar 12 11:53:31 Starting candle/standard
Mar 12 11:53:32 Finished candle/standard                                          0s  10MB
Mar 12 11:53:33 Starting candle/standard/syntax
Mar 12 11:53:46 Finished candle/standard/syntax                                  11s 806MB
Mar 12 11:53:47 Starting candle/standard/semantics
Mar 12 11:55:49 Finished candle/standard/semantics                             2m01s   1GB
Mar 12 11:55:50 Starting candle/standard/monadic
Mar 12 11:55:52 Finished candle/standard/monadic                                  1s 119MB
Mar 12 11:55:53 Starting candle/standard/ml_kernel
Mar 12 11:57:35 Finished candle/standard/ml_kernel                             1m41s   4GB
Mar 12 11:57:36 Starting candle/standard/ml_kernel/lisp
Mar 12 11:57:37 Finished candle/standard/ml_kernel/lisp                           0s  48MB
Mar 12 11:57:38 Starting candle/overloading
Mar 12 11:57:39 Finished candle/overloading                                       0s  11MB
Mar 12 11:57:40 Starting candle/overloading/syntax
Mar 12 12:00:47 Finished candle/overloading/syntax                             3m06s   2GB
Mar 12 12:00:48 Starting candle/overloading/semantics
Mar 12 12:11:57 Finished candle/overloading/semantics                         11m08s   4GB
Mar 12 12:11:58 Starting candle/overloading/monadic
Mar 12 12:14:15 Finished candle/overloading/monadic                            2m16s   2GB
Mar 12 12:14:16 Starting candle/overloading/ml_kernel
Mar 12 12:21:24 Finished candle/overloading/ml_kernel                          7m06s   5GB
Mar 12 12:21:25 Starting candle/overloading/ml_checker
Mar 12 12:23:36 Finished candle/overloading/ml_checker                         2m10s   6GB
Mar 12 12:23:37 Starting candle/prover
Mar 12 12:33:15 Finished candle/prover                                         9m36s   5GB
Mar 12 12:33:15 Starting candle/prover/compute
Mar 12 12:33:18 Finished candle/prover/compute                                    1s 145MB
Mar 12 12:33:19 Starting pancake
Mar 12 12:33:41 Finished pancake                                                 21s 844MB
Mar 12 12:33:42 Starting pancake/semantics
Mar 12 12:35:48 Finished pancake/semantics                                     2m05s   1GB
Mar 12 12:35:49 Starting pancake/parser
Mar 12 12:36:13 Finished pancake/parser                                          22s 441MB
Mar 12 12:36:14 Starting pancake/static_checker
Mar 12 12:36:51 Finished pancake/static_checker                                  36s   1GB
Mar 12 12:36:52 Starting pancake/proofs
Mar 12 12:53:00 Finished pancake/proofs                                       16m05s   8GB
Mar 12 12:53:00 Starting pancake/ta_progs
Mar 12 12:53:01 Finished pancake/ta_progs                                         0s  12MB
Mar 12 12:53:02 Starting compiler/dafny
Mar 12 12:55:53 Finished compiler/dafny                                        2m49s  12GB
Mar 12 12:55:53 Starting compiler/dafny/translation
Mar 12 13:15:02 Finished compiler/dafny/translation                           19m07s  20GB
Mar 12 13:15:03 Starting compiler/dafny/compilation
Mar 12 13:18:08 Finished compiler/dafny/compilation                            3m03s  11GB
Mar 12 13:18:09 Starting compiler/dafny/semantics
Mar 12 13:18:45 Finished compiler/dafny/semantics                                35s   1GB
Mar 12 13:18:46 Starting characteristic/examples
Mar 12 13:20:10 Finished characteristic/examples                               1m22s   4GB
Mar 12 13:20:11 Starting tutorial/solutions
Mar 12 13:22:34 Finished tutorial/solutions                                    2m21s   3GB
Mar 12 13:22:34 Starting translator/monadic/examples
Mar 12 13:25:29 Finished translator/monadic/examples                           2m53s   3GB
Mar 12 13:25:30 Starting examples
Mar 12 13:31:34 Finished examples                                              6m02s   4GB
Mar 12 13:31:35 Starting examples/compilation
Mar 12 13:31:36 Finished examples/compilation                                     0s  12MB
Mar 12 13:31:37 Starting examples/compilation/x64
Mar 12 13:38:40 Finished examples/compilation/x64                              7m02s   4GB
Mar 12 13:38:41 Starting examples/compilation/x64/proofs
Mar 12 13:41:08 Finished examples/compilation/x64/proofs                       2m25s   4GB
Mar 12 13:41:09 Starting examples/compilation/ag32
Mar 12 13:43:06 Finished examples/compilation/ag32                             1m55s   3GB
Mar 12 13:43:07 Starting examples/compilation/ag32/proofs
Mar 12 13:44:08 Finished examples/compilation/ag32/proofs                      1m00s   5GB
Mar 12 13:44:09 Starting examples/lpr_checker
Mar 12 13:44:40 Finished examples/lpr_checker                                    30s   1GB
Mar 12 13:44:41 Starting examples/lpr_checker/array
Mar 12 14:10:29 Finished examples/lpr_checker/array                           25m46s  23GB
Mar 12 14:10:30 Starting examples/lpr_checker/array/compilation
Mar 12 15:24:20 Finished examples/lpr_checker/array/compilation             1h13m48s 262GB
Mar 12 15:24:21 Starting examples/lpr_checker/array/compilation/proofs
Mar 12 15:25:33 Finished examples/lpr_checker/array/compilation/proofs         1m11s   6GB
Mar 12 15:25:34 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 12 15:26:42 Finished examples/lpr_checker/array/compilation/proofsARM8     1m06s   6GB
Mar 12 15:26:43 Starting .
Mar 12 15:26:46 FAILED: .
Scanning $(HOLDIR)/src/TeX
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/algorithms
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
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/real/analysis
Scanning $(HOLDIR)/examples/misc
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
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)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
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/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 $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/examples/compilation/x64
Scanning $(CAKEMLDIR)/examples/compilation/x64/proofs
Scanned 101 directories
Don't know how to build necessary target(s): /scratch/cakeml/regression/cakeml-2782/COPYING