Job 1543

CakeML:c58fde72075cfe3576748f861b8cbeebce691ac6
  Get tutorial to build again [Jun 11 07:19:48]
#829 (help)
Merging into:36d5c13ef89908d2c2bf082c13186087bd1502f6
  Merge pull request #828 from CakeML/sat_encodings [Jun 04 08:57:36]
HOL:b7716bd92d1115f6a85cbf82d4dd47e1bb88828a
  Remove unnecessary dependencies in examples/polynomial/polynomial [Jun 09 01:52:42]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 11 07:50:51 Claimed job
Jun 11 07:50:53 Reusing HOL
Jun 11 07:50:59 Starting developers
Jun 11 07:50:59 Finished developers                                               0s  33MB
Jun 11 07:51:00 Starting developers/bin
Jun 11 07:51:06 Finished developers/bin                                           6s   1GB
Jun 11 07:51:06 Starting semantics/ffi
Jun 11 07:51:17 Finished semantics/ffi                                           10s 296MB
Jun 11 07:51:17 Starting semantics
Jun 11 07:52:49 Finished semantics                                             1m31s   1GB
Jun 11 07:52:49 Starting semantics/proofs
Jun 11 07:56:22 Finished semantics/proofs                                      3m33s   1GB
Jun 11 07:56:23 Starting semantics/alt_semantics
Jun 11 07:56:32 Finished semantics/alt_semantics                                  8s 418MB
Jun 11 07:56:32 Starting semantics/alt_semantics/proofs
Jun 11 07:59:21 Finished semantics/alt_semantics/proofs                        2m49s   2GB
Jun 11 07:59:21 Starting basis/pure
Jun 11 08:00:27 Finished basis/pure                                            1m05s   1GB
Jun 11 08:00:27 Starting translator
Jun 11 08:04:18 Finished translator                                            3m50s   2GB
Jun 11 08:04:18 Starting compiler/parsing
Jun 11 08:05:28 Finished compiler/parsing                                      1m09s   4GB
Jun 11 08:05:29 Starting characteristic
Jun 11 08:11:17 Finished characteristic                                        5m48s   3GB
Jun 11 08:11:17 Starting translator/monadic
Jun 11 08:13:22 Finished translator/monadic                                    2m04s   1GB
Jun 11 08:13:22 Starting basis
Jun 11 08:57:16 Finished basis                                                43m53s  25GB
Jun 11 08:57:16 Starting compiler/inference
Jun 11 08:58:24 Finished compiler/inference                                    1m07s   1GB
Jun 11 08:58:24 Starting compiler/backend/reg_alloc
Jun 11 08:59:31 Finished compiler/backend/reg_alloc                            1m06s   2GB
Jun 11 08:59:31 Starting compiler/backend/gc
Jun 11 09:02:59 Finished compiler/backend/gc                                   3m27s   4GB
Jun 11 09:03:00 Starting compiler/backend
Jun 11 09:08:04 Finished compiler/backend                                      5m04s   4GB
Jun 11 09:08:05 Starting compiler/encoders/asm
Jun 11 09:08:28 Finished compiler/encoders/asm                                   22s   1GB
Jun 11 09:08:28 Starting compiler/encoders/x64
Jun 11 09:08:55 Finished compiler/encoders/x64                                   26s   1GB
Jun 11 09:08:55 Starting compiler/encoders/arm7
Jun 11 09:09:46 Finished compiler/encoders/arm7                                  50s   1GB
Jun 11 09:09:46 Starting compiler/encoders/arm8
Jun 11 09:10:00 Finished compiler/encoders/arm8                                  13s   1GB
Jun 11 09:10:00 Starting compiler/encoders/mips
Jun 11 09:10:18 Finished compiler/encoders/mips                                  18s   1GB
Jun 11 09:10:18 Starting compiler/encoders/riscv
Jun 11 09:10:34 Finished compiler/encoders/riscv                                 16s   1GB
Jun 11 09:10:35 Starting compiler/encoders/ag32
Jun 11 09:10:53 Finished compiler/encoders/ag32                                  18s 966MB
Jun 11 09:10:53 Starting compiler/backend/x64
Jun 11 09:11:12 Finished compiler/backend/x64                                    18s   1GB
Jun 11 09:11:12 Starting compiler/backend/arm7
Jun 11 09:11:34 Finished compiler/backend/arm7                                   21s   1GB
Jun 11 09:11:34 Starting compiler/backend/arm8
Jun 11 09:11:54 Finished compiler/backend/arm8                                   19s   1GB
Jun 11 09:11:54 Starting compiler/backend/mips
Jun 11 09:12:15 Finished compiler/backend/mips                                   20s   1GB
Jun 11 09:12:15 Starting compiler/backend/riscv
Jun 11 09:12:37 Finished compiler/backend/riscv                                  21s   1GB
Jun 11 09:12:37 Starting compiler/backend/ag32
Jun 11 09:13:49 Finished compiler/backend/ag32                                 1m12s   2GB
Jun 11 09:13:50 Starting compiler/parsing/proofs
Jun 11 09:19:34 Finished compiler/parsing/proofs                               5m43s   2GB
Jun 11 09:19:34 Starting compiler/inference/proofs
Jun 11 09:22:06 Finished compiler/inference/proofs                             2m31s   2GB
Jun 11 09:22:06 Starting compiler/backend/semantics
Jun 11 09:48:53 Finished compiler/backend/semantics                           26m47s   4GB
Jun 11 09:48:53 Starting compiler/backend/reg_alloc/proofs
Jun 11 09:52:10 Finished compiler/backend/reg_alloc/proofs                     3m16s   1GB
Jun 11 09:52:10 Starting compiler/backend/proofs
Jun 11 10:46:25 Finished compiler/backend/proofs                              54m13s  19GB
Jun 11 10:46:26 Starting compiler/encoders/x64/proofs
Jun 11 10:58:23 Finished compiler/encoders/x64/proofs                         11m57s   5GB
Jun 11 10:58:23 Starting compiler/encoders/arm7/proofs
Jun 11 11:11:09 Finished compiler/encoders/arm7/proofs                        12m46s   7GB
Jun 11 11:11:10 Starting compiler/encoders/arm8/proofs
Jun 11 11:17:38 Finished compiler/encoders/arm8/proofs                         6m27s   3GB
Jun 11 11:17:38 Starting compiler/encoders/mips/proofs
Jun 11 11:27:23 Finished compiler/encoders/mips/proofs                         9m44s   5GB
Jun 11 11:27:23 Starting compiler/encoders/riscv/proofs
Jun 11 11:35:47 Finished compiler/encoders/riscv/proofs                        8m23s   4GB
Jun 11 11:35:47 Starting compiler/encoders/ag32/proofs
Jun 11 11:38:07 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Jun 11 11:38:08 Starting compiler/backend/x64/proofs
Jun 11 11:38:31 Finished compiler/backend/x64/proofs                             22s   2GB
Jun 11 11:38:31 Starting compiler/backend/arm7/proofs
Jun 11 11:38:54 Finished compiler/backend/arm7/proofs                            23s   1GB
Jun 11 11:38:54 Starting compiler/backend/arm8/proofs
Jun 11 11:39:17 Finished compiler/backend/arm8/proofs                            22s   1GB
Jun 11 11:39:17 Starting compiler/backend/mips/proofs
Jun 11 11:39:40 Finished compiler/backend/mips/proofs                            22s   1GB
Jun 11 11:39:40 Starting compiler/backend/riscv/proofs
Jun 11 11:40:02 Finished compiler/backend/riscv/proofs                           22s   2GB
Jun 11 11:40:03 Starting compiler/backend/ag32/proofs
Jun 11 11:52:09 Finished compiler/backend/ag32/proofs                         12m06s   6GB
Jun 11 11:52:10 Starting compiler/proofs
Jun 11 11:53:54 Finished compiler/proofs                                       1m44s   6GB
Jun 11 11:53:54 Starting candle/set-theory
Jun 11 11:54:25 Finished candle/set-theory                                       29s   1GB
Jun 11 11:54:25 Starting candle/syntax-lib
Jun 11 11:54:36 Finished candle/syntax-lib                                       11s 811MB
Jun 11 11:54:37 Starting candle/standard/syntax
Jun 11 11:56:26 Finished candle/standard/syntax                                1m49s   1GB
Jun 11 11:56:26 Starting candle/standard/semantics
Jun 11 11:58:13 Finished candle/standard/semantics                             1m46s   2GB
Jun 11 11:58:13 Starting candle/standard/monadic
Jun 11 11:59:56 Finished candle/standard/monadic                               1m42s   1GB
Jun 11 11:59:56 Starting candle/standard/ml_kernel
Jun 11 12:05:26 Finished candle/standard/ml_kernel                             5m29s   6GB
Jun 11 12:05:26 Starting candle/overloading/syntax
Jun 11 12:08:37 Finished candle/overloading/syntax                             3m11s   1GB
Jun 11 12:08:37 Starting candle/overloading/semantics
Jun 11 12:20:43 Finished candle/overloading/semantics                         12m05s   9GB
Jun 11 12:20:43 Starting characteristic/examples
Jun 11 12:22:02 Finished characteristic/examples                               1m19s   4GB
Jun 11 12:22:02 Starting tutorial/solutions
Jun 11 12:37:40 Finished tutorial/solutions                                   15m37s  11GB
Jun 11 12:37:41 Starting translator/monadic/examples
Jun 11 12:41:07 Finished translator/monadic/examples                           3m26s   3GB
Jun 11 12:41:07 Starting examples
Jun 11 12:50:34 Finished examples                                              9m27s   6GB
Jun 11 12:50:35 Starting examples/compilation/x64
Jun 11 15:12:32 Finished examples/compilation/x64                           2h21m56s  24GB
Jun 11 15:12:32 Starting examples/compilation/x64/proofs
Jun 11 15:14:31 Finished examples/compilation/x64/proofs                       1m58s   3GB
Jun 11 15:14:31 Starting examples/compilation/ag32
Jun 11 15:48:52 Finished examples/compilation/ag32                            34m21s  11GB
Jun 11 15:48:52 Starting examples/compilation/ag32/proofs
Jun 11 15:49:45 Finished examples/compilation/ag32/proofs                        52s   5GB
Jun 11 15:49:45 Starting examples/cost
Jun 11 16:45:06 Finished examples/cost                                        55m21s  13GB
Jun 11 16:45:06 Starting examples/lpr_checker
Jun 11 16:46:39 FAILED: examples/lpr_checker
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
Starting work on satSemTheory
satSemTheory                                                                                                                                         real:   11s  user:   11s     OK
Starting work on lprTheory
lprTheory                                                                                                                                            real:   13s  user:   12s     OK
Starting work on parsingTheory
Starting work on ramseyTheory
parsingTheory                                                                                                                                        real:   14s  user:   13s     OK
Starting work on lpr_commonProgTheory
ramseyTheory                                                                                                                                         real:   23s  user:   21s     OK
lpr_commonProgTheory                                                                                                                                 real:   52s  user:   49sFAIL<1>
 
 which has type:
 
 :(int list sptree$num_map -> num -> int list sptree$num_map) ->
 int list sptree$num_map -> num list -> int list sptree$num_map
 
 Failed translation: check_lpr_step
 error in quse /home/myreen/regression/cakeml-1543/examples/lpr_checker/lpr_commonProgScript.sml : UnableToTranslate ?
 error in load /home/myreen/regression/cakeml-1543/examples/lpr_checker/lpr_commonProgScript : UnableToTranslate ?
 Uncaught exception: UnableToTranslate ?