Job 570

CakeML:b4ecf332bf00bd322db04077a28ce3b05745e85e
  Fix incorrect ag32 paths in build-sequence [Nov 21 04:22:22]
#554 (tiny)
Merging into:9b491cb24bd22174a6c514574e4bb6c057eafe2f
  Rename "backend_correct" to "encoder_correct" [Nov 20 18:08:31]
HOL:57ef4df497757f622a7fe2bfeda16116585da6d4
  Update experimental kernel for world free of Globals.priming [Nov 20 05:59:15]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Nov 21 05:27:20 Claimed job
Nov 21 05:27:25 Reusing HOL
Nov 21 05:27:34 Starting developers/bin
Nov 21 05:28:08 Finished developers/bin                                          33s 140MB
Nov 21 05:28:09 Starting semantics/ffi
Nov 21 05:28:20 Finished semantics/ffi                                           10s 269MB
Nov 21 05:28:21 Starting semantics
Nov 21 05:29:41 Finished semantics                                             1m19s 895MB
Nov 21 05:29:42 Starting semantics/proofs
Nov 21 05:32:53 Finished semantics/proofs                                      3m09s   1GB
Nov 21 05:32:54 Starting basis/pure
Nov 21 05:33:49 Finished basis/pure                                              55s 640MB
Nov 21 05:33:50 Starting translator
Nov 21 05:37:04 Finished translator                                            3m13s   1GB
Nov 21 05:37:05 Starting compiler/parsing
Nov 21 05:38:32 Finished compiler/parsing                                      1m26s   1GB
Nov 21 05:38:33 Starting characteristic
Nov 21 05:41:11 Finished characteristic                                        2m37s   1GB
Nov 21 05:41:12 Starting translator/monadic
Nov 21 05:42:42 Finished translator/monadic                                    1m29s   1GB
Nov 21 05:42:43 Starting basis
Nov 21 06:01:30 Finished basis                                                18m45s   2GB
Nov 21 06:01:30 Starting compiler/inference
Nov 21 06:03:03 Finished compiler/inference                                    1m31s   1GB
Nov 21 06:03:03 Starting compiler/backend/reg_alloc
Nov 21 06:03:57 Finished compiler/backend/reg_alloc                              52s   1GB
Nov 21 06:03:57 Starting compiler/backend/gc
Nov 21 06:11:31 Finished compiler/backend/gc                                   7m32s   1GB
Nov 21 06:11:32 Starting compiler/backend
Nov 21 06:11:34 Finished compiler/backend                                         2s  16MB
Nov 21 06:11:35 Starting compiler/encoders/asm
Nov 21 06:11:37 Finished compiler/encoders/asm                                    0s  12MB
Nov 21 06:11:37 Starting compiler/encoders/x64
Nov 21 06:11:55 Finished compiler/encoders/x64                                   17s 370MB
Nov 21 06:11:56 Starting compiler/encoders/arm6
Nov 21 06:12:46 Finished compiler/encoders/arm6                                  49s 440MB
Nov 21 06:12:46 Starting compiler/encoders/arm8
Nov 21 06:12:55 Finished compiler/encoders/arm8                                   7s 418MB
Nov 21 06:12:56 Starting compiler/encoders/mips
Nov 21 06:13:06 Finished compiler/encoders/mips                                   9s 527MB
Nov 21 06:13:07 Starting compiler/encoders/riscv
Nov 21 06:13:16 Finished compiler/encoders/riscv                                  8s 412MB
Nov 21 06:13:16 Starting compiler/encoders/ag32
Nov 21 06:13:34 Finished compiler/encoders/ag32                                  17s 667MB
Nov 21 06:13:35 Starting compiler/backend/x64
Nov 21 06:13:55 Finished compiler/backend/x64                                    19s 895MB
Nov 21 06:13:56 Starting compiler/backend/arm6
Nov 21 06:14:18 Finished compiler/backend/arm6                                   21s   1GB
Nov 21 06:14:19 Starting compiler/backend/arm8
Nov 21 06:14:40 Finished compiler/backend/arm8                                   20s 977MB
Nov 21 06:14:41 Starting compiler/backend/mips
Nov 21 06:15:01 Finished compiler/backend/mips                                   19s   1GB
Nov 21 06:15:02 Starting compiler/backend/riscv
Nov 21 06:15:23 Finished compiler/backend/riscv                                  19s   1GB
Nov 21 06:15:24 Starting compiler/backend/ag32
Nov 21 06:16:45 Finished compiler/backend/ag32                                 1m20s   1GB
Nov 21 06:16:46 Starting compiler/parsing/proofs
Nov 21 06:23:17 Finished compiler/parsing/proofs                               6m31s   1GB
Nov 21 06:23:18 Starting compiler/inference/proofs
Nov 21 06:26:38 Finished compiler/inference/proofs                             3m19s   1GB
Nov 21 06:26:39 Starting compiler/backend/semantics
Nov 21 06:37:44 Finished compiler/backend/semantics                           11m04s   1GB
Nov 21 06:37:45 Starting compiler/backend/reg_alloc/proofs
Nov 21 06:40:40 Finished compiler/backend/reg_alloc/proofs                     2m53s 577MB
Nov 21 06:40:41 Starting compiler/backend/proofs
Nov 21 07:39:00 Finished compiler/backend/proofs                              58m18s   3GB
Nov 21 07:39:01 Starting compiler/encoders/x64/proofs
Nov 21 07:48:55 Finished compiler/encoders/x64/proofs                          9m53s 889MB
Nov 21 07:48:55 Starting compiler/encoders/arm6/proofs
Nov 21 08:04:46 Finished compiler/encoders/arm6/proofs                        15m49s 767MB
Nov 21 08:04:46 Starting compiler/encoders/arm8/proofs
Nov 21 08:11:47 Finished compiler/encoders/arm8/proofs                         7m00s 694MB
Nov 21 08:11:48 Starting compiler/encoders/mips/proofs
Nov 21 08:22:52 Finished compiler/encoders/mips/proofs                        11m02s   2GB
Nov 21 08:22:52 Starting compiler/encoders/riscv/proofs
Nov 21 08:31:54 Finished compiler/encoders/riscv/proofs                        9m01s 798MB
Nov 21 08:31:55 Starting compiler/encoders/ag32/proofs
Nov 21 08:35:05 Finished compiler/encoders/ag32/proofs                         3m09s 629MB
Nov 21 08:35:06 Starting compiler/backend/x64/proofs
Nov 21 08:35:27 Finished compiler/backend/x64/proofs                             20s 784MB
Nov 21 08:35:28 Starting compiler/backend/arm6/proofs
Nov 21 08:35:53 Finished compiler/backend/arm6/proofs                            24s   1GB
Nov 21 08:35:54 Starting compiler/backend/arm8/proofs
Nov 21 08:36:15 Finished compiler/backend/arm8/proofs                            21s   1GB
Nov 21 08:36:16 Starting compiler/backend/mips/proofs
Nov 21 08:36:40 Finished compiler/backend/mips/proofs                            22s   1GB
Nov 21 08:36:40 Starting compiler/backend/riscv/proofs
Nov 21 08:37:03 Finished compiler/backend/riscv/proofs                           21s   1GB
Nov 21 08:37:04 Starting compiler/backend/ag32/proofs
Nov 21 08:48:26 Finished compiler/backend/ag32/proofs                         11m21s   2GB
Nov 21 08:48:27 Starting compiler/proofs
Nov 21 08:50:00 Finished compiler/proofs                                       1m32s   1GB
Nov 21 08:50:00 Starting candle/set-theory
Nov 21 08:50:30 Finished candle/set-theory                                       28s 592MB
Nov 21 08:50:30 Starting candle/syntax-lib
Nov 21 08:50:41 Finished candle/syntax-lib                                       10s 640MB
Nov 21 08:50:42 Starting candle/standard/syntax
Nov 21 08:52:26 Finished candle/standard/syntax                                1m43s 694MB
Nov 21 08:52:27 Starting candle/standard/semantics
Nov 21 08:54:00 Finished candle/standard/semantics                             1m31s 908MB
Nov 21 08:54:00 Starting candle/standard/monadic
Nov 21 08:55:51 Finished candle/standard/monadic                               1m49s   1GB
Nov 21 08:55:51 Starting candle/standard/ml_kernel
Nov 21 09:15:32 Finished candle/standard/ml_kernel                            19m39s   3GB
Nov 21 09:15:32 Starting candle/standard/opentheory
Nov 21 09:24:30 Finished candle/standard/opentheory                            8m56s   3GB
Nov 21 09:24:31 Starting candle/standard/opentheory/compilation
Nov 21 09:57:07 Finished candle/standard/opentheory/compilation               32m35s  13GB
Nov 21 09:57:08 Starting candle/standard/opentheory/compilation/proofs
Nov 21 09:57:47 Finished candle/standard/opentheory/compilation/proofs           37s   4GB
Nov 21 09:57:48 Starting characteristic/examples
Nov 21 09:59:19 Finished characteristic/examples                               1m30s   1GB
Nov 21 09:59:20 Starting tutorial/solutions
Nov 21 10:12:55 Finished tutorial/solutions                                   13m35s   7GB
Nov 21 10:12:56 Starting translator/monadic/examples
Nov 21 10:14:43 Finished translator/monadic/examples                           1m46s   2GB
Nov 21 10:14:44 Starting examples
Nov 21 10:20:40 Finished examples                                              5m55s   2GB
Nov 21 10:20:41 Starting examples/compilation/x64
Nov 21 12:15:40 Finished examples/compilation/x64                           1h54m57s   8GB
Nov 21 12:15:41 Starting examples/compilation/x64/proofs
Nov 21 12:17:34 Finished examples/compilation/x64/proofs                       1m52s   3GB
Nov 21 12:17:35 Starting examples/compilation/ag32
Nov 21 12:44:05 Finished examples/compilation/ag32                            26m29s   4GB
Nov 21 12:44:06 Starting examples/compilation/ag32/proofs
Nov 21 12:44:32 Finished examples/compilation/ag32/proofs                        25s   2GB
Nov 21 12:44:33 Starting compiler/benchmarks
Nov 21 12:44:33 Finished compiler/benchmarks                                      0s   4MB
Nov 21 12:44:34 Starting translator/okasaki-examples
Nov 21 12:44:58 FAILED: translator/okasaki-examples
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../basis/pure]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developers[1mWorking in ../../developers[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../basis/pure]0;Holmake: ../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../basis]0;Holmake: ../../characteristic]0;Holmake: ../../compiler/parsing]0;Holmake: ../../semantics]0;Holmake: ../../semantics/ffi]0;Holmake: ../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../semantics]0;Holmake: ../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../compiler/parsing]0;Holmake: ../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../characteristic]0;Holmake: ../../semantics/proofs]0;Holmake: ../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../characteristic]0;Holmake: ../../translator]0;Holmake: ../../semantics/alt_semantics/proofs]0;Holmake: ../../semantics/alt_semantics]0;Holmake: ../../semantics/alt_semantics[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics[0m
]0;Holmake: ../../semantics/alt_semantics/proofs]0;Holmake: ../../semantics/alt_semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
]0;Holmake: ../../translator]0;Holmake: ../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../characteristic]0;Holmake: ../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../basis]0;Holmake: ../../translator/monadic]0;Holmake: ../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../../basis]0;Holmake: ../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/translator/okasaki-examples[0m
Starting work on heap
heap                                                                                                       OK
Starting work on BankersQueueTheory
Starting work on BatchedQueueTheory
Starting work on okasaki_miscTheory
Starting work on HoodMelvilleQueueTheory
okasaki_miscTheory                                                                                         OK
Starting work on BinaryRandomAccessListsTheory
BatchedQueueTheory                                                                                         OK
Starting work on BinomialHeapTheory
BankersQueueTheory                                                                                         OK
Starting work on BottomUpMergeSortTheory
HoodMelvilleQueueTheory                                                                                    OK
Starting work on ImplicitQueueTheory
BinaryRandomAccessListsTheory                                                                              OK
Starting work on LazyPairingHeapTheory
BottomUpMergeSortTheory                                                                           FAILED! <1>
 Proof of 
 
 leq size segs n seg.
     WeakLinearOrder leq  n  0  sortable_inv leq (size,segs) n 
     SORTED leq seg  LENGTH seg = n 
     sortable_inv leq (size + 1,add_seg leq seg segs size) n
 
 failed.
 error in load BottomUpMergeSortScript : HOL_ERR {message = "on line 156, characters 14-16:\n\nType inference failure: unable to infer a type for the application of\n\n(LENGTH :\206\177 list -> num) :\206\177 list -> num\n\non line 156, characters 7-12\n\nto\n\n(seg :num -> num -> (\206\177, \206\178) path -> (\206\177, \206\178) path) :num -> num -> (\206\177, \206\178) path -> (\206\177, \206\178) path\n\non line 156, characters 14-16\n\nunification failure message: Attempt to unify different type operators: list$list and min$fun\n (THEN1 on line 163)", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 156, characters 14-16:\n\nType inference failure: unable to infer a type for the application of\n\n(LENGTH :\206\177 list -> num) :\206\177 list -> num\n\non line 156, characters 7-12\n\nto\n\n(seg :num -> num -> (\206\177, \206\178) path -> (\206\177, \206\178) path) :num -> num -> (\206\177, \206\178) path -> (\206\177, \206\178) path\n\non line 156, characters 14-16\n\nunification failure message: Attempt to unify different type operators: list$list and min$fun\n (THEN1 on line 163)", origin_function = "type-analysis", origin_structure = "Preterm"}
BinomialHeapTheory                                                                                   M-KILLED
ImplicitQueueTheory                                                                                  M-KILLED
LazyPairingHeapTheory                                                                                M-KILLED