OverviewCakeML:2d85a9fbcf10fb4eb1398f75958ce621218d4c19
Fix alt_semantics missing a case
#911 (libm_gen)
Merging into:59e14a942bb54a58350e86539c1953c541eff3f4
Merge pull request #909 from mktnk3/word_to_word_Pancake
HOL:52406bd0bb1d700af123bb9b3fe55c38be50c11c
Use Zorn's Lemma to show all strong orders can extend to linear ones
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 5s 112MB
Starting developers/bin
Finished developers/bin 5s 1GB
Starting compiler/proofs
Finished compiler/proofs 1h45m18s 23GB
Starting compiler/bootstrap/translation
Finished compiler/bootstrap/translation 4h51m17s 42GB
Starting semantics/ffi
Finished semantics/ffi 4s 142MB
Starting semantics
Finished semantics 1s 18MB
Starting semantics/proofs
Finished semantics/proofs 31s 851MB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 27s 537MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 11m52s 1GB
Starting basis/pure
Finished basis/pure 1s 32MB
Starting translator
Finished translator 1m46s 1GB
Starting compiler/parsing
Finished compiler/parsing 1s 18MB
Starting characteristic
Finished characteristic 1s 23MB
Starting translator/monadic
Finished translator/monadic 1s 35MB
Starting basis
Finished basis 3m26s 2GB
Starting compiler/inference
Finished compiler/inference 1s 23MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1s 32MB
Starting compiler/backend/gc
Finished compiler/backend/gc 2s 27MB
Starting compiler/backend
Finished compiler/backend 10s 554MB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 1s 20MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1s 23MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 1s 32MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 1s 32MB
Starting compiler/encoders/arm8_asl
Finished compiler/encoders/arm8_asl 3m05s 1GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1s 19MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1s 23MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 1s 20MB
Starting compiler/backend/x64
Finished compiler/backend/x64 2s 32MB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 2s 34MB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 2s 35MB
Starting compiler/backend/mips
Finished compiler/backend/mips 2s 34MB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 2s 34MB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m24s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 1s 20MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 1s 34MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 1m06s 1GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 1s 35MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 55s 3GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 2s 41MB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m46s 6GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 14m12s 5GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 7m23s 899MB
Starting compiler/encoders/arm8_asl/proofs
Finished compiler/encoders/arm8_asl/proofs 15m56s 2GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 10m38s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 9m03s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m39s 761MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 26s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 26s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 26s 1GB
Starting compiler/backend/arm8_asl
Finished compiler/backend/arm8_asl 20s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 25s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 26s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 13m42s 2GB
Starting candle/set-theory
Finished candle/set-theory 34s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 1s 33MB
Starting candle/standard/syntax
Finished candle/standard/syntax 8s 456MB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m43s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1s 34MB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 1m27s 2GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m12s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 12m08s 2GB
Starting candle/overloading/monadic
Finished candle/overloading/monadic 2m39s 1GB
Starting candle/overloading/ml_kernel
Finished candle/overloading/ml_kernel 7m26s 3GB
Starting candle/overloading/ml_checker
Finished candle/overloading/ml_checker 2m30s 3GB
Starting candle/prover
FAILED: candle/prover
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/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/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[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
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanning [1m$(CAKEMLDIR)/candle/prover/compute[0m
Scanned 37 directories
Starting work on compute_syntaxProofTheory
Starting work on README.md
Starting work on candle_kernel_permsTheory
README.md candle/prover (0s) OK
compute_syntaxProofTheory candle/prover/compute(106s) OK
Starting work on compute_evalProofTheory
candle_kernel_permsTheory candle/prover(187s) OK
compute_evalProofTheory candle/prover/compute (85s) OK
Starting work on compute_execProofTheory
compute_execProofTheory candle/prover/compute (11s) OK
Starting work on computeProofTheory
computeProofTheory candle/prover/compute (48s) OK
Finished $(CAKEMLDIR)/candle/prover/compute [#theories: 4] (252.881s)
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory candle/prover (79s) OK
Starting work on candle_prover_evaluateTheory
candle_prover_evaluateTheory candle/prover (44s)FAIL<1>
STATE ctxt st1 (loc. loc kernel_locs kernel_loc_ok st1 loc refs1)
(loc r. loc kernel_locs LLOOKUP refs1 loc = SOME r ref_ok ctxt r)
EVERY ok_event ffi1.io_events
case list_result res of
Rval vs => EVERY (v_ok ctxt) vs
| Rerr (Rraise v) => v_ok ctxt v
| Rerr (Rabort v8) => T
Failed to prove theorem do_app_ok.
Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}