Job 2040

CakeML:fd0b08a39c3fdb8cafa91b67d465b395600c261b
  Fix do_app_thm in pull_words [Nov 15 06:52:07]
#911 (libm_gen)
Merging into:3d27e77937edd037e810801a4e7849352300104f
  Add [schematic] to a definition (suggested by @mn200) [Nov 07 20:36:24]
HOL:126d898e2a2195a717f5757375b93570965286f1
  Cleanup and tweak release notes for next version in a few places [Nov 03 06:41:06]
Machine:oven3

Nov 15 06:52:34 Claimed job
Nov 15 06:52:37 Reusing HOL
Nov 15 06:53:30 Starting developers
Nov 15 06:53:40 Finished developers                                               9s 151MB
Nov 15 06:53:40 Starting developers/bin
Nov 15 06:53:52 Finished developers/bin                                          11s   1GB
Nov 15 06:53:52 Starting compiler/proofs
Nov 15 10:19:52 Finished compiler/proofs                                    3h25m58s  20GB
Nov 15 10:19:52 Starting compiler/bootstrap/translation
Nov 15 20:55:56 Finished compiler/bootstrap/translation                    10h36m03s  79GB
Nov 15 20:55:56 Starting semantics/ffi
Nov 15 20:56:07 Finished semantics/ffi                                           10s 140MB
Nov 15 20:56:07 Starting semantics
Nov 15 20:56:09 Finished semantics                                                2s  33MB
Nov 15 20:56:10 Starting semantics/proofs
Nov 15 20:57:26 Finished semantics/proofs                                      1m16s 613MB
Nov 15 20:57:26 Starting semantics/alt_semantics
Nov 15 20:58:24 Finished semantics/alt_semantics                                 57s 579MB
Nov 15 20:58:24 Starting semantics/alt_semantics/proofs
Nov 15 21:24:33 Finished semantics/alt_semantics/proofs                       26m08s   1GB
Nov 15 21:24:33 Starting basis/pure
Nov 15 21:24:35 Finished basis/pure                                               2s  34MB
Nov 15 21:24:36 Starting translator
Nov 15 21:28:17 Finished translator                                            3m40s   1GB
Nov 15 21:28:17 Starting compiler/parsing
Nov 15 21:28:20 Finished compiler/parsing                                         2s  19MB
Nov 15 21:28:20 Starting characteristic
Nov 15 21:28:23 Finished characteristic                                           3s  26MB
Nov 15 21:28:24 Starting translator/monadic
Nov 15 21:28:27 Finished translator/monadic                                       2s  28MB
Nov 15 21:28:27 Starting basis
Nov 15 21:36:06 Finished basis                                                 7m38s   3GB
Nov 15 21:36:06 Starting compiler/inference
Nov 15 21:36:09 Finished compiler/inference                                       2s  34MB
Nov 15 21:36:09 Starting compiler/backend/reg_alloc
Nov 15 21:36:12 Finished compiler/backend/reg_alloc                               2s  17MB
Nov 15 21:36:12 Starting compiler/backend/gc
Nov 15 21:36:16 Finished compiler/backend/gc                                      3s  32MB
Nov 15 21:36:16 Starting compiler/backend
Nov 15 21:36:40 Finished compiler/backend                                        23s 524MB
Nov 15 21:36:40 Starting compiler/encoders/asm
Nov 15 21:36:43 Finished compiler/encoders/asm                                    2s  24MB
Nov 15 21:36:43 Starting compiler/encoders/x64
Nov 15 21:36:46 Finished compiler/encoders/x64                                    2s  26MB
Nov 15 21:36:47 Starting compiler/encoders/arm7
Nov 15 21:36:50 Finished compiler/encoders/arm7                                   2s  27MB
Nov 15 21:36:50 Starting compiler/encoders/arm8
Nov 15 21:36:53 Finished compiler/encoders/arm8                                   2s  28MB
Nov 15 21:36:53 Starting compiler/encoders/arm8_asl
Nov 15 21:44:34 Finished compiler/encoders/arm8_asl                            7m40s   1GB
Nov 15 21:44:34 Starting compiler/encoders/mips
Nov 15 21:44:37 Finished compiler/encoders/mips                                   2s  26MB
Nov 15 21:44:37 Starting compiler/encoders/riscv
Nov 15 21:44:40 Finished compiler/encoders/riscv                                  2s  23MB
Nov 15 21:44:40 Starting compiler/encoders/ag32
Nov 15 21:44:43 Finished compiler/encoders/ag32                                   2s  26MB
Nov 15 21:44:43 Starting compiler/backend/x64
Nov 15 21:44:47 Finished compiler/backend/x64                                     3s  32MB
Nov 15 21:44:48 Starting compiler/backend/arm7
Nov 15 21:44:51 Finished compiler/backend/arm7                                    3s  33MB
Nov 15 21:44:52 Starting compiler/backend/arm8
Nov 15 21:44:55 Finished compiler/backend/arm8                                    3s  32MB
Nov 15 21:44:56 Starting compiler/backend/mips
Nov 15 21:44:59 Finished compiler/backend/mips                                    3s  32MB
Nov 15 21:45:00 Starting compiler/backend/riscv
Nov 15 21:45:03 Finished compiler/backend/riscv                                   3s  33MB
Nov 15 21:45:04 Starting compiler/backend/ag32
Nov 15 21:48:04 Finished compiler/backend/ag32                                 2m59s   1GB
Nov 15 21:48:04 Starting compiler/parsing/proofs
Nov 15 21:48:07 Finished compiler/parsing/proofs                                  2s  24MB
Nov 15 21:48:07 Starting compiler/inference/proofs
Nov 15 21:48:10 Finished compiler/inference/proofs                                2s  30MB
Nov 15 21:48:10 Starting compiler/backend/semantics
Nov 15 21:50:35 Finished compiler/backend/semantics                            2m24s   1GB
Nov 15 21:50:35 Starting compiler/backend/reg_alloc/proofs
Nov 15 21:50:38 Finished compiler/backend/reg_alloc/proofs                        3s  34MB
Nov 15 21:50:39 Starting compiler/backend/proofs
Nov 15 21:52:33 Finished compiler/backend/proofs                               1m54s   2GB
Nov 15 21:52:34 Starting compiler/backend/serialiser
Nov 15 21:52:39 Finished compiler/backend/serialiser                              5s  52MB
Nov 15 21:52:39 Starting compiler/encoders/x64/proofs
Nov 15 22:14:47 Finished compiler/encoders/x64/proofs                         22m06s   4GB
Nov 15 22:14:47 Starting compiler/encoders/arm7/proofs
Nov 15 22:45:52 Finished compiler/encoders/arm7/proofs                        31m04s   3GB
Nov 15 22:45:52 Starting compiler/encoders/arm8/proofs
Nov 15 23:01:52 Finished compiler/encoders/arm8/proofs                        15m59s   1GB
Nov 15 23:01:52 Starting compiler/encoders/arm8_asl/proofs
Nov 15 23:37:42 Finished compiler/encoders/arm8_asl/proofs                    35m49s   2GB
Nov 15 23:37:43 Starting compiler/encoders/mips/proofs
Nov 16 00:01:40 Finished compiler/encoders/mips/proofs                        23m56s   2GB
Nov 16 00:01:40 Starting compiler/encoders/riscv/proofs
Nov 16 00:22:26 Finished compiler/encoders/riscv/proofs                       20m46s   1GB
Nov 16 00:22:27 Starting compiler/encoders/ag32/proofs
Nov 16 00:28:24 Finished compiler/encoders/ag32/proofs                         5m56s   1GB
Nov 16 00:28:24 Starting compiler/backend/x64/proofs
Nov 16 00:29:20 Finished compiler/backend/x64/proofs                             55s   1GB
Nov 16 00:29:20 Starting compiler/backend/arm7/proofs
Nov 16 00:30:17 Finished compiler/backend/arm7/proofs                            56s   1GB
Nov 16 00:30:17 Starting compiler/backend/arm8/proofs
Nov 16 00:31:13 Finished compiler/backend/arm8/proofs                            56s   2GB
Nov 16 00:31:14 Starting compiler/backend/arm8_asl
Nov 16 00:31:57 Finished compiler/backend/arm8_asl                               43s   1GB
Nov 16 00:31:58 Starting compiler/backend/mips/proofs
Nov 16 00:32:55 Finished compiler/backend/mips/proofs                            56s   1GB
Nov 16 00:32:55 Starting compiler/backend/riscv/proofs
Nov 16 00:33:50 Finished compiler/backend/riscv/proofs                           54s   1GB
Nov 16 00:33:50 Starting compiler/backend/ag32/proofs
Nov 16 01:03:54 Finished compiler/backend/ag32/proofs                         30m03s   3GB
Nov 16 01:03:54 Starting candle/set-theory
Nov 16 01:05:02 Finished candle/set-theory                                     1m07s   1GB
Nov 16 01:05:02 Starting candle/syntax-lib
Nov 16 01:05:05 Finished candle/syntax-lib                                        2s  34MB
Nov 16 01:05:05 Starting candle/standard/syntax
Nov 16 01:05:25 Finished candle/standard/syntax                                  20s 544MB
Nov 16 01:05:26 Starting candle/standard/semantics
Nov 16 01:09:20 Finished candle/standard/semantics                             3m53s   1GB
Nov 16 01:09:20 Starting candle/standard/monadic
Nov 16 01:09:24 Finished candle/standard/monadic                                  3s  33MB
Nov 16 01:09:24 Starting candle/standard/ml_kernel
Nov 16 01:12:25 Finished candle/standard/ml_kernel                             3m01s   3GB
Nov 16 01:12:26 Starting candle/overloading/syntax
Nov 16 01:19:34 Finished candle/overloading/syntax                             7m08s   1GB
Nov 16 01:19:35 Starting candle/overloading/semantics
Nov 16 01:46:10 Finished candle/overloading/semantics                         26m34s   2GB
Nov 16 01:46:10 Starting candle/overloading/monadic
Nov 16 01:51:36 Finished candle/overloading/monadic                            5m26s   1GB
Nov 16 01:51:36 Starting candle/overloading/ml_kernel
Nov 16 02:07:28 Finished candle/overloading/ml_kernel                         15m51s   4GB
Nov 16 02:07:29 Starting candle/overloading/ml_checker
Nov 16 02:13:02 Finished candle/overloading/ml_checker                         5m33s   2GB
Nov 16 02:13:03 Starting candle/prover
Nov 16 02:35:38 Finished candle/prover                                        22m34s   3GB
Nov 16 02:35:38 Starting pancake
Nov 16 02:41:52 Finished pancake                                               6m13s   3GB
Nov 16 02:41:52 Starting pancake/ffi
Nov 16 02:41:53 Finished pancake/ffi                                              0s  11MB
Nov 16 02:41:53 Starting pancake/semantics
Nov 16 02:46:58 Finished pancake/semantics                                     5m04s   1GB
Nov 16 02:46:59 Starting pancake/proofs
Nov 16 02:53:16 Finished pancake/proofs                                        6m16s   1GB
Nov 16 02:53:16 Starting characteristic/examples
Nov 16 02:56:16 Finished characteristic/examples                               3m00s   2GB
Nov 16 02:56:17 Starting tutorial/solutions
Nov 16 03:30:51 Finished tutorial/solutions                                   34m34s   9GB
Nov 16 03:30:51 Starting translator/monadic/examples
Nov 16 03:37:44 Finished translator/monadic/examples                           6m52s   2GB
Nov 16 03:37:44 Starting examples
Nov 16 03:56:30 Finished examples                                             18m45s   4GB
Nov 16 03:56:30 Starting examples/compilation/x64
Nov 16 08:34:10 Finished examples/compilation/x64                           4h37m39s  23GB
Nov 16 08:34:10 Starting examples/compilation/x64/proofs
Nov 16 08:38:30 Finished examples/compilation/x64/proofs                       4m19s   3GB
Nov 16 08:38:30 Starting examples/compilation/ag32
Nov 16 09:52:48 Finished examples/compilation/ag32                          1h14m17s   9GB
Nov 16 09:52:48 Starting examples/compilation/ag32/proofs
Nov 16 09:54:28 Finished examples/compilation/ag32/proofs                      1m40s   3GB
Nov 16 09:54:29 Starting examples/compilation/to_word
Nov 16 10:01:18 Finished examples/compilation/to_word                          6m48s   6GB
Nov 16 10:01:18 Starting examples/lpr_checker
Nov 16 10:03:24 Finished examples/lpr_checker                                  2m05s 904MB
Nov 16 10:03:24 Starting examples/lpr_checker/array
Nov 16 11:22:24 Finished examples/lpr_checker/array                         1h18m58s   5GB
Nov 16 11:22:24 Starting examples/lpr_checker/array/compilation
Nov 16 12:45:04 Finished examples/lpr_checker/array/compilation             1h22m39s  37GB
Nov 16 12:45:04 Starting examples/lpr_checker/array/compilation/proofs
Nov 16 12:47:44 Finished examples/lpr_checker/array/compilation/proofs         2m39s   6GB
Nov 16 12:47:44 Starting examples/opentheory
Nov 16 13:09:58 Finished examples/opentheory                                  22m13s   5GB
Nov 16 13:09:58 Starting examples/opentheory
Nov 16 13:10:02 Finished examples/opentheory                                      3s  33MB
Nov 16 13:10:02 Starting examples/opentheory/compilation
Nov 16 14:37:51 Finished examples/opentheory/compilation                    1h27m48s  38GB
Nov 16 14:37:51 Starting examples/opentheory/compilation/proofs
Nov 16 14:39:54 Finished examples/opentheory/compilation/proofs                2m02s   3GB
Nov 16 14:39:54 Starting examples/opentheory/compilation/ag32
Nov 16 16:02:43 Finished examples/opentheory/compilation/ag32               1h22m48s  40GB
Nov 16 16:02:44 Starting examples/opentheory/compilation/ag32/proofs
Nov 16 16:06:20 Finished examples/opentheory/compilation/ag32/proofs           3m35s   5GB
Nov 16 16:06:20 Starting examples/sat_encodings
Nov 16 16:10:11 Finished examples/sat_encodings                                3m50s 781MB
Nov 16 16:10:12 Starting examples/sat_encodings/case_studies
Nov 16 16:13:50 Finished examples/sat_encodings/case_studies                   3m38s   1GB
Nov 16 16:13:51 Starting examples/sat_encodings/translation
Nov 16 16:25:34 Finished examples/sat_encodings/translation                   11m43s   5GB
Nov 16 16:25:35 Starting examples/sat_encodings/translation/compilation
Nov 16 17:52:33 Finished examples/sat_encodings/translation/compilation     1h26m57s  23GB
Nov 16 17:52:33 Starting examples/deflate
Nov 16 17:54:21 Finished examples/deflate                                      1m47s 811MB
Nov 16 17:54:21 Starting examples/deflate/translation
Nov 16 17:57:27 Finished examples/deflate/translation                          3m06s   3GB
Nov 16 17:57:28 Starting examples/deflate/translation/compilation
Nov 16 18:36:53 Finished examples/deflate/translation/compilation             39m25s  19GB
Nov 16 18:36:53 Starting translator/okasaki-examples
Nov 16 18:46:54 Finished translator/okasaki-examples                          10m00s   2GB
Nov 16 18:46:55 Starting translator/other-examples
Nov 16 18:48:21 Finished translator/other-examples                             1m26s   1GB
Nov 16 18:48:21 Starting compiler/parsing/tests
Nov 16 18:49:31 Finished compiler/parsing/tests                                1m09s 570MB
Nov 16 18:49:31 Starting compiler/inference/tests
Nov 16 19:06:02 Finished compiler/inference/tests                             16m30s   5GB
Nov 16 19:06:02 Starting compiler/printing/test
Nov 16 19:13:00 Finished compiler/printing/test                                6m58s   3GB
Nov 16 19:13:01 Starting floatingPoint/tools/flover
Nov 16 20:19:41 Finished floatingPoint/tools/flover                         1h06m39s   1GB
Nov 16 20:19:41 Starting floatingPoint/icing/
Nov 16 22:38:36 Finished floatingPoint/icing/                               2h18m54s   7GB
Nov 16 22:38:36 Starting floatingPoint/icing/examples
Nov 16 22:41:42 Finished floatingPoint/icing/examples                          3m05s   6GB
Nov 16 22:41:42 Starting floatingPoint/tools/dandelion
Nov 16 22:51:43 FAILED: floatingPoint/tools/dandelion
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/examples/algebra/monoid[0m
Scanning [1m$(HOLDIR)/examples/algebra/group[0m
Scanning [1m$(HOLDIR)/examples/algebra/ring[0m
Scanning [1m$(HOLDIR)/examples/algebra/field[0m
Scanning [1m$(HOLDIR)/examples/algebra/polynomial[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/Infra[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover/semantics[0m
Scanning [1m$(CAKEMLDIR)/floatingPoint/tools/flover[0m
Scanned 23 directories
Starting work on README.md
Starting work on moreRealTheory
Starting work on renameTheory
README.md                                                                                                                                                                                             (0s)     OK
renameTheory                                                                                                                                                                                         (32s)     OK
Starting work on realPolyTheory
Starting work on sturmTheory
moreRealTheory                                                                                                                                                                                       (49s)     OK
realPolyTheory                                                                                                                                                                                       (39s)     OK
Starting work on realPolyProofsTheory
Starting work on transcLangTheory
Starting work on floverConnTheory
floverConnTheory                                                                                                                                                                                     (35s)     OK
transcLangTheory                                                                                                                                                                                     (38s)     OK
Starting work on checkerDefsTheory
realPolyProofsTheory                                                                                                                                                                                 (42s)     OK
Starting work on mcLaurinApproxTheory
Starting work on transcReflectTheory
sturmTheory                                                                                                                                                                                          (89s)     OK
Starting work on drangTheory
checkerDefsTheory                                                                                                                                                                                    (39s)     OK
Starting work on pointCheckerTheory
transcReflectTheory                                                                                                                                                                                  (36s)     OK
Starting work on euclidDivTheory
drangTheory                                                                                                                                                                                          (39s)     OK
pointCheckerTheory                                                                                                                                                                                   (32s)     OK
Starting work on pointCheckerProofsTheory
euclidDivTheory                                                                                                                                                                                      (42s)     OK
Starting work on sturmComputeTheory
pointCheckerProofsTheory                                                                                                                                                                             (30s)     OK
sturmComputeTheory                                                                                                                                                                                   (30s)     OK
mcLaurinApproxTheory                                                                                                                                                                                (144s)     OK
Starting work on approxPolyTheory
approxPolyTheory                                                                                                                                                                                     (86s)     OK
Starting work on transcIntvSemTheory
transcIntvSemTheory                                                                                                                                                                                  (48s)     OK
Starting work on approxCompErrTheory
approxCompErrTheory                                                                                                                                                                                  (52s)     OK
Starting work on transcApproxSemTheory
transcApproxSemTheory                                                                                                                                                                                (49s)     OK
Starting work on checkerTheory
checkerTheory                                                                                                                                                                                        (42s)     OK
Starting work on cosDeg3Theory
Starting work on sinDeg3Theory
sinDeg3Theory                                                                                                                                                                                        (32s)FAIL<1>
 <<HOL message: Created theory "sinDeg3">>
 Saved definition ____ "sin_example_def"
 Testing sollya
 error in quse /local/regression_new/cakeml-2040/floatingPoint/tools/dandelion/sinDeg3Script.sml : Empty
 error in load /local/regression_new/cakeml-2040/floatingPoint/tools/dandelion/sinDeg3Script : Empty
 Uncaught exception: Empty
cosDeg3Theory                                                                                                                                                                                        (33s)MKILLED