Job 1801

CakeML:46ea63eec171a69d8344514f2c0b9688e63edfae
  Get basis to build again [Feb 25 12:09:48]
HOL:56dc1e0e615822dd6a135a511531a138bae2688c
  Refine definition of what it is to be a vacuous pattern [Feb 25 06:46:55]
Machine:oven3+4.19.67.1.amd64-smp+

Feb 25 14:28:07 Claimed job
Feb 25 14:28:11 Reusing+HOL
Feb 25 14:29:08 Starting+developers
Feb 25 14:29:17 Finished+developers++++++++++++++++++++++++++++++++++++++++8.62+161068
Feb 25 14:29:17 Starting+developers/bin
Feb 25 14:29:27 Finished+developers/bin++++++++++++++++++++++++++++++++++++10.29+678852
Feb 25 14:29:28 Starting+semantics/ffi
Feb 25 14:29:56 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++28.42+253532
Feb 25 14:29:56 Starting+semantics
Feb 25 14:34:07 Finished+semantics+++++++++++++++++++++++++++++++++++++++++250.67+1237412
Feb 25 14:34:07 Starting+semantics/proofs
Feb 25 14:42:17 Finished+semantics/proofs++++++++++++++++++++++++++++++++++489.22+1482568
Feb 25 14:42:17 Starting+semantics/alt_semantics
Feb 25 14:42:55 Finished+semantics/alt_semantics+++++++++++++++++++++++++++37.19+498700
Feb 25 14:42:55 Starting+semantics/alt_semantics/proofs
Feb 25 14:48:14 Finished+semantics/alt_semantics/proofs++++++++++++++++++++319.19+1298476
Feb 25 14:48:14 Starting+basis/pure
Feb 25 14:50:24 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++130.01+935860
Feb 25 14:50:25 Starting+translator
Feb 25 14:56:45 Finished+translator++++++++++++++++++++++++++++++++++++++++380.42+1455400
Feb 25 14:56:45 Starting+compiler/parsing
Feb 25 14:59:33 Finished+compiler/parsing++++++++++++++++++++++++++++++++++167.18+2337796
Feb 25 14:59:33 Starting+characteristic
Feb 25 15:13:11 Finished+characteristic++++++++++++++++++++++++++++++++++++817.74+2022240
Feb 25 15:13:11 Starting+translator/monadic
Feb 25 15:17:20 Finished+translator/monadic++++++++++++++++++++++++++++++++248.35+1546056
Feb 25 15:17:20 Starting+basis
Feb 25 17:00:38 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6196.39+17149668
Feb 25 17:00:39 Starting+compiler/inference
Feb 25 17:03:40 Finished+compiler/inference++++++++++++++++++++++++++++++++181.04+1556924
Feb 25 17:03:40 Starting+compiler/backend/reg_alloc
Feb 25 17:06:55 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++194.99+1685812
Feb 25 17:06:55 Starting+compiler/backend/gc
Feb 25 17:15:27 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++511.56+2285440
Feb 25 17:15:27 Starting+compiler/backend
Feb 25 17:26:12 Finished+compiler/backend++++++++++++++++++++++++++++++++++644.64+1945852
Feb 25 17:26:12 Starting+compiler/encoders/asm
Feb 25 17:27:16 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++63.96+678860
Feb 25 17:27:17 Starting+compiler/encoders/x64
Feb 25 17:29:46 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++149.31+1098924
Feb 25 17:29:46 Starting+compiler/encoders/arm7
Feb 25 17:34:31 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++284.66+1472544
Feb 25 17:34:31 Starting+compiler/encoders/arm8
Feb 25 17:36:04 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++92.45+694180
Feb 25 17:36:04 Starting+compiler/encoders/arm8_asl
Feb 25 21:49:08 Finished+compiler/encoders/arm8_asl++++++++++++++++++++++++15181.52+45292864
Feb 25 21:49:08 Starting+compiler/encoders/mips
Feb 25 21:52:35 Finished+compiler/encoders/mips++++++++++++++++++++++++++++206.62+1417508
Feb 25 21:52:35 Starting+compiler/encoders/riscv
Feb 25 21:56:29 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++234.02+803596
Feb 25 21:56:29 Starting+compiler/encoders/ag32
Feb 25 21:57:17 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++47.66+673820
Feb 25 21:57:17 Starting+compiler/backend/x64
Feb 25 21:58:04 Finished+compiler/backend/x64++++++++++++++++++++++++++++++46.59+1530436
Feb 25 21:58:04 Starting+compiler/backend/arm7
Feb 25 21:58:54 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++49.58+1538060
Feb 25 21:58:54 Starting+compiler/backend/arm8
Feb 25 21:59:43 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++48.02+1568356
Feb 25 21:59:43 Starting+compiler/backend/mips
Feb 25 22:00:29 Finished+compiler/backend/mips+++++++++++++++++++++++++++++46.20+1447868
Feb 25 22:00:29 Starting+compiler/backend/riscv
Feb 25 22:01:18 Finished+compiler/backend/riscv++++++++++++++++++++++++++++48.58+1445648
Feb 25 22:01:18 Starting+compiler/backend/ag32
Feb 25 22:04:19 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++180.17+1453064
Feb 25 22:04:19 Starting+compiler/parsing/proofs
Feb 25 22:12:58 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++519.21+1097768
Feb 25 22:12:59 Starting+compiler/inference/proofs
Feb 25 22:18:36 Finished+compiler/inference/proofs+++++++++++++++++++++++++337.02+1031240
Feb 25 22:18:36 Starting+compiler/backend/semantics
Feb 25 23:21:50 Finished+compiler/backend/semantics++++++++++++++++++++++++3794.00+1959924
Feb 25 23:21:51 Starting+compiler/backend/reg_alloc/proofs
Feb 25 23:29:50 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++479.03+876436
Feb 25 23:29:50 Starting+compiler/backend/proofs
Feb 26 01:12:11 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6140.83+13779728
Feb 26 01:12:11 Starting+compiler/backend/serialiser
Feb 26 01:15:29 Finished+compiler/backend/serialiser+++++++++++++++++++++++197.73+1939752
Feb 26 01:15:30 Starting+compiler/encoders/x64/proofs
Feb 26 01:37:15 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1305.79+4466048
Feb 26 01:37:16 Starting+compiler/encoders/arm7/proofs
Feb 26 02:06:49 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1773.41+3418840
Feb 26 02:06:49 Starting+compiler/encoders/arm8/proofs
Feb 26 02:22:21 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++930.20+1428280
Feb 26 02:22:21 Starting+compiler/encoders/arm8_asl/proofs
Feb 26 04:14:52 Finished+compiler/encoders/arm8_asl/proofs+++++++++++++++++6750.85+6180504
Feb 26 04:14:52 Starting+compiler/encoders/mips/proofs
Feb 26 04:37:22 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1348.98+3187792
Feb 26 04:37:22 Starting+compiler/encoders/riscv/proofs
Feb 26 04:57:04 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1181.59+1387276
Feb 26 04:57:04 Starting+compiler/encoders/ag32/proofs
Feb 26 05:02:48 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++344.55+865804
Feb 26 05:02:49 Starting+compiler/backend/x64/proofs
Feb 26 05:03:48 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++59.19+1696984
Feb 26 05:03:48 Starting+compiler/backend/arm7/proofs
Feb 26 05:04:46 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++57.53+1852416
Feb 26 05:04:46 Starting+compiler/backend/arm8/proofs
Feb 26 05:05:49 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++63.09+1626300
Feb 26 05:05:50 Starting+compiler/backend/arm8_asl
Feb 26 05:06:42 Finished+compiler/backend/arm8_asl+++++++++++++++++++++++++52.44+1716460
Feb 26 05:06:43 Starting+compiler/backend/mips/proofs
Feb 26 05:07:43 Finished+compiler/backend/mips/proofs++++++++++++++++++++++59.99+1380568
Feb 26 05:07:43 Starting+compiler/backend/riscv/proofs
Feb 26 05:08:43 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++60.06+1859416
Feb 26 05:08:43 Starting+compiler/backend/ag32/proofs
Feb 26 05:37:10 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1705.87+2450264
Feb 26 05:37:10 Starting+compiler/proofs
Feb 26 05:42:28 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++318.50+3261984
Feb 26 05:42:29 Starting+candle/set-theory
Feb 26 05:43:40 Finished+candle/set-theory+++++++++++++++++++++++++++++++++71.53+1010608
Feb 26 05:43:41 Starting+candle/syntax-lib
Feb 26 05:44:08 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++27.63+870908
Feb 26 05:44:09 Starting+candle/standard/syntax
Feb 26 05:48:39 Finished+candle/standard/syntax++++++++++++++++++++++++++++270.40+1262484
Feb 26 05:48:39 Starting+candle/standard/semantics
Feb 26 05:52:43 Finished+candle/standard/semantics+++++++++++++++++++++++++243.45+1046736
Feb 26 05:52:43 Starting+candle/standard/monadic
Feb 26 05:56:45 Finished+candle/standard/monadic+++++++++++++++++++++++++++241.75+1828896
Feb 26 05:56:46 Starting+candle/standard/ml_kernel
Feb 26 06:09:23 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++757.41+3712388
Feb 26 06:09:23 Starting+candle/overloading/syntax
Feb 26 06:16:13 Finished+candle/overloading/syntax+++++++++++++++++++++++++409.52+1221812
Feb 26 06:16:13 Starting+candle/overloading/semantics
Feb 26 06:42:22 Finished+candle/overloading/semantics++++++++++++++++++++++1567.96+2256044
Feb 26 06:42:22 Starting+candle/overloading/monadic
Feb 26 06:47:54 Finished+candle/overloading/monadic++++++++++++++++++++++++331.48+1937268
Feb 26 06:47:54 Starting+candle/overloading/ml_kernel
Feb 26 07:02:49 Finished+candle/overloading/ml_kernel++++++++++++++++++++++894.62+3233020
Feb 26 07:02:49 Starting+candle/overloading/ml_checker
Feb 26 07:08:10 Finished+candle/overloading/ml_checker+++++++++++++++++++++320.58+3506088
Feb 26 07:08:10 Starting+candle/prover
Feb 26 07:24:32 Finished+candle/prover+++++++++++++++++++++++++++++++++++++981.58+2877848
Feb 26 07:24:32 Starting+pancake
Feb 26 07:30:00 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++328.16+1931980
Feb 26 07:30:00 Starting+pancake/ffi
Feb 26 07:30:01 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.76+29764
Feb 26 07:30:02 Starting+pancake/semantics
Feb 26 07:35:28 Finished+pancake/semantics+++++++++++++++++++++++++++++++++326.22+1115908
Feb 26 07:35:28 Starting+pancake/proofs
Feb 26 08:01:29 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1558.48+6368240
Feb 26 08:01:29 Starting+characteristic/examples
Feb 26 08:04:42 Finished+characteristic/examples+++++++++++++++++++++++++++192.63+2866496
Feb 26 08:04:42 Starting+tutorial/solutions
Feb 26 08:41:13 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2191.25+9588132
Feb 26 08:41:13 Starting+translator/monadic/examples
Feb 26 08:48:07 Finished+translator/monadic/examples+++++++++++++++++++++++413.71+3444568
Feb 26 08:48:08 Starting+examples
Feb 26 08:52:08 FAILED:+examples
Scanning [1m$(HOLDIR)/src/sort[0m
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)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[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)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[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
Scanned 30 directories
Starting work on source_valuesTheory
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
README.md                                                                                                                                                                                   examples  (0s)     OK
Starting work on catProgTheory
source_valuesTheory                                                                                                                                                               examples/bootstrap  (4s)     OK
Starting work on source_syntaxTheory
source_syntaxTheory                                                                                                                                                               examples/bootstrap  (1s)     OK
Starting work on parsingTheory
regexp_parserTheory                                                                                                                                                examples/formal-languages/regular (25s)     OK
Starting work on printingTheory
printingTheory                                                                                                                                                                    examples/bootstrap  (8s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]                                                                                                                                     (25.235s) 
Starting work on lcsTheory
parsingTheory                                                                                                                                                                     examples/bootstrap (39s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                                                                                                                                                    (53.682s) 
Starting work on divTheory
lcsTheory                                                                                                                                                                                   examples (31s)     OK
Starting work on diffTheory
diffTheory                                                                                                                                                                                  examples (88s)     OK
Starting work on diffProgTheory
catProgTheory                                                                                                                                                                               examples(166s)     OK
Starting work on doubleProgTheory
quicksortProgTheory                                                                                                                                                                         examples(212s)     OK
Starting work on array_searchProgTheory
divTheory                                                                                                                                                                                   examples(181s)FAIL<1>
 
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn:
 between line 321, character 2 and line 322, character 59:
 at Defn.parse_quote:
 at boolSyntax.dest_eq(_ty):
 not an "="
 error in quse /root/regression/cakeml-1801/examples/divScript.sml : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 321, character 2 and line 322, character 59:\nat Defn.parse_quote:\nat boolSyntax.dest_eq(_ty):\nnot an \"=\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 error in load /root/regression/cakeml-1801/examples/divScript : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 321, character 2 and line 322, character 59:\nat Defn.parse_quote:\nat boolSyntax.dest_eq(_ty):\nnot an \"=\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 321, character 2 and line 322, character 59:\nat Defn.parse_quote:\nat boolSyntax.dest_eq(_ty):\nnot an \"=\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
diffProgTheory                                                                                                                                                                              examples (69s)MKILLED
doubleProgTheory                                                                                                                                                                            examples (56s)MKILLED
array_searchProgTheory                                                                                                                                                                      examples (14s)MKILLED