Job 448

CakeML:03d27b047dcb8058e2b386b9ae91ec2fc40e6d62
  Finish fixing data_to_word_assignProof [Aug 23 08:26:35]
#514 (linear-scan)
Merging into:48b96e8ed899928f3fa40f6f2237bb33e9ea8c25
  Merge pull request #512 from CakeML/translator-module-ctors [Aug 23 06:45:57]
HOL:b440d91de4ea0da60e3ebf207c5accaaf9892bf6
  Fix ParseDatatype bug when parsing Datatype syntax [Aug 23 00:55:32]
Machine:cakeml1798 4.4.0-98-generic x86_64 GNU/Linux

Aug 23 09:10:55 Claimed job
Aug 23 09:11:02 Reusing HOL
Aug 23 09:11:28 Starting developers/bin
Aug 23 09:11:38 Finished developers/bin                                           7s 142MB
Aug 23 09:11:40 Starting semantics/ffi
Aug 23 09:11:58 Finished semantics/ffi                                           16s 262MB
Aug 23 09:12:00 Starting semantics
Aug 23 09:13:58 Finished semantics                                             1m55s 798MB
Aug 23 09:14:00 Starting semantics/proofs
Aug 23 09:19:20 Finished semantics/proofs                                      5m18s   1GB
Aug 23 09:19:22 Starting basis/pure
Aug 23 09:20:53 Finished basis/pure                                            1m28s 722MB
Aug 23 09:20:55 Starting translator
Aug 23 09:22:50 Finished translator                                            1m53s 839MB
Aug 23 09:22:52 Starting compiler/parsing
Aug 23 09:25:14 Finished compiler/parsing                                      2m19s   3GB
Aug 23 09:25:16 Starting characteristic
Aug 23 09:29:49 Finished characteristic                                        4m31s   1GB
Aug 23 09:29:51 Starting translator/monadic
Aug 23 09:32:34 Finished translator/monadic                                    2m40s   1GB
Aug 23 09:32:36 Starting basis
Aug 23 10:00:40 Finished basis                                                28m02s   3GB
Aug 23 10:00:42 Starting compiler/inference
Aug 23 10:03:02 Finished compiler/inference                                    2m18s   1GB
Aug 23 10:03:04 Starting compiler/backend/reg_alloc
Aug 23 10:04:30 Finished compiler/backend/reg_alloc                            1m23s   1GB
Aug 23 10:04:32 Starting compiler/backend/gc
Aug 23 10:17:56 Finished compiler/backend/gc                                  13m21s   2GB
Aug 23 10:17:58 Starting compiler/backend
Aug 23 10:18:03 Finished compiler/backend                                         3s  18MB
Aug 23 10:18:05 Starting compiler/encoders/asm
Aug 23 10:18:08 Finished compiler/encoders/asm                                    0s  16MB
Aug 23 10:18:10 Starting compiler/encoders/x64
Aug 23 10:18:36 Finished compiler/encoders/x64                                   24s 424MB
Aug 23 10:18:38 Starting compiler/encoders/arm6
Aug 23 10:19:49 Finished compiler/encoders/arm6                                1m08s 378MB
Aug 23 10:19:51 Starting compiler/encoders/arm8
Aug 23 10:20:05 Finished compiler/encoders/arm8                                  11s 372MB
Aug 23 10:20:07 Starting compiler/encoders/mips
Aug 23 10:20:23 Finished compiler/encoders/mips                                  14s 503MB
Aug 23 10:20:25 Starting compiler/encoders/riscv
Aug 23 10:20:40 Finished compiler/encoders/riscv                                 12s 395MB
Aug 23 10:20:42 Starting compiler/backend/x64
Aug 23 10:21:15 Finished compiler/backend/x64                                    31s   1GB
Aug 23 10:21:17 Starting compiler/backend/arm6
Aug 23 10:21:52 Finished compiler/backend/arm6                                   33s   1GB
Aug 23 10:21:54 Starting compiler/backend/arm8
Aug 23 10:22:27 Finished compiler/backend/arm8                                   31s   1GB
Aug 23 10:22:29 Starting compiler/backend/mips
Aug 23 10:23:03 Finished compiler/backend/mips                                   31s   1GB
Aug 23 10:23:05 Starting compiler/backend/riscv
Aug 23 10:23:37 Finished compiler/backend/riscv                                  30s   1GB
Aug 23 10:23:39 Starting compiler/parsing/proofs
Aug 23 10:27:46 Finished compiler/parsing/proofs                               4m04s 691MB
Aug 23 10:27:48 Starting compiler/inference/proofs
Aug 23 10:32:40 Finished compiler/inference/proofs                             4m49s   1GB
Aug 23 10:32:42 Starting compiler/backend/semantics
Aug 23 10:47:06 Finished compiler/backend/semantics                           14m21s   2GB
Aug 23 10:47:08 Starting compiler/backend/reg_alloc/proofs
Aug 23 10:57:27 FAILED: compiler/backend/reg_alloc/proofs
]0;Holmake: ../../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/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: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]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: ..]0;Holmake: ../../../../translator/monadic]0;Holmake: ../../../../characteristic]0;Holmake: ../../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-b440d91de4ea0da60e3ebf207c5accaaf9892bf6/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../../basis/pure]0;Holmake: ../../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]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: ../../../../translator]0;Holmake: ../../../../semantics/proofs]0;Holmake: ../../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/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: ../../../../translator/monadic]0;Holmake: ../../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ..]0;Holmake: ../../../../unverified/reg_alloc]0;Holmake: ../../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Starting work on heap
heap                                                                                                                                                       OK
Starting work on reg_allocProofTheory
reg_allocProofTheory                                                                                                                                       OK
Starting work on linear_scanProofTheory
linear_scanProofTheory                                                                                                                            FAILED! <1>
 
 f d opt. f d = d  the d (lift f opt) = f (the d opt)
 
 failed.
 First unsolved sub-goal is
 
 the d (lift f NONE) = d
 
 Failed to prove theorem the_lift.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}