Job 1545

CakeML:b2d68ddc061e1d032927ef851971b935c365d89b
  Fix for change to List.foldl [Jun 13 07:51:42]
#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:stove 4.15.0-143-generic x86_64 GNU/Linux

Jun 13 07:51:59 Claimed job
Jun 13 07:52:02 Building HOL
Jun 13 08:07:03 Starting developers
Jun 13 08:07:07 Finished developers                                               4s  96MB
Jun 13 08:07:07 Starting developers/bin
Jun 13 08:07:14 Finished developers/bin                                           6s   1GB
Jun 13 08:07:14 Starting semantics/ffi
Jun 13 08:07:25 Finished semantics/ffi                                           10s 238MB
Jun 13 08:07:25 Starting semantics
Jun 13 08:08:56 Finished semantics                                             1m31s   1GB
Jun 13 08:08:56 Starting semantics/proofs
Jun 13 08:12:26 Finished semantics/proofs                                      3m29s   1GB
Jun 13 08:12:26 Starting semantics/alt_semantics
Jun 13 08:12:36 Finished semantics/alt_semantics                                  9s 362MB
Jun 13 08:12:36 Starting semantics/alt_semantics/proofs
Jun 13 08:14:49 Finished semantics/alt_semantics/proofs                        2m12s 903MB
Jun 13 08:14:49 Starting basis/pure
Jun 13 08:17:43 Finished basis/pure                                            2m53s   1GB
Jun 13 08:17:43 Starting translator
Jun 13 08:20:57 Finished translator                                            3m14s   1GB
Jun 13 08:20:57 Starting compiler/parsing
Jun 13 08:22:07 Finished compiler/parsing                                      1m10s   2GB
Jun 13 08:22:07 Starting characteristic
Jun 13 08:27:49 Finished characteristic                                        5m41s   2GB
Jun 13 08:27:49 Starting translator/monadic
Jun 13 08:29:31 Finished translator/monadic                                    1m42s   1GB
Jun 13 08:29:31 Starting basis
Jun 13 09:12:44 Finished basis                                                43m12s  16GB
Jun 13 09:12:44 Starting compiler/inference
Jun 13 09:13:59 Finished compiler/inference                                    1m14s   1GB
Jun 13 09:13:59 Starting compiler/backend/reg_alloc
Jun 13 09:15:07 Finished compiler/backend/reg_alloc                            1m08s   1GB
Jun 13 09:15:07 Starting compiler/backend/gc
Jun 13 09:18:39 Finished compiler/backend/gc                                   3m31s   2GB
Jun 13 09:18:39 Starting compiler/backend
Jun 13 09:23:29 Finished compiler/backend                                      4m50s   4GB
Jun 13 09:23:29 Starting compiler/encoders/asm
Jun 13 09:23:51 Finished compiler/encoders/asm                                   21s 740MB
Jun 13 09:23:51 Starting compiler/encoders/x64
Jun 13 09:24:52 Finished compiler/encoders/x64                                 1m00s   1GB
Jun 13 09:24:53 Starting compiler/encoders/arm7
Jun 13 09:26:54 Finished compiler/encoders/arm7                                2m01s   1GB
Jun 13 09:26:54 Starting compiler/encoders/arm8
Jun 13 09:27:32 Finished compiler/encoders/arm8                                  37s 994MB
Jun 13 09:27:32 Starting compiler/encoders/mips
Jun 13 09:29:00 Finished compiler/encoders/mips                                1m27s   1GB
Jun 13 09:29:00 Starting compiler/encoders/riscv
Jun 13 09:30:42 Finished compiler/encoders/riscv                               1m42s 913MB
Jun 13 09:30:42 Starting compiler/encoders/ag32
Jun 13 09:31:00 Finished compiler/encoders/ag32                                  17s 572MB
Jun 13 09:31:00 Starting compiler/backend/x64
Jun 13 09:31:20 Finished compiler/backend/x64                                    19s   1GB
Jun 13 09:31:20 Starting compiler/backend/arm7
Jun 13 09:31:41 Finished compiler/backend/arm7                                   21s   1GB
Jun 13 09:31:41 Starting compiler/backend/arm8
Jun 13 09:32:00 Finished compiler/backend/arm8                                   18s   1GB
Jun 13 09:32:00 Starting compiler/backend/mips
Jun 13 09:32:19 Finished compiler/backend/mips                                   18s   1GB
Jun 13 09:32:19 Starting compiler/backend/riscv
Jun 13 09:32:40 Finished compiler/backend/riscv                                  20s   1GB
Jun 13 09:32:40 Starting compiler/backend/ag32
Jun 13 09:33:49 Finished compiler/backend/ag32                                 1m09s   1GB
Jun 13 09:33:50 Starting compiler/parsing/proofs
Jun 13 09:39:43 Finished compiler/parsing/proofs                               5m53s   1GB
Jun 13 09:39:43 Starting compiler/inference/proofs
Jun 13 09:42:10 Finished compiler/inference/proofs                             2m27s   1GB
Jun 13 09:42:10 Starting compiler/backend/semantics
Jun 13 10:10:15 Finished compiler/backend/semantics                           28m04s   3GB
Jun 13 10:10:15 Starting compiler/backend/reg_alloc/proofs
Jun 13 10:13:41 Finished compiler/backend/reg_alloc/proofs                     3m25s 937MB
Jun 13 10:13:41 Starting compiler/backend/proofs
Jun 13 11:04:47 Finished compiler/backend/proofs                              51m06s  20GB
Jun 13 11:04:47 Starting compiler/encoders/x64/proofs
Jun 13 11:14:29 Finished compiler/encoders/x64/proofs                          9m41s   4GB
Jun 13 11:14:29 Starting compiler/encoders/arm7/proofs
Jun 13 11:27:26 Finished compiler/encoders/arm7/proofs                        12m56s   3GB
Jun 13 11:27:26 Starting compiler/encoders/arm8/proofs
Jun 13 11:34:08 Finished compiler/encoders/arm8/proofs                         6m41s   1GB
Jun 13 11:34:08 Starting compiler/encoders/mips/proofs
Jun 13 11:44:01 Finished compiler/encoders/mips/proofs                         9m52s   3GB
Jun 13 11:44:01 Starting compiler/encoders/riscv/proofs
Jun 13 11:52:53 Finished compiler/encoders/riscv/proofs                        8m51s   1GB
Jun 13 11:52:53 Starting compiler/encoders/ag32/proofs
Jun 13 11:55:25 Finished compiler/encoders/ag32/proofs                         2m31s 675MB
Jun 13 11:55:25 Starting compiler/backend/x64/proofs
Jun 13 11:55:47 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 13 11:55:47 Starting compiler/backend/arm7/proofs
Jun 13 11:56:10 Finished compiler/backend/arm7/proofs                            22s   1GB
Jun 13 11:56:10 Starting compiler/backend/arm8/proofs
Jun 13 11:56:33 Finished compiler/backend/arm8/proofs                            22s   1GB
Jun 13 11:56:33 Starting compiler/backend/mips/proofs
Jun 13 11:56:55 Finished compiler/backend/mips/proofs                            22s   1GB
Jun 13 11:56:55 Starting compiler/backend/riscv/proofs
Jun 13 11:57:18 Finished compiler/backend/riscv/proofs                           22s   1GB
Jun 13 11:57:18 Starting compiler/backend/ag32/proofs
Jun 13 12:09:40 Finished compiler/backend/ag32/proofs                         12m21s   3GB
Jun 13 12:09:40 Starting compiler/proofs
Jun 13 12:11:36 Finished compiler/proofs                                       1m55s   4GB
Jun 13 12:11:36 Starting candle/set-theory
Jun 13 12:12:05 Finished candle/set-theory                                       29s 751MB
Jun 13 12:12:05 Starting candle/syntax-lib
Jun 13 12:12:16 Finished candle/syntax-lib                                       10s 647MB
Jun 13 12:12:16 Starting candle/standard/syntax
Jun 13 12:14:07 Finished candle/standard/syntax                                1m50s   1GB
Jun 13 12:14:07 Starting candle/standard/semantics
Jun 13 12:15:50 Finished candle/standard/semantics                             1m42s   1GB
Jun 13 12:15:50 Starting candle/standard/monadic
Jun 13 12:17:31 Finished candle/standard/monadic                               1m41s   1GB
Jun 13 12:17:32 Starting candle/standard/ml_kernel
Jun 13 12:23:12 Finished candle/standard/ml_kernel                             5m40s   5GB
Jun 13 12:23:12 Starting candle/overloading/syntax
Jun 13 12:26:20 Finished candle/overloading/syntax                             3m07s   1GB
Jun 13 12:26:20 Starting candle/overloading/semantics
Jun 13 12:38:15 Finished candle/overloading/semantics                         11m55s   4GB
Jun 13 12:38:16 Starting characteristic/examples
Jun 13 12:39:36 Finished characteristic/examples                               1m20s   2GB
Jun 13 12:39:36 Starting tutorial/solutions
Jun 13 12:54:41 Finished tutorial/solutions                                   15m05s   9GB
Jun 13 12:54:41 Starting translator/monadic/examples
Jun 13 12:57:52 Finished translator/monadic/examples                           3m10s   2GB
Jun 13 12:57:52 Starting examples
Jun 13 13:06:21 Finished examples                                              8m28s   4GB
Jun 13 13:06:21 Starting examples/compilation/x64
Jun 13 15:31:16 Finished examples/compilation/x64                           2h24m55s  15GB
Jun 13 15:31:16 Starting examples/compilation/x64/proofs
Jun 13 15:33:05 Finished examples/compilation/x64/proofs                       1m48s   3GB
Jun 13 15:33:05 Starting examples/compilation/ag32
Jun 13 16:07:04 Finished examples/compilation/ag32                            33m59s   7GB
Jun 13 16:07:05 Starting examples/compilation/ag32/proofs
Jun 13 16:07:57 Finished examples/compilation/ag32/proofs                        52s   4GB
Jun 13 16:07:57 Starting examples/cost
Jun 13 17:01:43 Finished examples/cost                                        53m45s   7GB
Jun 13 17:01:43 Starting examples/lpr_checker
Jun 13 17:05:47 Finished examples/lpr_checker                                  4m03s   3GB
Jun 13 17:05:49 Starting examples/lpr_checker/compilation
Jun 13 17:23:51 Finished examples/lpr_checker/compilation                     18m01s   9GB
Jun 13 17:23:51 Starting examples/lpr_checker/compilation/proofs
Jun 13 17:24:49 Finished examples/lpr_checker/compilation/proofs                 58s   2GB
Jun 13 17:24:49 Starting examples/lpr_checker/array
Jun 13 17:38:50 Finished examples/lpr_checker/array                           14m00s   4GB
Jun 13 17:38:50 Starting examples/lpr_checker/array/compilation
Jun 13 17:58:43 Finished examples/lpr_checker/array/compilation               19m52s  13GB
Jun 13 17:58:43 Starting examples/lpr_checker/array/compilation/proofs
Jun 13 17:59:33 Finished examples/lpr_checker/array/compilation/proofs           49s   4GB
Jun 13 17:59:33 Starting examples/opentheory
Jun 13 18:04:55 FAILED: examples/opentheory
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
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 $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Starting work on README.md
Starting work on prettyTheory
README.md                                                                               real:    0s  user:    0s     OK
prettyTheory                                                                            real:   20s  user:   18s     OK
Starting work on readerTheory
readerTheory                                                                            real:   54s  user:   52s     OK
Starting work on reader_initTheory
reader_initTheory                                                                       real:   25s  user:   24s     OK
Starting work on readerProofTheory
readerProofTheory                                                                       real:   63s  user:   61s     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                                                   real:   17s  user:   15s     OK
reader_commonProgTheory                                                                 real:  156s  user:  153sFAIL<1>
 FOLDL
 
 
 which has type:
 
 :(mlstring app_list -> mlstring app_list -> mlstring app_list) ->
 mlstring app_list -> mlstring app_list list -> mlstring app_list
 
 Failed translation: st2str_applist
 Uncaught exception: UnableToTranslate ?