Job 2155

CakeML:191c21c2716bbd4cb630c7e15ca25168d3501a4e
  Get ag32/proofs to build again after changes to HOL master [Jun 20 01:10:55]
HOL:643c7c5191f649af6f9c0b347660ad62d9617dc2
  Fix ASL equivalence proofs [Jun 18 03:48:18]
Machine:pavlova

Jun 20 09:46:13 Claimed job
Jun 20 09:46:19 Building HOL
Jun 20 09:59:07 Starting developers
Jun 20 09:59:10 Finished developers                                               2s 202MB
Jun 20 09:59:11 Starting developers/bin
Jun 20 09:59:21 Finished developers/bin                                           9s   1GB
Jun 20 09:59:22 Starting compiler/proofs
Jun 20 11:43:11 Finished compiler/proofs                                    1h43m46s  42GB
Jun 20 11:43:12 Starting compiler/bootstrap/translation
Jun 20 19:41:50 Finished compiler/bootstrap/translation                     7h58m35s  73GB
Jun 20 19:41:50 Starting semantics/ffi
Jun 20 19:41:58 Finished semantics/ffi                                            7s 576MB
Jun 20 19:41:59 Starting semantics
Jun 20 19:42:00 Finished semantics                                                0s  63MB
Jun 20 19:42:01 Starting semantics/proofs
Jun 20 19:42:35 Finished semantics/proofs                                        33s   1GB
Jun 20 19:42:36 Starting semantics/alt_semantics
Jun 20 19:43:15 Finished semantics/alt_semantics                                 38s   1GB
Jun 20 19:43:16 Starting semantics/alt_semantics/proofs
Jun 20 19:54:14 Finished semantics/alt_semantics/proofs                       10m57s   6GB
Jun 20 19:54:15 Starting basis/pure
Jun 20 19:54:16 Finished basis/pure                                               0s  72MB
Jun 20 19:54:17 Starting translator
Jun 20 19:56:02 Finished translator                                            1m43s   3GB
Jun 20 19:56:03 Starting compiler/parsing
Jun 20 19:56:04 Finished compiler/parsing                                         0s  70MB
Jun 20 19:56:05 Starting characteristic
Jun 20 19:56:06 Finished characteristic                                           0s  93MB
Jun 20 19:56:07 Starting translator/monadic
Jun 20 19:56:09 Finished translator/monadic                                       0s  90MB
Jun 20 19:56:10 Starting basis
Jun 20 20:00:02 Finished basis                                                 3m51s   4GB
Jun 20 20:00:02 Starting compiler/inference
Jun 20 20:00:04 Finished compiler/inference                                       0s  82MB
Jun 20 20:00:05 Starting compiler/backend/reg_alloc
Jun 20 20:00:06 Finished compiler/backend/reg_alloc                               0s  68MB
Jun 20 20:00:07 Starting compiler/backend/gc
Jun 20 20:00:09 Finished compiler/backend/gc                                      0s 130MB
Jun 20 20:00:09 Starting compiler/backend
Jun 20 20:00:28 Finished compiler/backend                                        17s   1GB
Jun 20 20:00:29 Starting compiler/encoders/asm
Jun 20 20:00:30 Finished compiler/encoders/asm                                    0s  89MB
Jun 20 20:00:31 Starting compiler/encoders/x64
Jun 20 20:00:32 Finished compiler/encoders/x64                                    0s  90MB
Jun 20 20:00:33 Starting compiler/encoders/arm7
Jun 20 20:00:35 Finished compiler/encoders/arm7                                   0s  96MB
Jun 20 20:00:35 Starting compiler/encoders/arm8
Jun 20 20:00:37 Finished compiler/encoders/arm8                                   0s  90MB
Jun 20 20:00:38 Starting compiler/encoders/arm8_asl
Jun 20 22:21:03 Finished compiler/encoders/arm8_asl                         2h20m23s  42GB
Jun 20 22:21:04 Starting compiler/encoders/mips
Jun 20 22:21:05 Finished compiler/encoders/mips                                   0s  90MB
Jun 20 22:21:06 Starting compiler/encoders/riscv
Jun 20 22:21:07 Finished compiler/encoders/riscv                                  0s  93MB
Jun 20 22:21:08 Starting compiler/encoders/ag32
Jun 20 22:21:09 Finished compiler/encoders/ag32                                   0s  89MB
Jun 20 22:21:10 Starting compiler/backend/x64
Jun 20 22:21:12 Finished compiler/backend/x64                                     0s 130MB
Jun 20 22:21:13 Starting compiler/backend/arm7
Jun 20 22:21:14 Finished compiler/backend/arm7                                    0s 129MB
Jun 20 22:21:15 Starting compiler/backend/arm8
Jun 20 22:21:17 Finished compiler/backend/arm8                                    0s 130MB
Jun 20 22:21:18 Starting compiler/backend/mips
Jun 20 22:21:20 Finished compiler/backend/mips                                    0s 130MB
Jun 20 22:21:20 Starting compiler/backend/riscv
Jun 20 22:21:22 Finished compiler/backend/riscv                                   0s 130MB
Jun 20 22:21:23 Starting compiler/backend/ag32
Jun 20 22:22:44 Finished compiler/backend/ag32                                 1m20s   2GB
Jun 20 22:22:45 Starting compiler/parsing/proofs
Jun 20 22:22:46 Finished compiler/parsing/proofs                                  0s  72MB
Jun 20 22:22:47 Starting compiler/inference/proofs
Jun 20 22:22:49 Finished compiler/inference/proofs                                0s  80MB
Jun 20 22:22:49 Starting compiler/backend/semantics
Jun 20 22:24:19 Finished compiler/backend/semantics                            1m28s   3GB
Jun 20 22:24:20 Starting compiler/backend/reg_alloc/proofs
Jun 20 22:24:22 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Jun 20 22:24:22 Starting compiler/backend/proofs
Jun 20 22:25:23 Finished compiler/backend/proofs                               1m00s   3GB
Jun 20 22:25:24 Starting compiler/backend/serialiser
Jun 20 22:25:26 Finished compiler/backend/serialiser                              1s 181MB
Jun 20 22:25:27 Starting compiler/encoders/x64/proofs
Jun 20 22:34:50 Finished compiler/encoders/x64/proofs                          9m21s   5GB
Jun 20 22:34:51 Starting compiler/encoders/arm7/proofs
Jun 20 22:47:48 Finished compiler/encoders/arm7/proofs                        12m56s   8GB
Jun 20 22:47:49 Starting compiler/encoders/arm8/proofs
Jun 20 22:54:27 Finished compiler/encoders/arm8/proofs                         6m37s   6GB
Jun 20 22:54:28 Starting compiler/encoders/arm8_asl/proofs
Jun 20 23:41:48 Finished compiler/encoders/arm8_asl/proofs                    47m18s   9GB
Jun 20 23:41:49 Starting compiler/encoders/mips/proofs
Jun 20 23:51:57 Finished compiler/encoders/mips/proofs                        10m07s   6GB
Jun 20 23:51:57 Starting compiler/encoders/riscv/proofs
Jun 21 00:00:04 Finished compiler/encoders/riscv/proofs                        8m06s   3GB
Jun 21 00:00:05 Starting compiler/encoders/ag32/proofs
Jun 21 00:02:30 Finished compiler/encoders/ag32/proofs                         2m24s   2GB
Jun 21 00:02:31 Starting compiler/backend/x64/proofs
Jun 21 00:03:14 Finished compiler/backend/x64/proofs                             41s   2GB
Jun 21 00:03:15 Starting compiler/backend/arm7/proofs
Jun 21 00:03:59 Finished compiler/backend/arm7/proofs                            42s   2GB
Jun 21 00:03:59 Starting compiler/backend/arm8/proofs
Jun 21 00:04:40 Finished compiler/backend/arm8/proofs                            39s   3GB
Jun 21 00:04:40 Starting compiler/backend/arm8_asl
Jun 21 00:05:10 Finished compiler/backend/arm8_asl                               28s   2GB
Jun 21 00:05:10 Starting compiler/backend/mips/proofs
Jun 21 00:05:54 Finished compiler/backend/mips/proofs                            42s   3GB
Jun 21 00:05:55 Starting compiler/backend/riscv/proofs
Jun 21 00:06:43 Finished compiler/backend/riscv/proofs                           47s   3GB
Jun 21 00:06:44 Starting compiler/backend/ag32/proofs
Jun 21 00:19:51 Finished compiler/backend/ag32/proofs                         13m05s   5GB
Jun 21 00:19:52 Starting candle/set-theory
Jun 21 00:20:37 Finished candle/set-theory                                       44s   1GB
Jun 21 00:20:38 Starting candle/syntax-lib
Jun 21 00:20:39 Finished candle/syntax-lib                                        0s  71MB
Jun 21 00:20:40 Starting candle/standard/syntax
Jun 21 00:20:55 Finished candle/standard/syntax                                  14s   1GB
Jun 21 00:20:56 Starting candle/standard/semantics
Jun 21 00:23:23 Finished candle/standard/semantics                             2m25s   3GB
Jun 21 00:23:23 Starting candle/standard/monadic
Jun 21 00:23:25 Finished candle/standard/monadic                                  0s 105MB
Jun 21 00:23:26 Starting candle/standard/ml_kernel
Jun 21 00:25:16 Finished candle/standard/ml_kernel                             1m49s   5GB
Jun 21 00:25:17 Starting candle/overloading/syntax
Jun 21 00:28:41 Finished candle/overloading/syntax                             3m23s   2GB
Jun 21 00:28:42 Starting candle/overloading/semantics
Jun 21 00:39:58 Finished candle/overloading/semantics                         11m15s   6GB
Jun 21 00:39:59 Starting candle/overloading/monadic
Jun 21 00:42:36 Finished candle/overloading/monadic                            2m34s   3GB
Jun 21 00:42:36 Starting candle/overloading/ml_kernel
Jun 21 00:50:10 Finished candle/overloading/ml_kernel                          7m33s   6GB
Jun 21 00:50:11 Starting candle/overloading/ml_checker
Jun 21 00:52:41 Finished candle/overloading/ml_checker                         2m28s   7GB
Jun 21 00:52:41 Starting candle/prover
Jun 21 01:02:29 Finished candle/prover                                         9m46s   5GB
Jun 21 01:02:30 Starting pancake
Jun 21 01:03:32 Finished pancake                                               1m01s   1GB
Jun 21 01:03:33 Starting pancake/ffi
Jun 21 01:03:34 Finished pancake/ffi                                              0s  20MB
Jun 21 01:03:35 Starting pancake/semantics
Jun 21 01:05:58 Finished pancake/semantics                                     2m21s   2GB
Jun 21 01:05:59 Starting pancake/proofs
Jun 21 01:23:04 Finished pancake/proofs                                       17m04s   7GB
Jun 21 01:23:05 Starting characteristic/examples
Jun 21 01:24:11 FAILED: characteristic/examples
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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
Scanned 29 directories
Starting work on README.md
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
README.md                                                           (0s)     OK
cf_tutorialTheory                                                  (54s)     OK
cf_examplesTheory                                                  (58s)FAIL<1>
 Adding nsLookup representation thms for [cf_examples_env_5]
 Adding nsLookup representation thms for [init_env]
 Saved theorem _______ "nsLookup_cf_examples_env_6_pfun_eqs"
 Proved triviality _ "is_nil_spec"
 Adding nsLookup representation thms for [cf_examples_env_6]
 Saved theorem _______ "nsLookup_cf_examples_env_7_pfun_eqs"
 /scratch/cakeml/regression/cakeml-2155/characteristic/examples/cf_examplesScript.sml:148: error: ) expected but val was found
 error in quse /scratch/cakeml/regression/cakeml-2155/characteristic/examples/cf_examplesScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression/cakeml-2155/characteristic/examples/cf_examplesScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"