OverviewCakeML:ab7ea440afff89d5f90e2b85415c2e27f7894561
Use Theory.current_definitions instead of fetch
HOL:729baf5e526741114f4346767d17d0da3a1b6c20
Remove (generated file) Thm-sig.sml when cleaning src/thm
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 0s 22MB
Starting developers/bin
Finished developers/bin 34s 143MB
Starting semantics/ffi
Finished semantics/ffi 33s 510MB
Starting semantics
Finished semantics 1m33s 1GB
Starting semantics/proofs
Finished semantics/proofs 2m58s 1GB
Starting basis/pure
Finished basis/pure 3m36s 657MB
Starting translator
Finished translator 1m41s 1GB
Starting compiler/parsing
FAILED: compiler/parsing
]0;Holmake: .]0;Holmake: ~/regression/cakeml-780/misc]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-780/misc]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-780/misc]0;Holmake: ~/regression/cakeml-780/developers]0;Holmake: ~/regression/cakeml-780/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-780/misc]0;Holmake: ~/regression/cakeml-780/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-780/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-780/misc]0;Holmake: ~/regression/cakeml-780/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-780/semantics]0;Holmake: ~/regression/cakeml-780/semantics/ffi]0;Holmake: ~/regression/cakeml-780/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-780/semantics]0;Holmake: ~/regression/cakeml-780/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
Starting work on cmlPEGTheory
Starting work on fromSexpTheory
Starting work on lexer_implTheory
Starting work on README.md
README.md OK
cmlPEGTheory FAILED! <1>
/home/myreen/regression/cakeml-780/compiler/parsing/cmlPEGScript.sml:15: error: Value or constructor (new_storage_attribute) has not been declared
Found near new_storage_attribute "cakeml/parsing"
error in quse /home/myreen/regression/cakeml-780/compiler/parsing/cmlPEGScript.sml : Fail "Static Errors"
error in load cmlPEGScript : Fail "Static Errors"
Uncaught exception: Fail "Static Errors"
fromSexpTheory M-KILLED
lexer_implTheory M-KILLED