Job 911

CakeML:38556cc97d26ac563f2b30eac5c1f3f12ff77587
  Merge pull request #657 from CakeML/fp_translation [May 30 07:20:00]
HOL:6cd76208fd222c4b36e3e37b86df4a075b17df4f
  Fix white-space rule violations in b48f79ea1 [Jun 02 06:51:40]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 03 19:29:31 Claimed job
Jun 03 19:29:38 Building HOL
Jun 03 19:37:24 Starting developers
Jun 03 19:37:25 Finished developers                                               0s  21MB
Jun 03 19:37:25 Starting developers/bin
Jun 03 19:37:28 Finished developers/bin                                           2s 143MB
Jun 03 19:37:28 Starting semantics/ffi
Jun 03 19:38:02 Finished semantics/ffi                                           33s 408MB
Jun 03 19:38:02 Starting semantics
Jun 03 19:39:32 Finished semantics                                             1m29s   1GB
Jun 03 19:39:32 Starting semantics/proofs
Jun 03 19:42:30 Finished semantics/proofs                                      2m57s   1GB
Jun 03 19:42:30 Starting semantics/alt_semantics
Jun 03 19:42:36 Finished semantics/alt_semantics                                  5s 278MB
Jun 03 19:42:36 Starting semantics/alt_semantics/proofs
Jun 03 19:44:23 Finished semantics/alt_semantics/proofs                        1m46s 764MB
Jun 03 19:44:23 Starting basis/pure
Jun 03 19:47:53 Finished basis/pure                                            3m29s 778MB
Jun 03 19:47:53 Starting translator
Jun 03 19:49:31 Finished translator                                            1m37s   1GB
Jun 03 19:49:31 Starting compiler/parsing
Jun 03 19:50:28 Finished compiler/parsing                                        56s   1GB
Jun 03 19:50:28 Starting characteristic
Jun 03 19:55:31 Finished characteristic                                        5m02s   2GB
Jun 03 19:55:31 Starting translator/monadic
Jun 03 19:56:55 Finished translator/monadic                                    1m24s   1GB
Jun 03 19:56:55 Starting basis
Jun 03 20:13:43 Finished basis                                                16m47s   2GB
Jun 03 20:13:43 Starting compiler/inference
Jun 03 20:15:32 Finished compiler/inference                                    1m48s   1GB
Jun 03 20:15:33 Starting compiler/backend/reg_alloc
Jun 03 20:16:29 Finished compiler/backend/reg_alloc                              56s   1GB
Jun 03 20:16:30 Starting compiler/backend/gc
Jun 03 20:25:28 Finished compiler/backend/gc                                   8m58s   1GB
Jun 03 20:25:28 Starting compiler/backend
Jun 03 20:25:29 Finished compiler/backend                                         0s  43MB
Jun 03 20:25:29 Starting compiler/encoders/asm
Jun 03 20:25:30 Finished compiler/encoders/asm                                    0s  37MB
Jun 03 20:25:30 Starting compiler/encoders/x64
Jun 03 20:26:26 Finished compiler/encoders/x64                                   55s 837MB
Jun 03 20:26:26 Starting compiler/encoders/arm7
Jun 03 20:28:01 Finished compiler/encoders/arm7                                1m34s   1GB
Jun 03 20:28:01 Starting compiler/encoders/arm8
Jun 03 20:28:29 Finished compiler/encoders/arm8                                  27s 571MB
Jun 03 20:28:30 Starting compiler/encoders/mips
Jun 03 20:29:33 Finished compiler/encoders/mips                                1m02s   1GB
Jun 03 20:29:33 Starting compiler/encoders/riscv
Jun 03 20:30:48 Finished compiler/encoders/riscv                               1m14s 837MB
Jun 03 20:30:49 Starting compiler/encoders/ag32
Jun 03 20:31:04 Finished compiler/encoders/ag32                                  14s 730MB
Jun 03 20:31:04 Starting compiler/backend/x64
Jun 03 20:31:19 Finished compiler/backend/x64                                    14s   1GB
Jun 03 20:31:19 Starting compiler/backend/arm7
Jun 03 20:31:37 Finished compiler/backend/arm7                                   17s   1GB
Jun 03 20:31:38 Starting compiler/backend/arm8
Jun 03 20:31:53 Finished compiler/backend/arm8                                   15s   1GB
Jun 03 20:31:54 Starting compiler/backend/mips
Jun 03 20:32:09 Finished compiler/backend/mips                                   15s 890MB
Jun 03 20:32:09 Starting compiler/backend/riscv
Jun 03 20:32:26 Finished compiler/backend/riscv                                  16s   1GB
Jun 03 20:32:27 Starting compiler/backend/ag32
Jun 03 20:33:33 Finished compiler/backend/ag32                                 1m06s   1GB
Jun 03 20:33:34 Starting compiler/parsing/proofs
Jun 03 20:39:04 Finished compiler/parsing/proofs                               5m29s 806MB
Jun 03 20:39:04 Starting compiler/inference/proofs
Jun 03 20:41:44 Finished compiler/inference/proofs                             2m39s 818MB
Jun 03 20:41:44 Starting compiler/backend/semantics
Jun 03 20:48:43 Finished compiler/backend/semantics                            6m58s   1GB
Jun 03 20:48:43 Starting compiler/backend/reg_alloc/proofs
Jun 03 20:51:58 Finished compiler/backend/reg_alloc/proofs                     3m14s 826MB
Jun 03 20:51:58 Starting compiler/backend/proofs
Jun 03 21:30:28 Finished compiler/backend/proofs                              38m29s   3GB
Jun 03 21:30:28 Starting compiler/encoders/x64/proofs
Jun 03 21:40:29 Finished compiler/encoders/x64/proofs                         10m00s   4GB
Jun 03 21:40:29 Starting compiler/encoders/arm7/proofs
Jun 03 21:53:44 Finished compiler/encoders/arm7/proofs                        13m14s   4GB
Jun 03 21:53:44 Starting compiler/encoders/arm8/proofs
Jun 03 22:00:27 Finished compiler/encoders/arm8/proofs                         6m42s   1GB
Jun 03 22:00:27 Starting compiler/encoders/mips/proofs
Jun 03 22:10:21 Finished compiler/encoders/mips/proofs                         9m53s   3GB
Jun 03 22:10:21 Starting compiler/encoders/riscv/proofs
Jun 03 22:18:44 Finished compiler/encoders/riscv/proofs                        8m21s   1GB
Jun 03 22:18:44 Starting compiler/encoders/ag32/proofs
Jun 03 22:21:13 Finished compiler/encoders/ag32/proofs                         2m28s 701MB
Jun 03 22:21:13 Starting compiler/backend/x64/proofs
Jun 03 22:21:29 Finished compiler/backend/x64/proofs                             16s   1GB
Jun 03 22:21:30 Starting compiler/backend/arm7/proofs
Jun 03 22:21:46 Finished compiler/backend/arm7/proofs                            16s 834MB
Jun 03 22:21:47 Starting compiler/backend/arm8/proofs
Jun 03 22:22:03 Finished compiler/backend/arm8/proofs                            15s   1GB
Jun 03 22:22:03 Starting compiler/backend/mips/proofs
Jun 03 22:22:21 Finished compiler/backend/mips/proofs                            17s   1GB
Jun 03 22:22:21 Starting compiler/backend/riscv/proofs
Jun 03 22:22:37 Finished compiler/backend/riscv/proofs                           16s   1GB
Jun 03 22:22:38 Starting compiler/backend/ag32/proofs
Jun 03 22:31:38 Finished compiler/backend/ag32/proofs                          8m59s   2GB
Jun 03 22:31:38 Starting compiler/proofs
Jun 03 22:33:03 Finished compiler/proofs                                       1m23s   3GB
Jun 03 22:33:03 Starting candle/set-theory
Jun 03 22:33:28 Finished candle/set-theory                                       24s 825MB
Jun 03 22:33:28 Starting candle/syntax-lib
Jun 03 22:33:37 Finished candle/syntax-lib                                        8s 636MB
Jun 03 22:33:37 Starting candle/standard/syntax
Jun 03 22:35:18 Finished candle/standard/syntax                                1m39s 928MB
Jun 03 22:35:18 Starting candle/standard/semantics
Jun 03 22:36:50 Finished candle/standard/semantics                             1m32s   1GB
Jun 03 22:36:51 Starting candle/standard/monadic
Jun 03 22:38:23 Finished candle/standard/monadic                               1m31s   1GB
Jun 03 22:38:23 Starting candle/standard/ml_kernel
Jun 03 22:42:05 Finished candle/standard/ml_kernel                             3m41s   4GB
Jun 03 22:42:05 Starting candle/standard/opentheory
Jun 03 22:50:15 Finished candle/standard/opentheory                            8m10s   3GB
Jun 03 22:50:16 Starting candle/standard/opentheory/compilation
Jun 03 23:19:49 Finished candle/standard/opentheory/compilation               29m33s  14GB
Jun 03 23:19:49 Starting candle/standard/opentheory/compilation/proofs
Jun 03 23:20:24 Finished candle/standard/opentheory/compilation/proofs           34s   2GB
Jun 03 23:20:24 Starting characteristic/examples
Jun 03 23:21:46 Finished characteristic/examples                               1m21s   2GB
Jun 03 23:21:46 Starting tutorial/solutions
Jun 03 23:34:47 Finished tutorial/solutions                                   13m00s   7GB
Jun 03 23:34:47 Starting translator/monadic/examples
Jun 03 23:37:36 Finished translator/monadic/examples                           2m47s   2GB
Jun 03 23:37:36 Starting examples
Jun 03 23:40:53 FAILED: examples
]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/formal-languages]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-911/basis]0;Holmake: ~/regression/cakeml-911/basis/pure]0;Holmake: ~/regression/cakeml-911/misc]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-911/misc]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-6cd76208fd222c4b36e3e37b86df4a075b17df4f/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-911/misc]0;Holmake: ~/regression/cakeml-911/developers]0;Holmake: ~/regression/cakeml-911/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-911/misc]0;Holmake: ~/regression/cakeml-911/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-911/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-911/misc]0;Holmake: ~/regression/cakeml-911/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-911/basis/pure]0;Holmake: ~/regression/cakeml-911/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-911/basis]0;Holmake: ~/regression/cakeml-911/characteristic]0;Holmake: ~/regression/cakeml-911/compiler/parsing]0;Holmake: ~/regression/cakeml-911/semantics]0;Holmake: ~/regression/cakeml-911/semantics/ffi]0;Holmake: ~/regression/cakeml-911/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-911/semantics]0;Holmake: ~/regression/cakeml-911/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-911/compiler/parsing]0;Holmake: ~/regression/cakeml-911/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-911/characteristic]0;Holmake: ~/regression/cakeml-911/semantics/proofs]0;Holmake: ~/regression/cakeml-911/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-911/characteristic]0;Holmake: ~/regression/cakeml-911/translator]0;Holmake: ~/regression/cakeml-911/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-911/characteristic]0;Holmake: ~/regression/cakeml-911/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-911/basis]0;Holmake: ~/regression/cakeml-911/translator/monadic]0;Holmake: ~/regression/cakeml-911/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-911/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-911/translator/monadic]0;Holmake: ~/regression/cakeml-911/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-911/basis]0;Holmake: ~/regression/cakeml-911/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on divTheory
lcsTheory                                           OK
Starting work on diffTheory
diffTheory                                          OK
Starting work on diffProgTheory
catProgTheory                                       OK
Starting work on doubleProgTheory
quicksortProgTheory                                 OK
Starting work on array_searchProgTheory
divTheory                                           OK
Starting work on echoProgTheory
diffProgTheory                                      OK
Starting work on filterProgTheory
doubleProgTheory                                    OK
Starting work on grepProgTheory
filterProgTheory                           FAILED! <1>
   pattern completion has added 1 clause to the original specification.>>
 <<HOL message: mk_functional: 
   pattern completion has added 1 clause to the original specification.>>
 <<HOL message: Created theory "filterProg">>
 Loading translation: MapProg ... done.
 /home/myreen/regression/cakeml-911/examples/filterProgScript.sml:34: error: Value or constructor (mk_regexp) has not been declared in structure regexpSyntax
 Found near regexpSyntax.mk_regexp r
 error in quse /home/myreen/regression/cakeml-911/examples/filterProgScript.sml : Fail "Static Errors"
 error in load filterProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
array_searchProgTheory                        M-KILLED
echoProgTheory                                M-KILLED
grepProgTheory                                M-KILLED