Job 819

CakeML:9b8652b873e7f77ee756305eff8785ed0a764f74
  Fix comment [Apr 23 17:01:03]
#629 (vstte18)
Merging into:5206af9f67eb4da34374600de68d6fd8c1385a43
  Merge pull request #632 from CakeML/extend_arm8 [Apr 25 17:43:37]
HOL:d9d262ad8402d865a72735480268b9f2da63fcd9
  Change ThmSetData to store just theorem names in .dat files [Apr 21 04:26:27]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 27 07:16:14 Claimed job
Apr 27 07:16:19 Reusing HOL
Apr 27 07:16:24 Starting developers
Apr 27 07:16:25 Finished developers                                               0s  21MB
Apr 27 07:16:25 Starting developers/bin
Apr 27 07:17:00 Finished developers/bin                                          35s 142MB
Apr 27 07:17:01 Starting semantics/ffi
Apr 27 07:17:08 Finished semantics/ffi                                            7s 224MB
Apr 27 07:17:09 Starting semantics
Apr 27 07:18:26 Finished semantics                                             1m16s   1GB
Apr 27 07:18:26 Starting semantics/proofs
Apr 27 07:21:17 Finished semantics/proofs                                      2m50s 998MB
Apr 27 07:21:17 Starting basis/pure
Apr 27 07:22:02 Finished basis/pure                                              44s 699MB
Apr 27 07:22:02 Starting translator
Apr 27 07:23:39 Finished translator                                            1m36s   1GB
Apr 27 07:23:39 Starting compiler/parsing
Apr 27 07:24:36 Finished compiler/parsing                                        56s   1GB
Apr 27 07:24:36 Starting characteristic
Apr 27 07:29:38 Finished characteristic                                        5m01s   1GB
Apr 27 07:29:39 Starting translator/monadic
Apr 27 07:31:02 Finished translator/monadic                                    1m23s   1GB
Apr 27 07:31:03 Starting basis
Apr 27 07:47:39 Finished basis                                                16m36s   2GB
Apr 27 07:47:40 Starting compiler/inference
Apr 27 07:49:09 Finished compiler/inference                                    1m29s   1GB
Apr 27 07:49:10 Starting compiler/backend/reg_alloc
Apr 27 07:50:00 Finished compiler/backend/reg_alloc                              49s   1GB
Apr 27 07:50:00 Starting compiler/backend/gc
Apr 27 07:57:44 Finished compiler/backend/gc                                   7m43s   2GB
Apr 27 07:57:45 Starting compiler/backend
Apr 27 07:57:46 Finished compiler/backend                                         0s  42MB
Apr 27 07:57:46 Starting compiler/encoders/asm
Apr 27 07:57:47 Finished compiler/encoders/asm                                    0s  32MB
Apr 27 07:57:47 Starting compiler/encoders/x64
Apr 27 07:58:09 Finished compiler/encoders/x64                                   21s 946MB
Apr 27 07:58:10 Starting compiler/encoders/arm6
Apr 27 07:58:53 Finished compiler/encoders/arm6                                  43s 934MB
Apr 27 07:58:53 Starting compiler/encoders/arm8
Apr 27 07:59:05 Finished compiler/encoders/arm8                                  10s 644MB
Apr 27 07:59:05 Starting compiler/encoders/mips
Apr 27 07:59:20 Finished compiler/encoders/mips                                  14s 742MB
Apr 27 07:59:20 Starting compiler/encoders/riscv
Apr 27 07:59:34 Finished compiler/encoders/riscv                                 12s 884MB
Apr 27 07:59:34 Starting compiler/encoders/ag32
Apr 27 07:59:49 Finished compiler/encoders/ag32                                  14s 757MB
Apr 27 07:59:49 Starting compiler/backend/x64
Apr 27 08:00:06 Finished compiler/backend/x64                                    15s   1GB
Apr 27 08:00:06 Starting compiler/backend/arm6
Apr 27 08:00:23 Finished compiler/backend/arm6                                   17s   1GB
Apr 27 08:00:24 Starting compiler/backend/arm8
Apr 27 08:00:40 Finished compiler/backend/arm8                                   15s   1GB
Apr 27 08:00:40 Starting compiler/backend/mips
Apr 27 08:00:56 Finished compiler/backend/mips                                   15s   1GB
Apr 27 08:00:56 Starting compiler/backend/riscv
Apr 27 08:01:13 Finished compiler/backend/riscv                                  16s   1GB
Apr 27 08:01:13 Starting compiler/backend/ag32
Apr 27 08:02:20 Finished compiler/backend/ag32                                 1m06s   1GB
Apr 27 08:02:20 Starting compiler/parsing/proofs
Apr 27 08:07:45 Finished compiler/parsing/proofs                               5m24s 969MB
Apr 27 08:07:46 Starting compiler/inference/proofs
Apr 27 08:10:21 Finished compiler/inference/proofs                             2m35s   1GB
Apr 27 08:10:22 Starting compiler/backend/semantics
Apr 27 08:17:13 Finished compiler/backend/semantics                            6m51s   2GB
Apr 27 08:17:13 Starting compiler/backend/reg_alloc/proofs
Apr 27 08:19:52 Finished compiler/backend/reg_alloc/proofs                     2m37s 784MB
Apr 27 08:19:52 Starting compiler/backend/proofs
Apr 27 08:57:20 Finished compiler/backend/proofs                              37m27s   4GB
Apr 27 08:57:20 Starting compiler/encoders/x64/proofs
Apr 27 09:06:14 Finished compiler/encoders/x64/proofs                          8m53s   7GB
Apr 27 09:06:15 Starting compiler/encoders/arm6/proofs
Apr 27 09:18:30 Finished compiler/encoders/arm6/proofs                        12m15s   3GB
Apr 27 09:18:31 Starting compiler/encoders/arm8/proofs
Apr 27 09:25:04 Finished compiler/encoders/arm8/proofs                         6m32s   1GB
Apr 27 09:25:04 Starting compiler/encoders/mips/proofs
Apr 27 09:34:28 Finished compiler/encoders/mips/proofs                         9m23s   2GB
Apr 27 09:34:28 Starting compiler/encoders/riscv/proofs
Apr 27 09:42:44 Finished compiler/encoders/riscv/proofs                        8m15s   1GB
Apr 27 09:42:44 Starting compiler/encoders/ag32/proofs
Apr 27 09:45:12 Finished compiler/encoders/ag32/proofs                         2m27s 638MB
Apr 27 09:45:12 Starting compiler/backend/x64/proofs
Apr 27 09:45:29 Finished compiler/backend/x64/proofs                             16s   1GB
Apr 27 09:45:30 Starting compiler/backend/arm6/proofs
Apr 27 09:45:48 Finished compiler/backend/arm6/proofs                            18s   1GB
Apr 27 09:45:49 Starting compiler/backend/arm8/proofs
Apr 27 09:46:06 Finished compiler/backend/arm8/proofs                            16s   1GB
Apr 27 09:46:06 Starting compiler/backend/mips/proofs
Apr 27 09:46:23 Finished compiler/backend/mips/proofs                            16s 933MB
Apr 27 09:46:23 Starting compiler/backend/riscv/proofs
Apr 27 09:46:40 Finished compiler/backend/riscv/proofs                           16s 926MB
Apr 27 09:46:40 Starting compiler/backend/ag32/proofs
Apr 27 09:55:34 Finished compiler/backend/ag32/proofs                          8m53s   2GB
Apr 27 09:55:35 Starting compiler/proofs
Apr 27 09:56:46 Finished compiler/proofs                                       1m10s   2GB
Apr 27 09:56:46 Starting candle/set-theory
Apr 27 09:57:11 Finished candle/set-theory                                       24s 759MB
Apr 27 09:57:11 Starting candle/syntax-lib
Apr 27 09:57:21 Finished candle/syntax-lib                                        9s 653MB
Apr 27 09:57:21 Starting candle/standard/syntax
Apr 27 09:59:00 Finished candle/standard/syntax                                1m38s   1GB
Apr 27 09:59:01 Starting candle/standard/semantics
Apr 27 10:00:34 Finished candle/standard/semantics                             1m32s 888MB
Apr 27 10:00:34 Starting candle/standard/monadic
Apr 27 10:02:04 Finished candle/standard/monadic                               1m29s   1GB
Apr 27 10:02:04 Starting candle/standard/ml_kernel
Apr 27 10:05:43 Finished candle/standard/ml_kernel                             3m38s   3GB
Apr 27 10:05:43 Starting candle/standard/opentheory
Apr 27 10:14:05 Finished candle/standard/opentheory                            8m21s   3GB
Apr 27 10:14:06 Starting candle/standard/opentheory/compilation
Apr 27 10:43:36 Finished candle/standard/opentheory/compilation               29m29s  19GB
Apr 27 10:43:36 Starting candle/standard/opentheory/compilation/proofs
Apr 27 10:44:09 Finished candle/standard/opentheory/compilation/proofs           32s   3GB
Apr 27 10:44:09 Starting characteristic/examples
Apr 27 10:45:31 Finished characteristic/examples                               1m21s   1GB
Apr 27 10:45:31 Starting tutorial/solutions
Apr 27 10:46:16 FAILED: tutorial/solutions
]0;Holmake: .]0;Holmake: ~/regression/cakeml-819/basis]0;Holmake: ~/regression/cakeml-819/basis/pure]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/formal-languages]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-819/basis/pure]0;Holmake: ~/regression/cakeml-819/misc]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-819/misc]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-819/misc]0;Holmake: ~/regression/cakeml-819/developers]0;Holmake: ~/regression/cakeml-819/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-819/misc]0;Holmake: ~/regression/cakeml-819/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-819/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-819/misc]0;Holmake: ~/regression/cakeml-819/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-819/basis/pure]0;Holmake: ~/regression/cakeml-819/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-819/basis]0;Holmake: ~/regression/cakeml-819/characteristic]0;Holmake: ~/regression/cakeml-819/compiler/parsing]0;Holmake: ~/regression/cakeml-819/semantics]0;Holmake: ~/regression/cakeml-819/semantics/ffi]0;Holmake: ~/regression/cakeml-819/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-819/semantics]0;Holmake: ~/regression/cakeml-819/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-819/compiler/parsing]0;Holmake: ~/regression/cakeml-819/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-819/characteristic]0;Holmake: ~/regression/cakeml-819/semantics/proofs]0;Holmake: ~/regression/cakeml-819/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-819/characteristic]0;Holmake: ~/regression/cakeml-819/translator]0;Holmake: ~/regression/cakeml-819/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-819/characteristic]0;Holmake: ~/regression/cakeml-819/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-819/basis]0;Holmake: ~/regression/cakeml-819/translator/monadic]0;Holmake: ~/regression/cakeml-819/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-819/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-819/translator/monadic]0;Holmake: ~/regression/cakeml-819/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-819/basis]0;Holmake: ~/regression/cakeml-819/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-819/compiler]0;Holmake: ~/regression/cakeml-819/compiler/backend]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend]0;Holmake: ~/regression/cakeml-819/compiler/backend/reg_alloc]0;Holmake: ~/regression/cakeml-819/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-819/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/reg_alloc]0;Holmake: ~/regression/cakeml-819/compiler/backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend]0;Holmake: ~/regression/cakeml-819/compiler/encoders/asm]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/asm]0;Holmake: ~/regression/cakeml-819/compiler/encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend]0;Holmake: ~/regression/cakeml-819/compiler/backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ~/regression/cakeml-819/compiler]0;Holmake: ~/regression/cakeml-819/compiler/backend/ag32]0;Holmake: ~/regression/cakeml-819/compiler/encoders/ag32]0;Holmake: ~/regression/cakeml-819/compiler/encoders/ag32[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/ag32]0;Holmake: ~/regression/cakeml-819/compiler/backend/ag32[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32[0m
]0;Holmake: ~/regression/cakeml-819/compiler]0;Holmake: ~/regression/cakeml-819/compiler/backend/arm6]0;Holmake: ~/regression/cakeml-819/compiler/encoders/arm6]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/arm6]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/arm6]0;Holmake: ~/regression/cakeml-819/compiler/encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/arm6]0;Holmake: ~/regression/cakeml-819/compiler/backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ~/regression/cakeml-819/compiler]0;Holmake: ~/regression/cakeml-819/compiler/backend/arm8]0;Holmake: ~/regression/cakeml-819/compiler/encoders/arm8]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/arm8]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/arm8/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/arm8]0;Holmake: ~/regression/cakeml-819/compiler/encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/arm8]0;Holmake: ~/regression/cakeml-819/compiler/backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ~/regression/cakeml-819/compiler]0;Holmake: ~/regression/cakeml-819/compiler/backend/mips]0;Holmake: ~/regression/cakeml-819/compiler/encoders/mips]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/mips]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/mips/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/step[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/mips]0;Holmake: ~/regression/cakeml-819/compiler/encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/mips]0;Holmake: ~/regression/cakeml-819/compiler/backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ~/regression/cakeml-819/compiler]0;Holmake: ~/regression/cakeml-819/compiler/backend/riscv]0;Holmake: ~/regression/cakeml-819/compiler/encoders/riscv]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/riscv]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/riscv]0;Holmake: ~/regression/cakeml-819/compiler/encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/riscv]0;Holmake: ~/regression/cakeml-819/compiler/backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ~/regression/cakeml-819/compiler]0;Holmake: ~/regression/cakeml-819/compiler/backend/x64]0;Holmake: ~/regression/cakeml-819/compiler/encoders/x64]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/x64]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/x64]0;Holmake: ~/regression/cakeml-819/compiler/encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/x64]0;Holmake: ~/regression/cakeml-819/compiler/backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ~/regression/cakeml-819/compiler]0;Holmake: ~/regression/cakeml-819/compiler/inference]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/unification/triangular]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ~/regression/cakeml-819/compiler/inference]0;Holmake: ~/regression/cakeml-819/compiler/inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ~/regression/cakeml-819/compiler]0;Holmake: ~/regression/cakeml-819/compiler[1mWorking in $(CAKEMLDIR)/compiler[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-819/compiler/backend/proofs]0;Holmake: ~/regression/cakeml-819/compiler/backend/gc]0;Holmake: ~/regression/cakeml-819/compiler/backend/gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/proofs]0;Holmake: ~/regression/cakeml-819/compiler/backend/reg_alloc/proofs]0;Holmake: ~/regression/cakeml-819/compiler/backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/proofs]0;Holmake: ~/regression/cakeml-819/compiler/backend/semantics]0;Holmake: ~/regression/cakeml-819/compiler/backend/semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/proofs]0;Holmake: ~/regression/cakeml-819/compiler/backend/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-819/compiler/backend/x64/proofs]0;Holmake: ~/regression/cakeml-819/compiler/encoders/x64/proofs]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/x64/prog]0;Holmake: ~/regression/HOL-d9d262ad8402d865a72735480268b9f2da63fcd9/examples/l3-machine-code/x64/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/prog[0m
]0;Holmake: ~/regression/cakeml-819/compiler/encoders/x64/proofs]0;Holmake: ~/regression/cakeml-819/compiler/encoders/x64/proofs[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
]0;Holmake: ~/regression/cakeml-819/compiler/backend/x64/proofs]0;Holmake: ~/regression/cakeml-819/compiler/backend/x64/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/x64/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/tutorial/solutions[0m
Starting work on simple_bstTheory
Starting work on splitwordsTheory
Starting work on make_ex
make_ex                                             OK
Starting work on exercises
exercises                                           OK
simple_bstTheory                                    OK
splitwordsTheory                                    OK
Starting work on wordfreqProgTheory
wordfreqProgTheory                         FAILED! <1>
 Saved theorem _____ "nsLookup_wordfreqProg_env_5_pfun_eqs"
 Saved definition __ "valid_wordfreq_output_def"
 Saved theorem _____ "valid_wordfreq_output_exists"
 Saved theorem _____ "valid_wordfreq_output_unique"
 Saved theorem _____ "wordfreq_output_valid"
 Saved theorem _____ "wordfreq_output_spec_unique"
 Adding nsLookup representation thms for [wordfreqProg_env_5, wordfreqProg_env_4]
 error in quse /home/myreen/regression/cakeml-819/tutorial/solutions/wordfreqProgScript.sml : HOL_ERR {message = "on line 255, characters 39-44:\nRecord field foobar not registered", origin_function = "make_atom", origin_structure = "Parse_support"}
 error in load wordfreqProgScript : HOL_ERR {message = "on line 255, characters 39-44:\nRecord field foobar not registered", origin_function = "make_atom", origin_structure = "Parse_support"}
 Uncaught exception: HOL_ERR {message = "on line 255, characters 39-44:\nRecord field foobar not registered", origin_function = "make_atom", origin_structure = "Parse_support"}