CakeML Regression Test

Job 734

CakeML:b468cb6347ea2dace0ddfc6f3401900b16929b92
  Fix yet another term eqtype problem [Feb 19 07:15:24]
#618 (monadic-trans-cleanup)
Merging into:9feef1ec9f25ce1fd0474f285b4d07464ed21dbf
  Stop assuming term eqtype in ml_monad_translatorBase [Feb 16 11:48:28]
HOL:45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1
  Testing for src/Boolify [Feb 15 06:20:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 19 07:23:48 Claimed job
Feb 19 07:23:53 Reusing HOL
Feb 19 07:23:58 Starting developers
Feb 19 07:23:59 Finished developers                                               0s  31MB
Feb 19 07:23:59 Starting developers/bin
Feb 19 07:24:29 Finished developers/bin                                          28s 142MB
Feb 19 07:24:30 Starting semantics/ffi
Feb 19 07:24:38 Finished semantics/ffi                                            7s 225MB
Feb 19 07:24:39 Starting semantics
Feb 19 07:25:56 Finished semantics                                             1m16s   1GB
Feb 19 07:25:57 Starting semantics/proofs
Feb 19 07:28:54 Finished semantics/proofs                                      2m56s   1GB
Feb 19 07:28:54 Starting basis/pure
Feb 19 07:29:38 Finished basis/pure                                              43s 670MB
Feb 19 07:29:39 Starting translator
Feb 19 07:31:14 Finished translator                                            1m34s   1GB
Feb 19 07:31:15 Starting compiler/parsing
Feb 19 07:32:12 Finished compiler/parsing                                        56s   1GB
Feb 19 07:32:13 Starting characteristic
Feb 19 07:36:22 Finished characteristic                                        4m08s   1GB
Feb 19 07:36:23 Starting translator/monadic
Feb 19 07:37:45 Finished translator/monadic                                    1m21s   1GB
Feb 19 07:37:45 Starting basis
Feb 19 07:54:43 Finished basis                                                16m56s   3GB
Feb 19 07:54:43 Starting compiler/inference
Feb 19 07:56:13 Finished compiler/inference                                    1m29s   1GB
Feb 19 07:56:14 Starting compiler/backend/reg_alloc
Feb 19 07:57:05 Finished compiler/backend/reg_alloc                              50s   1GB
Feb 19 07:57:06 Starting compiler/backend/gc
Feb 19 08:04:46 Finished compiler/backend/gc                                   7m39s   2GB
Feb 19 08:04:47 Starting compiler/backend
Feb 19 08:04:49 Finished compiler/backend                                         0s  41MB
Feb 19 08:04:49 Starting compiler/encoders/asm
Feb 19 08:04:50 Finished compiler/encoders/asm                                    0s  32MB
Feb 19 08:04:51 Starting compiler/encoders/x64
Feb 19 08:05:14 Finished compiler/encoders/x64                                   21s 947MB
Feb 19 08:05:15 Starting compiler/encoders/arm6
Feb 19 08:05:58 Finished compiler/encoders/arm6                                  43s 757MB
Feb 19 08:05:59 Starting compiler/encoders/arm8
Feb 19 08:06:11 Finished compiler/encoders/arm8                                  11s 768MB
Feb 19 08:06:12 Starting compiler/encoders/mips
Feb 19 08:06:28 Finished compiler/encoders/mips                                  15s   1GB
Feb 19 08:06:28 Starting compiler/encoders/riscv
Feb 19 08:06:42 Finished compiler/encoders/riscv                                 12s 822MB
Feb 19 08:06:42 Starting compiler/encoders/ag32
Feb 19 08:06:58 Finished compiler/encoders/ag32                                  14s 767MB
Feb 19 08:06:59 Starting compiler/backend/x64
Feb 19 08:07:14 Finished compiler/backend/x64                                    14s 797MB
Feb 19 08:07:14 Starting compiler/backend/arm6
Feb 19 08:07:31 Finished compiler/backend/arm6                                   15s   1GB
Feb 19 08:07:32 Starting compiler/backend/arm8
Feb 19 08:07:47 Finished compiler/backend/arm8                                   15s   1GB
Feb 19 08:07:48 Starting compiler/backend/mips
Feb 19 08:08:05 Finished compiler/backend/mips                                   15s 795MB
Feb 19 08:08:06 Starting compiler/backend/riscv
Feb 19 08:08:22 Finished compiler/backend/riscv                                  15s 993MB
Feb 19 08:08:23 Starting compiler/backend/ag32
Feb 19 08:09:28 Finished compiler/backend/ag32                                 1m04s   1GB
Feb 19 08:09:29 Starting compiler/parsing/proofs
Feb 19 08:15:01 Finished compiler/parsing/proofs                               5m31s 985MB
Feb 19 08:15:02 Starting compiler/inference/proofs
Feb 19 08:17:40 Finished compiler/inference/proofs                             2m36s   1GB
Feb 19 08:17:40 Starting compiler/backend/semantics
Feb 19 08:24:31 Finished compiler/backend/semantics                            6m49s   2GB
Feb 19 08:24:32 Starting compiler/backend/reg_alloc/proofs
Feb 19 08:27:07 Finished compiler/backend/reg_alloc/proofs                     2m34s 691MB
Feb 19 08:27:07 Starting compiler/backend/proofs
Feb 19 09:03:59 Finished compiler/backend/proofs                              36m50s   3GB
Feb 19 09:04:00 Starting compiler/encoders/x64/proofs
Feb 19 09:05:50 FAILED: compiler/encoders/x64/proofs
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/prog]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/prog]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/x64/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/prog[0m
]0;Holmake: .]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-734/misc]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-734/misc]0;Holmake: ~/regression/cakeml-734/developers]0;Holmake: ~/regression/cakeml-734/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-734/misc]0;Holmake: ~/regression/cakeml-734/misc/lem_lib_stub]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/cakeml-734/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-734/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-734/misc]0;Holmake: ~/regression/cakeml-734/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-734/semantics]0;Holmake: ~/regression/cakeml-734/semantics/ffi]0;Holmake: ~/regression/cakeml-734/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-734/semantics]0;Holmake: ~/regression/cakeml-734/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../asm]0;Holmake: ../../asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Starting work on x64_targetProofTheory
Starting work on README.md
README.md                                           OK
x64_targetProofTheory                      FAILED! <1>
    Reason: Can't unify ''a to term (Requires equality type)
 Found near high_low_reg (Parse.Term [QUOTE " (*#loc 762 37*)r1: word4"])
 /home/myreen/regression/cakeml-734/compiler/encoders/x64/proofs/x64_targetProofScript.sml:763: error: Type error in function application.
    Function: high_low_reg : ''a -> term list -> bool * bool
    Argument: (Parse.Term [QUOTE " (*#loc 763 37*)r2: word4"]) : term
    Reason: Can't unify ''a to term (Requires equality type)
 Found near high_low_reg (Parse.Term [QUOTE " (*#loc 763 37*)r2: word4"])
 error in quse /home/myreen/regression/cakeml-734/compiler/encoders/x64/proofs/x64_targetProofScript.sml : Fail "Static Errors"
 error in load x64_targetProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"