CakeML Regression Test

Job 561

CakeML:60684bfedb3d540303284740ab19d911c93b4362
  Fix for renamed theorem [Nov 18 18:04:36]
#554 (tiny)
Merging into:8ee5d433f5e6a93e9a41ea5e46b961c65130c2ef
  Merge pull request #551 from CakeML/translator-alist-tree [Nov 17 12:09:47]
HOL:e48aefc60b7c4a206ed939646485d31a341e2bfc
  Fully protect wordsLib's use of parser [Nov 17 11:30:47]
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Nov 19 00:43:11 Claimed job
Nov 19 00:44:03 Building HOL
Nov 19 00:53:43 Starting developers/bin
Nov 19 00:54:51 Finished developers/bin                                        1m07s 916MB
Nov 19 00:54:52 Starting semantics/ffi
Nov 19 00:55:32 Finished semantics/ffi                                           39s 355MB
Nov 19 00:55:32 Starting semantics
Nov 19 00:57:12 Finished semantics                                             1m39s   1GB
Nov 19 00:57:13 Starting semantics/proofs
Nov 19 01:00:14 Finished semantics/proofs                                      3m00s   1GB
Nov 19 01:00:14 Starting basis/pure
Nov 19 01:04:02 Finished basis/pure                                            3m47s 685MB
Nov 19 01:04:03 Starting translator
Nov 19 01:07:15 Finished translator                                            3m12s   1GB
Nov 19 01:07:16 Starting compiler/parsing
Nov 19 01:08:37 Finished compiler/parsing                                      1m20s   1GB
Nov 19 01:08:37 Starting characteristic
Nov 19 01:11:17 Finished characteristic                                        2m38s   1GB
Nov 19 01:11:18 Starting translator/monadic
Nov 19 01:12:50 Finished translator/monadic                                    1m31s   1GB
Nov 19 01:12:50 Starting basis
Nov 19 01:29:54 Finished basis                                                17m03s   3GB
Nov 19 01:29:55 Starting compiler/inference
Nov 19 01:31:40 Finished compiler/inference                                    1m44s   1GB
Nov 19 01:31:40 Starting compiler/backend/reg_alloc
Nov 19 01:32:29 Finished compiler/backend/reg_alloc                              48s   1GB
Nov 19 01:32:30 Starting compiler/backend/gc
Nov 19 01:40:24 Finished compiler/backend/gc                                   7m53s   1GB
Nov 19 01:40:25 Starting compiler/backend
Nov 19 01:40:28 Finished compiler/backend                                         2s  18MB
Nov 19 01:40:28 Starting compiler/encoders/asm
Nov 19 01:40:30 Finished compiler/encoders/asm                                    0s  15MB
Nov 19 01:40:31 Starting compiler/encoders/x64
Nov 19 01:41:24 Finished compiler/encoders/x64                                   52s 625MB
Nov 19 01:41:25 Starting compiler/encoders/arm6
Nov 19 01:43:12 Finished compiler/encoders/arm6                                1m47s   1GB
Nov 19 01:43:13 Starting compiler/encoders/arm8
Nov 19 01:43:40 Finished compiler/encoders/arm8                                  26s 460MB
Nov 19 01:43:41 Starting compiler/encoders/mips
Nov 19 01:44:40 Finished compiler/encoders/mips                                  58s 862MB
Nov 19 01:44:41 Starting compiler/encoders/riscv
Nov 19 01:45:45 Finished compiler/encoders/riscv                               1m03s 678MB
Nov 19 01:45:46 Starting compiler/encoders/ag32
Nov 19 01:46:04 Finished compiler/encoders/ag32                                  17s 796MB
Nov 19 01:46:04 Starting compiler/backend/x64
Nov 19 09:56:59 Resuming compiler/backend/x64
Nov 19 09:57:03 Finished compiler/backend/x64                                     2s  12MB
Nov 19 09:57:04 Starting compiler/backend/arm6
Nov 19 09:57:32 Finished compiler/backend/arm6                                   28s 559MB
Nov 19 09:57:33 Starting compiler/backend/arm8
Nov 19 09:57:52 Finished compiler/backend/arm8                                   18s 901MB
Nov 19 09:57:52 Starting compiler/backend/mips
Nov 19 09:58:13 Finished compiler/backend/mips                                   19s   1GB
Nov 19 09:58:14 Starting compiler/backend/riscv
Nov 19 09:58:33 Finished compiler/backend/riscv                                  19s   1GB
Nov 19 09:58:34 Starting compiler/backend/ag32
Nov 19 09:59:52 Finished compiler/backend/ag32                                 1m17s   1GB
Nov 19 09:59:52 Starting compiler/parsing/proofs
Nov 19 10:06:11 Finished compiler/parsing/proofs                               6m17s 991MB
Nov 19 10:06:11 Starting compiler/inference/proofs
Nov 19 10:09:15 Finished compiler/inference/proofs                             3m02s   1GB
Nov 19 10:09:15 Starting compiler/backend/semantics
Nov 19 10:18:59 Finished compiler/backend/semantics                            9m43s   3GB
Nov 19 10:19:00 Starting compiler/backend/reg_alloc/proofs
Nov 19 10:21:53 Finished compiler/backend/reg_alloc/proofs                     2m52s 859MB
Nov 19 10:21:53 Starting compiler/backend/proofs
Nov 19 11:12:16 Finished compiler/backend/proofs                              50m22s   3GB
Nov 19 11:12:17 Starting compiler/encoders/x64/proofs
Nov 19 11:22:45 Finished compiler/encoders/x64/proofs                         10m27s   5GB
Nov 19 11:22:45 Starting compiler/encoders/arm6/proofs
Nov 19 11:38:31 Finished compiler/encoders/arm6/proofs                        15m44s   2GB
Nov 19 11:38:31 Starting compiler/encoders/arm8/proofs
Nov 19 11:44:53 Finished compiler/encoders/arm8/proofs                         6m21s   1GB
Nov 19 11:44:54 Starting compiler/encoders/mips/proofs
Nov 19 11:56:05 Finished compiler/encoders/mips/proofs                        11m10s   1GB
Nov 19 11:56:05 Starting compiler/encoders/riscv/proofs
Nov 19 12:04:29 Finished compiler/encoders/riscv/proofs                        8m22s 855MB
Nov 19 12:04:29 Starting compiler/encoders/ag32/proofs
Nov 19 12:07:21 Finished compiler/encoders/ag32/proofs                         2m51s 646MB
Nov 19 12:07:22 Starting compiler/backend/x64/proofs
Nov 19 12:07:44 Finished compiler/backend/x64/proofs                             21s   1GB
Nov 19 12:07:45 Starting compiler/backend/arm6/proofs
Nov 19 12:08:08 Finished compiler/backend/arm6/proofs                            22s 865MB
Nov 19 12:08:08 Starting compiler/backend/arm8/proofs
Nov 19 12:08:29 Finished compiler/backend/arm8/proofs                            19s 790MB
Nov 19 12:08:29 Starting compiler/backend/mips/proofs
Nov 19 12:08:52 Finished compiler/backend/mips/proofs                            22s   1GB
Nov 19 12:08:53 Starting compiler/backend/riscv/proofs
Nov 19 12:09:14 Finished compiler/backend/riscv/proofs                           21s   1GB
Nov 19 12:09:15 Starting compiler/backend/ag32/proofs
Nov 19 12:19:15 Finished compiler/backend/ag32/proofs                          9m58s   2GB
Nov 19 12:19:15 Starting compiler/proofs
Nov 19 12:20:42 Finished compiler/proofs                                       1m25s   2GB
Nov 19 12:20:42 Starting candle/set-theory
Nov 19 12:21:17 Finished candle/set-theory                                       34s 634MB
Nov 19 12:21:18 Starting candle/syntax-lib
Nov 19 12:21:29 Finished candle/syntax-lib                                       10s 623MB
Nov 19 12:21:30 Starting candle/standard/syntax
Nov 19 12:23:11 Finished candle/standard/syntax                                1m40s 640MB
Nov 19 12:23:12 Starting candle/standard/semantics
Nov 19 12:24:36 Finished candle/standard/semantics                             1m24s 827MB
Nov 19 12:24:37 Starting candle/standard/monadic
Nov 19 12:26:19 Finished candle/standard/monadic                               1m41s 990MB
Nov 19 12:26:20 Starting candle/standard/ml_kernel
Nov 19 12:42:52 Finished candle/standard/ml_kernel                            16m31s   3GB
Nov 19 12:42:53 Starting candle/standard/opentheory
Nov 19 12:51:21 Finished candle/standard/opentheory                            8m27s   2GB
Nov 19 12:51:22 Starting candle/standard/opentheory/compilation
Nov 19 13:21:36 Finished candle/standard/opentheory/compilation               30m13s  14GB
Nov 19 13:21:37 Starting candle/standard/opentheory/compilation/proofs
Nov 19 13:22:28 Finished candle/standard/opentheory/compilation/proofs           50s   3GB
Nov 19 13:22:29 Starting characteristic/examples
Nov 19 13:24:05 Finished characteristic/examples                               1m35s   1GB
Nov 19 13:24:05 Starting tutorial/solutions
Nov 19 13:38:16 Finished tutorial/solutions                                   14m09s   7GB
Nov 19 13:38:16 Starting translator/monadic/examples
Nov 19 13:40:18 Finished translator/monadic/examples                           2m00s   2GB
Nov 19 13:40:18 Starting examples
Nov 19 13:47:09 Finished examples                                              6m49s   2GB
Nov 19 13:47:09 Starting examples/compilation/x64
Nov 19 16:04:53 Finished examples/compilation/x64                           2h17m42s   9GB
Nov 19 16:04:54 Starting examples/compilation/x64/proofs
Nov 19 16:06:59 FAILED: examples/compilation/x64/proofs
]0;Holmake: ../../../../compiler/backend/proofs]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../../../compiler/backend/proofs]0;Holmake: ../../../../compiler/backend]0;Holmake: ../../../../basis/pure]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/balanced_bst]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../../basis/pure]0;Holmake: ../../../../misc]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[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: ../../../../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: ../../../../basis/pure]0;Holmake: ../../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../../../compiler/backend]0;Holmake: ../../../../compiler/backend/reg_alloc]0;Holmake: ../../../../translator/monadic]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: ../../../../semantics/proofs]0;Holmake: ../../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../../characteristic]0;Holmake: ../../../../translator]0;Holmake: ../../../../semantics/alt_semantics/proofs]0;Holmake: ../../../../semantics/alt_semantics]0;Holmake: ../../../../semantics/alt_semantics[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics[0m
]0;Holmake: ../../../../semantics/alt_semantics/proofs]0;Holmake: ../../../../semantics/alt_semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/alt_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: ../../../../compiler/backend/reg_alloc]0;Holmake: ../../../../unverified/reg_alloc]0;Holmake: ../../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../../../../compiler/backend/reg_alloc]0;Holmake: ../../../../compiler/backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ../../../../compiler/backend]0;Holmake: ../../../../compiler/encoders/asm]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../../../compiler/encoders/asm]0;Holmake: ../../../../compiler/encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ../../../../compiler/backend]0;Holmake: ../../../../compiler/backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ../../../../compiler/backend/proofs]0;Holmake: ../../../../compiler/backend/gc]0;Holmake: ../../../../compiler/backend/gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: ../../../../compiler/backend/proofs]0;Holmake: ../../../../compiler/backend/reg_alloc/proofs]0;Holmake: ../../../../compiler/backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: ../../../../compiler/backend/proofs]0;Holmake: ../../../../compiler/backend/semantics]0;Holmake: ../../../../compiler/backend/semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: ../../../../compiler/backend/proofs]0;Holmake: ../../../../compiler/backend/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
]0;Holmake: .]0;Holmake: ../../../../compiler/backend/x64/proofs]0;Holmake: ../../../../compiler/backend/x64]0;Holmake: ../../../../compiler/encoders/x64]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: ../../../../compiler/encoders/x64]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ../../../../compiler/encoders/x64]0;Holmake: ../../../../compiler/encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ../../../../compiler/backend/x64]0;Holmake: ../../../../compiler/backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ../../../../compiler/backend/x64/proofs]0;Holmake: ../../../../compiler/encoders/x64/proofs]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/x64/prog]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/x64/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/prog[0m
]0;Holmake: ../../../../compiler/encoders/x64/proofs]0;Holmake: ../../../../compiler/encoders/x64/proofs[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
]0;Holmake: ../../../../compiler/backend/x64/proofs]0;Holmake: ../../../../compiler/backend/x64/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/x64/proofs[0m
]0;Holmake: .]0;Holmake: ../../..]0;Holmake: ../../../../basis]0;Holmake: ../../../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: ../../..]0;Holmake: ../../..[1mWorking in $(CAKEMLDIR)/examples[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../../compiler]0;Holmake: ../../../../compiler/backend/ag32]0;Holmake: ../../../../compiler/encoders/ag32]0;Holmake: ../../../../compiler/encoders/ag32[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32[0m
]0;Holmake: ../../../../compiler/backend/ag32]0;Holmake: ../../../../compiler/backend/ag32[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32[0m
]0;Holmake: ../../../../compiler]0;Holmake: ../../../../compiler/backend/arm6]0;Holmake: ../../../../compiler/encoders/arm6]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ../../../../compiler/encoders/arm6]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ../../../../compiler/encoders/arm6]0;Holmake: ../../../../compiler/encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ../../../../compiler/backend/arm6]0;Holmake: ../../../../compiler/backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ../../../../compiler]0;Holmake: ../../../../compiler/backend/arm8]0;Holmake: ../../../../compiler/encoders/arm8]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: ../../../../compiler/encoders/arm8]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/arm8/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step[0m
]0;Holmake: ../../../../compiler/encoders/arm8]0;Holmake: ../../../../compiler/encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ../../../../compiler/backend/arm8]0;Holmake: ../../../../compiler/backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ../../../../compiler]0;Holmake: ../../../../compiler/backend/mips]0;Holmake: ../../../../compiler/encoders/mips]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: ../../../../compiler/encoders/mips]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/mips/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/step[0m
]0;Holmake: ../../../../compiler/encoders/mips]0;Holmake: ../../../../compiler/encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ../../../../compiler/backend/mips]0;Holmake: ../../../../compiler/backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ../../../../compiler]0;Holmake: ../../../../compiler/backend/riscv]0;Holmake: ../../../../compiler/encoders/riscv]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: ../../../../compiler/encoders/riscv]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ../../../../compiler/encoders/riscv]0;Holmake: ../../../../compiler/encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ../../../../compiler/backend/riscv]0;Holmake: ../../../../compiler/backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ../../../../compiler]0;Holmake: ../../../../compiler/inference]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/unification/triangular]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-e48aefc60b7c4a206ed939646485d31a341e2bfc/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ../../../../compiler/inference]0;Holmake: ../../../../compiler/inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ../../../../compiler]0;Holmake: ../../../../compiler[1mWorking in $(CAKEMLDIR)/compiler[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/examples/compilation/x64[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples/compilation/x64/proofs[0m
Linking catProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "catProof">>
Saved theorem _____ "cat_compiled_thm"
Exporting theory "catProof" ... done.
Theory "catProof" took 0.36257s to build
Linking diffProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "diffProof">>
Saved theorem _____ "diff_compiled_thm"
Exporting theory "diffProof" ... done.
Theory "diffProof" took 0.37891s to build
Linking echoProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "echoProof">>
Saved theorem _____ "echo_compiled_thm"
Exporting theory "echoProof" ... done.
Theory "echoProof" took 0.36164s to build
Linking grepProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "grepProof">>
Saved theorem _____ "grep_compiled_thm"
Exporting theory "grepProof" ... done.
Theory "grepProof" took 0.44319s to build
Linking helloErrProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "helloErrProof">>
Saved theorem _____ "hello_compiled_thm"
Exporting theory "helloErrProof" ... done.
Theory "helloErrProof" took 0.35625s to build
Linking helloProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "helloProof">>
Saved theorem _____ "hello_compiled_thm"
Exporting theory "helloProof" ... done.
Theory "helloProof" took 0.35199s to build
Linking iocatProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "iocatProof">>
Saved theorem _____ "cat_compiled_thm"
Exporting theory "iocatProof" ... done.
Theory "iocatProof" took 0.34834s to build
Linking patchProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "patchProof">>
Saved theorem _____ "patch_compiled_thm"
Exporting theory "patchProof" ... done.
Theory "patchProof" took 0.38111s to build
Linking sortProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "sortProof">>
Saved theorem _____ "sort_compiled_thm"
Exporting theory "sortProof" ... done.
Theory "sortProof" took 0.36964s to build
Linking wordcountProofScript.uo to produce theory-builder executable
<<HOL message: Created theory "wordcountProof">>
error in quse /home/cake/regression/cakeml-561/examples/compilation/x64/proofs/wordcountProofScript.sml : HOL_ERR {message = "variable not found", origin_function = "GEN", origin_structure = "Q"}
error in load wordcountProofScript : HOL_ERR {message = "variable not found", origin_function = "GEN", origin_structure = "Q"}
Uncaught exception: HOL_ERR {message = "variable not found", origin_function = "GEN", origin_structure = "Q"}
Failed script build for wordcountProofScript - exited with code 1