Job 2515

CakeML:b8fa08a1c4627fc3098567615d6a93b622a04976
  Fix a proof in repl_init [Jul 31 06:33:20]
#1032 (new-double-ffi)
Merging into:cfaaf93a40910a30ef16b5d3c5ece7d68e97daa2
  Merge pull request #1033 from CakeML/fix-translator-pair-type [Aug 01 15:02:04]
HOL:718d989039b65d4ab82e8b979876c68c04869da1
  Implement general Quote syntax [Jul 26 07:07:20]
Machine:lammmington

Aug 01 15:42:31 Claimed job
Aug 01 15:42:35 Reusing HOL
Aug 01 15:42:46 Starting developers
Aug 01 15:42:49 Finished developers                                               2s 193MB
Aug 01 15:42:50 Starting developers/bin
Aug 01 15:43:00 Finished developers/bin                                           8s   1GB
Aug 01 15:43:01 Starting compiler/proofs
Aug 01 17:36:43 Finished compiler/proofs                                    1h53m41s  31GB
Aug 01 17:36:44 Starting compiler/bootstrap/translation
Aug 02 01:53:42 Finished compiler/bootstrap/translation                     8h16m57s  55GB
Aug 02 01:53:43 Starting semantics/ffi
Aug 02 01:53:52 Finished semantics/ffi                                            7s 657MB
Aug 02 01:53:53 Starting semantics
Aug 02 01:53:54 Finished semantics                                                0s  69MB
Aug 02 01:53:55 Starting semantics/proofs
Aug 02 01:54:32 Finished semantics/proofs                                        35s   2GB
Aug 02 01:54:32 Starting semantics/alt_semantics
Aug 02 01:55:13 Finished semantics/alt_semantics                                 40s   1GB
Aug 02 01:55:14 Starting semantics/alt_semantics/proofs
Aug 02 02:06:19 Finished semantics/alt_semantics/proofs                       11m03s   3GB
Aug 02 02:06:20 Starting basis/pure
Aug 02 02:06:21 Finished basis/pure                                               0s  76MB
Aug 02 02:06:22 Starting translator
Aug 02 02:08:10 Finished translator                                            1m47s   3GB
Aug 02 02:08:11 Starting compiler/parsing
Aug 02 02:08:13 Finished compiler/parsing                                         0s  69MB
Aug 02 02:08:13 Starting characteristic
Aug 02 02:08:15 Finished characteristic                                           0s  94MB
Aug 02 02:08:16 Starting translator/monadic
Aug 02 02:08:17 Finished translator/monadic                                       0s 102MB
Aug 02 02:08:18 Starting basis
Aug 02 02:08:49 FAILED: basis
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanned 28 directories
Starting work on DoubleFFITheory
Starting work on HashtableProofTheory
Starting work on README.md
Starting work on UnsafeProgTheory
README.md                                                           (0s)     OK
Starting work on basis_ffi.o
basis_ffi.o                                                         (0s)     OK
DoubleFFITheory                                                    (25s)FAIL<1>
 Saved definition ____ "ffi_ln_def"
 Saved definition ____ "ffi_exp_def"
 Saved definition ____ "ffi_floor_def"
 Saved definition ____ "dest_iNum_def"
 Saved definition ____ "encode_def"
 Proved triviality ___ "encode_11"
 Proved triviality ___ "encode_decode_exists"
 error in quse /scratch/cakeml/regression2/cakeml-2515/basis/DoubleFFIScript.sml : DUP "decode_encode"
 error in load /scratch/cakeml/regression2/cakeml-2515/basis/DoubleFFIScript : DUP "decode_encode"
 Uncaught exception: DUP "decode_encode"
HashtableProofTheory                                               (25s)MKILLED
UnsafeProgTheory                                                   (24s)MKILLED