Job 1440

CakeML:6539672c805fd7a4af8f6b82d699f9555f641574
  Tidy some READMEs [Jan 15 15:30:28]
#810 (master)
Merging into:3c6495906dc020e093e2f5cf101cea1cba2fc468
  Fix breakage caused by change to sorted_map in HOL [Jan 05 15:57:59]
HOL:07dca05c1eb441bb9b18556ae55f275d2518bade
  Fix bugs in Makefiles/lib files preventing Lassie from compiling [Jan 06 06:03:07]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 15 15:33:22 Claimed job
Jan 15 15:33:26 Reusing HOL
Jan 15 15:34:14 Starting developers
Jan 15 15:34:18 Finished developers                                               4s 102MB
Jan 15 15:34:19 Starting developers/bin
Jan 15 15:34:26 Finished developers/bin                                           6s   1GB
Jan 15 15:34:26 Starting semantics/ffi
Jan 15 15:34:37 Finished semantics/ffi                                           11s 248MB
Jan 15 15:34:37 Starting semantics
Jan 15 15:36:04 Finished semantics                                             1m26s   1GB
Jan 15 15:36:05 Starting semantics/proofs
Jan 15 15:39:39 Finished semantics/proofs                                      3m34s   1GB
Jan 15 15:39:40 Starting semantics/alt_semantics
Jan 15 15:39:49 Finished semantics/alt_semantics                                  8s 306MB
Jan 15 15:39:49 Starting semantics/alt_semantics/proofs
Jan 15 15:42:02 Finished semantics/alt_semantics/proofs                        2m13s   1GB
Jan 15 15:42:03 Starting basis/pure
Jan 15 15:42:54 Finished basis/pure                                              51s 857MB
Jan 15 15:42:54 Starting translator
Jan 15 15:45:42 Finished translator                                            2m46s   1GB
Jan 15 15:45:42 Starting compiler/parsing
Jan 15 15:46:57 Finished compiler/parsing                                      1m14s   2GB
Jan 15 15:46:57 Starting characteristic
Jan 15 15:53:08 Finished characteristic                                        6m11s   2GB
Jan 15 15:53:08 Starting translator/monadic
Jan 15 15:54:53 Finished translator/monadic                                    1m44s   1GB
Jan 15 15:54:53 Starting basis
Jan 15 16:31:20 Finished basis                                                36m26s  13GB
Jan 15 16:31:20 Starting compiler/inference
Jan 15 16:32:25 Finished compiler/inference                                    1m04s   1GB
Jan 15 16:32:25 Starting compiler/backend/reg_alloc
Jan 15 16:33:32 Finished compiler/backend/reg_alloc                            1m06s   1GB
Jan 15 16:33:32 Starting compiler/backend/gc
Jan 15 16:37:05 Finished compiler/backend/gc                                   3m33s   2GB
Jan 15 16:37:06 Starting compiler/backend
Jan 15 16:42:01 Finished compiler/backend                                      4m55s   3GB
Jan 15 16:42:01 Starting compiler/encoders/asm
Jan 15 16:42:24 Finished compiler/encoders/asm                                   22s 857MB
Jan 15 16:42:24 Starting compiler/encoders/x64
Jan 15 16:42:50 Finished compiler/encoders/x64                                   25s 769MB
Jan 15 16:42:51 Starting compiler/encoders/arm7
Jan 15 16:43:43 Finished compiler/encoders/arm7                                  51s 707MB
Jan 15 16:43:43 Starting compiler/encoders/arm8
Jan 15 16:43:56 Finished compiler/encoders/arm8                                  13s 617MB
Jan 15 16:43:56 Starting compiler/encoders/mips
Jan 15 16:44:15 Finished compiler/encoders/mips                                  18s   1GB
Jan 15 16:44:15 Starting compiler/encoders/riscv
Jan 15 16:44:30 Finished compiler/encoders/riscv                                 14s 788MB
Jan 15 16:44:30 Starting compiler/encoders/ag32
Jan 15 16:44:49 Finished compiler/encoders/ag32                                  18s 848MB
Jan 15 16:44:49 Starting compiler/backend/x64
Jan 15 16:45:09 Finished compiler/backend/x64                                    19s   1GB
Jan 15 16:45:09 Starting compiler/backend/arm7
Jan 15 16:45:30 Finished compiler/backend/arm7                                   20s   1GB
Jan 15 16:45:30 Starting compiler/backend/arm8
Jan 15 16:45:51 Finished compiler/backend/arm8                                   19s   1GB
Jan 15 16:45:51 Starting compiler/backend/mips
Jan 15 16:46:11 Finished compiler/backend/mips                                   20s   1GB
Jan 15 16:46:12 Starting compiler/backend/riscv
Jan 15 16:46:31 Finished compiler/backend/riscv                                  19s   1GB
Jan 15 16:46:31 Starting compiler/backend/ag32
Jan 15 16:47:45 Finished compiler/backend/ag32                                 1m13s   1GB
Jan 15 16:47:46 Starting compiler/parsing/proofs
Jan 15 16:53:34 Finished compiler/parsing/proofs                               5m48s   1GB
Jan 15 16:53:34 Starting compiler/inference/proofs
Jan 15 16:56:11 Finished compiler/inference/proofs                             2m36s 990MB
Jan 15 16:56:11 Starting compiler/backend/semantics
Jan 15 17:29:02 Finished compiler/backend/semantics                           32m50s   2GB
Jan 15 17:29:02 Starting compiler/backend/reg_alloc/proofs
Jan 15 17:32:52 Finished compiler/backend/reg_alloc/proofs                     3m49s 844MB
Jan 15 17:32:53 Starting compiler/backend/proofs
Jan 15 18:30:57 Finished compiler/backend/proofs                              58m03s  18GB
Jan 15 18:30:57 Starting compiler/encoders/x64/proofs
Jan 15 18:41:20 Finished compiler/encoders/x64/proofs                         10m22s   4GB
Jan 15 18:41:21 Starting compiler/encoders/arm7/proofs
Jan 15 18:55:19 Finished compiler/encoders/arm7/proofs                        13m58s   3GB
Jan 15 18:55:20 Starting compiler/encoders/arm8/proofs
Jan 15 19:02:27 Finished compiler/encoders/arm8/proofs                         7m07s   1GB
Jan 15 19:02:28 Starting compiler/encoders/mips/proofs
Jan 15 19:13:06 Finished compiler/encoders/mips/proofs                        10m37s   2GB
Jan 15 19:13:06 Starting compiler/encoders/riscv/proofs
Jan 15 19:22:50 Finished compiler/encoders/riscv/proofs                        9m43s   1GB
Jan 15 19:22:50 Starting compiler/encoders/ag32/proofs
Jan 15 19:25:39 Finished compiler/encoders/ag32/proofs                         2m48s 611MB
Jan 15 19:25:39 Starting compiler/backend/x64/proofs
Jan 15 19:26:01 Finished compiler/backend/x64/proofs                             21s   1GB
Jan 15 19:26:01 Starting compiler/backend/arm7/proofs
Jan 15 19:26:24 Finished compiler/backend/arm7/proofs                            23s   1GB
Jan 15 19:26:25 Starting compiler/backend/arm8/proofs
Jan 15 19:26:47 Finished compiler/backend/arm8/proofs                            21s   1GB
Jan 15 19:26:47 Starting compiler/backend/mips/proofs
Jan 15 19:27:10 Finished compiler/backend/mips/proofs                            22s   1GB
Jan 15 19:27:10 Starting compiler/backend/riscv/proofs
Jan 15 19:27:32 Finished compiler/backend/riscv/proofs                           22s   1GB
Jan 15 19:27:33 Starting compiler/backend/ag32/proofs
Jan 15 19:41:11 Finished compiler/backend/ag32/proofs                         13m38s   2GB
Jan 15 19:41:11 Starting compiler/proofs
Jan 15 19:42:50 Finished compiler/proofs                                       1m37s   2GB
Jan 15 19:42:50 Starting candle/set-theory
Jan 15 19:43:20 Finished candle/set-theory                                       29s 701MB
Jan 15 19:43:20 Starting candle/syntax-lib
Jan 15 19:43:31 Finished candle/syntax-lib                                       10s 475MB
Jan 15 19:43:31 Starting candle/standard/syntax
Jan 15 19:45:27 Finished candle/standard/syntax                                1m55s   1GB
Jan 15 19:45:27 Starting candle/standard/semantics
Jan 15 19:47:16 Finished candle/standard/semantics                             1m48s   1GB
Jan 15 19:47:16 Starting candle/standard/monadic
Jan 15 19:49:05 Finished candle/standard/monadic                               1m48s   1GB
Jan 15 19:49:05 Starting candle/standard/ml_kernel
Jan 15 19:54:51 Finished candle/standard/ml_kernel                             5m46s   4GB
Jan 15 19:54:51 Starting candle/overloading/syntax
Jan 15 19:58:11 Finished candle/overloading/syntax                             3m19s 973MB
Jan 15 19:58:11 Starting candle/overloading/semantics
Jan 15 20:11:09 Finished candle/overloading/semantics                         12m57s   2GB
Jan 15 20:11:09 Starting characteristic/examples
Jan 15 20:12:29 Finished characteristic/examples                               1m19s   3GB
Jan 15 20:12:29 Starting tutorial/solutions
Jan 15 20:27:50 Finished tutorial/solutions                                   15m21s   8GB
Jan 15 20:27:50 Starting translator/monadic/examples
Jan 15 20:31:09 Finished translator/monadic/examples                           3m18s   2GB
Jan 15 20:31:09 Starting examples
Jan 15 20:40:01 Finished examples                                              8m51s   3GB
Jan 15 20:40:01 Starting examples/compilation/x64
Jan 15 23:07:32 Finished examples/compilation/x64                           2h27m30s  13GB
Jan 15 23:07:33 Starting examples/compilation/x64/proofs
Jan 15 23:09:20 Finished examples/compilation/x64/proofs                       1m47s   3GB
Jan 15 23:09:21 Starting examples/compilation/ag32
Jan 15 23:43:01 Finished examples/compilation/ag32                            33m40s   8GB
Jan 15 23:43:01 Starting examples/compilation/ag32/proofs
Jan 15 23:44:10 Finished examples/compilation/ag32/proofs                      1m08s   3GB
Jan 15 23:44:10 Starting examples/cost
Jan 16 00:41:30 Finished examples/cost                                        57m19s   7GB
Jan 16 00:41:31 Starting examples/lpr_checker
Jan 16 00:45:39 Finished examples/lpr_checker                                  4m08s   2GB
Jan 16 00:45:40 Starting examples/lpr_checker/compilation
Jan 16 01:04:39 Finished examples/lpr_checker/compilation                     18m59s  14GB
Jan 16 01:04:39 Starting examples/lpr_checker/compilation/proofs
Jan 16 01:05:20 Finished examples/lpr_checker/compilation/proofs                 41s   3GB
Jan 16 01:05:21 Starting examples/lpr_checker/array
Jan 16 01:20:53 Finished examples/lpr_checker/array                           15m32s   4GB
Jan 16 01:20:53 Starting examples/lpr_checker/array/compilation
Jan 16 01:41:14 Finished examples/lpr_checker/array/compilation               20m19s  13GB
Jan 16 01:41:14 Starting examples/lpr_checker/array/compilation/proofs
Jan 16 01:42:22 Finished examples/lpr_checker/array/compilation/proofs         1m08s   3GB
Jan 16 01:42:22 Starting examples/opentheory
Jan 16 01:52:25 Finished examples/opentheory                                  10m02s   5GB
Jan 16 01:52:25 Starting examples/opentheory
Jan 16 01:52:26 Finished examples/opentheory                                      1s  23MB
Jan 16 01:52:26 Starting examples/opentheory/compilation
Jan 16 02:26:27 Finished examples/opentheory/compilation                      34m00s  17GB
Jan 16 02:26:27 Starting examples/opentheory/compilation/proofs
Jan 16 02:27:14 Finished examples/opentheory/compilation/proofs                  46s   3GB
Jan 16 02:27:14 Starting examples/opentheory/compilation/ag32
Jan 16 03:02:57 Finished examples/opentheory/compilation/ag32                 35m43s  18GB
Jan 16 03:02:58 Starting examples/opentheory/compilation/ag32/proofs
Jan 16 03:04:50 Finished examples/opentheory/compilation/ag32/proofs           1m51s   5GB
Jan 16 03:04:50 Starting translator/okasaki-examples
Jan 16 03:09:18 Finished translator/okasaki-examples                           4m28s   1GB
Jan 16 03:09:18 Starting translator/other-examples
Jan 16 03:11:22 Finished translator/other-examples                             2m03s   1GB
Jan 16 03:11:22 Starting compiler/parsing/tests
Jan 16 03:11:49 Finished compiler/parsing/tests                                  26s 516MB
Jan 16 03:11:49 Starting compiler/inference/tests
Jan 16 03:19:41 Finished compiler/inference/tests                              7m51s   4GB
Jan 16 03:19:41 Starting compiler/bootstrap/translation
Jan 16 04:22:50 FAILED: compiler/bootstrap/translation
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
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 $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
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/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
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/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/unification/triangular
Scanning $(HOLDIR)/examples/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Starting work on monadic_encTheory
Starting work on README.md
Starting work on to_flatProgTheory
README.md                                       real:    0s  user:    0s     OK
monadic_encTheory                               real:   10s  user:    9s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc64Theory                             real:   14s  user:   14s     OK
monadic_enc32Theory                             real:   15s  user:   14s     OK
to_flatProgTheory                               real:  450s  user:  443s     OK
Starting work on to_closProgTheory
to_closProgTheory                               real:  534s  user:  527s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                real:  406s  user:  398s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                real:  347s  user:  341s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                               real:  192s  user:  188s     OK
Starting work on lexerProgTheory
lexerProgTheory                                 real:  288s  user:  283s     OK
Starting work on parserProgTheory
parserProgTheory                                real:  534s  user:  522s     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                             real: 1032s  user: 1022sFAIL<1>
 error in load /home/cake/oven/regression/cakeml-1440/compiler/bootstrap/translation/reg_allocProgScript : UnableToTranslate ?
 difference
 
 
 which has type:
 
 :sptree$num_set -> sptree$num_set -> sptree$num_set
 
 Failed translation: !
 Uncaught exception: UnableToTranslate ?