Job 769

CakeML:363f4063657209f371cfe85a62fd00695856a200
  Linear scan: change the name of the theorem `set_MAP_FST_toAList` in  [Apr 03 07:31:27]
#623 (linear-scan)
Merging into:4e837ffdd2b7c207dc897fe6802efd3407fce74d
  Merge pull request #624 from CakeML/cf-div [Mar 31 19:10:45]
HOL:d872621acf3aa74495543d022b8e3e4d9b72ed25
  Remove unused CT from DB.sig (it's used internally but not elsewhere) [Mar 30 06:56:26]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 03 07:45:23 Claimed job
Apr 03 07:45:27 Reusing HOL
Apr 03 07:46:21 Starting developers
Apr 03 07:46:23 Finished developers                                               2s  20MB
Apr 03 07:46:23 Starting developers/bin
Apr 03 07:47:33 Finished developers/bin                                        1m09s 918MB
Apr 03 07:47:34 Starting semantics/ffi
Apr 03 07:47:44 Finished semantics/ffi                                           10s 211MB
Apr 03 07:47:44 Starting semantics
Apr 03 07:49:05 Finished semantics                                             1m20s   1GB
Apr 03 07:49:06 Starting semantics/proofs
Apr 03 07:52:02 Finished semantics/proofs                                      2m56s   1GB
Apr 03 07:52:02 Starting basis/pure
Apr 03 07:52:50 Finished basis/pure                                              47s 589MB
Apr 03 07:52:50 Starting translator
Apr 03 07:54:30 Finished translator                                            1m40s   1GB
Apr 03 07:54:30 Starting compiler/parsing
Apr 03 07:55:28 Finished compiler/parsing                                        56s   2GB
Apr 03 07:55:28 Starting characteristic
Apr 03 08:00:41 Finished characteristic                                        5m12s   1GB
Apr 03 08:00:41 Starting translator/monadic
Apr 03 08:02:09 Finished translator/monadic                                    1m27s   1GB
Apr 03 08:02:09 Starting basis
Apr 03 08:18:46 Finished basis                                                16m36s   2GB
Apr 03 08:18:46 Starting compiler/inference
Apr 03 08:20:19 Finished compiler/inference                                    1m32s   2GB
Apr 03 08:20:19 Starting compiler/backend/reg_alloc
Apr 03 08:21:18 Finished compiler/backend/reg_alloc                              59s   1GB
Apr 03 08:21:19 Starting compiler/backend/gc
Apr 03 08:29:18 Finished compiler/backend/gc                                   7m58s   1GB
Apr 03 08:29:18 Starting compiler/backend
Apr 03 08:29:21 Finished compiler/backend                                         2s  16MB
Apr 03 08:29:21 Starting compiler/encoders/asm
Apr 03 08:29:23 Finished compiler/encoders/asm                                    1s  13MB
Apr 03 08:29:23 Starting compiler/encoders/x64
Apr 03 08:29:47 Finished compiler/encoders/x64                                   24s 925MB
Apr 03 08:29:48 Starting compiler/encoders/arm6
Apr 03 08:30:32 Finished compiler/encoders/arm6                                  44s 752MB
Apr 03 08:30:33 Starting compiler/encoders/arm8
Apr 03 08:30:46 Finished compiler/encoders/arm8                                  12s 594MB
Apr 03 08:30:46 Starting compiler/encoders/mips
Apr 03 08:31:05 Finished compiler/encoders/mips                                  18s 902MB
Apr 03 08:31:05 Starting compiler/encoders/riscv
Apr 03 08:31:21 Finished compiler/encoders/riscv                                 15s 788MB
Apr 03 08:31:21 Starting compiler/encoders/ag32
Apr 03 08:31:38 Finished compiler/encoders/ag32                                  16s 657MB
Apr 03 08:31:39 Starting compiler/backend/x64
Apr 03 08:31:57 Finished compiler/backend/x64                                    17s 793MB
Apr 03 08:31:57 Starting compiler/backend/arm6
Apr 03 08:32:17 Finished compiler/backend/arm6                                   19s   1GB
Apr 03 08:32:17 Starting compiler/backend/arm8
Apr 03 08:32:35 Finished compiler/backend/arm8                                   17s 917MB
Apr 03 08:32:35 Starting compiler/backend/mips
Apr 03 08:32:54 Finished compiler/backend/mips                                   18s   1GB
Apr 03 08:32:55 Starting compiler/backend/riscv
Apr 03 08:33:13 Finished compiler/backend/riscv                                  18s   1GB
Apr 03 08:33:13 Starting compiler/backend/ag32
Apr 03 08:34:20 Finished compiler/backend/ag32                                 1m06s   1GB
Apr 03 08:34:20 Starting compiler/parsing/proofs
Apr 03 08:39:54 Finished compiler/parsing/proofs                               5m33s 964MB
Apr 03 08:39:54 Starting compiler/inference/proofs
Apr 03 08:42:34 Finished compiler/inference/proofs                             2m39s   1GB
Apr 03 08:42:35 Starting compiler/backend/semantics
Apr 03 08:49:23 Finished compiler/backend/semantics                            6m48s   2GB
Apr 03 08:49:23 Starting compiler/backend/reg_alloc/proofs
Apr 03 08:52:28 Finished compiler/backend/reg_alloc/proofs                     3m04s 821MB
Apr 03 08:52:28 Starting compiler/backend/proofs
Apr 03 09:29:25 Finished compiler/backend/proofs                              36m56s   3GB
Apr 03 09:29:25 Starting compiler/encoders/x64/proofs
Apr 03 10:57:49 Resuming compiler/encoders/x64/proofs
Apr 03 10:57:51 Finished compiler/encoders/x64/proofs                             1s  16MB
Apr 03 10:57:51 Starting compiler/encoders/arm6/proofs
Apr 03 11:09:45 Finished compiler/encoders/arm6/proofs                        11m53s   6GB
Apr 03 11:09:45 Starting compiler/encoders/arm8/proofs
Apr 03 11:15:10 Finished compiler/encoders/arm8/proofs                         5m24s   1GB
Apr 03 11:15:11 Starting compiler/encoders/mips/proofs
Apr 03 11:24:21 Finished compiler/encoders/mips/proofs                         9m09s   2GB
Apr 03 11:24:21 Starting compiler/encoders/riscv/proofs
Apr 03 11:32:35 Finished compiler/encoders/riscv/proofs                        8m14s 960MB
Apr 03 11:32:36 Starting compiler/encoders/ag32/proofs
Apr 03 11:35:03 Finished compiler/encoders/ag32/proofs                         2m26s 649MB
Apr 03 11:35:03 Starting compiler/backend/x64/proofs
Apr 03 11:35:22 Finished compiler/backend/x64/proofs                             18s 795MB
Apr 03 11:35:22 Starting compiler/backend/arm6/proofs
Apr 03 11:35:44 Finished compiler/backend/arm6/proofs                            21s   1GB
Apr 03 11:35:45 Starting compiler/backend/arm8/proofs
Apr 03 11:36:03 Finished compiler/backend/arm8/proofs                            18s 786MB
Apr 03 11:36:04 Starting compiler/backend/mips/proofs
Apr 03 11:36:24 Finished compiler/backend/mips/proofs                            19s   1GB
Apr 03 11:36:24 Starting compiler/backend/riscv/proofs
Apr 03 11:36:44 Finished compiler/backend/riscv/proofs                           20s   1GB
Apr 03 11:36:44 Starting compiler/backend/ag32/proofs
Apr 03 11:45:16 Finished compiler/backend/ag32/proofs                          8m30s   2GB
Apr 03 11:45:16 Starting compiler/proofs
Apr 03 11:46:32 Finished compiler/proofs                                       1m15s   2GB
Apr 03 11:46:32 Starting candle/set-theory
Apr 03 11:46:59 Finished candle/set-theory                                       26s 717MB
Apr 03 11:46:59 Starting candle/syntax-lib
Apr 03 11:47:10 Finished candle/syntax-lib                                       10s 532MB
Apr 03 11:47:10 Starting candle/standard/syntax
Apr 03 11:48:54 Finished candle/standard/syntax                                1m43s 902MB
Apr 03 11:48:54 Starting candle/standard/semantics
Apr 03 11:50:31 Finished candle/standard/semantics                             1m36s   1GB
Apr 03 11:50:31 Starting candle/standard/monadic
Apr 03 11:52:04 Finished candle/standard/monadic                               1m32s   1GB
Apr 03 11:52:04 Starting candle/standard/ml_kernel
Apr 03 11:55:50 Finished candle/standard/ml_kernel                             3m45s   3GB
Apr 03 11:55:50 Starting candle/standard/opentheory
Apr 03 12:04:03 Finished candle/standard/opentheory                            8m13s   3GB
Apr 03 12:04:03 Starting candle/standard/opentheory/compilation
Apr 03 12:32:58 Finished candle/standard/opentheory/compilation               28m54s  14GB
Apr 03 12:32:58 Starting candle/standard/opentheory/compilation/proofs
Apr 03 12:33:43 Finished candle/standard/opentheory/compilation/proofs           44s   2GB
Apr 03 12:33:43 Starting characteristic/examples
Apr 03 12:35:06 Finished characteristic/examples                               1m22s   2GB
Apr 03 12:35:06 Starting tutorial/solutions
Apr 03 12:48:09 Finished tutorial/solutions                                   13m02s   5GB
Apr 03 12:48:09 Starting translator/monadic/examples
Apr 03 12:50:34 Finished translator/monadic/examples                           2m24s   2GB
Apr 03 12:50:34 Starting examples
Apr 03 12:58:50 Finished examples                                              8m15s   3GB
Apr 03 12:58:50 Starting examples/compilation/x64
Apr 03 14:52:04 Finished examples/compilation/x64                           1h53m13s  11GB
Apr 03 14:52:04 Starting examples/compilation/x64/proofs
Apr 03 14:53:29 Finished examples/compilation/x64/proofs                       1m24s   2GB
Apr 03 14:53:29 Starting examples/compilation/ag32
Apr 03 15:21:19 Finished examples/compilation/ag32                            27m49s   6GB
Apr 03 15:21:19 Starting examples/compilation/ag32/proofs
Apr 03 15:22:09 Finished examples/compilation/ag32/proofs                        49s   3GB
Apr 03 15:22:09 Starting translator/okasaki-examples
Apr 03 15:26:08 Finished translator/okasaki-examples                           3m58s   1GB
Apr 03 15:26:08 Starting translator/other-examples
Apr 03 15:26:50 Finished translator/other-examples                               42s   1GB
Apr 03 15:26:51 Starting compiler/parsing/tests
Apr 03 15:27:17 Finished compiler/parsing/tests                                  25s 540MB
Apr 03 15:27:17 Starting compiler/inference/tests
Apr 03 15:31:22 Finished compiler/inference/tests                              4m04s   3GB
Apr 03 15:31:22 Starting compiler/bootstrap/translation
Apr 03 16:19:26 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/lib]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm8/model]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/mips/model]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/riscv/model]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/x64/model]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-769/basis]0;Holmake: ~/oven/regression/cakeml-769/basis/pure]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/oven/regression/cakeml-769/basis/pure]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/oven/regression/cakeml-769/basis/pure]0;Holmake: ~/oven/regression/cakeml-769/misc]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/oven/regression/cakeml-769/misc]0;Holmake: ~/oven/regression/cakeml-769/developers]0;Holmake: ~/oven/regression/cakeml-769/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/oven/regression/cakeml-769/misc]0;Holmake: ~/oven/regression/cakeml-769/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-769/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/oven/regression/cakeml-769/misc]0;Holmake: ~/oven/regression/cakeml-769/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/oven/regression/cakeml-769/basis/pure]0;Holmake: ~/oven/regression/cakeml-769/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/oven/regression/cakeml-769/basis]0;Holmake: ~/oven/regression/cakeml-769/characteristic]0;Holmake: ~/oven/regression/cakeml-769/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-769/semantics]0;Holmake: ~/oven/regression/cakeml-769/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-769/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/oven/regression/cakeml-769/semantics]0;Holmake: ~/oven/regression/cakeml-769/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/oven/regression/cakeml-769/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-769/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/oven/regression/cakeml-769/characteristic]0;Holmake: ~/oven/regression/cakeml-769/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-769/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/oven/regression/cakeml-769/characteristic]0;Holmake: ~/oven/regression/cakeml-769/translator]0;Holmake: ~/oven/regression/cakeml-769/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/oven/regression/cakeml-769/characteristic]0;Holmake: ~/oven/regression/cakeml-769/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/oven/regression/cakeml-769/basis]0;Holmake: ~/oven/regression/cakeml-769/translator/monadic]0;Holmake: ~/oven/regression/cakeml-769/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-769/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/oven/regression/cakeml-769/translator/monadic]0;Holmake: ~/oven/regression/cakeml-769/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/oven/regression/cakeml-769/basis]0;Holmake: ~/oven/regression/cakeml-769/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ~/oven/regression/cakeml-769/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-769/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ../../backend]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ../..]0;Holmake: ../../backend/ag32]0;Holmake: ../../encoders/ag32]0;Holmake: ../../encoders/ag32[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32[0m
]0;Holmake: ../../backend/ag32]0;Holmake: ../../backend/ag32[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm6]0;Holmake: ../../encoders/arm6]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm8]0;Holmake: ../../encoders/arm8]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm8/step]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/arm8/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step[0m
]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ../..]0;Holmake: ../../backend/mips]0;Holmake: ../../encoders/mips]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/mips/step]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/mips/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/step[0m
]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ../..]0;Holmake: ../../backend/riscv]0;Holmake: ../../encoders/riscv]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ../..]0;Holmake: ../../backend/x64]0;Holmake: ../../encoders/x64]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/x64/step]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ../..]0;Holmake: ../../inference]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/unification/triangular]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-d872621acf3aa74495543d022b8e3e4d9b72ed25/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ../../inference]0;Holmake: ../../inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ../..]0;Holmake: ../..[1mWorking in $(CAKEMLDIR)/compiler[0m
]0;Holmake: .]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofs[1mWorking in $(CAKEMLDIR)/compiler/inference/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/bootstrap/translation[0m
Starting work on to_flatProgTheory
Starting work on README.md
README.md                                                                    OK
to_flatProgTheory                                                            OK
Starting work on to_patProgTheory
to_patProgTheory                                                             OK
Starting work on to_closProgTheory
to_closProgTheory                                                            OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                             OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                             OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                            OK
Starting work on lexerProgTheory
lexerProgTheory                                                              OK
Starting work on parserProgTheory
parserProgTheory                                                             OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                 FAILED! <1>
 Saved theorem _____ "linear_scan_hidden_state_sorted_regs_fupd_v_thm"
 Translating linear_scan_hidden_state_sorted_moves_fupd
 Adding nsLookup representation thms for [reg_allocProg_env_135]
 Saved theorem _____ "nsLookup_reg_allocProg_env_136_pfun_eqs"
 Saved theorem _____ "linear_scan_hidden_state_sorted_moves_fupd_v_thm"
 Translating monadic run: run_linear_reg_alloc_intervals
 Defining local functions: 32 31 30 29 28 27 26 25 24 23 22 21 20 19 18 17 16 15 14 13 12 11 10 9 8 7 6 5 4 3 2 1 
 error in quse /home/cake/oven/regression/cakeml-769/compiler/bootstrap/translation/reg_allocProgScript.sml : Empty
 error in load reg_allocProgScript : Empty
 Uncaught exception: Empty