OverviewCakeML:f99af5a3ce396207686cb57a9c71820469fbc64c
fix the broken proofs
#861 (pan-to-mc_updated)
Merging into:f18f45a1f5d90a31c62adc297d68971f6e948c43
Fix following change in Define in HOL
HOL:707434f48dcd4d8f5d06ccae4cdc957b3fc7b4bd
Tweak one_line_ify for case structures not quite aligning with eqns
Machine:oven3+4.19.67.1.amd64-smp+
Claimed job
Building+HOL
Starting+developers
Finished+developers++++++++++++++++++++++++++++++++++++++++8.06+159500
Starting+developers/bin
Finished+developers/bin++++++++++++++++++++++++++++++++++++9.88+677344
Starting+semantics/ffi
Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++25.89+256352
Starting+semantics
Finished+semantics+++++++++++++++++++++++++++++++++++++++++270.18+1119532
Starting+semantics/proofs
Finished+semantics/proofs++++++++++++++++++++++++++++++++++482.15+1759212
Starting+semantics/alt_semantics
Finished+semantics/alt_semantics+++++++++++++++++++++++++++37.18+498820
Starting+semantics/alt_semantics/proofs
Finished+semantics/alt_semantics/proofs++++++++++++++++++++324.16+1014068
Starting+basis/pure
Finished+basis/pure++++++++++++++++++++++++++++++++++++++++361.46+1097100
Starting+translator
Finished+translator++++++++++++++++++++++++++++++++++++++++378.00+1671380
Starting+compiler/parsing
Finished+compiler/parsing++++++++++++++++++++++++++++++++++167.38+2781416
Starting+characteristic
Finished+characteristic++++++++++++++++++++++++++++++++++++794.40+2065700
Starting+translator/monadic
Finished+translator/monadic++++++++++++++++++++++++++++++++240.95+1534296
Starting+basis
Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6175.02+19019696
Starting+compiler/inference
Finished+compiler/inference++++++++++++++++++++++++++++++++187.66+1279544
Starting+compiler/backend/reg_alloc
Finished+compiler/backend/reg_alloc++++++++++++++++++++++++192.39+1822668
Starting+compiler/backend/gc
Finished+compiler/backend/gc+++++++++++++++++++++++++++++++502.65+2082976
Starting+compiler/backend
Finished+compiler/backend++++++++++++++++++++++++++++++++++626.67+2207148
Starting+compiler/encoders/asm
Finished+compiler/encoders/asm+++++++++++++++++++++++++++++64.35+805884
Starting+compiler/encoders/x64
Finished+compiler/encoders/x64+++++++++++++++++++++++++++++154.99+1157156
Starting+compiler/encoders/arm7
Finished+compiler/encoders/arm7++++++++++++++++++++++++++++285.06+1647024
Starting+compiler/encoders/arm8
Finished+compiler/encoders/arm8++++++++++++++++++++++++++++93.65+649968
Starting+compiler/encoders/arm8_asl
Finished+compiler/encoders/arm8_asl++++++++++++++++++++++++14774.14+27169864
Starting+compiler/encoders/mips
Finished+compiler/encoders/mips++++++++++++++++++++++++++++199.54+1280172
Starting+compiler/encoders/riscv
Finished+compiler/encoders/riscv+++++++++++++++++++++++++++232.15+1135136
Starting+compiler/encoders/ag32
Finished+compiler/encoders/ag32++++++++++++++++++++++++++++47.14+890796
Starting+compiler/backend/x64
Finished+compiler/backend/x64++++++++++++++++++++++++++++++47.61+1419416
Starting+compiler/backend/arm7
Finished+compiler/backend/arm7+++++++++++++++++++++++++++++53.23+1543704
Starting+compiler/backend/arm8
Finished+compiler/backend/arm8+++++++++++++++++++++++++++++50.97+1391572
Starting+compiler/backend/mips
Finished+compiler/backend/mips+++++++++++++++++++++++++++++49.63+1597488
Starting+compiler/backend/riscv
Finished+compiler/backend/riscv++++++++++++++++++++++++++++49.81+1542312
Starting+compiler/backend/ag32
Finished+compiler/backend/ag32+++++++++++++++++++++++++++++177.78+1440932
Starting+compiler/parsing/proofs
Finished+compiler/parsing/proofs+++++++++++++++++++++++++++511.51+1259760
Starting+compiler/inference/proofs
Finished+compiler/inference/proofs+++++++++++++++++++++++++332.51+1071768
Starting+compiler/backend/semantics
Finished+compiler/backend/semantics++++++++++++++++++++++++3744.00+2679536
Starting+compiler/backend/reg_alloc/proofs
Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++474.48+876720
Starting+compiler/backend/proofs
Finished+compiler/backend/proofs+++++++++++++++++++++++++++6193.68+13053052
Starting+compiler/backend/serialiser
Finished+compiler/backend/serialiser+++++++++++++++++++++++204.67+2255384
Starting+compiler/encoders/x64/proofs
Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1299.44+5993628
Starting+compiler/encoders/arm7/proofs
Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1810.29+3661544
Starting+compiler/encoders/arm8/proofs
Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++929.13+1261268
Starting+compiler/encoders/arm8_asl/proofs
Finished+compiler/encoders/arm8_asl/proofs+++++++++++++++++6800.53+5500880
Starting+compiler/encoders/mips/proofs
Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1346.28+2920948
Starting+compiler/encoders/riscv/proofs
Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1198.83+1353288
Starting+compiler/encoders/ag32/proofs
Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++344.64+857196
Starting+compiler/backend/x64/proofs
Finished+compiler/backend/x64/proofs+++++++++++++++++++++++58.84+1336556
Starting+compiler/backend/arm7/proofs
Finished+compiler/backend/arm7/proofs++++++++++++++++++++++62.35+1888968
Starting+compiler/backend/arm8/proofs
Finished+compiler/backend/arm8/proofs++++++++++++++++++++++60.36+1618792
Starting+compiler/backend/arm8_asl
Finished+compiler/backend/arm8_asl+++++++++++++++++++++++++49.72+1646156
Starting+compiler/backend/mips/proofs
Finished+compiler/backend/mips/proofs++++++++++++++++++++++59.90+1694128
Starting+compiler/backend/riscv/proofs
Finished+compiler/backend/riscv/proofs+++++++++++++++++++++59.48+1394900
Starting+compiler/backend/ag32/proofs
Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1761.84+2984560
Starting+compiler/proofs
Finished+compiler/proofs+++++++++++++++++++++++++++++++++++313.32+3483424
Starting+candle/set-theory
Finished+candle/set-theory+++++++++++++++++++++++++++++++++69.68+1098580
Starting+candle/syntax-lib
Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++28.81+627264
Starting+candle/standard/syntax
Finished+candle/standard/syntax++++++++++++++++++++++++++++258.23+1068560
Starting+candle/standard/semantics
Finished+candle/standard/semantics+++++++++++++++++++++++++241.24+1173776
Starting+candle/standard/monadic
Finished+candle/standard/monadic+++++++++++++++++++++++++++235.77+1586904
Starting+candle/standard/ml_kernel
Finished+candle/standard/ml_kernel+++++++++++++++++++++++++783.24+3331364
Starting+candle/overloading/syntax
Finished+candle/overloading/syntax+++++++++++++++++++++++++414.44+1478688
Starting+candle/overloading/semantics
Finished+candle/overloading/semantics++++++++++++++++++++++1569.38+2524384
Starting+candle/overloading/monadic
Finished+candle/overloading/monadic++++++++++++++++++++++++322.88+1631616
Starting+candle/overloading/ml_kernel
Finished+candle/overloading/ml_kernel++++++++++++++++++++++901.52+3351948
Starting+candle/overloading/ml_checker
Finished+candle/overloading/ml_checker+++++++++++++++++++++316.88+3369172
Starting+candle/prover
Finished+candle/prover+++++++++++++++++++++++++++++++++++++995.72+2621064
Starting+pancake
Finished+pancake+++++++++++++++++++++++++++++++++++++++++++464.10+3871072
Starting+pancake/ffi
Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.77+30568
Starting+pancake/semantics
Finished+pancake/semantics+++++++++++++++++++++++++++++++++310.42+1157760
Starting+pancake/proofs
Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1593.45+5421396
Starting+characteristic/examples
Finished+characteristic/examples+++++++++++++++++++++++++++177.31+2921220
Starting+tutorial/solutions
Finished+tutorial/solutions++++++++++++++++++++++++++++++++2185.35+10239764
Starting+translator/monadic/examples
FAILED:+translator/monadic/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)/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$(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 29 directories
Starting work on README.md
Starting work on array_global_stateProgTheory
Starting work on array_local_stateProgTheory
Starting work on array_searchProgTheory
README.md (0s) OK
Starting work on doubleProgTheory
doubleProgTheory (60s) OK
Starting work on exceptionProgTheory
array_searchProgTheory (65s) OK
Starting work on exception_arity_testProgTheory
array_global_stateProgTheory (88s) OK
Starting work on fibProgTheory
array_local_stateProgTheory (117s) OK
Starting work on floyd_warshallProgTheory
exceptionProgTheory (58s) OK
Starting work on helloProgTheory
exception_arity_testProgTheory (66s) OK
Starting work on poly_array_sortProgTheory
fibProgTheory (99s) OK
Starting work on ref_stateProgTheory
floyd_warshallProgTheory (83s) OK
Starting work on runProgTheory
helloProgTheory (104s) OK
Starting work on test_assumProgTheory
ref_stateProgTheory (62s) OK
Starting work on test_precondProgTheory
runProgTheory (82s) OK
Starting work on test_runTheory
test_assumProgTheory (75s)FAIL<1>
Saved theorem _______ "nsLookup_test_assumProg_env_13_pfun_eqs"
Adding nsLookup representation thms for [test_assumProg_env_12]
Adding nsLookup representation thms for [test_assumProg_env_13]
Saved theorem _______ "length_v_thm"
<<HOL message: mk_functional:
pattern completion has added 1 clause to the original specification.>>
error in quse /root/regression/cakeml-1805/translator/monadic/examples/test_assumProgScript.sml : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
error in load /root/regression/cakeml-1805/translator/monadic/examples/test_assumProgScript : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
Failed translation: ZIP
Uncaught exception: HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
poly_array_sortProgTheory (170s)MKILLED
test_precondProgTheory (50s)MKILLED
test_runTheory (20s)MKILLED