Overview

Job 561

CakeML:60684bfedb3d540303284740ab19d911c93b4362
  Fix for renamed theorem
#554 (tiny)
Merging into:8ee5d433f5e6a93e9a41ea5e46b961c65130c2ef
  Merge pull request #551 from CakeML/translator-alist-tree
HOL:e48aefc60b7c4a206ed939646485d31a341e2bfc
  Fully protect wordsLib's use of parser
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers/bin
 Finished developers/bin                                        1m07s 916MB
 Starting semantics/ffi
 Finished semantics/ffi                                           39s 355MB
 Starting semantics
 Finished semantics                                             1m39s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m00s   1GB
 Starting basis/pure
 Finished basis/pure                                            3m47s 685MB
 Starting translator
 Finished translator                                            3m12s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m20s   1GB
 Starting characteristic
 Finished characteristic                                        2m38s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m31s   1GB
 Starting basis
 Finished basis                                                17m03s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    1m44s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              48s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   7m53s   1GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  18MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  15MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   52s 625MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                1m47s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  26s 460MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  58s 862MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m03s 678MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  17s 796MB
 Starting compiler/backend/x64
 Resuming compiler/backend/x64
 Finished compiler/backend/x64                                     2s  12MB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   28s 559MB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   18s 901MB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   19s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  19s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m17s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               6m17s 991MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             3m02s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            9m43s   3GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     2m52s 859MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              50m22s   3GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         10m27s   5GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        15m44s   2GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m21s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        11m10s   1GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m22s 855MB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m51s 646MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             21s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            22s 865MB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            19s 790MB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            22s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           21s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                          9m58s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m25s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                       34s 634MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       10s 623MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m40s 640MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m24s 827MB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m41s 990MB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            16m31s   3GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                            8m27s   2GB
 Starting candle/standard/opentheory/compilation
 Finished candle/standard/opentheory/compilation               30m13s  14GB
 Starting candle/standard/opentheory/compilation/proofs
 Finished candle/standard/opentheory/compilation/proofs           50s   3GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m35s   1GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   14m09s   7GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           2m00s   2GB
 Starting examples
 Finished examples                                              6m49s   2GB
 Starting examples/compilation/x64
 Finished examples/compilation/x64                           2h17m42s   9GB
 Starting examples/compilation/x64/proofs
 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