Job 1828

CakeML:141a00a2070744e5529a2810967141cb80d5041f
  Fix `arm8_asl` proof [Mar 24 09:53:34]
#869 (ffi-changes)
Merging into:94ac4b68ba71917ede94f5bb752deb85333acb21
  Fix a build error caused by HOL-Theorem-Prover/HOL@60adf92493ffff [Mar 17 04:55:12]
HOL:0fd5e8a4264261eaf15f8a9f4dcaf83838e47355
  Ensure % is safely printed to TeX as \% (when used as integer mod) [Mar 22 23:24:14]
Machine:oven3

Mar 24 11:59:26 Claimed job
Mar 24 11:59:40 Building+HOL
Mar 24 12:19:47 Starting+developers
Mar 24 12:19:56 Finished+developers++++++++++++++++++++++++++++++++++++++++8.84+150504
Mar 24 12:19:56 Starting+developers/bin
Mar 24 12:20:37 Finished+developers/bin++++++++++++++++++++++++++++++++++++40.74+1253076
Mar 24 12:20:37 Starting+semantics/ffi
Mar 24 12:21:04 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++25.94+250724
Mar 24 12:21:04 Starting+semantics
Mar 24 12:25:27 Finished+semantics+++++++++++++++++++++++++++++++++++++++++262.81+1477620
Mar 24 12:25:27 Starting+semantics/proofs
Mar 24 12:34:30 Finished+semantics/proofs++++++++++++++++++++++++++++++++++542.39+4055544
Mar 24 12:34:30 Starting+semantics/alt_semantics
Mar 24 12:35:09 Finished+semantics/alt_semantics+++++++++++++++++++++++++++38.59+475552
Mar 24 12:35:09 Starting+semantics/alt_semantics/proofs
Mar 24 12:40:33 Finished+semantics/alt_semantics/proofs++++++++++++++++++++323.88+1149356
Mar 24 12:40:33 Starting+basis/pure
Mar 24 12:47:15 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++401.88+1160776
Mar 24 12:47:15 Starting+translator
Mar 24 12:53:36 Finished+translator++++++++++++++++++++++++++++++++++++++++379.84+1503556
Mar 24 12:53:36 Starting+compiler/parsing
Mar 24 12:56:29 Finished+compiler/parsing++++++++++++++++++++++++++++++++++172.94+2020200
Mar 24 12:56:29 Starting+characteristic
Mar 24 13:09:49 Finished+characteristic++++++++++++++++++++++++++++++++++++799.34+2996700
Mar 24 13:09:49 Starting+translator/monadic
Mar 24 13:13:56 Finished+translator/monadic++++++++++++++++++++++++++++++++246.83+1934200
Mar 24 13:13:56 Starting+basis
Mar 24 14:55:53 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6116.77+15923808
Mar 24 14:55:53 Starting+compiler/inference
Mar 24 14:59:03 Finished+compiler/inference++++++++++++++++++++++++++++++++189.12+1485436
Mar 24 14:59:03 Starting+compiler/backend/reg_alloc
Mar 24 15:02:15 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++192.29+1953780
Mar 24 15:02:16 Starting+compiler/backend/gc
Mar 24 15:10:44 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++508.70+3362228
Mar 24 15:10:45 Starting+compiler/backend
Mar 24 15:22:02 Finished+compiler/backend++++++++++++++++++++++++++++++++++676.98+2215252
Mar 24 15:22:02 Starting+compiler/encoders/asm
Mar 24 15:23:06 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++63.27+784344
Mar 24 15:23:06 Starting+compiler/encoders/x64
Mar 24 15:25:39 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++153.42+1130308
Mar 24 15:25:40 Starting+compiler/encoders/arm7
Mar 24 15:30:34 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++294.14+1720560
Mar 24 15:30:34 Starting+compiler/encoders/arm8
Mar 24 15:32:07 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++92.99+1016960
Mar 24 15:32:08 Starting+compiler/encoders/arm8_asl
Mar 24 19:39:28 Finished+compiler/encoders/arm8_asl++++++++++++++++++++++++14839.90+33517532
Mar 24 19:39:28 Starting+compiler/encoders/mips
Mar 24 19:42:57 Finished+compiler/encoders/mips++++++++++++++++++++++++++++208.68+905500
Mar 24 19:42:57 Starting+compiler/encoders/riscv
Mar 24 19:46:54 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++236.80+935244
Mar 24 19:46:54 Starting+compiler/encoders/ag32
Mar 24 19:47:44 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++49.03+997972
Mar 24 19:47:44 Starting+compiler/backend/x64
Mar 24 19:48:32 Finished+compiler/backend/x64++++++++++++++++++++++++++++++47.74+1563288
Mar 24 19:48:32 Starting+compiler/backend/arm7
Mar 24 19:49:22 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++49.51+1517900
Mar 24 19:49:22 Starting+compiler/backend/arm8
Mar 24 19:50:09 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++47.18+1400744
Mar 24 19:50:10 Starting+compiler/backend/mips
Mar 24 19:50:57 Finished+compiler/backend/mips+++++++++++++++++++++++++++++47.21+1455972
Mar 24 19:50:57 Starting+compiler/backend/riscv
Mar 24 19:51:46 Finished+compiler/backend/riscv++++++++++++++++++++++++++++48.86+1461192
Mar 24 19:51:46 Starting+compiler/backend/ag32
Mar 24 19:54:47 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++180.59+1405696
Mar 24 19:54:47 Starting+compiler/parsing/proofs
Mar 24 20:03:22 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++513.93+1241592
Mar 24 20:03:22 Starting+compiler/inference/proofs
Mar 24 20:09:02 Finished+compiler/inference/proofs+++++++++++++++++++++++++339.69+1336408
Mar 24 20:09:02 Starting+compiler/backend/semantics
Mar 24 21:12:33 Finished+compiler/backend/semantics++++++++++++++++++++++++3810.21+1858328
Mar 24 21:12:34 Starting+compiler/backend/reg_alloc/proofs
Mar 24 21:20:46 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++492.66+855496
Mar 24 21:20:47 Starting+compiler/backend/proofs
Mar 24 23:01:21 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6033.54+17088668
Mar 24 23:01:21 Starting+compiler/backend/serialiser
Mar 24 23:04:44 Finished+compiler/backend/serialiser+++++++++++++++++++++++203.36+2401976
Mar 24 23:04:44 Starting+compiler/encoders/x64/proofs
Mar 24 23:26:50 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1325.82+4667272
Mar 24 23:26:51 Starting+compiler/encoders/arm7/proofs
Mar 24 23:56:54 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1803.25+3811948
Mar 24 23:56:54 Starting+compiler/encoders/arm8/proofs
Mar 25 00:12:42 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++947.40+1584404
Mar 25 00:12:42 Starting+compiler/encoders/arm8_asl/proofs
Mar 25 02:06:04 Finished+compiler/encoders/arm8_asl/proofs+++++++++++++++++6801.70+5466936
Mar 25 02:06:05 Starting+compiler/encoders/mips/proofs
Mar 25 02:30:28 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1463.30+2571372
Mar 25 02:30:28 Starting+compiler/encoders/riscv/proofs
Mar 25 02:51:24 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1255.19+1226188
Mar 25 02:51:24 Starting+compiler/encoders/ag32/proofs
Mar 25 02:57:13 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++348.59+975616
Mar 25 02:57:13 Starting+compiler/backend/x64/proofs
Mar 25 02:58:10 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++56.71+1607180
Mar 25 02:58:10 Starting+compiler/backend/arm7/proofs
Mar 25 02:59:13 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++62.59+1792632
Mar 25 02:59:13 Starting+compiler/backend/arm8/proofs
Mar 25 03:00:11 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++57.23+1145556
Mar 25 03:00:11 Starting+compiler/backend/arm8_asl
Mar 25 03:00:59 Finished+compiler/backend/arm8_asl+++++++++++++++++++++++++48.01+1126192
Mar 25 03:00:59 Starting+compiler/backend/mips/proofs
Mar 25 03:02:00 Finished+compiler/backend/mips/proofs++++++++++++++++++++++60.29+1458352
Mar 25 03:02:00 Starting+compiler/backend/riscv/proofs
Mar 25 03:02:58 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++57.92+1740308
Mar 25 03:02:58 Starting+compiler/backend/ag32/proofs
Mar 25 03:28:17 FAILED:+compiler/backend/ag32/proofs
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
Scanned 52 directories
Starting work on stateTheory
Starting work on README.md
Starting work on ag32_configProofTheory
README.md                                                                                                                                                               compiler/backend/ag32/proofs  (0s)     OK
stateTheory                                                                                                                                                          examples/l3-machine-code/common  (9s)     OK
Starting work on temporal_stateTheory
temporal_stateTheory                                                                                                                                                 examples/l3-machine-code/common  (7s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/common [#theories: 2]                                                                                                                                       (17.404s) 
Starting work on ag32_progTheory
ag32_configProofTheory                                                                                                                                                  compiler/backend/ag32/proofs (49s)     OK
Starting work on ag32_machine_configTheory
ag32_progTheory                                                                                                                                                         compiler/backend/ag32/proofs (41s)     OK
Starting work on ag32_ffi_codeProofTheory
ag32_machine_configTheory                                                                                                                                               compiler/backend/ag32/proofs (48s)     OK
Starting work on ag32_memoryProofTheory
ag32_ffi_codeProofTheory                                                                                                                                                compiler/backend/ag32/proofs(195s)     OK
ag32_memoryProofTheory                                                                                                                                                  compiler/backend/ag32/proofs(836s)     OK
Starting work on ag32_basis_ffiProofTheory
ag32_basis_ffiProofTheory                                                                                                                                               compiler/backend/ag32/proofs(551s)FAIL<1>
 Saved theorem _______ "ag32_ffi_interfer_close"
 Saved theorem _______ "ag32_ffi_interfer_get_arg_count"
 Saved theorem _______ "cline_in_memory_has_n_args"
 Saved theorem _______ "ag32_ffi_interfer_get_arg_length"
 Saved theorem _______ "ag32_ffi_interfer_get_arg"
 Saved theorem _______ "ag32_ffi_interfer_"
 Saved theorem _______ "SUBSET_ffi_names_IMP_LENGTH_LESS_EQ"
 error in quse /root/regression/cakeml-1828/compiler/backend/ag32/proofs/ag32_basis_ffiProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load /root/regression/cakeml-1828/compiler/backend/ag32/proofs/ag32_basis_ffiProofScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}