CakeML Regression Test

Job 782

CakeML:3ce6ad702be68d639bf61ff0454511bbca4d6b12
  Really make fix for change to ThmSetData API [Apr 10 10:46:19]
#628 (ThmSetData-API-change)
Merging into:ab7ea440afff89d5f90e2b85415c2e27f7894561
  Use Theory.current_definitions instead of fetch [Apr 10 09:36:45]
HOL:729baf5e526741114f4346767d17d0da3a1b6c20
  Remove (generated file) Thm-sig.sml when cleaning src/thm [Apr 07 04:31:14]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 10 10:55:02 Claimed job
Apr 10 10:55:05 Reusing HOL
Apr 10 10:55:53 Starting developers
Apr 10 10:55:55 Finished developers                                               2s  22MB
Apr 10 10:55:55 Starting developers/bin
Apr 10 10:57:09 Finished developers/bin                                        1m13s 918MB
Apr 10 10:57:09 Starting semantics/ffi
Apr 10 10:57:20 Finished semantics/ffi                                           10s 237MB
Apr 10 10:57:20 Starting semantics
Apr 10 10:58:42 Finished semantics                                             1m21s   1GB
Apr 10 10:58:42 Starting semantics/proofs
Apr 10 11:01:39 Finished semantics/proofs                                      2m56s   1GB
Apr 10 11:01:39 Starting basis/pure
Apr 10 11:02:27 Finished basis/pure                                              47s 624MB
Apr 10 11:02:27 Starting translator
Apr 10 11:04:06 Finished translator                                            1m38s   1GB
Apr 10 11:04:06 Starting compiler/parsing
Apr 10 11:05:03 Finished compiler/parsing                                        56s   1GB
Apr 10 11:05:03 Starting characteristic
Apr 10 11:10:15 Finished characteristic                                        5m12s   1GB
Apr 10 11:10:16 Starting translator/monadic
Apr 10 11:11:47 Finished translator/monadic                                    1m31s   1GB
Apr 10 11:11:47 Starting basis
Apr 10 11:28:17 Finished basis                                                16m29s   3GB
Apr 10 11:28:17 Starting compiler/inference
Apr 10 11:30:06 Finished compiler/inference                                    1m48s   1GB
Apr 10 11:30:06 Starting compiler/backend/reg_alloc
Apr 10 11:30:59 Finished compiler/backend/reg_alloc                              53s   1GB
Apr 10 11:31:00 Starting compiler/backend/gc
Apr 10 11:40:03 Finished compiler/backend/gc                                   9m03s   1GB
Apr 10 11:40:04 Starting compiler/backend
Apr 10 11:40:06 Finished compiler/backend                                         2s  17MB
Apr 10 11:40:07 Starting compiler/encoders/asm
Apr 10 11:40:08 Finished compiler/encoders/asm                                    1s  13MB
Apr 10 11:40:08 Starting compiler/encoders/x64
Apr 10 11:41:10 Finished compiler/encoders/x64                                 1m01s 897MB
Apr 10 11:41:10 Starting compiler/encoders/arm6
Apr 10 11:42:49 Finished compiler/encoders/arm6                                1m38s   1GB
Apr 10 11:42:49 Starting compiler/encoders/arm8
Apr 10 11:43:23 Finished compiler/encoders/arm8                                  33s 817MB
Apr 10 11:43:23 Starting compiler/encoders/mips
Apr 10 11:44:31 Finished compiler/encoders/mips                                1m07s   1GB
Apr 10 11:44:31 Starting compiler/encoders/riscv
Apr 10 11:45:53 Finished compiler/encoders/riscv                               1m21s 742MB
Apr 10 11:45:53 Starting compiler/encoders/ag32
Apr 10 11:46:10 Finished compiler/encoders/ag32                                  16s 494MB
Apr 10 11:46:10 Starting compiler/backend/x64
Apr 10 11:46:29 Finished compiler/backend/x64                                    18s   1GB
Apr 10 11:46:29 Starting compiler/backend/arm6
Apr 10 11:46:47 Finished compiler/backend/arm6                                   18s   1GB
Apr 10 11:46:48 Starting compiler/backend/arm8
Apr 10 11:47:06 Finished compiler/backend/arm8                                   18s   1GB
Apr 10 11:47:06 Starting compiler/backend/mips
Apr 10 11:47:25 Finished compiler/backend/mips                                   18s   1GB
Apr 10 11:47:25 Starting compiler/backend/riscv
Apr 10 11:47:45 Finished compiler/backend/riscv                                  19s   1GB
Apr 10 11:47:45 Starting compiler/backend/ag32
Apr 10 11:48:52 Finished compiler/backend/ag32                                 1m06s   1GB
Apr 10 11:48:52 Starting compiler/parsing/proofs
Apr 10 11:54:30 Finished compiler/parsing/proofs                               5m38s   1GB
Apr 10 11:54:30 Starting compiler/inference/proofs
Apr 10 11:57:12 Finished compiler/inference/proofs                             2m40s   1GB
Apr 10 11:57:12 Starting compiler/backend/semantics
Apr 10 12:04:05 Finished compiler/backend/semantics                            6m53s   1GB
Apr 10 12:04:06 Starting compiler/backend/reg_alloc/proofs
Apr 10 12:06:43 Finished compiler/backend/reg_alloc/proofs                     2m36s   1GB
Apr 10 12:06:43 Starting compiler/backend/proofs
Apr 10 12:43:42 Finished compiler/backend/proofs                              36m58s   3GB
Apr 10 12:43:43 Starting compiler/encoders/x64/proofs
Apr 10 12:53:37 Finished compiler/encoders/x64/proofs                          9m54s   5GB
Apr 10 12:53:37 Starting compiler/encoders/arm6/proofs
Apr 10 13:06:41 Finished compiler/encoders/arm6/proofs                        13m03s   6GB
Apr 10 13:06:41 Starting compiler/encoders/arm8/proofs
Apr 10 13:12:17 Finished compiler/encoders/arm8/proofs                         5m35s   1GB
Apr 10 13:12:17 Starting compiler/encoders/mips/proofs
Apr 10 13:22:08 Finished compiler/encoders/mips/proofs                         9m51s   2GB
Apr 10 13:22:09 Starting compiler/encoders/riscv/proofs
Apr 10 13:30:28 Finished compiler/encoders/riscv/proofs                        8m19s 993MB
Apr 10 13:30:28 Starting compiler/encoders/ag32/proofs
Apr 10 13:32:56 Finished compiler/encoders/ag32/proofs                         2m27s 694MB
Apr 10 13:32:56 Starting compiler/backend/x64/proofs
Apr 10 13:33:16 Finished compiler/backend/x64/proofs                             19s 776MB
Apr 10 13:33:16 Starting compiler/backend/arm6/proofs
Apr 10 13:33:37 Finished compiler/backend/arm6/proofs                            20s 917MB
Apr 10 13:33:37 Starting compiler/backend/arm8/proofs
Apr 10 13:33:58 Finished compiler/backend/arm8/proofs                            20s   1GB
Apr 10 13:33:58 Starting compiler/backend/mips/proofs
Apr 10 13:34:18 Finished compiler/backend/mips/proofs                            19s   1GB
Apr 10 13:34:18 Starting compiler/backend/riscv/proofs
Apr 10 13:34:38 Finished compiler/backend/riscv/proofs                           20s   1GB
Apr 10 13:34:39 Starting compiler/backend/ag32/proofs
Apr 10 13:43:25 Finished compiler/backend/ag32/proofs                          8m45s   2GB
Apr 10 13:43:25 Starting compiler/proofs
Apr 10 13:44:54 Finished compiler/proofs                                       1m29s   3GB
Apr 10 13:44:54 Starting candle/set-theory
Apr 10 13:45:21 Finished candle/set-theory                                       26s 644MB
Apr 10 13:45:21 Starting candle/syntax-lib
Apr 10 13:45:32 Finished candle/syntax-lib                                       10s 630MB
Apr 10 13:45:33 Starting candle/standard/syntax
Apr 10 13:47:17 Finished candle/standard/syntax                                1m44s   1GB
Apr 10 13:47:17 Starting candle/standard/semantics
Apr 10 13:48:55 Finished candle/standard/semantics                             1m37s   1GB
Apr 10 13:48:55 Starting candle/standard/monadic
Apr 10 13:50:27 Finished candle/standard/monadic                               1m31s   1GB
Apr 10 13:50:28 Starting candle/standard/ml_kernel
Apr 10 13:54:11 Finished candle/standard/ml_kernel                             3m42s   3GB
Apr 10 13:54:11 Starting candle/standard/opentheory
Apr 10 14:02:26 Finished candle/standard/opentheory                            8m14s   3GB
Apr 10 14:02:26 Starting candle/standard/opentheory/compilation
Apr 10 14:02:49 FAILED: candle/standard/opentheory/compilation
]0;Holmake: ~/oven/regression/cakeml-782/basis/pure]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-782/basis/pure]0;Holmake: ~/oven/regression/cakeml-782/misc]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-782/misc]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-782/misc]0;Holmake: ~/oven/regression/cakeml-782/developers]0;Holmake: ~/oven/regression/cakeml-782/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-782/misc]0;Holmake: ~/oven/regression/cakeml-782/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-782/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-782/misc]0;Holmake: ~/oven/regression/cakeml-782/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-782/basis/pure]0;Holmake: ~/oven/regression/cakeml-782/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-782/basis]0;Holmake: ~/oven/regression/cakeml-782/characteristic]0;Holmake: ~/oven/regression/cakeml-782/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-782/semantics]0;Holmake: ~/oven/regression/cakeml-782/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-782/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-782/semantics]0;Holmake: ~/oven/regression/cakeml-782/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-782/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-782/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-782/characteristic]0;Holmake: ~/oven/regression/cakeml-782/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-782/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-782/characteristic]0;Holmake: ~/oven/regression/cakeml-782/translator]0;Holmake: ~/oven/regression/cakeml-782/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-782/characteristic]0;Holmake: ~/oven/regression/cakeml-782/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-782/basis]0;Holmake: ~/oven/regression/cakeml-782/translator/monadic]0;Holmake: ~/oven/regression/cakeml-782/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-782/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-782/translator/monadic]0;Holmake: ~/oven/regression/cakeml-782/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-782/basis]0;Holmake: ~/oven/regression/cakeml-782/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-782/compiler]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/reg_alloc]0;Holmake: ~/oven/regression/cakeml-782/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-782/unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/reg_alloc]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/asm]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/asm]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend]0;Holmake: ~/oven/regression/cakeml-782/compiler/backendWorking in $(CAKEMLDIR)/compiler/backend
]0;Holmake: ~/oven/regression/cakeml-782/compiler]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/ag32]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/ag32]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/ag32Working in $(CAKEMLDIR)/compiler/encoders/ag32
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/ag32]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/ag32Working in $(CAKEMLDIR)/compiler/backend/ag32
]0;Holmake: ~/oven/regression/cakeml-782/compiler]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/arm6]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/arm6]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/lib]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/arm6]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm/step
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/arm6]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/arm6Working in $(CAKEMLDIR)/compiler/encoders/arm6
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/arm6]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/arm6Working in $(CAKEMLDIR)/compiler/backend/arm6
]0;Holmake: ~/oven/regression/cakeml-782/compiler]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/arm8]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/arm8]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm8/model]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/arm8]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm8/step]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/arm8/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/arm8]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/arm8Working in $(CAKEMLDIR)/compiler/encoders/arm8
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/arm8]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/arm8Working in $(CAKEMLDIR)/compiler/backend/arm8
]0;Holmake: ~/oven/regression/cakeml-782/compiler]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/mips]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/mips]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/mips/model]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/mips]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/mips/step]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/mips/stepWorking in $(HOLDIR)/examples/l3-machine-code/mips/step
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/mips]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/mipsWorking in $(CAKEMLDIR)/compiler/encoders/mips
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/mips]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/mipsWorking in $(CAKEMLDIR)/compiler/backend/mips
]0;Holmake: ~/oven/regression/cakeml-782/compiler]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/riscv]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/riscv]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/riscv/model]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/riscv]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/riscv/stepWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/riscv]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/riscvWorking in $(CAKEMLDIR)/compiler/encoders/riscv
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/riscv]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/riscvWorking in $(CAKEMLDIR)/compiler/backend/riscv
]0;Holmake: ~/oven/regression/cakeml-782/compiler]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/x64]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/x64]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/x64/model]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/x64/modelWorking in $(HOLDIR)/examples/l3-machine-code/x64/model
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/x64]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/x64/step]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/l3-machine-code/x64/stepWorking in $(HOLDIR)/examples/l3-machine-code/x64/step
]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/x64]0;Holmake: ~/oven/regression/cakeml-782/compiler/encoders/x64Working in $(CAKEMLDIR)/compiler/encoders/x64
]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/x64]0;Holmake: ~/oven/regression/cakeml-782/compiler/backend/x64Working in $(CAKEMLDIR)/compiler/backend/x64
]0;Holmake: ~/oven/regression/cakeml-782/compiler]0;Holmake: ~/oven/regression/cakeml-782/compiler/inference]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/unification/triangular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/unification/triangular/first-orderWorking in $(HOLDIR)/examples/unification/triangular/first-order
]0;Holmake: ~/oven/regression/cakeml-782/compiler/inference]0;Holmake: ~/oven/regression/cakeml-782/compiler/inferenceWorking in $(CAKEMLDIR)/compiler/inference
]0;Holmake: ~/oven/regression/cakeml-782/compiler]0;Holmake: ~/oven/regression/cakeml-782/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"