OverviewCakeML:14d1ade7e9e38783dddcb1731990c8cca3fb4d4c
Remove extra-files from semantics
#831 (pancake)
Merging into:76ed0b05089a77059dee72d197fc56c3dae661e8
Merge pull request #829 from CakeML/help
HOL:0c88037d251b8041b38bd16fc401fa1336041787
Holmake: make fooTheory target build .uo file not just .dat file
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 0s 34MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 309MB
Starting semantics
Finished semantics 1m27s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m31s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 8s 408MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m12s 2GB
Starting basis/pure
Finished basis/pure 53s 1GB
Starting translator
Finished translator 3m31s 2GB
Starting compiler/parsing
Finished compiler/parsing 1m15s 4GB
Starting characteristic
Finished characteristic 6m02s 4GB
Starting translator/monadic
Finished translator/monadic 1m48s 2GB
Starting basis
Finished basis 43m57s 41GB
Starting compiler/inference
Finished compiler/inference 1m09s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m07s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m29s 3GB
Starting compiler/backend
Finished compiler/backend 5m08s 5GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 22s 1GB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 26s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 50s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 13s 1GB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 18s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 15s 1GB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 18s 966MB
Starting compiler/backend/x64
Finished compiler/backend/x64 19s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 21s 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 20s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m10s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m43s 2GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m34s 2GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 27m02s 5GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m20s 1GB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 53m44s 16GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m18s 5GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m45s 5GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m27s 3GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m41s 5GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m19s 3GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m18s 2GB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 21s 2GB
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 22s 2GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 12m09s 5GB
Starting compiler/proofs
Finished compiler/proofs 1m45s 6GB
Starting candle/set-theory
Finished candle/set-theory 30s 1GB
Starting candle/syntax-lib
Finished candle/syntax-lib 10s 805MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m53s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m46s 2GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m43s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m34s 6GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m12s 2GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 12m01s 9GB
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: 8s OK
Starting work on timeLangTheory
loopLangTheory real: 13s user: 13s OK
Starting work on loop_callTheory
panLangTheory real: 15s user: 14s OK
Starting work on loop_removeTheory
crepLangTheory real: 16s user: 15s OK
Starting work on pan_simpTheory
timeLangTheory real: 10s 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: 13s OK
Starting work on taParserTheory
pan_to_crepTheory real: 13s 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-1553/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-1553/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-1553/pancake/ta_progs/readmePrefix