Job 3352

CakeML:30ffe1b793173413b26752a285c8421ead3e560c
  fix from_pancake trans [May 21 13:36:19]
#1395 (loop-break-n)
Merging into:8f45236bf0e0e3798826dac24bebf25265cb80ea
  Mcandidate fix (#1396) [May 22 13:21:47]
HOL:9bc51265f47dd73330c063de58178125f58b6b6d
  docs -> html_docs [May 22 02:21:44]
Machine:lammmington

May 22 13:35:51 Claimed job
May 22 13:35:55 Reusing HOL
May 22 13:36:11 Starting developers
May 22 13:36:16 Finished developers                                               4s 227MB
May 22 13:36:17 Starting developers/bin
May 22 13:36:22 Finished developers/bin                                           3s  93MB
May 22 13:36:23 Starting misc
May 22 13:36:36 Finished misc                                                    12s 703MB
May 22 13:36:37 Starting compiler/proofs
May 22 13:37:54 Finished compiler/proofs                                       1m16s   3GB
May 22 13:37:55 Starting compiler/bootstrap/compilation/x64/64/proofs
May 22 16:20:42 Finished compiler/bootstrap/compilation/x64/64/proofs       2h42m45s 108GB
May 22 16:20:42 Starting semantics/ffi
May 22 16:20:47 Finished semantics/ffi                                            3s  79MB
May 22 16:20:48 Starting semantics
May 22 16:20:52 Finished semantics                                                3s  93MB
May 22 16:20:53 Starting semantics/proofs
May 22 16:20:58 Finished semantics/proofs                                         4s  93MB
May 22 16:20:59 Starting semantics/alt_semantics
May 22 16:21:03 Finished semantics/alt_semantics                                  3s  91MB
May 22 16:21:04 Starting semantics/alt_semantics/proofs
May 22 16:21:10 Finished semantics/alt_semantics/proofs                           4s  95MB
May 22 16:21:11 Starting basis/pure
May 22 16:21:15 Finished basis/pure                                               3s  82MB
May 22 16:21:16 Starting translator
May 22 16:21:22 Finished translator                                               4s  96MB
May 22 16:21:22 Starting compiler/parsing
May 22 16:21:27 Finished compiler/parsing                                         4s  96MB
May 22 16:21:28 Starting characteristic
May 22 16:21:34 Finished characteristic                                           4s 109MB
May 22 16:21:35 Starting translator/monadic
May 22 16:21:41 Finished translator/monadic                                       5s 114MB
May 22 16:21:42 Starting translator/monadic/monad_base
May 22 16:21:46 Finished translator/monadic/monad_base                            3s  81MB
May 22 16:21:47 Starting profiler
May 22 16:21:53 Finished profiler                                                 4s 113MB
May 22 16:21:54 Starting basis
May 22 16:22:06 Finished basis                                                   11s 238MB
May 22 16:22:07 Starting compiler
May 22 16:22:20 Finished compiler                                                12s 228MB
May 22 16:22:21 Starting compiler/inference
May 22 16:22:27 Finished compiler/inference                                       4s 108MB
May 22 16:22:28 Starting compiler/backend/reg_alloc
May 22 16:22:32 Finished compiler/backend/reg_alloc                               3s  86MB
May 22 16:22:33 Starting compiler/backend/gc
May 22 16:22:39 Finished compiler/backend/gc                                      5s 144MB
May 22 16:22:40 Starting compiler/backend
May 22 16:22:47 Finished compiler/backend                                         5s 135MB
May 22 16:22:47 Starting compiler/encoders/asm
May 22 16:22:52 Finished compiler/encoders/asm                                    3s 100MB
May 22 16:22:53 Starting compiler/encoders/x64
May 22 16:22:58 Finished compiler/encoders/x64                                    4s 107MB
May 22 16:22:59 Starting compiler/encoders/arm7
May 22 16:23:04 Finished compiler/encoders/arm7                                   4s 108MB
May 22 16:23:05 Starting compiler/encoders/arm8
May 22 16:23:10 Finished compiler/encoders/arm8                                   3s 106MB
May 22 16:23:10 Starting compiler/encoders/arm8_asl
May 22 18:24:39 Finished compiler/encoders/arm8_asl                         2h01m27s  22GB
May 22 18:24:40 Starting compiler/encoders/mips
May 22 18:24:44 Finished compiler/encoders/mips                                   3s 111MB
May 22 18:24:45 Starting compiler/encoders/riscv
May 22 18:24:50 Finished compiler/encoders/riscv                                  3s 109MB
May 22 18:24:51 Starting compiler/encoders/ag32
May 22 18:24:56 Finished compiler/encoders/ag32                                   3s 100MB
May 22 18:24:57 Starting compiler/encoders/tests
May 22 18:25:02 Finished compiler/encoders/tests                                  4s 133MB
May 22 18:25:03 Starting compiler/encoders/monadic_enc
May 22 18:25:31 Finished compiler/encoders/monadic_enc                           26s   1GB
May 22 18:25:31 Starting compiler/backend/x64
May 22 18:25:38 Finished compiler/backend/x64                                     5s 138MB
May 22 18:25:39 Starting compiler/backend/arm7
May 22 18:25:45 Finished compiler/backend/arm7                                    5s 154MB
May 22 18:25:46 Starting compiler/backend/arm8
May 22 18:25:53 Finished compiler/backend/arm8                                    5s 134MB
May 22 18:25:53 Starting compiler/backend/mips
May 22 18:26:00 Finished compiler/backend/mips                                    5s 137MB
May 22 18:26:01 Starting compiler/backend/riscv
May 22 18:26:07 Finished compiler/backend/riscv                                   5s 134MB
May 22 18:26:08 Starting compiler/backend/ag32
May 22 18:27:14 Finished compiler/backend/ag32                                 1m04s   2GB
May 22 18:27:15 Starting compiler/backend/pattern_matching
May 22 18:27:19 Finished compiler/backend/pattern_matching                        3s  94MB
May 22 18:27:20 Starting compiler/parsing/ocaml
May 22 18:29:10 Finished compiler/parsing/ocaml                                1m48s   1GB
May 22 18:29:11 Starting compiler/printing
May 22 18:30:07 Finished compiler/printing                                       55s   1GB
May 22 18:30:08 Starting compiler/parsing/proofs
May 22 18:30:13 Finished compiler/parsing/proofs                                  4s  97MB
May 22 18:30:14 Starting compiler/inference/proofs
May 22 18:30:20 Finished compiler/inference/proofs                                5s 111MB
May 22 18:30:21 Starting compiler/backend/semantics
May 22 18:33:08 Finished compiler/backend/semantics                            2m46s   3GB
May 22 18:33:09 Starting compiler/backend/reg_alloc/proofs
May 22 18:33:15 Finished compiler/backend/reg_alloc/proofs                        5s 122MB
May 22 18:33:16 Starting compiler/backend/proofs
May 22 18:34:06 Finished compiler/backend/proofs                                 49s   2GB
May 22 18:34:07 Starting compiler/backend/serialiser
May 22 18:34:14 Finished compiler/backend/serialiser                              5s 141MB
May 22 18:34:15 Starting compiler/encoders/x64/proofs
May 22 18:34:20 Finished compiler/encoders/x64/proofs                             4s 106MB
May 22 18:34:21 Starting compiler/encoders/arm7/proofs
May 22 18:44:48 Finished compiler/encoders/arm7/proofs                        10m25s   9GB
May 22 18:44:48 Starting compiler/encoders/arm8/proofs
May 22 18:51:08 Finished compiler/encoders/arm8/proofs                         6m18s   8GB
May 22 18:51:09 Starting compiler/encoders/arm8_asl/proofs
May 22 19:37:25 Finished compiler/encoders/arm8_asl/proofs                    46m15s   9GB
May 22 19:37:26 Starting compiler/encoders/mips/proofs
May 22 19:46:18 Finished compiler/encoders/mips/proofs                         8m51s  11GB
May 22 19:46:19 Starting compiler/encoders/riscv/proofs
May 22 19:53:52 Finished compiler/encoders/riscv/proofs                        7m32s   4GB
May 22 19:53:52 Starting compiler/encoders/ag32/proofs
May 22 19:56:24 Finished compiler/encoders/ag32/proofs                         2m31s   2GB
May 22 19:56:25 Starting compiler/backend/x64/proofs
May 22 19:56:38 Finished compiler/backend/x64/proofs                             11s 218MB
May 22 19:56:39 Starting compiler/backend/arm7/proofs
May 22 19:57:25 Finished compiler/backend/arm7/proofs                            45s   2GB
May 22 19:57:26 Starting compiler/backend/arm8/proofs
May 22 19:58:10 Finished compiler/backend/arm8/proofs                            43s   2GB
May 22 19:58:11 Starting compiler/backend/arm8_asl
May 22 19:58:52 Finished compiler/backend/arm8_asl                               39s   1GB
May 22 19:58:53 Starting compiler/backend/mips/proofs
May 22 19:59:39 Finished compiler/backend/mips/proofs                            45s   2GB
May 22 19:59:40 Starting compiler/backend/riscv/proofs
May 22 20:00:28 Finished compiler/backend/riscv/proofs                           46s   2GB
May 22 20:00:29 Starting compiler/backend/ag32/proofs
May 22 20:08:26 Finished compiler/backend/ag32/proofs                          7m56s   4GB
May 22 20:08:27 Starting compiler/backend/cv_compute
May 22 20:09:02 Finished compiler/backend/cv_compute                             33s   1GB
May 22 20:09:02 Starting cv_translator
May 22 20:14:03 Finished cv_translator                                         4m59s   3GB
May 22 20:14:04 Starting candle
May 22 20:14:05 Finished candle                                                   0s   6MB
May 22 20:14:06 Starting candle/set-theory
May 22 20:14:39 Finished candle/set-theory                                       31s 890MB
May 22 20:14:40 Starting candle/syntax-lib
May 22 20:14:44 Finished candle/syntax-lib                                        3s  80MB
May 22 20:14:45 Starting candle/standard
May 22 20:14:46 Finished candle/standard                                          0s   6MB
May 22 20:14:47 Starting candle/standard/syntax
May 22 20:15:05 Finished candle/standard/syntax                                  17s 771MB
May 22 20:15:06 Starting candle/standard/semantics
May 22 20:17:17 Finished candle/standard/semantics                             2m10s   2GB
May 22 20:17:18 Starting candle/standard/monadic
May 22 20:17:24 Finished candle/standard/monadic                                  5s 116MB
May 22 20:17:25 Starting candle/standard/ml_kernel
May 22 20:19:32 Finished candle/standard/ml_kernel                             2m06s   4GB
May 22 20:19:33 Starting candle/overloading
May 22 20:19:34 Finished candle/overloading                                       0s   6MB
May 22 20:19:35 Starting candle/overloading/syntax
May 22 20:22:25 Finished candle/overloading/syntax                             2m49s   2GB
May 22 20:22:26 Starting candle/overloading/semantics
May 22 20:30:56 Finished candle/overloading/semantics                          8m28s   8GB
May 22 20:30:57 Starting candle/overloading/monadic
May 22 20:32:54 Finished candle/overloading/monadic                            1m56s   1GB
May 22 20:32:55 Starting candle/overloading/ml_kernel
May 22 20:39:15 Finished candle/overloading/ml_kernel                          6m18s   7GB
May 22 20:39:16 Starting candle/overloading/ml_checker
May 22 20:41:46 Finished candle/overloading/ml_checker                         2m29s   6GB
May 22 20:41:47 Starting candle/prover
May 22 20:42:05 Finished candle/prover                                           16s 402MB
May 22 20:42:06 Starting candle/prover/compute
May 22 20:42:18 Finished candle/prover/compute                                   11s 299MB
May 22 20:42:19 Starting pancake
May 22 20:42:26 Finished pancake                                                  5s 142MB
May 22 20:42:26 Starting pancake/semantics
May 22 20:45:23 Finished pancake/semantics                                     2m55s   1GB
May 22 20:45:24 Starting pancake/parser
May 22 20:46:01 Finished pancake/parser                                          36s 474MB
May 22 20:46:02 Starting pancake/static_checker
May 22 20:48:07 Finished pancake/static_checker                                2m04s   1GB
May 22 20:48:08 Starting pancake/proofs
May 22 21:03:32 Finished pancake/proofs                                       15m23s   5GB
May 22 21:03:33 Starting compiler/dafny
May 22 21:04:00 Finished compiler/dafny                                          26s 668MB
May 22 21:04:01 Starting compiler/dafny/translation
May 22 21:13:27 Finished compiler/dafny/translation                            9m24s   7GB
May 22 21:13:28 Starting compiler/dafny/compilation
May 22 21:15:31 Finished compiler/dafny/compilation                            2m02s   6GB
May 22 21:15:32 Starting compiler/dafny/semantics
May 22 21:16:13 Finished compiler/dafny/semantics                                39s 497MB
May 22 21:16:13 Starting compiler/dafny/proofs
May 22 21:17:44 Finished compiler/dafny/proofs                                 1m29s   1GB
May 22 21:17:45 Starting compiler/dafny/vcg
May 22 21:17:50 Finished compiler/dafny/vcg                                       4s 107MB
May 22 21:17:51 Starting compiler/dafny/vcg/examples
May 22 21:18:19 Finished compiler/dafny/vcg/examples                             27s   1GB
May 22 21:18:20 Starting compiler/scheme
May 22 21:18:54 Finished compiler/scheme                                         33s   1GB
May 22 21:18:55 Starting compiler/scheme/translation
May 22 21:24:58 Finished compiler/scheme/translation                           6m02s   9GB
May 22 21:24:59 Starting compiler/scheme/compilation
May 22 21:26:33 Finished compiler/scheme/compilation                           1m32s   4GB
May 22 21:26:34 Starting compiler/scheme/proofs
May 22 21:32:07 Finished compiler/scheme/proofs                                5m32s   4GB
May 22 21:32:08 Starting characteristic/examples
May 22 21:33:42 Finished characteristic/examples                               1m32s   5GB
May 22 21:33:42 Starting tutorial/solutions
May 22 21:36:42 Finished tutorial/solutions                                    2m58s   5GB
May 22 21:36:43 Starting translator/monadic/examples
May 22 21:39:50 Finished translator/monadic/examples                           3m06s   4GB
May 22 21:39:51 Starting examples
May 22 21:43:37 FAILED: examples
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
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/floating-point
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(HOLDIR)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
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)/compiler/printing
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanned 66 directories
Starting work on md5Theory
Starting work on source_valuesTheory
Starting work on regexp_parserTheory
Starting work on README.md
README.md                                                 examples  (0s)     OK
Starting work on quicksortProgTheory
source_valuesTheory                             examples/bootstrap  (2s)     OK
Starting work on source_syntaxTheory
source_syntaxTheory                             examples/bootstrap  (0s)     OK
Starting work on parsingTheory
md5Theory                                      examples/Crypto/MD5  (7s)     OK
Finished $(HOLDIR)/examples/Crypto/MD5 [#theories: 1]                  (7.970s) 
Starting work on printingTheory
parsingTheory                                   examples/bootstrap  (6s)     OK
Starting work on catProgTheory
regexp_parserTheory              examples/formal-languages/regular (11s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]   (11.580s) 
Starting work on lcsTheory
printingTheory                                  examples/bootstrap  (5s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                  (14.380s) 
Starting work on divTheory
lcsTheory                                                 examples  (6s)     OK
Starting work on diffTheory
quicksortProgTheory                                       examples (40s)     OK
Starting work on array_searchProgTheory
diffTheory                                                examples (26s)     OK
Starting work on diffProgTheory
catProgTheory                                             examples (39s)     OK
Starting work on doubleArgProgTheory
divTheory                                                 examples (48s)     OK
Starting work on echoProgTheory
array_searchProgTheory                                    examples (35s)     OK
Starting work on filterProgTheory
doubleArgProgTheory                                       examples (25s)     OK
Starting work on grepProgTheory
diffProgTheory                                            examples (46s)     OK
Starting work on helloErrProgTheory
echoProgTheory                                            examples (31s)     OK
Starting work on helloProgTheory
filterProgTheory                                          examples (44s)     OK
Starting work on insertSortProgTheory
helloProgTheory                                           examples (31s)     OK
Starting work on lispProgTheory
helloErrProgTheory                                        examples (39s)     OK
Starting work on md5ProgTheory
insertSortProgTheory                                      examples (21s)     OK
Starting work on patchProgTheory
lispProgTheory                                            examples (23s)     OK
Starting work on queueProgTheory
md5ProgTheory                                             examples (41s)     OK
Starting work on sortProgTheory
queueProgTheory                                           examples (30s)     OK
Starting work on splitwordsTheory
splitwordsTheory                                          examples  (0s) CACHED
Starting work on stackProgTheory
patchProgTheory                                           examples (50s)     OK
Starting work on wordcountProgTheory
wordcountProgTheory                                       examples  (0s)FAIL<1>
grepProgTheory                                            examples(118s) killed
sortProgTheory                                            examples (18s) killed
stackProgTheory                                           examples (11s) killed
*** Holmake aborted - 1 target failed:
*** wordcountProgTheory in examples (status 1)
 Checking cache for prebuilt theory...
 Cache miss; theory will be built locally.
 /scratch/cakeml/regression3/cakeml-3352/examples/splitwordsTheory.sml:9: error: Structure (backend_x64_cvTheory) has not been declared
 Found near open backend_x64_cvTheory fsFFIPropsTheory
 error in quse /scratch/cakeml/regression3/cakeml-3352/examples/splitwordsTheory.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/examples/splitwordsTheory : Fail "Static Errors"
 error in load /scratch/cakeml/regression3/cakeml-3352/examples/wordcountProgScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression3/cakeml-3352/examples/.hol/logs/wordcountProgTheory