CakeML Regression Test

Job 1711

CakeML:7625014b02cfc85842255146d0497020af0ce1d7
  Make pp code compatible with candle basis reqs [Jan 14 07:26:23]
#856 (printing)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
  Merge pull request #852 from CakeML/tidy-up [Jan 05 17:40:32]
HOL:6b1dbc7559064a70fabbe71836947411103b499e
  Fix INCLUDES for src/coalgebras [Jan 07 05:56:33]
Machine:oven3+4.19.67.1.amd64-smp+

Jan 14 08:18:05 Claimed job
Jan 14 08:18:12 Reusing+HOL
Jan 14 08:19:04 Starting+developers
Jan 14 08:19:12 Finished+developers++++++++++++++++++++++++++++++++++++++++7.70+160832
Jan 14 08:19:12 Starting+developers/bin
Jan 14 08:19:23 Finished+developers/bin++++++++++++++++++++++++++++++++++++10.35+681748
Jan 14 08:19:23 Starting+semantics/ffi
Jan 14 08:19:43 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++19.68+254200
Jan 14 08:19:43 Starting+semantics
Jan 14 08:22:33 Finished+semantics+++++++++++++++++++++++++++++++++++++++++169.50+1106144
Jan 14 08:22:33 Starting+semantics/proofs
Jan 14 08:30:31 Finished+semantics/proofs++++++++++++++++++++++++++++++++++478.16+1036200
Jan 14 08:30:32 Starting+semantics/alt_semantics
Jan 14 08:30:57 Finished+semantics/alt_semantics+++++++++++++++++++++++++++25.29+394876
Jan 14 08:30:57 Starting+semantics/alt_semantics/proofs
Jan 14 08:36:09 Finished+semantics/alt_semantics/proofs++++++++++++++++++++311.40+1140144
Jan 14 08:36:09 Starting+basis/pure
Jan 14 08:38:00 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++110.14+874100
Jan 14 08:38:00 Starting+translator
Jan 14 08:43:48 Finished+translator++++++++++++++++++++++++++++++++++++++++348.33+1518688
Jan 14 08:43:48 Starting+compiler/parsing
Jan 14 08:46:28 Finished+compiler/parsing++++++++++++++++++++++++++++++++++159.74+3190392
Jan 14 08:46:29 Starting+characteristic
Jan 14 08:58:34 Finished+characteristic++++++++++++++++++++++++++++++++++++724.72+1800204
Jan 14 08:58:34 Starting+translator/monadic
Jan 14 09:02:02 Finished+translator/monadic++++++++++++++++++++++++++++++++208.20+1613880
Jan 14 09:02:03 Starting+basis
Jan 14 10:43:18 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6075.21+15378316
Jan 14 10:43:18 Starting+compiler/inference
Jan 14 10:45:42 Finished+compiler/inference++++++++++++++++++++++++++++++++143.53+1003892
Jan 14 10:45:42 Starting+compiler/backend/reg_alloc
Jan 14 10:47:47 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++124.54+1316236
Jan 14 10:47:47 Starting+compiler/backend/gc
Jan 14 10:54:21 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++394.01+2123900
Jan 14 10:54:22 Starting+compiler/backend
Jan 14 11:03:10 Finished+compiler/backend++++++++++++++++++++++++++++++++++528.22+2341400
Jan 14 11:03:10 Starting+compiler/encoders/asm
Jan 14 11:04:01 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++50.77+740420
Jan 14 11:04:01 Starting+compiler/encoders/x64
Jan 14 11:04:56 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++54.79+981876
Jan 14 11:04:57 Starting+compiler/encoders/arm7
Jan 14 11:06:54 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++116.73+696180
Jan 14 11:06:54 Starting+compiler/encoders/arm8
Jan 14 11:07:23 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++28.87+575068
Jan 14 11:07:23 Starting+compiler/encoders/mips
Jan 14 11:08:01 Finished+compiler/encoders/mips++++++++++++++++++++++++++++37.59+1267952
Jan 14 11:08:01 Starting+compiler/encoders/riscv
Jan 14 11:08:34 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++32.21+974436
Jan 14 11:08:34 Starting+compiler/encoders/ag32
Jan 14 11:09:13 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++38.71+635328
Jan 14 11:09:13 Starting+compiler/backend/x64
Jan 14 11:09:55 Finished+compiler/backend/x64++++++++++++++++++++++++++++++42.40+1307664
Jan 14 11:09:56 Starting+compiler/backend/arm7
Jan 14 11:10:45 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++49.41+1333436
Jan 14 11:10:45 Starting+compiler/backend/arm8
Jan 14 11:11:27 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++41.12+1494376
Jan 14 11:11:27 Starting+compiler/backend/mips
Jan 14 11:12:11 Finished+compiler/backend/mips+++++++++++++++++++++++++++++43.62+1474240
Jan 14 11:12:11 Starting+compiler/backend/riscv
Jan 14 11:12:55 Finished+compiler/backend/riscv++++++++++++++++++++++++++++44.04+1139312
Jan 14 11:12:56 Starting+compiler/backend/ag32
Jan 14 11:15:21 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++145.75+1479120
Jan 14 11:15:22 Starting+compiler/parsing/proofs
Jan 14 11:23:48 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++506.38+1243724
Jan 14 11:23:48 Starting+compiler/inference/proofs
Jan 14 11:29:09 Finished+compiler/inference/proofs+++++++++++++++++++++++++320.63+1075328
Jan 14 11:29:10 Starting+compiler/backend/semantics
Jan 14 12:31:09 Finished+compiler/backend/semantics++++++++++++++++++++++++3719.17+2118456
Jan 14 12:31:09 Starting+compiler/backend/reg_alloc/proofs
Jan 14 12:38:31 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++441.01+925700
Jan 14 12:38:31 Starting+compiler/backend/proofs
Jan 14 14:19:46 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6075.12+15721400
Jan 14 14:19:46 Starting+compiler/backend/serialiser
Jan 14 14:22:18 Finished+compiler/backend/serialiser+++++++++++++++++++++++151.11+1613964
Jan 14 14:22:18 Starting+compiler/encoders/x64/proofs
Jan 14 14:43:31 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1273.14+4942224
Jan 14 14:43:31 Starting+compiler/encoders/arm7/proofs
Jan 14 15:12:53 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1761.97+3750240
Jan 14 15:12:54 Starting+compiler/encoders/arm8/proofs
Jan 14 15:28:26 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++931.88+1681392
Jan 14 15:28:26 Starting+compiler/encoders/mips/proofs
Jan 14 15:51:14 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1367.35+3104072
Jan 14 15:51:14 Starting+compiler/encoders/riscv/proofs
Jan 14 16:11:45 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1230.74+1168596
Jan 14 16:11:45 Starting+compiler/encoders/ag32/proofs
Jan 14 16:17:21 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++335.87+849088
Jan 14 16:17:21 Starting+compiler/backend/x64/proofs
Jan 14 16:18:11 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++48.98+1364956
Jan 14 16:18:11 Starting+compiler/backend/arm7/proofs
Jan 14 16:19:05 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++54.05+1714776
Jan 14 16:19:05 Starting+compiler/backend/arm8/proofs
Jan 14 16:19:58 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++52.31+1652572
Jan 14 16:19:58 Starting+compiler/backend/mips/proofs
Jan 14 16:20:50 Finished+compiler/backend/mips/proofs++++++++++++++++++++++52.20+1595772
Jan 14 16:20:51 Starting+compiler/backend/riscv/proofs
Jan 14 16:21:41 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++49.70+1651176
Jan 14 16:21:41 Starting+compiler/backend/ag32/proofs
Jan 14 16:50:50 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1749.18+2366384
Jan 14 16:50:51 Starting+compiler/proofs
Jan 14 16:54:31 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++220.64+3228956
Jan 14 16:54:32 Starting+candle/set-theory
Jan 14 16:55:30 Finished+candle/set-theory+++++++++++++++++++++++++++++++++58.60+795900
Jan 14 16:55:31 Starting+candle/syntax-lib
Jan 14 16:55:55 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++24.18+657196
Jan 14 16:55:55 Starting+candle/standard/syntax
Jan 14 16:59:45 Finished+candle/standard/syntax++++++++++++++++++++++++++++229.28+1350012
Jan 14 16:59:45 Starting+candle/standard/semantics
Jan 14 17:03:29 Finished+candle/standard/semantics+++++++++++++++++++++++++223.90+1357336
Jan 14 17:03:29 Starting+candle/standard/monadic
Jan 14 17:06:53 Finished+candle/standard/monadic+++++++++++++++++++++++++++203.71+1395368
Jan 14 17:06:53 Starting+candle/standard/ml_kernel
Jan 14 17:21:12 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++858.86+3847956
Jan 14 17:21:12 Starting+candle/overloading/syntax
Jan 14 17:27:46 Finished+candle/overloading/syntax+++++++++++++++++++++++++393.64+1125476
Jan 14 17:27:46 Starting+candle/overloading/semantics
Jan 14 17:52:47 Finished+candle/overloading/semantics++++++++++++++++++++++1499.97+2859992
Jan 14 17:52:47 Starting+candle/prover
Jan 14 18:09:07 Finished+candle/prover+++++++++++++++++++++++++++++++++++++979.98+4928432
Jan 14 18:09:07 Starting+pancake
Jan 14 18:11:58 FAILED:+pancake
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)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[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)/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$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[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$(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$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Finished $(CAKEMLDIR)/compiler                                                                                                                                                                                                      (0.000s) 
Starting work on README.md
Starting work on crepLangTheory
Starting work on loopLangTheory
Starting work on panLangTheory
README.md                                                                                                                                                                                                               pancake  (0s)     OK
Starting work on pan_commonTheory
pan_commonTheory                                                                                                                                                                                                        pancake (16s)     OK
Starting work on timeLangTheory
loopLangTheory                                                                                                                                                                                                          pancake (24s)     OK
Starting work on loop_callTheory
panLangTheory                                                                                                                                                                                                           pancake (25s)     OK
Starting work on loop_removeTheory
crepLangTheory                                                                                                                                                                                                          pancake (26s)     OK
Starting work on pan_simpTheory
timeLangTheory                                                                                                                                                                                                          pancake (16s)     OK
Starting work on pan_to_crepTheory
loop_callTheory                                                                                                                                                                                                         pancake (16s)     OK
Starting work on loop_liveTheory
loop_removeTheory                                                                                                                                                                                                       pancake (18s)     OK
Starting work on loop_to_wordTheory
pan_simpTheory                                                                                                                                                                                                          pancake (18s)     OK
Starting work on taParserTheory
pan_to_crepTheory                                                                                                                                                                                                       pancake (20s)     OK
Starting work on time_to_panTheory
loop_liveTheory                                                                                                                                                                                                         pancake (18s)     OK
Starting work on crep_to_loopTheory
taParserTheory                                                                                                                                                                                                          pancake (14s)     OK
loop_to_wordTheory                                                                                                                                                                                                      pancake (18s)     OK
time_to_panTheory                                                                                                                                                                                                       pancake (25s)     OK
crep_to_loopTheory                                                                                                                                                                                                      pancake (19s)     OK
Starting work on pan_to_wordTheory
pan_to_wordTheory                                                                                                                                                                                                       pancake (16s)     OK
Starting work on pan_to_targetTheory
pan_to_targetTheory                                                                                                                                                                                                     pancake (25s)     OK
Starting work on time_to_targetTheory
time_to_targetTheory                                                                                                                                                                                                    pancake (22s)     OK
Starting work on time_evalTheory
time_evalTheory                                                                                                                                                                                                         pancake  (8s)FAIL<1>
 Found near
   [
      mlstringTheory.implode_def,
      mlstringTheory.str_def,
      mlstringTheory.concat_thm,
      mlstringTheory.explode_thm,
      mloptionTheory.getOpt_def,
      ...
      ]
 Uncaught exception: Fail "Static Errors"