Overview

Job 1711

CakeML:7625014b02cfc85842255146d0497020af0ce1d7
  Make pp code compatible with candle basis reqs
#856 (printing)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
  Merge pull request #852 from CakeML/tidy-up
HOL:6b1dbc7559064a70fabbe71836947411103b499e
  Fix INCLUDES for src/coalgebras
Machine:oven3+4.19.67.1.amd64-smp+

 Claimed job
 Reusing+HOL
 Starting+developers
 Finished+developers++++++++++++++++++++++++++++++++++++++++7.70+160832
 Starting+developers/bin
 Finished+developers/bin++++++++++++++++++++++++++++++++++++10.35+681748
 Starting+semantics/ffi
 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++19.68+254200
 Starting+semantics
 Finished+semantics+++++++++++++++++++++++++++++++++++++++++169.50+1106144
 Starting+semantics/proofs
 Finished+semantics/proofs++++++++++++++++++++++++++++++++++478.16+1036200
 Starting+semantics/alt_semantics
 Finished+semantics/alt_semantics+++++++++++++++++++++++++++25.29+394876
 Starting+semantics/alt_semantics/proofs
 Finished+semantics/alt_semantics/proofs++++++++++++++++++++311.40+1140144
 Starting+basis/pure
 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++110.14+874100
 Starting+translator
 Finished+translator++++++++++++++++++++++++++++++++++++++++348.33+1518688
 Starting+compiler/parsing
 Finished+compiler/parsing++++++++++++++++++++++++++++++++++159.74+3190392
 Starting+characteristic
 Finished+characteristic++++++++++++++++++++++++++++++++++++724.72+1800204
 Starting+translator/monadic
 Finished+translator/monadic++++++++++++++++++++++++++++++++208.20+1613880
 Starting+basis
 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6075.21+15378316
 Starting+compiler/inference
 Finished+compiler/inference++++++++++++++++++++++++++++++++143.53+1003892
 Starting+compiler/backend/reg_alloc
 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++124.54+1316236
 Starting+compiler/backend/gc
 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++394.01+2123900
 Starting+compiler/backend
 Finished+compiler/backend++++++++++++++++++++++++++++++++++528.22+2341400
 Starting+compiler/encoders/asm
 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++50.77+740420
 Starting+compiler/encoders/x64
 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++54.79+981876
 Starting+compiler/encoders/arm7
 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++116.73+696180
 Starting+compiler/encoders/arm8
 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++28.87+575068
 Starting+compiler/encoders/mips
 Finished+compiler/encoders/mips++++++++++++++++++++++++++++37.59+1267952
 Starting+compiler/encoders/riscv
 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++32.21+974436
 Starting+compiler/encoders/ag32
 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++38.71+635328
 Starting+compiler/backend/x64
 Finished+compiler/backend/x64++++++++++++++++++++++++++++++42.40+1307664
 Starting+compiler/backend/arm7
 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++49.41+1333436
 Starting+compiler/backend/arm8
 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++41.12+1494376
 Starting+compiler/backend/mips
 Finished+compiler/backend/mips+++++++++++++++++++++++++++++43.62+1474240
 Starting+compiler/backend/riscv
 Finished+compiler/backend/riscv++++++++++++++++++++++++++++44.04+1139312
 Starting+compiler/backend/ag32
 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++145.75+1479120
 Starting+compiler/parsing/proofs
 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++506.38+1243724
 Starting+compiler/inference/proofs
 Finished+compiler/inference/proofs+++++++++++++++++++++++++320.63+1075328
 Starting+compiler/backend/semantics
 Finished+compiler/backend/semantics++++++++++++++++++++++++3719.17+2118456
 Starting+compiler/backend/reg_alloc/proofs
 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++441.01+925700
 Starting+compiler/backend/proofs
 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6075.12+15721400
 Starting+compiler/backend/serialiser
 Finished+compiler/backend/serialiser+++++++++++++++++++++++151.11+1613964
 Starting+compiler/encoders/x64/proofs
 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1273.14+4942224
 Starting+compiler/encoders/arm7/proofs
 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1761.97+3750240
 Starting+compiler/encoders/arm8/proofs
 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++931.88+1681392
 Starting+compiler/encoders/mips/proofs
 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1367.35+3104072
 Starting+compiler/encoders/riscv/proofs
 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1230.74+1168596
 Starting+compiler/encoders/ag32/proofs
 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++335.87+849088
 Starting+compiler/backend/x64/proofs
 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++48.98+1364956
 Starting+compiler/backend/arm7/proofs
 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++54.05+1714776
 Starting+compiler/backend/arm8/proofs
 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++52.31+1652572
 Starting+compiler/backend/mips/proofs
 Finished+compiler/backend/mips/proofs++++++++++++++++++++++52.20+1595772
 Starting+compiler/backend/riscv/proofs
 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++49.70+1651176
 Starting+compiler/backend/ag32/proofs
 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1749.18+2366384
 Starting+compiler/proofs
 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++220.64+3228956
 Starting+candle/set-theory
 Finished+candle/set-theory+++++++++++++++++++++++++++++++++58.60+795900
 Starting+candle/syntax-lib
 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++24.18+657196
 Starting+candle/standard/syntax
 Finished+candle/standard/syntax++++++++++++++++++++++++++++229.28+1350012
 Starting+candle/standard/semantics
 Finished+candle/standard/semantics+++++++++++++++++++++++++223.90+1357336
 Starting+candle/standard/monadic
 Finished+candle/standard/monadic+++++++++++++++++++++++++++203.71+1395368
 Starting+candle/standard/ml_kernel
 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++858.86+3847956
 Starting+candle/overloading/syntax
 Finished+candle/overloading/syntax+++++++++++++++++++++++++393.64+1125476
 Starting+candle/overloading/semantics
 Finished+candle/overloading/semantics++++++++++++++++++++++1499.97+2859992
 Starting+candle/prover
 Finished+candle/prover+++++++++++++++++++++++++++++++++++++979.98+4928432
 Starting+pancake
 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"