Job 912

CakeML:38556cc97d26ac563f2b30eac5c1f3f12ff77587
  Merge pull request #657 from CakeML/fp_translation [May 30 07:20:00]
HOL:52d62131e6d5569360e8eee918011d10af7912e0
  Merge remote-tracking branch 'origin/develop' into thibault-wip [Jun 03 20:17:39]
Machine:brain08 4.14.89.1.amd64-smp x86_64 GNU/Linux

Jun 04 09:37:39 Claimed job
Jun 04 09:37:45 Building HOL
Jun 04 09:53:04 Starting developers
Jun 04 09:53:05 Finished developers                                               1s  34MB
Jun 04 09:53:05 Starting developers/bin
Jun 04 09:53:14 Finished developers/bin                                           8s 927MB
Jun 04 09:53:14 Starting semantics/ffi
Jun 04 09:54:25 Finished semantics/ffi                                         1m10s 600MB
Jun 04 09:54:25 Starting semantics
Jun 04 09:57:21 Finished semantics                                             2m55s   1GB
Jun 04 09:57:21 Starting semantics/proofs
Jun 04 10:03:23 Finished semantics/proofs                                      6m01s   1GB
Jun 04 10:03:23 Starting semantics/alt_semantics
Jun 04 10:03:35 Finished semantics/alt_semantics                                 12s 293MB
Jun 04 10:03:36 Starting semantics/alt_semantics/proofs
Jun 04 10:07:05 Finished semantics/alt_semantics/proofs                        3m28s   1GB
Jun 04 10:07:05 Starting basis/pure
Jun 04 10:13:51 Finished basis/pure                                            6m45s 738MB
Jun 04 10:13:51 Starting translator
Jun 04 10:17:06 Finished translator                                            3m14s   1GB
Jun 04 10:17:06 Starting compiler/parsing
Jun 04 10:18:52 Finished compiler/parsing                                      1m45s   1GB
Jun 04 10:18:52 Starting characteristic
Jun 04 10:29:15 Finished characteristic                                       10m23s   1GB
Jun 04 10:29:15 Starting translator/monadic
Jun 04 10:32:04 Finished translator/monadic                                    2m48s   1GB
Jun 04 10:32:04 Starting basis
Jun 04 11:03:59 Finished basis                                                31m54s   2GB
Jun 04 11:04:00 Starting compiler/inference
Jun 04 11:07:50 Finished compiler/inference                                    3m50s   1GB
Jun 04 11:07:50 Starting compiler/backend/reg_alloc
Jun 04 11:09:26 Finished compiler/backend/reg_alloc                            1m35s   1GB
Jun 04 11:09:26 Starting compiler/backend/gc
Jun 04 11:26:12 Finished compiler/backend/gc                                  16m46s   1GB
Jun 04 11:26:12 Starting compiler/backend
Jun 04 11:26:21 Finished compiler/backend                                         8s 288MB
Jun 04 11:26:21 Starting compiler/encoders/asm
Jun 04 11:26:22 Finished compiler/encoders/asm                                    0s  26MB
Jun 04 11:26:22 Starting compiler/encoders/x64
Jun 04 11:28:18 Finished compiler/encoders/x64                                 1m55s 878MB
Jun 04 11:28:18 Starting compiler/encoders/arm7
Jun 04 11:31:48 Finished compiler/encoders/arm7                                3m29s   2GB
Jun 04 11:31:48 Starting compiler/encoders/arm8
Jun 04 11:32:53 Finished compiler/encoders/arm8                                1m04s   1GB
Jun 04 11:32:53 Starting compiler/encoders/mips
Jun 04 11:35:04 Finished compiler/encoders/mips                                2m10s   1GB
Jun 04 11:35:04 Starting compiler/encoders/riscv
Jun 04 11:37:39 Finished compiler/encoders/riscv                               2m34s   1GB
Jun 04 11:37:39 Starting compiler/encoders/ag32
Jun 04 11:38:08 Finished compiler/encoders/ag32                                  29s 768MB
Jun 04 11:38:08 Starting compiler/backend/x64
Jun 04 11:38:48 Finished compiler/backend/x64                                    39s   1GB
Jun 04 11:38:48 Starting compiler/backend/arm7
Jun 04 11:39:31 Finished compiler/backend/arm7                                   42s   1GB
Jun 04 11:39:31 Starting compiler/backend/arm8
Jun 04 11:40:12 Finished compiler/backend/arm8                                   40s   1GB
Jun 04 11:40:13 Starting compiler/backend/mips
Jun 04 11:40:51 Finished compiler/backend/mips                                   37s   1GB
Jun 04 11:40:51 Starting compiler/backend/riscv
Jun 04 11:41:31 Finished compiler/backend/riscv                                  40s   1GB
Jun 04 11:41:32 Starting compiler/backend/ag32
Jun 04 11:43:47 Finished compiler/backend/ag32                                 2m15s   1GB
Jun 04 11:43:47 Starting compiler/parsing/proofs
Jun 04 11:54:30 Finished compiler/parsing/proofs                              10m42s 900MB
Jun 04 11:54:30 Starting compiler/inference/proofs
Jun 04 12:00:02 Finished compiler/inference/proofs                             5m31s   1GB
Jun 04 12:00:03 Starting compiler/backend/semantics
Jun 04 12:13:40 Finished compiler/backend/semantics                           13m37s   1GB
Jun 04 12:13:40 Starting compiler/backend/reg_alloc/proofs
Jun 04 12:20:32 Finished compiler/backend/reg_alloc/proofs                     6m51s   1GB
Jun 04 12:20:33 Starting compiler/backend/proofs
Jun 04 13:30:29 Finished compiler/backend/proofs                            1h09m55s   4GB
Jun 04 13:30:29 Starting compiler/encoders/x64/proofs
Jun 04 13:50:54 Finished compiler/encoders/x64/proofs                         20m24s   4GB
Jun 04 13:50:54 Starting compiler/encoders/arm7/proofs
Jun 04 14:19:06 Finished compiler/encoders/arm7/proofs                        28m12s   4GB
Jun 04 14:19:07 Starting compiler/encoders/arm8/proofs
Jun 04 14:32:44 Finished compiler/encoders/arm8/proofs                        13m37s   1GB
Jun 04 14:32:45 Starting compiler/encoders/mips/proofs
Jun 04 14:52:50 Finished compiler/encoders/mips/proofs                        20m04s   2GB
Jun 04 14:52:50 Starting compiler/encoders/riscv/proofs
Jun 04 15:09:50 Finished compiler/encoders/riscv/proofs                       16m59s   1GB
Jun 04 15:09:50 Starting compiler/encoders/ag32/proofs
Jun 04 15:14:46 Finished compiler/encoders/ag32/proofs                         4m55s 812MB
Jun 04 15:14:46 Starting compiler/backend/x64/proofs
Jun 04 15:15:28 Finished compiler/backend/x64/proofs                             41s   1GB
Jun 04 15:15:28 Starting compiler/backend/arm7/proofs
Jun 04 15:16:06 Finished compiler/backend/arm7/proofs                            38s 912MB
Jun 04 15:16:06 Starting compiler/backend/arm8/proofs
Jun 04 15:16:45 Finished compiler/backend/arm8/proofs                            38s   1GB
Jun 04 15:16:46 Starting compiler/backend/mips/proofs
Jun 04 15:17:28 Finished compiler/backend/mips/proofs                            42s   1GB
Jun 04 15:17:28 Starting compiler/backend/riscv/proofs
Jun 04 15:18:10 Finished compiler/backend/riscv/proofs                           41s   1GB
Jun 04 15:18:10 Starting compiler/backend/ag32/proofs
Jun 04 15:36:11 Finished compiler/backend/ag32/proofs                         18m00s   1GB
Jun 04 15:36:11 Starting compiler/proofs
Jun 04 15:38:40 Finished compiler/proofs                                       2m28s   2GB
Jun 04 15:38:40 Starting candle/set-theory
Jun 04 15:39:29 Finished candle/set-theory                                       48s 674MB
Jun 04 15:39:29 Starting candle/syntax-lib
Jun 04 15:39:52 Finished candle/syntax-lib                                       22s 600MB
Jun 04 15:39:52 Starting candle/standard/syntax
Jun 04 15:43:14 Finished candle/standard/syntax                                3m22s   1GB
Jun 04 15:43:15 Starting candle/standard/semantics
Jun 04 15:46:28 Finished candle/standard/semantics                             3m13s   1GB
Jun 04 15:46:28 Starting candle/standard/monadic
Jun 04 15:49:43 Finished candle/standard/monadic                               3m14s   1GB
Jun 04 15:49:44 Starting candle/standard/ml_kernel
Jun 04 15:57:16 Finished candle/standard/ml_kernel                             7m31s   3GB
Jun 04 15:57:16 Starting candle/standard/opentheory
Jun 04 16:14:38 Finished candle/standard/opentheory                           17m21s   3GB
Jun 04 16:14:38 Starting candle/standard/opentheory/compilation
Jun 04 17:07:19 Finished candle/standard/opentheory/compilation               52m41s  12GB
Jun 04 17:07:20 Starting candle/standard/opentheory/compilation/proofs
Jun 04 17:08:56 Finished candle/standard/opentheory/compilation/proofs         1m35s   2GB
Jun 04 17:08:56 Starting characteristic/examples
Jun 04 17:11:53 Finished characteristic/examples                               2m57s   2GB
Jun 04 17:11:54 Starting tutorial/solutions
Jun 04 17:37:50 Finished tutorial/solutions                                   25m56s   5GB
Jun 04 17:37:51 Starting translator/monadic/examples
Jun 04 17:42:21 Finished translator/monadic/examples                           4m30s   2GB
Jun 04 17:42:21 Starting examples
Jun 04 17:47:26 FAILED: examples
]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/formal-languages]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/formal-languages/context-free]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
Starting work on regexp2dfa
regexp2dfa                                                                                                                       OK
]0;Holmake: .]0;Holmake: /local/hbecker/regression/cakeml-912/basis]0;Holmake: /local/hbecker/regression/cakeml-912/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-912/misc]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/fun-op-sem/lprefix_lub]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: /local/hbecker/regression/cakeml-912/misc]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/machine-code/hoare-triple]0;Holmake: /local/hbecker/regression/HOL-52d62131e6d5569360e8eee918011d10af7912e0/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: /local/hbecker/regression/cakeml-912/misc]0;Holmake: /local/hbecker/regression/cakeml-912/developers]0;Holmake: /local/hbecker/regression/cakeml-912/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: /local/hbecker/regression/cakeml-912/misc]0;Holmake: /local/hbecker/regression/cakeml-912/misc/lem_lib_stub]0;Holmake: /local/hbecker/regression/cakeml-912/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: /local/hbecker/regression/cakeml-912/misc]0;Holmake: /local/hbecker/regression/cakeml-912/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: /local/hbecker/regression/cakeml-912/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-912/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: /local/hbecker/regression/cakeml-912/basis]0;Holmake: /local/hbecker/regression/cakeml-912/characteristic]0;Holmake: /local/hbecker/regression/cakeml-912/compiler/parsing]0;Holmake: /local/hbecker/regression/cakeml-912/semantics]0;Holmake: /local/hbecker/regression/cakeml-912/semantics/ffi]0;Holmake: /local/hbecker/regression/cakeml-912/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: /local/hbecker/regression/cakeml-912/semantics]0;Holmake: /local/hbecker/regression/cakeml-912/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: /local/hbecker/regression/cakeml-912/compiler/parsing]0;Holmake: /local/hbecker/regression/cakeml-912/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: /local/hbecker/regression/cakeml-912/characteristic]0;Holmake: /local/hbecker/regression/cakeml-912/semantics/proofs]0;Holmake: /local/hbecker/regression/cakeml-912/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: /local/hbecker/regression/cakeml-912/characteristic]0;Holmake: /local/hbecker/regression/cakeml-912/translator]0;Holmake: /local/hbecker/regression/cakeml-912/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: /local/hbecker/regression/cakeml-912/characteristic]0;Holmake: /local/hbecker/regression/cakeml-912/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: /local/hbecker/regression/cakeml-912/basis]0;Holmake: /local/hbecker/regression/cakeml-912/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-912/translator/monadic/monad_base]0;Holmake: /local/hbecker/regression/cakeml-912/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: /local/hbecker/regression/cakeml-912/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-912/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: /local/hbecker/regression/cakeml-912/basis]0;Holmake: /local/hbecker/regression/cakeml-912/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/examples
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
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.
 error in quse /local/hbecker/regression/cakeml-912/examples/filterProgScript.sml : Fail "Static Errors"
 error in load filterProgScript : Fail "Static Errors"
 /local/hbecker/regression/cakeml-912/examples/filterProgScript.sml:34: error: Value or constructor (mk_regexp) has not been declared in structure regexpSyntax
 Found near regexpSyntax.mk_regexp r
 Uncaught exception: Fail "Static Errors"
doubleProgTheory                                                                                                           M-KILLED
array_searchProgTheory                                                                                                     M-KILLED
echoProgTheory                                                                                                             M-KILLED