OverviewCakeML:cf744e4847dd4efe45d686907646cd5cbce61c03
Update candle_boot.ml
#863 (repl)
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:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 2s 103MB
Starting developers/bin
Finished developers/bin 1m01s 675MB
Starting semantics/ffi
Finished semantics/ffi 9s 309MB
Starting semantics
Finished semantics 2m12s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m36s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 15s 519MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m22s 1GB
Starting basis/pure
Finished basis/pure 3m01s 1GB
Starting translator
Finished translator 2m59s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m17s 2GB
Starting characteristic
Finished characteristic 6m45s 3GB
Starting translator/monadic
Finished translator/monadic 2m34s 3GB
Starting basis
Finished basis 52m48s 38GB
Starting compiler/inference
Finished compiler/inference 1m28s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m46s 2GB
Starting compiler/backend/gc
Finished compiler/backend/gc 4m58s 2GB
Starting compiler/backend
Finished compiler/backend 6m57s 4GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 31s 1GB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m15s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 2m13s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 44s 1GB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 2h03m41s 35GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m30s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m46s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 22s 1GB
Starting compiler/backend/x64
Finished compiler/backend/x64 21s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 23s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 22s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 22s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 23s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m22s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 2m38s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m27s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 27m10s 5GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m17s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 49m32s 15GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 1m32s 2GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m16s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m49s 7GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m36s 3GB
Starting compiler/encoders/arm8_asl/proofs
Finished compiler/encoders/arm8_asl/proofs 49m10s 11GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m55s 7GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m30s 4GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m20s 1GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 27s 2GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 27s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 27s 1GB
Starting compiler/backend/arm8_asl
Finished compiler/backend/arm8_asl 21s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 26s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 28s 2GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 12m01s 3GB
Starting compiler/proofs
Finished compiler/proofs 2m24s 5GB
Starting candle/set-theory
Finished candle/set-theory 35s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 13s 896MB
Starting candle/standard/syntax
Finished candle/standard/syntax 2m02s 2GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m49s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m48s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m51s 5GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m10s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 10m40s 4GB
Starting candle/overloading/monadic
Finished candle/overloading/monadic 2m24s 2GB
Starting candle/overloading/ml_kernel
Finished candle/overloading/ml_kernel 6m43s 4GB
Starting candle/overloading/ml_checker
Finished candle/overloading/ml_checker 2m18s 5GB
Starting candle/prover
Finished candle/prover 7m28s 4GB
Starting pancake
Finished pancake 2m47s 3GB
Starting pancake/ffi
Finished pancake/ffi 0s 35MB
Starting pancake/semantics
Finished pancake/semantics 2m25s 1GB
Starting pancake/proofs
Finished pancake/proofs 11m15s 5GB
Starting characteristic/examples
Finished characteristic/examples 1m23s 4GB
Starting tutorial/solutions
Finished tutorial/solutions 18m24s 18GB
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)/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
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 (45s) OK
Starting work on exceptionProgTheory
array_searchProgTheory (49s) OK
Starting work on exception_arity_testProgTheory
array_global_stateProgTheory (65s) OK
Starting work on fibProgTheory
array_local_stateProgTheory (84s) OK
Starting work on floyd_warshallProgTheory
exceptionProgTheory (43s) OK
Starting work on helloProgTheory
exception_arity_testProgTheory (48s) OK
Starting work on poly_array_sortProgTheory
fibProgTheory (68s) OK
Starting work on ref_stateProgTheory
floyd_warshallProgTheory (61s) OK
Starting work on runProgTheory
helloProgTheory (78s) OK
Starting work on test_assumProgTheory
ref_stateProgTheory (53s) OK
Starting work on test_precondProgTheory
runProgTheory (80s) OK
Starting work on test_runTheory
poly_array_sortProgTheory (133s) OK
test_assumProgTheory (73s)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.>>
Failed translation: ZIP
error in quse /home/myreen/regression/cakeml-1806/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 /home/myreen/regression/cakeml-1806/translator/monadic/examples/test_assumProgScript : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
Uncaught exception: HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
test_precondProgTheory (58s)MKILLED
test_runTheory (16s)MKILLED