Job 1168

CakeML:25e198b89b3ee9574dc7f3e507fa272d2da4158c
  tweak basis_ffi.c around exit and cml_exit [Jan 28 08:32:32]
#721 (exit_stderr)
Merging into:3d28c489453fa89e98bc364190bb20380bbb184b
  Be more specific about PolyML version [Jan 24 14:50:33]
HOL:b219f4bb4132ea21f42769a8edf7e3abde4cc48d
  emacs-mode: some indentation tweaks [Jan 22 06:44:58]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 28 09:01:03 Claimed job
Jan 28 09:01:06 Reusing HOL
Jan 28 09:01:53 Starting developers
Jan 28 09:01:57 Finished developers                                               4s  88MB
Jan 28 09:01:58 Starting developers/bin
Jan 28 09:02:05 Finished developers/bin                                           7s   1GB
Jan 28 09:02:05 Starting semantics/ffi
Jan 28 09:02:16 Finished semantics/ffi                                           10s 218MB
Jan 28 09:02:16 Starting semantics
Jan 28 09:03:39 Finished semantics                                             1m22s   1GB
Jan 28 09:03:39 Starting semantics/proofs
Jan 28 09:07:07 Finished semantics/proofs                                      3m27s   1GB
Jan 28 09:07:07 Starting semantics/alt_semantics
Jan 28 09:07:16 Finished semantics/alt_semantics                                  8s 326MB
Jan 28 09:07:16 Starting semantics/alt_semantics/proofs
Jan 28 09:09:26 Finished semantics/alt_semantics/proofs                        2m10s 842MB
Jan 28 09:09:27 Starting basis/pure
Jan 28 09:10:16 Finished basis/pure                                              49s 695MB
Jan 28 09:10:17 Starting translator
Jan 28 09:12:55 Finished translator                                            2m38s   1GB
Jan 28 09:12:55 Starting compiler/parsing
Jan 28 09:14:05 Finished compiler/parsing                                      1m09s   2GB
Jan 28 09:14:05 Starting characteristic
Jan 28 09:20:04 Finished characteristic                                        5m58s   1GB
Jan 28 09:20:04 Starting translator/monadic
Jan 28 09:21:42 Finished translator/monadic                                    1m37s   1GB
Jan 28 09:21:42 Starting basis
Jan 28 09:57:27 Finished basis                                                35m44s  10GB
Jan 28 09:57:27 Starting compiler/inference
Jan 28 09:59:39 Finished compiler/inference                                    2m12s   1GB
Jan 28 09:59:40 Starting compiler/backend/reg_alloc
Jan 28 10:00:43 Finished compiler/backend/reg_alloc                            1m03s   1GB
Jan 28 10:00:43 Starting compiler/backend/gc
Jan 28 10:04:00 Finished compiler/backend/gc                                   3m16s   1GB
Jan 28 10:04:00 Starting compiler/backend
Jan 28 10:08:34 Finished compiler/backend                                      4m34s   3GB
Jan 28 10:08:34 Starting compiler/encoders/asm
Jan 28 10:08:57 Finished compiler/encoders/asm                                   22s 930MB
Jan 28 10:08:57 Starting compiler/encoders/x64
Jan 28 10:09:23 Finished compiler/encoders/x64                                   25s 937MB
Jan 28 10:09:23 Starting compiler/encoders/arm7
Jan 28 10:10:11 Finished compiler/encoders/arm7                                  48s 732MB
Jan 28 10:10:12 Starting compiler/encoders/arm8
Jan 28 10:10:25 Finished compiler/encoders/arm8                                  13s 867MB
Jan 28 10:10:25 Starting compiler/encoders/mips
Jan 28 10:10:43 Finished compiler/encoders/mips                                  17s   1GB
Jan 28 10:10:43 Starting compiler/encoders/riscv
Jan 28 10:10:58 Finished compiler/encoders/riscv                                 14s   1GB
Jan 28 10:10:58 Starting compiler/encoders/ag32
Jan 28 10:11:16 Finished compiler/encoders/ag32                                  17s 743MB
Jan 28 10:11:16 Starting compiler/backend/x64
Jan 28 10:11:34 Finished compiler/backend/x64                                    17s 952MB
Jan 28 10:11:34 Starting compiler/backend/arm7
Jan 28 10:11:54 Finished compiler/backend/arm7                                   20s   1GB
Jan 28 10:11:54 Starting compiler/backend/arm8
Jan 28 10:12:13 Finished compiler/backend/arm8                                   18s   1GB
Jan 28 10:12:13 Starting compiler/backend/mips
Jan 28 10:12:33 Finished compiler/backend/mips                                   19s   1GB
Jan 28 10:12:33 Starting compiler/backend/riscv
Jan 28 10:12:52 Finished compiler/backend/riscv                                  18s   1GB
Jan 28 10:12:52 Starting compiler/backend/ag32
Jan 28 10:14:04 Finished compiler/backend/ag32                                 1m11s   1GB
Jan 28 10:14:04 Starting compiler/parsing/proofs
Jan 28 10:19:51 Finished compiler/parsing/proofs                               5m46s   1GB
Jan 28 10:19:51 Starting compiler/inference/proofs
Jan 28 10:22:58 Finished compiler/inference/proofs                             3m06s   1GB
Jan 28 10:22:59 Starting compiler/backend/semantics
Jan 28 10:54:01 Finished compiler/backend/semantics                           31m02s   2GB
Jan 28 10:54:01 Starting compiler/backend/reg_alloc/proofs
Jan 28 10:57:44 Finished compiler/backend/reg_alloc/proofs                     3m42s 918MB
Jan 28 10:57:44 Starting compiler/backend/proofs
Jan 28 12:03:39 Finished compiler/backend/proofs                            1h05m54s  13GB
Jan 28 12:03:40 Starting compiler/encoders/x64/proofs
Jan 28 12:13:29 Finished compiler/encoders/x64/proofs                          9m49s   4GB
Jan 28 12:13:29 Starting compiler/encoders/arm7/proofs
Jan 28 12:26:49 Finished compiler/encoders/arm7/proofs                        13m19s   4GB
Jan 28 12:26:49 Starting compiler/encoders/arm8/proofs
Jan 28 12:33:28 Finished compiler/encoders/arm8/proofs                         6m38s   1GB
Jan 28 12:33:28 Starting compiler/encoders/mips/proofs
Jan 28 12:43:43 Finished compiler/encoders/mips/proofs                        10m15s   2GB
Jan 28 12:43:44 Starting compiler/encoders/riscv/proofs
Jan 28 12:52:50 Finished compiler/encoders/riscv/proofs                        9m06s   1GB
Jan 28 12:52:50 Starting compiler/encoders/ag32/proofs
Jan 28 12:55:29 Finished compiler/encoders/ag32/proofs                         2m38s   1GB
Jan 28 12:55:29 Starting compiler/backend/x64/proofs
Jan 28 12:55:50 Finished compiler/backend/x64/proofs                             20s   1GB
Jan 28 12:55:50 Starting compiler/backend/arm7/proofs
Jan 28 12:56:10 Finished compiler/backend/arm7/proofs                            19s   1GB
Jan 28 12:56:10 Starting compiler/backend/arm8/proofs
Jan 28 12:56:30 Finished compiler/backend/arm8/proofs                            19s   1GB
Jan 28 12:56:30 Starting compiler/backend/mips/proofs
Jan 28 12:56:51 Finished compiler/backend/mips/proofs                            20s   1GB
Jan 28 12:56:51 Starting compiler/backend/riscv/proofs
Jan 28 12:57:10 Finished compiler/backend/riscv/proofs                           19s   1GB
Jan 28 12:57:11 Starting compiler/backend/ag32/proofs
Jan 28 13:07:07 Finished compiler/backend/ag32/proofs                          9m55s   2GB
Jan 28 13:07:07 Starting compiler/proofs
Jan 28 13:08:31 Finished compiler/proofs                                       1m23s   2GB
Jan 28 13:08:31 Starting candle/set-theory
Jan 28 13:08:59 Finished candle/set-theory                                       27s   1GB
Jan 28 13:08:59 Starting candle/syntax-lib
Jan 28 13:09:10 Finished candle/syntax-lib                                       10s 672MB
Jan 28 13:09:11 Starting candle/standard/syntax
Jan 28 13:11:02 Finished candle/standard/syntax                                1m50s 909MB
Jan 28 13:11:02 Starting candle/standard/semantics
Jan 28 13:12:46 Finished candle/standard/semantics                             1m44s 857MB
Jan 28 13:12:46 Starting candle/standard/monadic
Jan 28 13:14:26 Finished candle/standard/monadic                               1m39s   1GB
Jan 28 13:14:27 Starting candle/standard/ml_kernel
Jan 28 13:20:02 Finished candle/standard/ml_kernel                             5m34s   2GB
Jan 28 13:20:02 Starting candle/standard/opentheory
Jan 28 13:29:56 Finished candle/standard/opentheory                            9m54s   4GB
Jan 28 13:29:56 Starting candle/standard/opentheory/compilation
Jan 28 14:03:58 Finished candle/standard/opentheory/compilation               34m02s  12GB
Jan 28 14:03:59 Starting candle/standard/opentheory/compilation/proofs
Jan 28 14:04:38 Finished candle/standard/opentheory/compilation/proofs           38s   2GB
Jan 28 14:04:38 Starting characteristic/examples
Jan 28 14:06:14 Finished characteristic/examples                               1m36s   2GB
Jan 28 14:06:15 Starting tutorial/solutions
Jan 28 14:21:00 Finished tutorial/solutions                                   14m44s   7GB
Jan 28 14:21:00 Starting translator/monadic/examples
Jan 28 14:23:59 Finished translator/monadic/examples                           2m59s   2GB
Jan 28 14:24:00 Starting examples
Jan 28 14:29:53 FAILED: examples
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
README.md                                       real:    0s  user:    0s     OK
Starting work on divTheory
lcsTheory                                       real:   14s  user:   13s     OK
Starting work on diffTheory
diffTheory                                      real:   50s  user:   49s     OK
Starting work on diffProgTheory
catProgTheory                                   real:   94s  user:   92s     OK
Starting work on doubleProgTheory
quicksortProgTheory                             real:  126s  user:  123s     OK
Starting work on array_searchProgTheory
diffProgTheory                                  real:  104s  user:  101s     OK
Starting work on echoProgTheory
divTheory                                       real:  175s  user:  172s     OK
Starting work on filterProgTheory
doubleProgTheory                                real:  121s  user:  119s     OK
Starting work on grepProgTheory
echoProgTheory                                  real:   75s  user:   72s     OK
Starting work on helloErrProgTheory
array_searchProgTheory                          real:  131s  user:  128s     OK
Starting work on helloProgTheory
filterProgTheory                                real:  121s  user:  118s     OK
Starting work on insertSortProgTheory
helloErrProgTheory                              real:   68s  user:   66s     OK
Starting work on iocatProgTheory
helloProgTheory                                 real:   66s  user:   63s     OK
Starting work on patchProgTheory
iocatProgTheory                                 real:   38s  user:   36sFAIL<1>
 <<HOL message: Created theory "iocatProg">>
 Loading translation: basisProg ... done.
 Saved theorem _____ "nsLookup_iocatProg_env_pfun_eqs"
 Saved definition __ "file_contents_def"
 error in quse /home/cake/oven/regression/cakeml-1168/examples/iocatProgScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1168/examples/iocatProgScript : Fail "Static Errors"
 Saved definition __ "catfiles_string_def"
 /home/cake/oven/regression/cakeml-1168/examples/iocatProgScript.sml:94: error: Value or constructor (MEM_FST_ALOOKUP_SOME) has not been declared
 Found near [MEM_FST_ALOOKUP_SOME]
 Uncaught exception: Fail "Static Errors"
grepProgTheory                                                          M-KILLED
insertSortProgTheory                                                    M-KILLED
patchProgTheory                                                         M-KILLED