Job 330

CakeML:1d04062bbb2d74197e2533403a3fdce3680fe7d7
  Fix backend proofs for irule change [May 30 12:44:54]
HOL:58365d9a025ae1a931842abcd5e3938d77761948
  added regexp for valid utf-8 strings to test files. Other changes are [May 30 12:58:00]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

May 30 14:03:02 Claimed job
May 30 14:03:13 Building HOL
May 30 14:14:32 Starting developers/bin
May 30 14:14:42 Finished developers/bin                                           8s 224MB
May 30 14:14:44 Starting semantics/ffi
May 30 14:15:44 Finished semantics/ffi                                           58s 493MB
May 30 14:15:46 Starting semantics
May 30 14:18:04 Finished semantics                                             2m15s 919MB
May 30 14:18:06 Starting semantics/proofs
May 30 14:21:19 Finished semantics/proofs                                      3m11s   1GB
May 30 14:21:21 Starting basis/pure
May 30 14:27:06 Finished basis/pure                                            5m43s 540MB
May 30 14:27:08 Starting translator
May 30 14:33:44 Finished translator                                            6m33s 881MB
May 30 14:33:46 Starting compiler/parsing
May 30 14:35:57 Finished compiler/parsing                                      2m08s   2GB
May 30 14:35:59 Starting characteristic
May 30 14:40:18 Finished characteristic                                        4m17s   1GB
May 30 14:40:20 Starting basis
May 30 15:08:41 Finished basis                                                28m18s   2GB
May 30 15:08:43 Starting translator/monadic
May 30 15:08:47 Finished translator/monadic                                       2s  16MB
May 30 15:08:49 Starting compiler/inference
May 30 15:11:29 Finished compiler/inference                                    2m37s   1GB
May 30 15:11:31 Starting compiler/backend/reg_alloc
May 30 15:12:27 Finished compiler/backend/reg_alloc                              54s 988MB
May 30 15:12:29 Starting compiler/backend/gc
May 30 15:27:16 Finished compiler/backend/gc                                  14m44s   3GB
May 30 15:27:18 Starting compiler/backend
May 30 15:27:23 Finished compiler/backend                                         3s  14MB
May 30 15:27:25 Starting compiler/encoders/asm
May 30 15:27:28 Finished compiler/encoders/asm                                    0s  25MB
May 30 15:27:30 Starting compiler/encoders/x64
May 30 15:28:57 Finished compiler/encoders/x64                                 1m25s 508MB
May 30 15:28:59 Starting compiler/encoders/arm6
May 30 15:31:59 Finished compiler/encoders/arm6                                2m57s   1GB
May 30 15:32:01 Starting compiler/encoders/arm8
May 30 15:32:44 Finished compiler/encoders/arm8                                  41s 409MB
May 30 15:32:46 Starting compiler/encoders/mips
May 30 15:34:26 Finished compiler/encoders/mips                                1m37s 667MB
May 30 15:34:28 Starting compiler/encoders/riscv
May 30 15:36:03 Finished compiler/encoders/riscv                               1m32s 716MB
May 30 15:36:05 Starting compiler/backend/x64
May 30 15:36:36 Finished compiler/backend/x64                                    29s 821MB
May 30 15:36:38 Starting compiler/backend/arm6
May 30 15:37:15 Finished compiler/backend/arm6                                   34s   1GB
May 30 15:37:17 Starting compiler/backend/arm8
May 30 15:37:50 Finished compiler/backend/arm8                                   31s   1GB
May 30 15:37:52 Starting compiler/backend/mips
May 30 15:38:27 Finished compiler/backend/mips                                   33s   1GB
May 30 15:38:29 Starting compiler/backend/riscv
May 30 15:39:02 Finished compiler/backend/riscv                                  30s   1GB
May 30 15:39:04 Starting compiler/parsing/proofs
May 30 15:43:04 Finished compiler/parsing/proofs                               3m58s 762MB
May 30 15:43:06 Starting compiler/inference/proofs
May 30 15:47:03 Finished compiler/inference/proofs                             3m55s   1GB
May 30 15:47:05 Starting compiler/backend/semantics
May 30 16:05:25 Finished compiler/backend/semantics                           18m17s   2GB
May 30 16:05:27 Starting compiler/backend/reg_alloc/proofs
May 30 16:06:51 Finished compiler/backend/reg_alloc/proofs                     1m22s 381MB
May 30 16:06:53 Starting compiler/backend/proofs
May 30 17:02:45 Finished compiler/backend/proofs                              55m49s   4GB
May 30 17:02:47 Starting compiler/encoders/x64/proofs
May 30 17:14:34 Finished compiler/encoders/x64/proofs                         11m44s   2GB
May 30 17:14:36 Starting compiler/encoders/arm6/proofs
May 30 17:26:54 Finished compiler/encoders/arm6/proofs                        12m16s   3GB
May 30 17:26:56 Starting compiler/encoders/arm8/proofs
May 30 17:35:14 Finished compiler/encoders/arm8/proofs                         8m16s   1GB
May 30 17:35:16 Starting compiler/encoders/mips/proofs
May 30 17:46:52 Finished compiler/encoders/mips/proofs                        11m33s   2GB
May 30 17:46:54 Starting compiler/encoders/riscv/proofs
May 30 17:59:24 Finished compiler/encoders/riscv/proofs                       12m26s 944MB
May 30 17:59:26 Starting compiler/backend/x64/proofs
May 30 18:00:03 Finished compiler/backend/x64/proofs                             35s   1GB
May 30 18:00:05 Starting compiler/backend/arm6/proofs
May 30 18:00:42 Finished compiler/backend/arm6/proofs                            34s   1GB
May 30 18:00:44 Starting compiler/backend/arm8/proofs
May 30 18:01:19 Finished compiler/backend/arm8/proofs                            33s   1GB
May 30 18:01:21 Starting compiler/backend/mips/proofs
May 30 18:01:57 Finished compiler/backend/mips/proofs                            33s   1GB
May 30 18:01:59 Starting compiler/backend/riscv/proofs
May 30 18:02:35 Finished compiler/backend/riscv/proofs                           33s   1GB
May 30 18:02:37 Starting compiler/proofs
May 30 18:04:59 Finished compiler/proofs                                       2m19s   1GB
May 30 18:05:01 Starting candle/set-theory
May 30 18:06:39 Finished candle/set-theory                                     1m35s 582MB
May 30 18:06:41 Starting candle/syntax-lib
May 30 18:07:00 Finished candle/syntax-lib                                       17s 551MB
May 30 18:07:02 Starting candle/standard/syntax
May 30 18:09:46 Finished candle/standard/syntax                                2m42s 721MB
May 30 18:09:48 Starting candle/standard/semantics
May 30 18:12:04 Finished candle/standard/semantics                             2m13s   1GB
May 30 18:12:06 Starting candle/standard/monadic
May 30 18:14:33 Finished candle/standard/monadic                               2m25s   1GB
May 30 18:14:35 Starting candle/standard/ml_kernel
May 30 18:15:55 FAILED: candle/standard/ml_kernel
]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-58365d9a025ae1a931842abcd5e3938d77761948/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ../../../basis]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../basis]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../../../basis]0;Holmake: ../../../basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: ../monadic]0;Holmake: ../syntax]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-libWorking in $(CAKEMLDIR)/candle/syntax-lib
]0;Holmake: ../syntax]0;Holmake: ../syntaxWorking in $(CAKEMLDIR)/candle/standard/syntax
]0;Holmake: ../monadic]0;Holmake: ../monadicWorking in $(CAKEMLDIR)/candle/standard/monadic
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/candle/standard/ml_kernel
Starting work on heap
heap                                                                                            OK
Starting work on ml_hol_kernelProgTheory
ml_hol_kernelProgTheory                                                                FAILED! <1>
 Proof of 
 
 state p.
     state.the_type_constants = init_type_constants 
     state.the_term_constants = init_term_constants 
     state.the_axioms = init_axioms  state.the_context = init_context 
     REFS_PRED (HOL_STORE,p) state (auto_state_14 ffi)
 
 failed.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic", origin_function = "THEN1", origin_structure = "Tactical"}