Job 493

CakeML:1eac9d010b210e5bbcc05c5a01b6e76b19804dd3
  FFI: create files with sensible (0644) permissions [Sep 13 00:50:17]
#525 (file-create-permissions)
Merging into:306e73e0ef0314393ecdbb996b50cf799375f15d
  Use Git's -C option [Sep 14 21:28:55]
HOL:2a42da875092fdec35e1cd69454995735c890117
  Merge pull request #590 from binghe/PSL.fix [Sep 20 03:54:57]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Sep 20 23:28:40 Claimed job
Sep 20 23:28:45 Reusing HOL
Sep 20 23:29:49 Starting developers/bin
Sep 20 23:30:02 Finished developers/bin                                          11s 916MB
Sep 20 23:30:03 Starting semantics/ffi
Sep 20 23:31:08 Finished semantics/ffi                                         1m02s 551MB
Sep 20 23:31:10 Starting semantics
Sep 20 23:33:26 Finished semantics                                             2m14s 855MB
Sep 20 23:33:27 Starting semantics/proofs
Sep 20 23:37:34 Finished semantics/proofs                                      4m04s 993MB
Sep 20 23:37:35 Starting basis/pure
Sep 20 23:43:00 Finished basis/pure                                            5m23s 743MB
Sep 20 23:43:02 Starting translator
Sep 20 23:44:52 Finished translator                                            1m48s 989MB
Sep 20 23:44:54 Starting compiler/parsing
Sep 20 23:47:15 Finished compiler/parsing                                      2m19s   3GB
Sep 20 23:47:17 Starting characteristic
Sep 20 23:51:17 Finished characteristic                                        3m58s   1GB
Sep 20 23:51:19 Starting translator/monadic
Sep 20 23:53:36 Finished translator/monadic                                    2m15s   1GB
Sep 20 23:53:38 Starting basis
Sep 21 00:19:31 Finished basis                                                25m51s   2GB
Sep 21 00:19:33 Starting compiler/inference
Sep 21 00:22:14 Finished compiler/inference                                    2m38s   1GB
Sep 21 00:22:15 Starting compiler/backend/reg_alloc
Sep 21 00:23:34 Finished compiler/backend/reg_alloc                            1m16s   1GB
Sep 21 00:23:35 Starting compiler/backend/gc
Sep 21 00:37:16 Finished compiler/backend/gc                                  13m39s   3GB
Sep 21 00:37:18 Starting compiler/backend
Sep 21 00:37:23 Finished compiler/backend                                         3s  15MB
Sep 21 00:37:25 Starting compiler/encoders/asm
Sep 21 00:37:28 Finished compiler/encoders/asm                                    1s  14MB
Sep 21 00:37:30 Starting compiler/encoders/x64
Sep 21 00:39:01 Finished compiler/encoders/x64                                 1m29s 606MB
Sep 21 00:39:02 Starting compiler/encoders/arm6
Sep 21 00:42:03 Finished compiler/encoders/arm6                                2m59s   1GB
Sep 21 00:42:05 Starting compiler/encoders/arm8
Sep 21 00:42:54 Finished compiler/encoders/arm8                                  47s 484MB
Sep 21 00:42:55 Starting compiler/encoders/mips
Sep 21 00:44:33 Finished compiler/encoders/mips                                1m35s 836MB
Sep 21 00:44:34 Starting compiler/encoders/riscv
Sep 21 00:46:15 Finished compiler/encoders/riscv                               1m38s 831MB
Sep 21 00:46:16 Starting compiler/backend/x64
Sep 21 00:46:45 Finished compiler/backend/x64                                    27s 848MB
Sep 21 00:46:47 Starting compiler/backend/arm6
Sep 21 00:47:20 Finished compiler/backend/arm6                                   31s   1GB
Sep 21 00:47:21 Starting compiler/backend/arm8
Sep 21 00:47:53 Finished compiler/backend/arm8                                   30s   1GB
Sep 21 00:47:55 Starting compiler/backend/mips
Sep 21 00:48:29 Finished compiler/backend/mips                                   31s 844MB
Sep 21 00:48:30 Starting compiler/backend/riscv
Sep 21 00:49:01 Finished compiler/backend/riscv                                  29s   1GB
Sep 21 00:49:03 Starting compiler/parsing/proofs
Sep 21 00:59:03 Finished compiler/parsing/proofs                               9m58s   1GB
Sep 21 00:59:05 Starting compiler/inference/proofs
Sep 21 01:03:30 Finished compiler/inference/proofs                             4m23s   1GB
Sep 21 01:03:32 Starting compiler/backend/semantics
Sep 21 01:16:55 Finished compiler/backend/semantics                           13m21s   2GB
Sep 21 01:16:56 Starting compiler/backend/reg_alloc/proofs
Sep 21 01:27:40 Finished compiler/backend/reg_alloc/proofs                    10m41s 689MB
Sep 21 01:27:41 Starting compiler/backend/proofs
Sep 21 01:41:56 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developers[1mWorking in ../../../developers[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../translator]0;Holmake: ../../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
Starting work on heap
heap                                                                                                                                                       OK
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
Starting work on bvi_letProofTheory
data_simpProofTheory                                                                                                                                       OK
Starting work on bvi_tailrecProofTheory
data_spaceProofTheory                                                                                                                                      OK
Starting work on bvl_constProofTheory
bvi_letProofTheory                                                                                                                                         OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                                                                                                                                        OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                                                                                                                                       OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                                                                                                                                   OK
Starting work on clos_callProofTheory
bvl_constProofTheory                                                                                                                                       OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                                                                                                                                      OK
Starting work on bvl_inlineProofTheory
bvi_to_dataProofTheory                                                                                                                                     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                                                                                                      OK
Starting work on clos_knownProofTheory
bvl_inlineProofTheory                                                                                                                                      OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                                                                                                                                        OK
Starting work on clos_numberProofTheory
clos_numberProofTheory                                                                                                                                     OK
Starting work on word_simpProofTheory
clos_knownProofTheory                                                                                                                                 CHEATED
Starting work on word_bignumProofTheory
bvi_tailrecProofTheory                                                                                                                                     OK
Starting work on bvl_to_bviProofTheory
clos_callProofTheory                                                                                                                                  CHEATED
Starting work on clos_to_bvlProofTheory
word_simpProofTheory                                                                                                                                       OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory                                                                                                                                     OK
Starting work on data_to_word_memoryProofTheory
word_bignumProofTheory                                                                                                                                     OK
Starting work on word_allocProofTheory
bvl_to_bviProofTheory                                                                                                                                      OK
Starting work on word_instProofTheory
word_instProofTheory                                                                                                                                       OK
Starting work on word_removeProofTheory
word_removeProofTheory                                                                                                                                     OK
Starting work on flat_to_patProofTheory
clos_to_bvlProofTheory                                                                                                                                CHEATED
Starting work on lab_filterProofTheory
lab_filterProofTheory                                                                                                                                      OK
Starting work on stack_removeProofTheory
word_allocProofTheory                                                                                                                             FAILED! <1>
 error in load word_allocProofScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 3988) (THEN1 on line 4016) (THEN1 on line 4019) (THEN1 on line 4022) (THEN1 on line 4035) (THEN1 on line 4039)", origin_function = "THEN1", origin_structure = "Tactical"}
 Proof of 
 
 prog ssa na prog' ssa' na'.
     ssa_cc_trans prog ssa na = (prog',ssa',na')  ssa_map_ok na ssa 
     is_alloc_var na 
     na  na'  is_alloc_var na'  ssa_map_ok na' ssa'
 
 failed.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 3988) (THEN1 on line 4016) (THEN1 on line 4019) (THEN1 on line 4022) (THEN1 on line 4035) (THEN1 on line 4039)", origin_function = "THEN1", origin_structure = "Tactical"}
data_to_word_memoryProofTheory                                                                                                                       M-KILLED
flat_to_patProofTheory                                                                                                                               M-KILLED
stack_removeProofTheory                                                                                                                              M-KILLED