CakeML:59f00ec36c1f7da7b3815d624bf69dd075aaa3e5
Fix one more proof in permsScript
#865 (Iced_cake)
Merging into:c2be5d64270ec1538eded2eed51612b7708c5d50
Merge pull request #872 from talsewell/printing-type-check-each-dec
HOL:a161807cb4e0ea25b8781f3307a590b78703da6f
Fix some overlong lines
Machine:oven3
Claimed job
Reusing HOL
Starting developers
Finished developers 9s 177MB
Starting developers/bin
Finished developers/bin 49s 1GB
Starting semantics/ffi
Finished semantics/ffi 23s 252MB
Starting semantics
Finished semantics 4m53s 1GB
Starting semantics/proofs
Finished semantics/proofs 16m05s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 56s 532MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 25m27s 1GB
Starting basis/pure
Finished basis/pure 2m16s 1GB
Starting translator
Finished translator 7m48s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m45s 3GB
Starting characteristic
Finished characteristic 14m46s 2GB
Starting translator/monadic
Finished translator/monadic 4m15s 1GB
Starting basis
FAILED: basis
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/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[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/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
Scanned 28 directories
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md (0s) OK
Starting work on runtimeFFITheory
MarshallingTheory (23s) OK
Starting work on fsFFITheory
runtimeFFITheory (26s) OK
Starting work on basis_ffi.o
basis_ffi.o (0s) OK
clFFITheory (29s) OK
RuntimeProgTheory (53s) OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory (44s) OK
Starting work on fsFFIPropsTheory
OptionProgTheory (32s) OK
Starting work on ListProgTheory
RuntimeProofTheory (57s) OK
fsFFIPropsTheory (108s) OK
ListProgTheory (101s) OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory (56s) OK
VectorProgTheory (65s) OK
Starting work on StringProgTheory
StringProgTheory (82s) OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory (83s) OK
Starting work on IntProgTheory
IntProgTheory (79s) OK
Starting work on PrettyPrinterProgTheory
PrettyPrinterProgTheory (59s) OK
Starting work on RatProgTheory
RatProgTheory (95s) OK
Starting work on CharProgTheory
CharProgTheory (72s) OK
Starting work on Word64ProgTheory
Word64ProgTheory (76s) OK
Starting work on Word8ProgTheory
Word8ProgTheory (70s) OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory (71s) OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory (84s) OK
ArrayProgTheory (176s) OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory (95s)FAIL<1>
error in load /root/regression/cakeml-1878/basis/MapProgScript : UnableToTranslate ?
mapWithKey
which has type:
:( -> -> ) -> (, ) balanced_map -> (, ) balanced_map
Failed translation: map
Uncaught exception: UnableToTranslate ?
ArrayProofTheory (96s)MKILLED