Overview

Job 1689

CakeML:c8028962805c7859f46a5d42c5ab2c95a995ea61
  Comment out unused(?) broken parts
#850 (eval)
Merging into:ac6dd83f48ab211455fb85c60d3e20e212dc7b8a
  Remove some primes
HOL:9511d2021f824ef967db312f1d1a41c58dbf7acb
  Fix a proof in face of automatic simp change in affbde85bd8
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               4s  96MB
 Starting developers/bin
 Finished developers/bin                                           5s 670MB
 Starting semantics/ffi
 Finished semantics/ffi                                            8s 230MB
 Starting semantics
 Finished semantics                                             1m24s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m49s 993MB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 11s 403MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m34s   1GB
 Starting basis/pure
 Finished basis/pure                                              51s 685MB
 Starting translator
 Finished translator                                            2m57s   1GB
 Starting compiler/parsing
 FAILED: compiler/parsing
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
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)/semantics/proofs
Starting work on simpleSexpTheory
Starting work on README.md
Starting work on cmlPEGTheory
Starting work on lexer_implTheory
README.md                                         compiler/parsing  (0s)     OK
simpleSexpTheory            examples/formal-languages/context-free  (4s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1] (4.514s) 
Starting work on fromSexpTheory
fromSexpTheory                                    compiler/parsing  (8s)FAIL<1>
 <<HOL message: mk_functional: 
   pattern completion has added 1 clause to the original specification.>>
 Saved definition ____ "decode_control_def"
 Saved induction _____ "decode_control_ind"
 error in quse /home/cake/oven/regression/cakeml-1689/compiler/parsing/fromSexpScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1689/compiler/parsing/fromSexpScript : Fail "Static Errors"
 Saved theorem _______ "EVERY_isPrint_encode_control"
 /home/cake/oven/regression/cakeml-1689/compiler/parsing/fromSexpScript.sml:175: error: Value or constructor (LIST_LENGTH_2) has not been declared in structure quantHeuristicsTheory
 Found near [quantHeuristicsTheory.LIST_LENGTH_2]
 Uncaught exception: Fail "Static Errors"
cmlPEGTheory                                      compiler/parsing (14s)MKILLED
lexer_implTheory                                  compiler/parsing (14s)MKILLED