CakeML Regression Test

Job 808

CakeML:0e4fa06ab0d36c1241d6932a06a3ca93303d0c19
  Remove compute-attribute-losing save_thm in Candle's monadic kernel [Apr 19 07:40:16]
HOL:057a3046e41b50db616e5d385e9b63e940b4957e
  Deal with bad rebindings of theorems under src/ [Apr 15 07:09:08]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 19 13:45:01 Claimed job
Apr 19 13:45:05 Reusing HOL
Apr 19 13:45:52 Starting developers
Apr 19 13:45:54 Finished developers                                               2s  20MB
Apr 19 13:45:54 Starting developers/bin
Apr 19 13:47:06 Finished developers/bin                                        1m11s 918MB
Apr 19 13:47:06 Starting semantics/ffi
Apr 19 13:47:16 Finished semantics/ffi                                            9s 235MB
Apr 19 13:47:16 Starting semantics
Apr 19 13:48:39 Finished semantics                                             1m22s   1GB
Apr 19 13:48:39 Starting semantics/proofs
Apr 19 13:51:33 Finished semantics/proofs                                      2m53s   1GB
Apr 19 13:51:33 Starting basis/pure
Apr 19 13:52:20 Finished basis/pure                                              46s 710MB
Apr 19 13:52:20 Starting translator
Apr 19 13:53:59 Finished translator                                            1m38s   1GB
Apr 19 13:53:59 Starting compiler/parsing
Apr 19 13:54:57 Finished compiler/parsing                                        57s   1GB
Apr 19 13:54:57 Starting characteristic
Apr 19 14:00:09 Finished characteristic                                        5m11s   1GB
Apr 19 14:00:09 Starting translator/monadic
Apr 19 14:01:40 Finished translator/monadic                                    1m30s   1GB
Apr 19 14:01:40 Starting basis
Apr 19 14:18:07 Finished basis                                                16m26s   1GB
Apr 19 14:18:07 Starting compiler/inference
Apr 19 14:19:40 Finished compiler/inference                                    1m32s   1GB
Apr 19 14:19:40 Starting compiler/backend/reg_alloc
Apr 19 14:20:33 Finished compiler/backend/reg_alloc                              52s   1GB
Apr 19 14:20:33 Starting compiler/backend/gc
Apr 19 14:28:32 Finished compiler/backend/gc                                   7m58s   1GB
Apr 19 14:28:32 Starting compiler/backend
Apr 19 14:28:35 Finished compiler/backend                                         2s  23MB
Apr 19 14:28:35 Starting compiler/encoders/asm
Apr 19 14:28:37 Finished compiler/encoders/asm                                    1s  16MB
Apr 19 14:28:37 Starting compiler/encoders/x64
Apr 19 14:29:02 Finished compiler/encoders/x64                                   24s 555MB
Apr 19 14:29:02 Starting compiler/encoders/arm6
Apr 19 14:29:48 Finished compiler/encoders/arm6                                  45s 732MB
Apr 19 14:29:48 Starting compiler/encoders/arm8
Apr 19 14:30:01 Finished compiler/encoders/arm8                                  13s 619MB
Apr 19 14:30:02 Starting compiler/encoders/mips
Apr 19 14:30:19 Finished compiler/encoders/mips                                  17s   1GB
Apr 19 14:30:20 Starting compiler/encoders/riscv
Apr 19 14:30:35 Finished compiler/encoders/riscv                                 14s 960MB
Apr 19 14:30:35 Starting compiler/encoders/ag32
Apr 19 14:30:52 Finished compiler/encoders/ag32                                  17s 744MB
Apr 19 14:30:53 Starting compiler/backend/x64
Apr 19 14:31:10 Finished compiler/backend/x64                                    17s 855MB
Apr 19 14:31:10 Starting compiler/backend/arm6
Apr 19 14:31:29 Finished compiler/backend/arm6                                   18s   1GB
Apr 19 14:31:29 Starting compiler/backend/arm8
Apr 19 14:31:48 Finished compiler/backend/arm8                                   18s   1GB
Apr 19 14:31:48 Starting compiler/backend/mips
Apr 19 14:32:08 Finished compiler/backend/mips                                   19s   1GB
Apr 19 14:32:08 Starting compiler/backend/riscv
Apr 19 14:32:28 Finished compiler/backend/riscv                                  19s   1GB
Apr 19 14:32:28 Starting compiler/backend/ag32
Apr 19 14:33:35 Finished compiler/backend/ag32                                 1m06s   1GB
Apr 19 14:33:35 Starting compiler/parsing/proofs
Apr 19 14:39:06 Finished compiler/parsing/proofs                               5m30s   1GB
Apr 19 14:39:06 Starting compiler/inference/proofs
Apr 19 14:41:45 Finished compiler/inference/proofs                             2m39s   1GB
Apr 19 14:41:45 Starting compiler/backend/semantics
Apr 19 14:48:36 Finished compiler/backend/semantics                            6m50s   2GB
Apr 19 14:48:36 Starting compiler/backend/reg_alloc/proofs
Apr 19 14:51:14 Finished compiler/backend/reg_alloc/proofs                     2m37s 810MB
Apr 19 14:51:14 Starting compiler/backend/proofs
Apr 19 15:28:24 Finished compiler/backend/proofs                              37m10s   3GB
Apr 19 15:28:25 Starting compiler/encoders/x64/proofs
Apr 19 15:37:17 Finished compiler/encoders/x64/proofs                          8m52s   5GB
Apr 19 15:37:17 Starting compiler/encoders/arm6/proofs
Apr 19 15:49:12 Finished compiler/encoders/arm6/proofs                        11m55s   6GB
Apr 19 15:49:13 Starting compiler/encoders/arm8/proofs
Apr 19 15:54:37 Finished compiler/encoders/arm8/proofs                         5m24s   1GB
Apr 19 15:54:37 Starting compiler/encoders/mips/proofs
Apr 19 16:03:54 Finished compiler/encoders/mips/proofs                         9m16s   2GB
Apr 19 16:03:55 Starting compiler/encoders/riscv/proofs
Apr 19 16:12:03 Finished compiler/encoders/riscv/proofs                        8m08s   1GB
Apr 19 16:12:03 Starting compiler/encoders/ag32/proofs
Apr 19 16:14:31 Finished compiler/encoders/ag32/proofs                         2m27s 634MB
Apr 19 16:14:31 Starting compiler/backend/x64/proofs
Apr 19 16:14:51 Finished compiler/backend/x64/proofs                             19s   1GB
Apr 19 16:14:51 Starting compiler/backend/arm6/proofs
Apr 19 16:15:13 Finished compiler/backend/arm6/proofs                            21s   1GB
Apr 19 16:15:14 Starting compiler/backend/arm8/proofs
Apr 19 16:15:34 Finished compiler/backend/arm8/proofs                            20s   1GB
Apr 19 16:15:35 Starting compiler/backend/mips/proofs
Apr 19 16:15:55 Finished compiler/backend/mips/proofs                            20s   1GB
Apr 19 16:15:55 Starting compiler/backend/riscv/proofs
Apr 19 16:16:16 Finished compiler/backend/riscv/proofs                           20s   1GB
Apr 19 16:16:16 Starting compiler/backend/ag32/proofs
Apr 19 16:25:00 Finished compiler/backend/ag32/proofs                          8m43s   2GB
Apr 19 16:25:01 Starting compiler/proofs
Apr 19 16:26:36 Finished compiler/proofs                                       1m35s   3GB
Apr 19 16:26:36 Starting candle/set-theory
Apr 19 16:27:03 Finished candle/set-theory                                       26s 743MB
Apr 19 16:27:03 Starting candle/syntax-lib
Apr 19 16:27:14 Finished candle/syntax-lib                                       10s 672MB
Apr 19 16:27:14 Starting candle/standard/syntax
Apr 19 16:28:59 Finished candle/standard/syntax                                1m44s   1GB
Apr 19 16:28:59 Starting candle/standard/semantics
Apr 19 16:30:37 Finished candle/standard/semantics                             1m37s   1GB
Apr 19 16:30:37 Starting candle/standard/monadic
Apr 19 16:32:10 Finished candle/standard/monadic                               1m32s   1GB
Apr 19 16:32:10 Starting candle/standard/ml_kernel
Apr 19 16:36:04 Finished candle/standard/ml_kernel                             3m54s   3GB
Apr 19 16:36:05 Starting candle/standard/opentheory
Apr 19 16:44:58 Finished candle/standard/opentheory                            8m53s   3GB
Apr 19 16:44:59 Starting candle/standard/opentheory/compilation
Apr 19 16:45:30 FAILED: candle/standard/opentheory/compilation
]0;Holmake: ~/oven/regression/cakeml-808/basis/pure]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-808/basis/pure]0;Holmake: ~/oven/regression/cakeml-808/misc]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-808/misc]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-808/misc]0;Holmake: ~/oven/regression/cakeml-808/developers]0;Holmake: ~/oven/regression/cakeml-808/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-808/misc]0;Holmake: ~/oven/regression/cakeml-808/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-808/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-808/misc]0;Holmake: ~/oven/regression/cakeml-808/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-808/basis/pure]0;Holmake: ~/oven/regression/cakeml-808/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-808/basis]0;Holmake: ~/oven/regression/cakeml-808/characteristic]0;Holmake: ~/oven/regression/cakeml-808/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-808/semantics]0;Holmake: ~/oven/regression/cakeml-808/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-808/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-808/semantics]0;Holmake: ~/oven/regression/cakeml-808/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-808/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-808/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-808/characteristic]0;Holmake: ~/oven/regression/cakeml-808/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-808/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-808/characteristic]0;Holmake: ~/oven/regression/cakeml-808/translator]0;Holmake: ~/oven/regression/cakeml-808/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-808/characteristic]0;Holmake: ~/oven/regression/cakeml-808/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-808/basis]0;Holmake: ~/oven/regression/cakeml-808/translator/monadic]0;Holmake: ~/oven/regression/cakeml-808/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-808/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-808/translator/monadic]0;Holmake: ~/oven/regression/cakeml-808/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-808/basis]0;Holmake: ~/oven/regression/cakeml-808/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: ..]0;Holmake: ../../ml_kernel]0;Holmake: ../../monadic]0;Holmake: ../../syntax]0;Holmake: ../../../syntax-lib]0;Holmake: ../../../syntax-libWorking in $(CAKEMLDIR)/candle/syntax-lib
]0;Holmake: ../../syntax]0;Holmake: ../../syntaxWorking in $(CAKEMLDIR)/candle/standard/syntax
]0;Holmake: ../../monadic]0;Holmake: ../../monadicWorking in $(CAKEMLDIR)/candle/standard/monadic
]0;Holmake: ../../ml_kernel]0;Holmake: ../../ml_kernelWorking in $(CAKEMLDIR)/candle/standard/ml_kernel
]0;Holmake: ..]0;Holmake: ../../semantics]0;Holmake: ../../../set-theory]0;Holmake: ../../../set-theoryWorking in $(CAKEMLDIR)/candle/set-theory
]0;Holmake: ../../semantics]0;Holmake: ../../semanticsWorking in $(CAKEMLDIR)/candle/standard/semantics
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/candle/standard/opentheory
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-808/compiler]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/reg_alloc]0;Holmake: ~/oven/regression/cakeml-808/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-808/unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/reg_alloc]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/asm]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/asm]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend]0;Holmake: ~/oven/regression/cakeml-808/compiler/backendWorking in $(CAKEMLDIR)/compiler/backend
]0;Holmake: ~/oven/regression/cakeml-808/compiler]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/ag32]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/ag32]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/ag32Working in $(CAKEMLDIR)/compiler/encoders/ag32
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/ag32]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/ag32Working in $(CAKEMLDIR)/compiler/backend/ag32
]0;Holmake: ~/oven/regression/cakeml-808/compiler]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/arm6]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/arm6]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/lib]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/arm6]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm/step
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/arm6]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/arm6Working in $(CAKEMLDIR)/compiler/encoders/arm6
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/arm6]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/arm6Working in $(CAKEMLDIR)/compiler/backend/arm6
]0;Holmake: ~/oven/regression/cakeml-808/compiler]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/arm8]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/arm8]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm8/model]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/arm8]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm8/step]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/arm8/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/arm8]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/arm8Working in $(CAKEMLDIR)/compiler/encoders/arm8
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/arm8]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/arm8Working in $(CAKEMLDIR)/compiler/backend/arm8
]0;Holmake: ~/oven/regression/cakeml-808/compiler]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/mips]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/mips]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/mips/model]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/mips]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/mips/step]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/mips/stepWorking in $(HOLDIR)/examples/l3-machine-code/mips/step
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/mips]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/mipsWorking in $(CAKEMLDIR)/compiler/encoders/mips
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/mips]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/mipsWorking in $(CAKEMLDIR)/compiler/backend/mips
]0;Holmake: ~/oven/regression/cakeml-808/compiler]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/riscv]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/riscv]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/riscv/model]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/riscv]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/riscv/stepWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/riscv]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/riscvWorking in $(CAKEMLDIR)/compiler/encoders/riscv
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/riscv]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/riscvWorking in $(CAKEMLDIR)/compiler/backend/riscv
]0;Holmake: ~/oven/regression/cakeml-808/compiler]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/x64]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/x64]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/x64/model]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/x64/modelWorking in $(HOLDIR)/examples/l3-machine-code/x64/model
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/x64]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/x64/step]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/l3-machine-code/x64/stepWorking in $(HOLDIR)/examples/l3-machine-code/x64/step
]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/x64]0;Holmake: ~/oven/regression/cakeml-808/compiler/encoders/x64Working in $(CAKEMLDIR)/compiler/encoders/x64
]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/x64]0;Holmake: ~/oven/regression/cakeml-808/compiler/backend/x64Working in $(CAKEMLDIR)/compiler/backend/x64
]0;Holmake: ~/oven/regression/cakeml-808/compiler]0;Holmake: ~/oven/regression/cakeml-808/compiler/inference]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/unification/triangular]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-057a3046e41b50db616e5d385e9b63e940b4957e/examples/unification/triangular/first-orderWorking in $(HOLDIR)/examples/unification/triangular/first-order
]0;Holmake: ~/oven/regression/cakeml-808/compiler/inference]0;Holmake: ~/oven/regression/cakeml-808/compiler/inferenceWorking in $(CAKEMLDIR)/compiler/inference
]0;Holmake: ~/oven/regression/cakeml-808/compiler]0;Holmake: ~/oven/regression/cakeml-808/compilerWorking in $(CAKEMLDIR)/compiler
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/candle/standard/opentheory/compilation
Starting work on readerCompileTheory
Starting work on README.md
README.md                                                                    OK
readerCompileTheory                                                 FAILED! <1>
         backend_commonTheory.bind_tag_def,
         backend_commonTheory.chr_tag_def,
         ...
         ],
      computeLib.Tys [(... ...)],
      computeLib.Defs [...],
      ... ...,
      ...
      ]
 Uncaught exception: Fail "Static Errors"