CakeML:9de970f156e7009f364216fa237d50063c22b451
Fix for change to finite_mapSyntax in HOL
HOL:8a1c5607fb8c5be3be18fbe7a3653c704b0ea4da
Manual: mention that LaTeX munging handles record types OK
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 5s 118MB
Starting developers/bin
Finished developers/bin 5s 1GB
Starting compiler/proofs
FAILED: compiler/proofs
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/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[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$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/proofs[0m
Scanned 83 directories
Starting work on byteTheory
Starting work on libTheory
Starting work on ag32Theory
Finished $(HOLDIR)/examples/l3-machine-code/mips/model (0.000s)
Starting work on mips-heap
libTheory misc (3s) OK
Starting work on ffiTheory
ag32Theory compiler/encoders/ag32 (6s) OK
Finished $(HOLDIR)/examples/l3-machine-code/riscv/model (0.000s)
Starting work on riscv-heap
mips-heap examples/l3-machine-code/mips/step (12s) OK
Starting work on mips_stepTheory
byteTheory misc (7s) OK
Starting work on miscTheory
ffiTheory semantics/ffi (3s) OK
Finished $(CAKEMLDIR)/semantics/ffi [#theories: 1] (3.939s)
Finished $(HOLDIR)/examples/l3-machine-code/x64/model (0.000s)
Starting work on x64-heap
x64-heap examples/l3-machine-code/x64/step (7s) OK
Starting work on x64_stepTheory
riscv-heap examples/l3-machine-code/riscv/step (10s) OK
Starting work on riscv_stepTheory
mips_stepTheory examples/l3-machine-code/mips/step (16s) OK
Finished $(HOLDIR)/examples/l3-machine-code/mips/step [#theories: 1] (28.732s)
Starting work on commonUnifTheory
commonUnifTheory examples/algorithms/unification/triangular (0s) OK
Finished $(HOLDIR)/examples/algorithms/unification/triangular [#theories: 1] (0.918s)
Starting work on termTheory
termTheory examples/algorithms/unification/triangular/first-order (1s) OK
Starting work on substTheory
x64_stepTheory examples/l3-machine-code/x64/step (18s) OK
Finished $(HOLDIR)/examples/l3-machine-code/x64/step [#theories: 1] (25.795s)
Starting work on panLexerTheory
substTheory examples/algorithms/unification/triangular/first-order (3s) OK
Starting work on walkTheory
walkTheory examples/algorithms/unification/triangular/first-order (2s) OK
Starting work on walkstarTheory
walkstarTheory examples/algorithms/unification/triangular/first-order (2s) OK
Starting work on collapseTheory
panLexerTheory pancake/parser (5s) OK
Starting work on unifDefTheory
collapseTheory examples/algorithms/unification/triangular/first-order (1s) OK
Starting work on panPEGTheory
unifDefTheory examples/algorithms/unification/triangular/first-order (4s) OK
Starting work on unifPropsTheory
riscv_stepTheory examples/l3-machine-code/riscv/step (31s) OK
Finished $(HOLDIR)/examples/l3-machine-code/riscv/step [#theories: 1] (42.345s)
Starting work on README.md
README.md compiler/proofs (0s) OK
miscTheory misc (38s) OK
Starting work on cakeml-heap
Starting work on mllistTheory
unifPropsTheory examples/algorithms/unification/triangular/first-order (4s) OK
Starting work on mloptionTheory
panPEGTheory pancake/parser (12s) OK
Starting work on mlmapTheory
cakeml-heap misc (11s) OK
Finished $(CAKEMLDIR)/misc [#theories: 3] (61.802s)
Starting work on fpValTreeTheory
fpValTreeTheory semantics (1s) OK
Starting work on fpOptTheory
mllistTheory basis/pure (11s) OK
Starting work on namespaceTheory
mloptionTheory basis/pure (11s) OK
Starting work on realOpsTheory
realOpsTheory semantics (1s) OK
Starting work on tokensTheory
namespaceTheory semantics (2s) OK
Starting work on mlstringTheory
fpOptTheory semantics (5s) OK
Starting work on fpSemTheory
mlmapTheory basis/pure (11s) OK
Starting work on mlvectorTheory
tokensTheory semantics (3s) OK
Starting work on gramTheory
fpSemTheory semantics (2s) OK
Starting work on astTheory
gramTheory semantics (8s) OK
Starting work on tokenUtilsTheory
astTheory semantics (8s) OK
Starting work on semanticPrimitivesTheory
mlvectorTheory basis/pure (15s) OK
Starting work on lexer_funTheory
tokenUtilsTheory semantics (10s) OK
Starting work on cmlPtreeConversionTheory
mlstringTheory basis/pure (27s) OK
Starting work on mlintTheory
lexer_funTheory semantics (9s) OK
Starting work on gramPropsTheory
gramPropsTheory semantics/proofs (9s)FAIL<1>
/home/cug/hk324/cml-regression/cakeml-2130/semantics/proofs/gramPropsScript.sml:123: error: Value or constructor (fapply_t) has not been declared in structure finite_mapSyntax
Found near finite_mapSyntax.fapply_t
error in quse /home/cug/hk324/cml-regression/cakeml-2130/semantics/proofs/gramPropsScript.sml : Fail "Static Errors"
error in load /home/cug/hk324/cml-regression/cakeml-2130/semantics/proofs/gramPropsScript : Fail "Static Errors"
Uncaught exception: Fail "Static Errors"
semanticPrimitivesTheory semantics (26s)MKILLED
cmlPtreeConversionTheory semantics (16s)MKILLED
mlintTheory basis/pure (13s)MKILLED