Job 756

CakeML:7eeab6cb5075c775f1be13e9b8dbdc0bb4e69cf5
  astToSexprLib: fix printing of nil strings [Mar 21 05:12:32]
#621 (unverified-sexpr-fix)
Merging into: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 21 05:38:25 Claimed job
Mar 21 05:39:07 Building HOL
Mar 21 05:48:25 Starting developers
Mar 21 05:48:28 Finished developers                                               2s  20MB
Mar 21 05:48:28 Starting developers/bin
Mar 21 05:49:42 Finished developers/bin                                        1m13s 918MB
Mar 21 05:49:43 Starting semantics/ffi
Mar 21 05:50:21 Finished semantics/ffi                                           37s 500MB
Mar 21 05:50:22 Starting semantics
Mar 21 05:51:58 Finished semantics                                             1m35s   1GB
Mar 21 05:51:59 Starting semantics/proofs
Mar 21 05:54:56 Finished semantics/proofs                                      2m56s   1GB
Mar 21 05:54:57 Starting basis/pure
Mar 21 05:58:34 Finished basis/pure                                            3m36s 703MB
Mar 21 05:58:35 Starting translator
Mar 21 06:00:15 Finished translator                                            1m39s   1GB
Mar 21 06:00:15 Starting compiler/parsing
Mar 21 06:01:13 Finished compiler/parsing                                        57s   2GB
Mar 21 06:01:14 Starting characteristic
Mar 21 06:05:32 Finished characteristic                                        4m17s   1GB
Mar 21 06:05:33 Starting translator/monadic
Mar 21 06:07:00 Finished translator/monadic                                    1m27s   1GB
Mar 21 06:07:01 Starting basis
Mar 21 06:23:22 Finished basis                                                16m19s   2GB
Mar 21 06:23:22 Starting compiler/inference
Mar 21 06:25:15 Finished compiler/inference                                    1m51s   1GB
Mar 21 06:25:15 Starting compiler/backend/reg_alloc
Mar 21 06:26:08 Finished compiler/backend/reg_alloc                              52s   1GB
Mar 21 06:26:09 Starting compiler/backend/gc
Mar 21 06:35:08 Finished compiler/backend/gc                                   8m58s   1GB
Mar 21 06:35:08 Starting compiler/backend
Mar 21 06:35:11 Finished compiler/backend                                         2s  24MB
Mar 21 06:35:12 Starting compiler/encoders/asm
Mar 21 06:35:14 Finished compiler/encoders/asm                                    1s  15MB
Mar 21 06:35:15 Starting compiler/encoders/x64
Mar 21 06:36:15 Finished compiler/encoders/x64                                   59s 700MB
Mar 21 06:36:16 Starting compiler/encoders/arm6
Mar 21 06:37:52 Finished compiler/encoders/arm6                                1m35s   1GB
Mar 21 06:37:52 Starting compiler/encoders/arm8
Mar 21 06:38:25 Finished compiler/encoders/arm8                                  31s 553MB
Mar 21 06:38:25 Starting compiler/encoders/mips
Mar 21 06:39:31 Finished compiler/encoders/mips                                1m04s   1GB
Mar 21 06:39:31 Starting compiler/encoders/riscv
Mar 21 06:40:48 Finished compiler/encoders/riscv                               1m16s   1GB
Mar 21 06:40:49 Starting compiler/encoders/ag32
Mar 21 06:41:06 Finished compiler/encoders/ag32                                  16s 797MB
Mar 21 06:41:07 Starting compiler/backend/x64
Mar 21 06:41:26 Finished compiler/backend/x64                                    18s 962MB
Mar 21 06:41:27 Starting compiler/backend/arm6
Mar 21 06:41:45 Finished compiler/backend/arm6                                   18s   1GB
Mar 21 06:41:46 Starting compiler/backend/arm8
Mar 21 06:42:05 Finished compiler/backend/arm8                                   18s   1GB
Mar 21 06:42:06 Starting compiler/backend/mips
Mar 21 06:42:26 Finished compiler/backend/mips                                   19s   1GB
Mar 21 06:42:26 Starting compiler/backend/riscv
Mar 21 06:42:46 Finished compiler/backend/riscv                                  18s   1GB
Mar 21 06:42:46 Starting compiler/backend/ag32
Mar 21 06:43:54 Finished compiler/backend/ag32                                 1m07s 872MB
Mar 21 06:43:55 Starting compiler/parsing/proofs
Mar 21 06:49:36 Finished compiler/parsing/proofs                               5m40s   1GB
Mar 21 06:49:36 Starting compiler/inference/proofs
Mar 21 06:52:14 Finished compiler/inference/proofs                             2m37s 929MB
Mar 21 06:52:15 Starting compiler/backend/semantics
Mar 21 06:59:06 Finished compiler/backend/semantics                            6m50s   1GB
Mar 21 06:59:07 Starting compiler/backend/reg_alloc/proofs
Mar 21 07:01:44 Finished compiler/backend/reg_alloc/proofs                     2m36s 728MB
Mar 21 07:01:45 Starting compiler/backend/proofs
Mar 21 07:38:29 Finished compiler/backend/proofs                              36m43s   3GB
Mar 21 07:38:30 Starting compiler/encoders/x64/proofs
Mar 21 07:48:26 Finished compiler/encoders/x64/proofs                          9m55s   4GB
Mar 21 07:48:27 Starting compiler/encoders/arm6/proofs
Mar 21 08:01:43 Finished compiler/encoders/arm6/proofs                        13m15s   3GB
Mar 21 08:01:43 Starting compiler/encoders/arm8/proofs
Mar 21 08:07:27 Finished compiler/encoders/arm8/proofs                         5m43s   1GB
Mar 21 08:07:28 Starting compiler/encoders/mips/proofs
Mar 21 08:17:17 Finished compiler/encoders/mips/proofs                         9m48s   2GB
Mar 21 08:17:18 Starting compiler/encoders/riscv/proofs
Mar 21 08:18:26 FAILED: compiler/encoders/riscv/proofs
]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/prog]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/model]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/lib]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/model]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/stepWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step
]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/prog]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/l3-machine-code/riscv/progWorking in $(HOLDIR)/examples/l3-machine-code/riscv/prog
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: ~/oven/regression/cakeml-756/misc]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-756/misc]0;Holmake: ~/oven/regression/cakeml-756/developers]0;Holmake: ~/oven/regression/cakeml-756/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-756/misc]0;Holmake: ~/oven/regression/cakeml-756/misc/lem_lib_stub]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-86a5bc67f59c5c9dce294f45c1b68611e1be2b15/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/cakeml-756/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-756/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-756/misc]0;Holmake: ~/oven/regression/cakeml-756/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../asm]0;Holmake: ~/oven/regression/cakeml-756/semantics]0;Holmake: ~/oven/regression/cakeml-756/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-756/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-756/semantics]0;Holmake: ~/oven/regression/cakeml-756/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../asm]0;Holmake: ../../asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: .]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/encoders/riscv
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Starting work on riscv_targetProofTheory
Starting work on README.md
README.md                                                                    OK
riscv_targetProofTheory                                             FAILED! <1>
 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/cake/oven/regression/cakeml-756/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"}
 Proof of 
 
 encoder_correct riscv_target
 
 failed.
 Failed to prove theorem riscv_encoder_correct.
 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"}