Overview

Job 1876

CakeML:6e7811d25dda83981d6de1b0eec056b6e61a09d3
  Fix permsScript to support value trees
#865 (Iced_cake)
Merging into:915403669818aaaea2c42cd400fad0542de3fa99
  Merge pull request #878 from CakeML/array-appi-fix
HOL:a161807cb4e0ea25b8781f3307a590b78703da6f
  Fix some overlong lines
Machine:oven3

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               9s 158MB
 Starting developers/bin
 Finished developers/bin                                          13s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           24s 254MB
 Starting semantics
 Finished semantics                                             4m54s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                     15m23s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 57s 521MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                       25m22s   1GB
 Starting basis/pure
 Finished basis/pure                                            2m18s   1GB
 Starting translator
 Finished translator                                            7m56s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m49s   5GB
 Starting characteristic
 Finished characteristic                                       15m02s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    4m14s   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                                                                                                                                                                                    (25s)     OK
Starting work on fsFFITheory
runtimeFFITheory                                                                                                                                                                                     (26s)     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                                                                                                                                           (0s)     OK
clFFITheory                                                                                                                                                                                          (29s)     OK
RuntimeProgTheory                                                                                                                                                                                    (56s)     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                                                                                                                                          (42s)     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                                                                                                                                                     (37s)     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                                                                                                                                                   (60s)     OK
fsFFIPropsTheory                                                                                                                                                                                    (110s)     OK
ListProgTheory                                                                                                                                                                                      (110s)     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                                                                                                                                                      (56s)     OK
VectorProgTheory                                                                                                                                                                                     (67s)     OK
Starting work on StringProgTheory
StringProgTheory                                                                                                                                                                                     (78s)     OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                                                                                                                                                                                   (81s)     OK
Starting work on IntProgTheory
IntProgTheory                                                                                                                                                                                        (79s)     OK
Starting work on PrettyPrinterProgTheory
PrettyPrinterProgTheory                                                                                                                                                                              (66s)     OK
Starting work on RatProgTheory
RatProgTheory                                                                                                                                                                                        (99s)     OK
Starting work on CharProgTheory
CharProgTheory                                                                                                                                                                                       (68s)     OK
Starting work on Word64ProgTheory
Word64ProgTheory                                                                                                                                                                                     (78s)     OK
Starting work on Word8ProgTheory
Word8ProgTheory                                                                                                                                                                                      (68s)     OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory                                                                                                                                                                                 (68s)     OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory                                                                                                                                                                                (86s)     OK
ArrayProgTheory                                                                                                                                                                                     (173s)     OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory                                                                                                                                                                                       (100s)FAIL<1>
 error in load /root/regression/cakeml-1876/basis/MapProgScript : UnableToTranslate ?
 mapWithKey
 
 
 which has type:
 
 :( ->  -> ) -> (, ) balanced_map -> (, ) balanced_map
 
 Failed translation: map
 Uncaught exception: UnableToTranslate ?
ArrayProofTheory                                                                                                                                                                                    (102s)MKILLED