Job 754

CakeML:2d7716e211a3e687d5ba9f237de202f78cbc253b
  Merge pull request #619 from CakeML/reader-jlamp [Mar 05 06:58:18]
HOL:86a5bc67f59c5c9dce294f45c1b68611e1be2b15
  Add emacs key-binding (C-S-h) for Greek letter chi ( [Mar 19 03:50:42]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Mar 20 00:36:49 Claimed job
Mar 20 00:37:10 Building HOL
Mar 20 00:44:56 Starting developers
Mar 20 00:44:57 Finished developers                                               0s  29MB
Mar 20 00:44:57 Starting developers/bin
Mar 20 00:45:37 Finished developers/bin                                          39s 204MB
Mar 20 00:45:38 Starting semantics/ffi
Mar 20 00:46:13 Finished semantics/ffi                                           33s 469MB
Mar 20 00:46:13 Starting semantics
Mar 20 00:47:43 Finished semantics                                             1m29s   1GB
Mar 20 00:47:44 Starting semantics/proofs
Mar 20 00:50:38 Finished semantics/proofs                                      2m53s   1GB
Mar 20 00:50:39 Starting basis/pure
Mar 20 00:54:10 Finished basis/pure                                            3m30s 644MB
Mar 20 00:54:10 Starting translator
Mar 20 00:55:47 Finished translator                                            1m35s   1GB
Mar 20 00:55:48 Starting compiler/parsing
Mar 20 00:56:46 Finished compiler/parsing                                        57s   1GB
Mar 20 00:56:46 Starting characteristic
Mar 20 01:01:01 Finished characteristic                                        4m14s   2GB
Mar 20 01:01:02 Starting translator/monadic
Mar 20 01:02:27 Finished translator/monadic                                    1m24s   1GB
Mar 20 01:02:28 Starting basis
Mar 20 01:18:30 Finished basis                                                16m01s   2GB
Mar 20 01:18:30 Starting compiler/inference
Mar 20 01:20:15 Finished compiler/inference                                    1m43s   1GB
Mar 20 01:20:16 Starting compiler/backend/reg_alloc
Mar 20 01:21:06 Finished compiler/backend/reg_alloc                              49s   1GB
Mar 20 01:21:07 Starting compiler/backend/gc
Mar 20 01:29:50 Finished compiler/backend/gc                                   8m42s   1GB
Mar 20 01:29:51 Starting compiler/backend
Mar 20 01:29:53 Finished compiler/backend                                         0s  42MB
Mar 20 01:29:53 Starting compiler/encoders/asm
Mar 20 01:29:54 Finished compiler/encoders/asm                                    0s  32MB
Mar 20 01:29:55 Starting compiler/encoders/x64
Mar 20 01:30:51 Finished compiler/encoders/x64                                   55s 688MB
Mar 20 01:30:52 Starting compiler/encoders/arm6
Mar 20 01:32:25 Finished compiler/encoders/arm6                                1m32s   1GB
Mar 20 01:32:26 Starting compiler/encoders/arm8
Mar 20 01:32:54 Finished compiler/encoders/arm8                                  26s 558MB
Mar 20 01:32:54 Starting compiler/encoders/mips
Mar 20 01:33:56 Finished compiler/encoders/mips                                1m00s   1GB
Mar 20 01:33:57 Starting compiler/encoders/riscv
Mar 20 01:35:10 Finished compiler/encoders/riscv                               1m13s 789MB
Mar 20 01:35:11 Starting compiler/encoders/ag32
Mar 20 01:35:26 Finished compiler/encoders/ag32                                  14s 793MB
Mar 20 01:35:27 Starting compiler/backend/x64
Mar 20 01:35:43 Finished compiler/backend/x64                                    15s   1GB
Mar 20 01:35:44 Starting compiler/backend/arm6
Mar 20 01:36:00 Finished compiler/backend/arm6                                   15s   1GB
Mar 20 01:36:01 Starting compiler/backend/arm8
Mar 20 01:36:17 Finished compiler/backend/arm8                                   15s 876MB
Mar 20 01:36:18 Starting compiler/backend/mips
Mar 20 01:36:33 Finished compiler/backend/mips                                   14s 773MB
Mar 20 01:36:34 Starting compiler/backend/riscv
Mar 20 01:36:51 Finished compiler/backend/riscv                                  16s   1GB
Mar 20 01:36:52 Starting compiler/backend/ag32
Mar 20 01:37:57 Finished compiler/backend/ag32                                 1m04s   1GB
Mar 20 01:37:58 Starting compiler/parsing/proofs
Mar 20 01:43:31 Finished compiler/parsing/proofs                               5m32s 862MB
Mar 20 01:43:32 Starting compiler/inference/proofs
Mar 20 01:46:10 Finished compiler/inference/proofs                             2m36s   1GB
Mar 20 01:46:11 Starting compiler/backend/semantics
Mar 20 01:53:04 Finished compiler/backend/semantics                            6m52s   2GB
Mar 20 01:53:05 Starting compiler/backend/reg_alloc/proofs
Mar 20 01:55:42 Finished compiler/backend/reg_alloc/proofs                     2m36s 717MB
Mar 20 01:55:43 Starting compiler/backend/proofs
Mar 20 02:32:43 Finished compiler/backend/proofs                              37m00s   3GB
Mar 20 02:32:44 Starting compiler/encoders/x64/proofs
Mar 20 02:42:43 Finished compiler/encoders/x64/proofs                          9m58s   4GB
Mar 20 02:42:44 Starting compiler/encoders/arm6/proofs
Mar 20 02:56:23 Finished compiler/encoders/arm6/proofs                        13m37s   3GB
Mar 20 02:56:23 Starting compiler/encoders/arm8/proofs
Mar 20 03:02:06 Finished compiler/encoders/arm8/proofs                         5m42s   1GB
Mar 20 03:02:07 Starting compiler/encoders/mips/proofs
Mar 20 03:12:03 Finished compiler/encoders/mips/proofs                         9m55s   2GB
Mar 20 03:12:03 Starting compiler/encoders/riscv/proofs
Mar 20 03:13:10 FAILED: compiler/encoders/riscv/proofs
]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/prog]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/prog]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/prog[0m
Starting work on riscv-step-heap
riscv-step-heap                                                                                            OK
Starting work on riscv_progTheory
riscv_progTheory                                                                                           OK
]0;Holmake: .]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-754/misc]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-754/misc]0;Holmake: ~/regression/cakeml-754/developers]0;Holmake: ~/regression/cakeml-754/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-754/misc]0;Holmake: ~/regression/cakeml-754/misc/lem_lib_stub]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/cakeml-754/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-754/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-754/misc]0;Holmake: ~/regression/cakeml-754/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-754/semantics]0;Holmake: ~/regression/cakeml-754/semantics/ffi]0;Holmake: ~/regression/cakeml-754/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-754/semantics]0;Holmake: ~/regression/cakeml-754/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/riscv[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv/proofs[0m
Starting work on riscv_targetProofTheory
Starting work on README.md
README.md                                                                                                  OK
riscv_targetProofTheory                                                                           FAILED! <1>
 encoder_correct riscv_target
 
 failed.
 Failed to prove theorem riscv_encoder_correct.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 457) (THEN1 on line 464) (THEN1 on line 479) (THEN1 on line 544) (THEN1 on line 452) (THEN1 on line 563) (THEN1 on line 568) (THEN1 on line 605) (THEN1 on line 610) (THEN1 on line 617)
 error in quse /home/myreen/regression/cakeml-754/compiler/encoders/riscv/proofs/riscv_targetProofScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 457) (THEN1 on line 464) (THEN1 on line 479) (THEN1 on line 544) (THEN1 on line 452) (THEN1 on line 563) (THEN1 on line 568) (THEN1 on line 605) (THEN1 on line 610) (THEN1 on line 617)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load riscv_targetProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 457) (THEN1 on line 464) (THEN1 on line 479) (THEN1 on line 544) (THEN1 on line 452) (THEN1 on line 563) (THEN1 on line 568) (THEN1 on line 605) (THEN1 on line 610) (THEN1 on line 617)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 457) (THEN1 on line 464) (THEN1 on line 479) (THEN1 on line 544) (THEN1 on line 452) (THEN1 on line 563) (THEN1 on line 568) (THEN1 on line 605) (THEN1 on line 610) (THEN1 on line 617)", origin_function = "THEN1", origin_structure = "Tactical"}