OverviewCakeML:14d1ade7e9e38783dddcb1731990c8cca3fb4d4c
Remove extra-files from semantics
#831 (pancake)
Merging into:76ed0b05089a77059dee72d197fc56c3dae661e8
Merge pull request #829 from CakeML/help
HOL:ce49c6542adf54f809665caba71e33707dcddda8
Prove little lemma about being a subset of a singleton
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 0s 35MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 9s 267MB
Starting semantics
Finished semantics 1m35s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m31s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 8s 419MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m12s 1GB
Starting basis/pure
Finished basis/pure 2m44s 1GB
Starting translator
Finished translator 3m15s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m07s 4GB
Starting characteristic
Finished characteristic 5m43s 3GB
Starting translator/monadic
Finished translator/monadic 1m47s 3GB
Starting basis
Finished basis 44m29s 26GB
Starting compiler/inference
Finished compiler/inference 1m12s 2GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m07s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m38s 3GB
Starting compiler/backend
Finished compiler/backend 5m05s 4GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 23s 1GB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m04s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 2m03s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 39s 1GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m25s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m40s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 18s 945MB
Starting compiler/backend/x64
Finished compiler/backend/x64 19s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 22s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 20s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 20s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 21s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m10s 2GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m48s 2GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m33s 2GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 26m59s 3GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m17s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 53m34s 20GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m23s 6GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m43s 6GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m29s 3GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m45s 5GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m10s 4GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m19s 1GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 22s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 23s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 21s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 21s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 24s 2GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 12m10s 5GB
Starting compiler/proofs
Finished compiler/proofs 2m01s 6GB
Starting candle/set-theory
Finished candle/set-theory 30s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 11s 813MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m52s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m47s 2GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m42s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m34s 5GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m12s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 12m07s 8GB
Starting pancake
FAILED: pancake
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)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Starting work on crepLangTheory
Starting work on loopLangTheory
Starting work on panLangTheory
Starting work on pan_commonTheory
pan_commonTheory real: 9s user: 9s OK
Starting work on timeLangTheory
loopLangTheory real: 13s user: 13s OK
Starting work on loop_callTheory
panLangTheory real: 15s user: 15s OK
Starting work on loop_removeTheory
crepLangTheory real: 16s user: 15s OK
Starting work on pan_simpTheory
timeLangTheory real: 11s user: 10s OK
Starting work on pan_to_crepTheory
loop_callTheory real: 11s user: 10s OK
Starting work on loop_liveTheory
loop_removeTheory real: 12s user: 11s OK
Starting work on loop_to_wordTheory
pan_simpTheory real: 13s user: 12s OK
Starting work on taParserTheory
pan_to_crepTheory real: 14s user: 13s OK
Starting work on time_to_panTheory
loop_liveTheory real: 12s user: 11s OK
Starting work on crep_to_loopTheory
taParserTheory real: 9s user: 8sFAIL<1>
<<HOL message: Created theory "taParser">>
Exception raised at TotalDefn.Define:
roughly in frag 0, between row 0 col 1 and row 12 col 5:
at Defn.prim_mk_defn:
Free variables (CVar) on RHS of nullary definition
error in quse /home/myreen/regression/cakeml-1554/pancake/taParserScript.sml : HOL_ERR {message = "roughly in frag 0, between row 0 col 1 and row 12 col 5:\nat Defn.prim_mk_defn:\nFree variables (CVar) on RHS of nullary definition", origin_function = "Define", origin_structure = "TotalDefn"}
error in load /home/myreen/regression/cakeml-1554/pancake/taParserScript : HOL_ERR {message = "roughly in frag 0, between row 0 col 1 and row 12 col 5:\nat Defn.prim_mk_defn:\nFree variables (CVar) on RHS of nullary definition", origin_function = "Define", origin_structure = "TotalDefn"}
Uncaught exception: HOL_ERR {message = "roughly in frag 0, between row 0 col 1 and row 12 col 5:\nat Defn.prim_mk_defn:\nFree variables (CVar) on RHS of nullary definition", origin_function = "Define", origin_structure = "TotalDefn"}
loop_to_wordTheory M-KILLED
time_to_panTheory M-KILLED
crep_to_loopTheory M-KILLED
Don't know how to build necessary target(s): /home/myreen/regression/cakeml-1554/pancake/ta_progs/readmePrefix