CakeML Regression Test

Job 735

CakeML:8763d47216b4bc7f35d0d144659d92c0e034a8df
  Stop assuming term eqtype in monadic translator [Feb 19 11:13:05]
#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 11:46:01 Claimed job
Feb 19 11:46:07 Reusing HOL
Feb 19 11:46:12 Starting developers
Feb 19 11:46:13 Finished developers                                               0s  22MB
Feb 19 11:46:14 Starting developers/bin
Feb 19 11:46:48 Finished developers/bin                                          32s 143MB
Feb 19 11:46:48 Starting semantics/ffi
Feb 19 11:46:57 Finished semantics/ffi                                            7s 224MB
Feb 19 11:46:58 Starting semantics
Feb 19 11:48:14 Finished semantics                                             1m15s   1GB
Feb 19 11:48:15 Starting semantics/proofs
Feb 19 11:51:11 Finished semantics/proofs                                      2m54s   1GB
Feb 19 11:51:12 Starting basis/pure
Feb 19 11:51:55 Finished basis/pure                                              42s 723MB
Feb 19 11:51:56 Starting translator
Feb 19 11:53:31 Finished translator                                            1m34s   1GB
Feb 19 11:53:32 Starting compiler/parsing
Feb 19 11:54:28 Finished compiler/parsing                                        55s   2GB
Feb 19 11:54:29 Starting characteristic
Feb 19 11:58:39 Finished characteristic                                        4m09s   1GB
Feb 19 11:58:39 Starting translator/monadic
Feb 19 12:00:04 Finished translator/monadic                                    1m23s   1GB
Feb 19 12:00:05 Starting basis
Feb 19 12:16:54 Finished basis                                                16m48s   2GB
Feb 19 12:16:55 Starting compiler/inference
Feb 19 12:18:26 Finished compiler/inference                                    1m30s   1GB
Feb 19 12:18:27 Starting compiler/backend/reg_alloc
Feb 19 12:19:18 Finished compiler/backend/reg_alloc                              50s   1GB
Feb 19 12:19:18 Starting compiler/backend/gc
Feb 19 12:26:55 Finished compiler/backend/gc                                   7m35s   1GB
Feb 19 12:26:56 Starting compiler/backend
Feb 19 12:26:57 Finished compiler/backend                                         0s  41MB
Feb 19 12:26:58 Starting compiler/encoders/asm
Feb 19 12:26:59 Finished compiler/encoders/asm                                    0s  32MB
Feb 19 12:27:00 Starting compiler/encoders/x64
Feb 19 12:27:22 Finished compiler/encoders/x64                                   21s 925MB
Feb 19 12:27:23 Starting compiler/encoders/arm6
Feb 19 12:28:06 Finished compiler/encoders/arm6                                  42s 735MB
Feb 19 12:28:07 Starting compiler/encoders/arm8
Feb 19 12:28:19 Finished compiler/encoders/arm8                                  10s 879MB
Feb 19 12:28:20 Starting compiler/encoders/mips
Feb 19 12:28:35 Finished compiler/encoders/mips                                  15s   1GB
Feb 19 12:28:36 Starting compiler/encoders/riscv
Feb 19 12:28:49 Finished compiler/encoders/riscv                                 12s 708MB
Feb 19 12:28:50 Starting compiler/encoders/ag32
Feb 19 12:29:05 Finished compiler/encoders/ag32                                  14s 702MB
Feb 19 12:29:06 Starting compiler/backend/x64
Feb 19 12:29:22 Finished compiler/backend/x64                                    15s 845MB
Feb 19 12:29:23 Starting compiler/backend/arm6
Feb 19 12:29:41 Finished compiler/backend/arm6                                   17s   1GB
Feb 19 12:29:42 Starting compiler/backend/arm8
Feb 19 12:29:58 Finished compiler/backend/arm8                                   15s   1GB
Feb 19 12:29:59 Starting compiler/backend/mips
Feb 19 12:30:15 Finished compiler/backend/mips                                   15s   1GB
Feb 19 12:30:16 Starting compiler/backend/riscv
Feb 19 12:30:32 Finished compiler/backend/riscv                                  15s   1GB
Feb 19 12:30:33 Starting compiler/backend/ag32
Feb 19 12:31:39 Finished compiler/backend/ag32                                 1m04s 804MB
Feb 19 12:31:39 Starting compiler/parsing/proofs
Feb 19 12:37:11 Finished compiler/parsing/proofs                               5m31s 876MB
Feb 19 12:37:12 Starting compiler/inference/proofs
Feb 19 12:39:58 Finished compiler/inference/proofs                             2m45s   1GB
Feb 19 12:39:59 Starting compiler/backend/semantics
Feb 19 12:47:54 Finished compiler/backend/semantics                            7m54s   2GB
Feb 19 12:47:55 Starting compiler/backend/reg_alloc/proofs
Feb 19 12:50:35 Finished compiler/backend/reg_alloc/proofs                     2m39s 760MB
Feb 19 12:50:36 Starting compiler/backend/proofs
Feb 19 13:28:30 Finished compiler/backend/proofs                              37m52s   3GB
Feb 19 13:28:31 Starting compiler/encoders/x64/proofs
Feb 19 13:37:33 Finished compiler/encoders/x64/proofs                          9m00s   4GB
Feb 19 13:37:34 Starting compiler/encoders/arm6/proofs
Feb 19 13:40:10 FAILED: compiler/encoders/arm6/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]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/arm/step]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/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/arm/model]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/prog]0;Holmake: ~/regression/HOL-45d15cd2a50ae6443bffb0631c58de3f6c0fe4b1/examples/l3-machine-code/arm/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/prog[0m
Starting work on arm-step-heap
arm-step-heap                                                                                              OK
Starting work on arm_progTheory
arm_progTheory                                                                                             OK
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-735/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-735/misc]0;Holmake: ~/regression/cakeml-735/developers]0;Holmake: ~/regression/cakeml-735/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-735/misc]0;Holmake: ~/regression/cakeml-735/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-735/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-735/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-735/misc]0;Holmake: ~/regression/cakeml-735/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-735/semantics]0;Holmake: ~/regression/cakeml-735/semantics/ffi]0;Holmake: ~/regression/cakeml-735/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-735/semantics]0;Holmake: ~/regression/cakeml-735/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../asm]0;Holmake: ../../asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6/proofs[0m
Starting work on arm6_targetProofTheory
Starting work on README.md
README.md                                                                                                  OK
arm6_targetProofTheory                                                                            FAILED! <1>
       (goal, thm) gentactic * (''a list * 'b -> goal list * validation)
    Reason: Can't unify term to ''a (Requires equality type)
 Found near
   (
   let val ... as ... = ... ...; val ... = ...; val ...; ... in
      ... \\ ... \\ ... ... \\ TRY (... ...) end
   handle List.Empty => FAIL_TAC "next_state_tac: empty") (asl, g)
 error in quse /home/myreen/regression/cakeml-735/compiler/encoders/arm6/proofs/arm6_targetProofScript.sml : Fail "Static Errors"
 error in load arm6_targetProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"