Job 446

CakeML:a388060409ae4f10df27563404444c22fddd8348
  Work on fixing data_to_word_assignProof [Aug 22 20:04:39]
#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 06:57:47 Claimed job
Aug 23 06:57:59 Building HOL
Aug 23 07:10:32 Starting developers/bin
Aug 23 07:10:42 Finished developers/bin                                           7s 143MB
Aug 23 07:10:44 Starting semantics/ffi
Aug 23 07:11:46 Finished semantics/ffi                                           59s 324MB
Aug 23 07:11:48 Starting semantics
Aug 23 07:14:08 Finished semantics                                             2m18s 766MB
Aug 23 07:14:10 Starting semantics/proofs
Aug 23 07:19:24 Finished semantics/proofs                                      5m11s   1GB
Aug 23 07:19:26 Starting basis/pure
Aug 23 07:25:14 Finished basis/pure                                            5m46s 731MB
Aug 23 07:25:16 Starting translator
Aug 23 07:27:15 Finished translator                                            1m56s   1GB
Aug 23 07:27:17 Starting compiler/parsing
Aug 23 07:29:39 Finished compiler/parsing                                      2m20s   2GB
Aug 23 07:29:41 Starting characteristic
Aug 23 07:34:16 Finished characteristic                                        4m33s   1GB
Aug 23 07:34:18 Starting translator/monadic
Aug 23 07:36:58 Finished translator/monadic                                    2m38s   1GB
Aug 23 07:37:00 Starting basis
Aug 23 08:05:20 Finished basis                                                28m17s   2GB
Aug 23 08:05:22 Starting compiler/inference
Aug 23 08:08:12 Finished compiler/inference                                    2m48s   2GB
Aug 23 08:08:14 Starting compiler/backend/reg_alloc
Aug 23 08:09:38 Finished compiler/backend/reg_alloc                            1m22s   1GB
Aug 23 08:09:40 Starting compiler/backend/gc
Aug 23 08:24:33 Finished compiler/backend/gc                                  14m50s   3GB
Aug 23 08:24:35 Starting compiler/backend
Aug 23 08:24:40 Finished compiler/backend                                         3s  14MB
Aug 23 08:24:42 Starting compiler/encoders/asm
Aug 23 08:24:45 Finished compiler/encoders/asm                                    0s  12MB
Aug 23 08:24:47 Starting compiler/encoders/x64
Aug 23 08:26:15 Finished compiler/encoders/x64                                 1m26s 496MB
Aug 23 08:26:17 Starting compiler/encoders/arm6
Aug 23 08:29:24 Finished compiler/encoders/arm6                                3m04s   1GB
Aug 23 08:29:26 Starting compiler/encoders/arm8
Aug 23 08:30:12 Finished compiler/encoders/arm8                                  43s 389MB
Aug 23 08:30:14 Starting compiler/encoders/mips
Aug 23 08:31:51 Finished compiler/encoders/mips                                1m35s 869MB
Aug 23 08:31:53 Starting compiler/encoders/riscv
Aug 23 08:33:30 Finished compiler/encoders/riscv                               1m34s 667MB
Aug 23 08:33:32 Starting compiler/backend/x64
Aug 23 08:34:05 Finished compiler/backend/x64                                    30s   1GB
Aug 23 08:34:07 Starting compiler/backend/arm6
Aug 23 08:34:43 Finished compiler/backend/arm6                                   33s   1GB
Aug 23 08:34:45 Starting compiler/backend/arm8
Aug 23 08:35:16 Finished compiler/backend/arm8                                   29s   1GB
Aug 23 08:35:18 Starting compiler/backend/mips
Aug 23 08:35:52 Finished compiler/backend/mips                                   31s   1GB
Aug 23 08:35:54 Starting compiler/backend/riscv
Aug 23 08:36:24 Finished compiler/backend/riscv                                  28s 974MB
Aug 23 08:36:26 Starting compiler/parsing/proofs
Aug 23 08:40:51 Finished compiler/parsing/proofs                               4m22s 817MB
Aug 23 08:40:53 Starting compiler/inference/proofs
Aug 23 08:45:42 Finished compiler/inference/proofs                             4m47s   1GB
Aug 23 08:45:44 Starting compiler/backend/semantics
Aug 23 09:00:20 Finished compiler/backend/semantics                           14m32s   2GB
Aug 23 09:00:22 Starting compiler/backend/reg_alloc/proofs
Aug 23 09:10:47 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"}