Job 2810

CakeML:70ce28ac902fe04650309ae4d8435135bc1da810
  Remove various debris from timeLang [Apr 25 12:41:33]
#1161 (untime)
Merging into:f37b65230f6b4665a5ac7b1730ef01bcf24115de
  Merge pull request #1159 from CakeML/clos-op-split [Apr 24 12:13:27]
HOL:48a676cadda70ad7fc2f6c7b17ecd434f84db113
  Fix more grammars [Apr 11 03:19:32]
Machine:pavlova

Apr 25 12:46:04 Claimed job
Apr 25 12:46:08 Reusing HOL
Apr 25 12:46:19 Starting developers
Apr 25 12:46:23 Finished developers                                               3s 222MB
Apr 25 12:46:24 Starting developers/bin
Apr 25 12:46:30 Finished developers/bin                                           4s 591MB
Apr 25 12:46:30 Starting misc
Apr 25 12:47:13 Finished misc                                                    41s   1GB
Apr 25 12:47:14 Starting compiler/proofs
Apr 25 14:25:42 Finished compiler/proofs                                    1h38m27s  38GB
Apr 25 14:25:43 Starting compiler/bootstrap/translation
Apr 25 20:06:53 Finished compiler/bootstrap/translation                     5h41m09s 103GB
Apr 25 20:06:54 Starting semantics/ffi
Apr 25 20:07:04 Finished semantics/ffi                                            9s 594MB
Apr 25 20:07:05 Starting semantics
Apr 25 20:07:06 Finished semantics                                                0s  52MB
Apr 25 20:07:07 Starting semantics/proofs
Apr 25 20:07:30 Finished semantics/proofs                                        22s 879MB
Apr 25 20:07:31 Starting semantics/alt_semantics
Apr 25 20:07:53 Finished semantics/alt_semantics                                 20s 889MB
Apr 25 20:07:53 Starting semantics/alt_semantics/proofs
Apr 25 20:18:04 Finished semantics/alt_semantics/proofs                       10m09s   3GB
Apr 25 20:18:04 Starting basis/pure
Apr 25 20:18:06 Finished basis/pure                                               0s  92MB
Apr 25 20:18:07 Starting translator
Apr 25 20:19:41 Finished translator                                            1m32s   2GB
Apr 25 20:19:42 Starting compiler/parsing
Apr 25 20:19:43 Finished compiler/parsing                                         0s  62MB
Apr 25 20:19:44 Starting characteristic
Apr 25 20:19:46 Finished characteristic                                           1s 110MB
Apr 25 20:19:47 Starting translator/monadic
Apr 25 20:19:49 Finished translator/monadic                                       1s 114MB
Apr 25 20:19:50 Starting translator/monadic/monad_base
Apr 25 20:19:51 Finished translator/monadic/monad_base                            0s  56MB
Apr 25 20:19:52 Starting basis
Apr 25 20:22:11 Finished basis                                                 2m18s   4GB
Apr 25 20:22:12 Starting compiler
Apr 25 20:22:15 Finished compiler                                                 1s 214MB
Apr 25 20:22:16 Starting compiler/inference
Apr 25 20:22:18 Finished compiler/inference                                       1s 119MB
Apr 25 20:22:19 Starting compiler/backend/reg_alloc
Apr 25 20:22:20 Finished compiler/backend/reg_alloc                               0s  55MB
Apr 25 20:22:21 Starting compiler/backend/gc
Apr 25 20:22:23 Finished compiler/backend/gc                                      1s 138MB
Apr 25 20:22:24 Starting compiler/backend
Apr 25 20:22:29 Finished compiler/backend                                         4s 255MB
Apr 25 20:22:30 Starting compiler/encoders/asm
Apr 25 20:22:32 Finished compiler/encoders/asm                                    0s  88MB
Apr 25 20:22:32 Starting compiler/encoders/x64
Apr 25 20:22:34 Finished compiler/encoders/x64                                    0s  86MB
Apr 25 20:22:35 Starting compiler/encoders/arm7
Apr 25 20:22:37 Finished compiler/encoders/arm7                                   0s  89MB
Apr 25 20:22:38 Starting compiler/encoders/arm8
Apr 25 20:22:39 Finished compiler/encoders/arm8                                   0s  87MB
Apr 25 20:22:40 Starting compiler/encoders/arm8_asl
Apr 25 20:23:37 Finished compiler/encoders/arm8_asl                              55s  20GB
Apr 25 20:23:38 Starting compiler/encoders/mips
Apr 25 20:23:40 Finished compiler/encoders/mips                                   0s  88MB
Apr 25 20:23:40 Starting compiler/encoders/riscv
Apr 25 20:23:42 Finished compiler/encoders/riscv                                  0s  84MB
Apr 25 20:23:43 Starting compiler/encoders/ag32
Apr 25 20:23:45 Finished compiler/encoders/ag32                                   0s  85MB
Apr 25 20:23:46 Starting compiler/encoders/tests
Apr 25 20:23:47 Finished compiler/encoders/tests                                  0s 104MB
Apr 25 20:23:48 Starting compiler/encoders/monadic_enc
Apr 25 20:23:50 Finished compiler/encoders/monadic_enc                            1s 141MB
Apr 25 20:23:51 Starting compiler/backend/x64
Apr 25 20:23:54 Finished compiler/backend/x64                                     1s 135MB
Apr 25 20:23:54 Starting compiler/backend/arm7
Apr 25 20:23:57 Finished compiler/backend/arm7                                    1s 136MB
Apr 25 20:23:57 Starting compiler/backend/arm8
Apr 25 20:24:00 Finished compiler/backend/arm8                                    1s 135MB
Apr 25 20:24:00 Starting compiler/backend/mips
Apr 25 20:24:03 Finished compiler/backend/mips                                    1s 136MB
Apr 25 20:24:04 Starting compiler/backend/riscv
Apr 25 20:24:06 Finished compiler/backend/riscv                                   1s 136MB
Apr 25 20:24:07 Starting compiler/backend/ag32
Apr 25 20:25:14 Finished compiler/backend/ag32                                 1m06s   3GB
Apr 25 20:25:15 Starting compiler/backend/pattern_matching
Apr 25 20:25:16 Finished compiler/backend/pattern_matching                        0s  51MB
Apr 25 20:25:17 Starting compiler/parsing/ocaml
Apr 25 20:27:00 Finished compiler/parsing/ocaml                                1m42s   1GB
Apr 25 20:27:01 Starting compiler/printing
Apr 25 20:27:03 Finished compiler/printing                                        1s 120MB
Apr 25 20:27:04 Starting compiler/parsing/proofs
Apr 25 20:27:06 Finished compiler/parsing/proofs                                  0s  61MB
Apr 25 20:27:07 Starting compiler/inference/proofs
Apr 25 20:27:09 Finished compiler/inference/proofs                                1s 110MB
Apr 25 20:27:09 Starting compiler/backend/semantics
Apr 25 20:30:17 Finished compiler/backend/semantics                            3m06s   2GB
Apr 25 20:30:18 Starting compiler/backend/reg_alloc/proofs
Apr 25 20:30:20 Finished compiler/backend/reg_alloc/proofs                        1s 113MB
Apr 25 20:30:21 Starting compiler/backend/proofs
Apr 25 20:31:06 Finished compiler/backend/proofs                                 44s   3GB
Apr 25 20:31:07 Starting compiler/backend/serialiser
Apr 25 20:31:09 Finished compiler/backend/serialiser                              1s 139MB
Apr 25 20:31:10 Starting compiler/encoders/x64/proofs
Apr 25 20:41:26 Finished compiler/encoders/x64/proofs                         10m15s   4GB
Apr 25 20:41:27 Starting compiler/encoders/arm7/proofs
Apr 25 20:54:31 Finished compiler/encoders/arm7/proofs                        13m02s   5GB
Apr 25 20:54:32 Starting compiler/encoders/arm8/proofs
Apr 25 21:01:26 Finished compiler/encoders/arm8/proofs                         6m52s   3GB
Apr 25 21:01:27 Starting compiler/encoders/arm8_asl/proofs
Apr 25 21:16:55 Finished compiler/encoders/arm8_asl/proofs                    15m26s   2GB
Apr 25 21:16:56 Starting compiler/encoders/mips/proofs
Apr 25 21:27:13 Finished compiler/encoders/mips/proofs                        10m15s  10GB
Apr 25 21:27:14 Starting compiler/encoders/riscv/proofs
Apr 25 21:35:21 Finished compiler/encoders/riscv/proofs                        8m06s   4GB
Apr 25 21:35:22 Starting compiler/encoders/ag32/proofs
Apr 25 21:38:12 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
Apr 25 21:38:13 Starting compiler/backend/x64/proofs
Apr 25 21:38:44 Finished compiler/backend/x64/proofs                             29s   2GB
Apr 25 21:38:45 Starting compiler/backend/arm7/proofs
Apr 25 21:39:15 Finished compiler/backend/arm7/proofs                            28s   1GB
Apr 25 21:39:16 Starting compiler/backend/arm8/proofs
Apr 25 21:39:45 Finished compiler/backend/arm8/proofs                            28s   2GB
Apr 25 21:39:46 Starting compiler/backend/arm8_asl
Apr 25 21:40:07 Finished compiler/backend/arm8_asl                               19s   1GB
Apr 25 21:40:08 Starting compiler/backend/mips/proofs
Apr 25 21:40:38 Finished compiler/backend/mips/proofs                            29s   2GB
Apr 25 21:40:38 Starting compiler/backend/riscv/proofs
Apr 25 21:41:10 Finished compiler/backend/riscv/proofs                           30s   2GB
Apr 25 21:41:11 Starting compiler/backend/ag32/proofs
Apr 25 21:54:51 Finished compiler/backend/ag32/proofs                         13m38s   5GB
Apr 25 21:54:52 Starting compiler/backend/cv_compute
Apr 25 21:56:02 Finished compiler/backend/cv_compute                           1m09s   2GB
Apr 25 21:56:03 Starting cv_translator
Apr 25 22:16:03 Finished cv_translator                                        19m59s   6GB
Apr 25 22:16:04 Starting candle
Apr 25 22:16:05 Finished candle                                                   0s  10MB
Apr 25 22:16:06 Starting candle/set-theory
Apr 25 22:16:40 Finished candle/set-theory                                       33s   1GB
Apr 25 22:16:41 Starting candle/syntax-lib
Apr 25 22:16:43 Finished candle/syntax-lib                                        0s  94MB
Apr 25 22:16:44 Starting candle/standard
Apr 25 22:16:45 Finished candle/standard                                          0s  12MB
Apr 25 22:16:46 Starting candle/standard/syntax
Apr 25 22:16:58 Finished candle/standard/syntax                                  11s 784MB
Apr 25 22:16:59 Starting candle/standard/semantics
Apr 25 22:19:02 Finished candle/standard/semantics                             2m01s   2GB
Apr 25 22:19:03 Starting candle/standard/monadic
Apr 25 22:19:05 Finished candle/standard/monadic                                  1s 126MB
Apr 25 22:19:06 Starting candle/standard/ml_kernel
Apr 25 22:20:51 Finished candle/standard/ml_kernel                             1m44s   4GB
Apr 25 22:20:52 Starting candle/standard/ml_kernel/lisp
Apr 25 22:20:53 Finished candle/standard/ml_kernel/lisp                           0s  50MB
Apr 25 22:20:54 Starting candle/overloading
Apr 25 22:20:55 Finished candle/overloading                                       0s  12MB
Apr 25 22:20:56 Starting candle/overloading/syntax
Apr 25 22:24:08 Finished candle/overloading/syntax                             3m10s   2GB
Apr 25 22:24:08 Starting candle/overloading/semantics
Apr 25 22:35:05 Finished candle/overloading/semantics                         10m55s   4GB
Apr 25 22:35:06 Starting candle/overloading/monadic
Apr 25 22:37:25 Finished candle/overloading/monadic                            2m18s   2GB
Apr 25 22:37:26 Starting candle/overloading/ml_kernel
Apr 25 22:44:33 Finished candle/overloading/ml_kernel                          7m06s   5GB
Apr 25 22:44:34 Starting candle/overloading/ml_checker
Apr 25 22:46:47 Finished candle/overloading/ml_checker                         2m11s   6GB
Apr 25 22:46:47 Starting candle/prover
Apr 25 22:56:23 Finished candle/prover                                         9m34s   5GB
Apr 25 22:56:24 Starting candle/prover/compute
Apr 25 22:56:26 Finished candle/prover/compute                                    1s 141MB
Apr 25 22:56:27 Starting pancake
Apr 25 22:56:29 Finished pancake                                                  1s 141MB
Apr 25 22:56:30 Starting pancake/semantics
Apr 25 22:56:34 FAILED: pancake/semantics
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/algorithms
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
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)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
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)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/pancake
Scanned 50 directories
Starting work on README.md
Starting work on compactDSLSemTheory
Starting work on panSemTheory
Starting work on pan_commonPropsTheory
README.md                                                           (0s)     OK
Starting work on loopSemTheory
compactDSLSemTheory                                                 (0s)FAIL<1>
 /scratch/cakeml/regression/cakeml-2810/pancake/semantics/compactDSLSemScript.sml:6: error: Structure (timeLangTheory) has not been declared
 Found near open preamble timeLangTheory
 error in quse /scratch/cakeml/regression/cakeml-2810/pancake/semantics/compactDSLSemScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression/cakeml-2810/pancake/semantics/compactDSLSemScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
panSemTheory                                                        (0s)MKILLED
pan_commonPropsTheory                                               (0s)MKILLED
loopSemTheory                                                       (0s)MKILLED