CakeML Regression Test

Job 2804

CakeML:8ea3640e9c76f53cd35724642349f46665fb0630
  Merge pull request #1152 from CakeML/lexer-fix [Apr 09 07:17:23]
HOL:48a676cadda70ad7fc2f6c7b17ecd434f84db113
  Fix more grammars [Apr 11 03:19:32]
Machine:pavlova

Apr 11 08:55:39 Claimed job
Apr 11 08:55:47 Building HOL
Apr 11 09:06:37 Starting developers
Apr 11 09:06:41 Finished developers                                               3s 213MB
Apr 11 09:06:42 Starting developers/bin
Apr 11 09:06:48 Finished developers/bin                                           5s 746MB
Apr 11 09:06:49 Starting misc
Apr 11 09:07:47 Finished misc                                                    56s   2GB
Apr 11 09:07:48 Starting compiler/proofs
Apr 11 09:12:24 FAILED: compiler/proofs
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/formal-languages/context-free
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/examples/misc
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
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
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanned 92 directories
Starting work on NTpropertiesTheory
Starting work on simpleSexpTheory
Starting work on balanced_mapTheory
Starting work on FormalLangTheory
FormalLangTheory                         examples/formal-languages  (2s)     OK
Finished $(HOLDIR)/examples/formal-languages [#theories: 1]            (2.010s) 
Starting work on charsetTheory
NTpropertiesTheory          examples/formal-languages/context-free  (4s)     OK
Starting work on vec_mapTheory
simpleSexpTheory            examples/formal-languages/context-free  (5s)     OK
Starting work on simpleSexpPEGTheory
vec_mapTheory                    examples/formal-languages/regular  (1s)     OK
Starting work on temporalTheory
simpleSexpPEGTheory         examples/formal-languages/context-free  (3s)     OK
Starting work on simpleSexpParseTheory
temporalTheory                  examples/machine-code/hoare-triple  (3s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 1]   (3.050s) 
Starting work on ffiTheory
charsetTheory                    examples/formal-languages/regular  (7s)     OK
Starting work on regexpTheory
ffiTheory                                            semantics/ffi  (8s)     OK
Finished $(CAKEMLDIR)/semantics/ffi [#theories: 1]                     (8.090s) 
Starting work on fpValTreeTheory
simpleSexpParseTheory       examples/formal-languages/context-free (10s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 4] (23.080s) 
Starting work on namespaceTheory
fpValTreeTheory                                          semantics  (1s)     OK
Starting work on fpOptTheory
namespaceTheory                                          semantics  (1s)     OK
Starting work on realOpsTheory
realOpsTheory                                            semantics  (1s)     OK
Starting work on tokensTheory
fpOptTheory                                              semantics  (4s)     OK
Starting work on fpSemTheory
regexpTheory                     examples/formal-languages/regular (14s)     OK
Starting work on mllistTheory
tokensTheory                                             semantics  (3s)     OK
Starting work on gramTheory
fpSemTheory                                              semantics  (1s)     OK
Starting work on astTheory
mllistTheory                                            basis/pure  (2s)     OK
Starting work on tokenUtilsTheory
astTheory                                                semantics  (7s)     OK
Starting work on semanticPrimitivesTheory
gramTheory                                               semantics  (7s)     OK
Starting work on lexer_funTheory
tokenUtilsTheory                                         semantics  (7s)     OK
Starting work on cmlPtreeConversionTheory
cmlPtreeConversionTheory                                 semantics (18s)     OK
Starting work on mlstringTheory
mlstringTheory                                          basis/pure (12s)     OK
Starting work on mlintTheory
semanticPrimitivesTheory                                 semantics (34s)     OK
Starting work on evaluateTheory
lexer_funTheory                                          semantics (38s)     OK
Starting work on typeSystemTheory
evaluateTheory                                           semantics  (5s)     OK
Starting work on mloptionTheory
mlintTheory                                             basis/pure  (7s)     OK
Starting work on mlratTheory
mloptionTheory                                          basis/pure  (2s)     OK
Starting work on typeDecToPPTheory
typeDecToPPTheory                                       basis/pure  (2s)     OK
Starting work on astPropsTheory
mlratTheory                                             basis/pure  (3s)     OK
Starting work on gramPropsTheory
astPropsTheory                                    semantics/proofs  (1s)     OK
Starting work on namespacePropsTheory
typeSystemTheory                                         semantics (12s)     OK
Starting work on primTypesTheory
primTypesTheory                                          semantics  (2s)     OK
Starting work on semanticsTheory
namespacePropsTheory                              semantics/proofs  (6s)     OK
Starting work on fpOptPropsTheory
semanticsTheory                                          semantics  (4s)     OK
Finished $(CAKEMLDIR)/semantics [#theories: 16]                      (152.870s) 
Starting work on semanticPrimitivesPropsTheory
fpOptPropsTheory                                  semantics/proofs  (5s)     OK
Starting work on fpSemPropsTheory
gramPropsTheory                                   semantics/proofs (14s)     OK
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                         semantics/proofs  (4s)     OK
Starting work on cmlPEGTheory
semanticPrimitivesPropsTheory                     semantics/proofs (35s)     OK
Starting work on typeSysPropsTheory
balanced_mapTheory                           examples/balanced_bst(133s)     OK
Starting work on osetTheory
osetTheory                                   examples/balanced_bst  (4s)     OK
Finished $(HOLDIR)/examples/balanced_bst [#theories: 2]              (138.260s) 
Starting work on regexp_mapTheory
regexp_mapTheory                 examples/formal-languages/regular  (3s)     OK
Starting work on regexp_compilerTheory
typeSysPropsTheory                                semantics/proofs (19s)     OK
Starting work on mlmapTheory
mlmapTheory                                             basis/pure  (4s)     OK
Starting work on mlsetTheory
regexp_compilerTheory            examples/formal-languages/regular (14s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 5]   (41.850s) 
Starting work on mlvectorTheory
mlsetTheory                                             basis/pure  (2s)     OK
Starting work on primSemEnvTheory
mlvectorTheory                                          basis/pure  (4s)     OK
Starting work on mlprettyprinterTheory
cmlPEGTheory                                      compiler/parsing (62s)     OK
Starting work on weakeningTheory
primSemEnvTheory                                  semantics/proofs  (7s)     OK
Starting work on cmlParseTheory
mlprettyprinterTheory                                   basis/pure  (7s)     OK
Finished $(CAKEMLDIR)/basis/pure [#theories: 10]                      (49.310s) 
Starting work on fromSexpTheory
weakeningTheory                                   semantics/proofs  (5s)     OK
Starting work on lexer_implTheory
cmlParseTheory                                    compiler/parsing  (8s)     OK
Starting work on cfFFITypeTheory
cfFFITypeTheory                                     characteristic  (4s)     OK
Starting work on ml_monadBaseTheory
fpSemPropsTheory                                  semantics/proofs (89s)     OK
Starting work on evaluatePropsTheory
ml_monadBaseTheory                   translator/monadic/monad_base (15s)     OK
Finished $(CAKEMLDIR)/translator/monadic/monad_base [#theories: 1]    (15.730s) 
Starting work on MarshallingTheory
MarshallingTheory                                            basis  (3s)     OK
Starting work on spt_closureTheory
spt_closureTheory                              examples/algorithms  (1s)     OK
Finished $(HOLDIR)/examples/algorithms [#theories: 1]                  (1.570s) 
Starting work on multiwordTheory
lexer_implTheory                                  compiler/parsing (44s)     OK
Starting work on pattern_commonTheory
pattern_commonTheory             compiler/backend/pattern_matching  (9s)     OK
Starting work on pattern_semanticsTheory
multiwordTheory                    examples/machine-code/multiword (25s)     OK
Starting work on mc_multiwordTheory
pattern_semanticsTheory          compiler/backend/pattern_matching (13s)     OK
Starting work on pattern_compTheory
fromSexpTheory                                    compiler/parsing (67s)     OK
Finished $(CAKEMLDIR)/compiler/parsing [#theories: 4]                (181.840s) 
Starting work on reg_allocTheory
reg_allocTheory                         compiler/backend/reg_alloc  (9s)FAIL<1>
 /scratch/cakeml/regression/cakeml-2804/translator/monadic/monad_base/ml_monadBaseLib.sml:15: error: Value or constructor (ml_monadBase_grammars) has not been declared in structure ml_monadBaseTheory
 Found near parse_from_grammars ml_monadBaseTheory.ml_monadBase_grammars
 error in quse /scratch/cakeml/regression/cakeml-2804/translator/monadic/monad_base/ml_monadBaseLib.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/translator/monadic/monad_base/ml_monadBaseLib : Fail "Static Errors"
 error in load /scratch/cakeml/regression/cakeml-2804/compiler/backend/reg_alloc/reg_allocScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
evaluatePropsTheory                               semantics/proofs (72s)MKILLED
mc_multiwordTheory                 examples/machine-code/multiword (25s)MKILLED
pattern_compTheory               compiler/backend/pattern_matching (11s)MKILLED