Overview

Job 1441

CakeML:82a6a52180a50be3f374f0be862f54087aefae18
  Move alt_semantics down the build-seq temporarily
#811 (eval)
Merging into:3c6495906dc020e093e2f5cf101cea1cba2fc468
  Fix breakage caused by change to sorted_map in HOL
HOL:07dca05c1eb441bb9b18556ae55f275d2518bade
  Fix bugs in Makefiles/lib files preventing Lassie from compiling
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               2s  76MB
 Starting developers/bin
 Finished developers/bin                                           6s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                            9s 306MB
 Starting semantics
 Finished semantics                                             1m27s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m31s   1GB
 Starting basis/pure
 Finished basis/pure                                              53s   1GB
 Starting translator
 Finished translator                                            3m17s   2GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m11s   3GB
 Starting characteristic
 Finished characteristic                                        5m39s   3GB
 Starting translator/monadic
 Finished translator/monadic                                    1m45s   2GB
 Starting basis
 FAILED: basis
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)/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/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[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
Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on MarshallingTheory
Starting work on README.md
README.md                                                                     real:    0s  user:    0s     OK
Starting work on runtimeFFITheory
MarshallingTheory                                                             real:   11s  user:   11s     OK
Starting work on fsFFITheory
runtimeFFITheory                                                              real:   12s  user:   11s     OK
Starting work on basis_ffi.o
basis_ffi.o                                                                   real:    0s  user:    0s     OK
clFFITheory                                                                   real:   13s  user:   12s     OK
RuntimeProgTheory                                                             real:   27s  user:   26s     OK
Starting work on OptionProgTheory
Starting work on RuntimeProofTheory
fsFFITheory                                                                   real:   17s  user:   16s     OK
Starting work on fsFFIPropsTheory
OptionProgTheory                                                              real:   18s  user:   17s     OK
Starting work on ListProgTheory
RuntimeProofTheory                                                            real:   30s  user:   29s     OK
fsFFIPropsTheory                                                              real:   59s  user:   58s     OK
ListProgTheory                                                                real:   49s  user:   47s     OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                               real:   30s  user:   29s     OK
VectorProgTheory                                                              real:   34s  user:   33s     OK
Starting work on StringProgTheory
StringProgTheory                                                              real:   36s  user:   35s     OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                                                            real:   35s  user:   34s     OK
Starting work on IntProgTheory
IntProgTheory                                                                 real:   37s  user:   35s     OK
Starting work on RatProgTheory
RatProgTheory                                                                 real:   44s  user:   42s     OK
Starting work on CharProgTheory
CharProgTheory                                                                real:   32s  user:   31s     OK
Starting work on Word64ProgTheory
Word64ProgTheory                                                              real:   33s  user:   31s     OK
Starting work on Word8ProgTheory
Word8ProgTheory                                                               real:   32s  user:   30s     OK
Starting work on Word8ArrayProgTheory
Word8ArrayProgTheory                                                          real:   31s  user:   29s     OK
Starting work on ArrayProgTheory
Starting work on Word8ArrayProofTheory
Word8ArrayProofTheory                                                         real:   40s  user:   39s     OK
ArrayProgTheory                                                               real:   75s  user:   73s     OK
Starting work on ArrayProofTheory
Starting work on MapProgTheory
MapProgTheory                                                                 real:   57s  user:   56s     OK
Starting work on HashtableProgTheory
ArrayProofTheory                                                              real:   65s  user:   64s     OK
HashtableProgTheory                                                           real:   55s  user:   54s     OK
Starting work on CommandLineProgTheory
Starting work on HashtableProofTheory
HashtableProofTheory                                                          real:   40s  user:   38sFAIL<1>
     (POSTv htv. HASHTABLE a b hf cmp FEMPTY htv)
 
 failed.
 Failed to prove theorem hashtable_empty_spec.
 
 Exception raised at Q.EXISTS_TAC:
 goal not an exists (THEN1 on line 519) (THEN1 on line 520) (THEN1 on line 521) (THEN1 on line 522) (THEN1 on line 498) (THEN1 on line 527) (THEN1 on line 530) (THEN1 on line 534) (THEN1 on line 547) (THEN1 on line 551) (THEN1 on line 552) (THEN1 on line 553) (THEN1 on line 554) (THEN1 on line 557)
 error in quse /home/myreen/regression/cakeml-1441/basis/HashtableProofScript.sml : HOL_ERR {message = "goal not an exists (THEN1 on line 519) (THEN1 on line 520) (THEN1 on line 521) (THEN1 on line 522) (THEN1 on line 498) (THEN1 on line 527) (THEN1 on line 530) (THEN1 on line 534) (THEN1 on line 547) (THEN1 on line 551) (THEN1 on line 552) (THEN1 on line 553) (THEN1 on line 554) (THEN1 on line 557)", origin_function = "EXISTS_TAC", origin_structure = "Q"}
 error in load /home/myreen/regression/cakeml-1441/basis/HashtableProofScript : HOL_ERR {message = "goal not an exists (THEN1 on line 519) (THEN1 on line 520) (THEN1 on line 521) (THEN1 on line 522) (THEN1 on line 498) (THEN1 on line 527) (THEN1 on line 530) (THEN1 on line 534) (THEN1 on line 547) (THEN1 on line 551) (THEN1 on line 552) (THEN1 on line 553) (THEN1 on line 554) (THEN1 on line 557)", origin_function = "EXISTS_TAC", origin_structure = "Q"}
 Uncaught exception: HOL_ERR {message = "goal not an exists (THEN1 on line 519) (THEN1 on line 520) (THEN1 on line 521) (THEN1 on line 522) (THEN1 on line 498) (THEN1 on line 527) (THEN1 on line 530) (THEN1 on line 534) (THEN1 on line 547) (THEN1 on line 551) (THEN1 on line 552) (THEN1 on line 553) (THEN1 on line 554) (THEN1 on line 557)", origin_function = "EXISTS_TAC", origin_structure = "Q"}
CommandLineProgTheory                                                                                 M-KILLED