Job 1081

CakeML:05a85a96ad0702868b7b20ad1701f38ab7b37e9b
  Add numerator and denominator functions to Ratio [Nov 06 12:58:14]
#698 (cakeml-rat-proj)
Merging into:a0a73be366a40123567f97a747fbaffa114b6352
  Merge pull request #700 from CakeML/iocatprog-fix [Nov 10 16:39:33]
HOL:98729fa718256b0fa48d19ca8a978029674fe5a9
  Clean an AKS theory for --expk; examples/AKS now builds there [Nov 11 23:10:55]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Nov 12 23:16:18 Claimed job
Nov 12 23:16:22 Building HOL
Nov 12 23:26:41 Starting developers
Nov 12 23:26:45 Finished developers                                               3s 149MB
Nov 12 23:26:45 Starting developers/bin
Nov 12 23:26:51 Finished developers/bin                                           5s 964MB
Nov 12 23:26:51 Starting semantics/ffi
Nov 12 23:27:00 Finished semantics/ffi                                            9s 231MB
Nov 12 23:27:00 Starting semantics
Nov 12 23:28:22 Finished semantics                                             1m21s   1GB
Nov 12 23:28:22 Starting semantics/proofs
Nov 12 23:31:11 Finished semantics/proofs                                      2m48s   1GB
Nov 12 23:31:11 Starting semantics/alt_semantics
Nov 12 23:31:19 Finished semantics/alt_semantics                                  7s 290MB
Nov 12 23:31:19 Starting semantics/alt_semantics/proofs
Nov 12 23:33:02 Finished semantics/alt_semantics/proofs                        1m43s 800MB
Nov 12 23:33:02 Starting basis/pure
Nov 12 23:35:39 Finished basis/pure                                            2m36s 816MB
Nov 12 23:35:39 Starting translator
Nov 12 23:37:20 Finished translator                                            1m41s   1GB
Nov 12 23:37:20 Starting compiler/parsing
Nov 12 23:38:16 Finished compiler/parsing                                        56s   3GB
Nov 12 23:38:16 Starting characteristic
Nov 12 23:43:24 Finished characteristic                                        5m07s   1GB
Nov 12 23:43:24 Starting translator/monadic
Nov 12 23:44:50 Finished translator/monadic                                    1m25s   1GB
Nov 12 23:44:50 Starting basis
Nov 13 00:03:13 Finished basis                                                18m23s   2GB
Nov 13 00:03:13 Starting compiler/inference
Nov 13 00:04:54 Finished compiler/inference                                    1m40s   1GB
Nov 13 00:04:54 Starting compiler/backend/reg_alloc
Nov 13 00:05:50 Finished compiler/backend/reg_alloc                              56s   1GB
Nov 13 00:05:50 Starting compiler/backend/gc
Nov 13 00:08:52 Finished compiler/backend/gc                                   3m01s   2GB
Nov 13 00:08:52 Starting compiler/backend
Nov 13 00:12:22 Finished compiler/backend                                      3m30s   2GB
Nov 13 00:12:22 Starting compiler/encoders/asm
Nov 13 00:12:42 Finished compiler/encoders/asm                                   19s 817MB
Nov 13 00:12:42 Starting compiler/encoders/x64
Nov 13 00:13:33 Finished compiler/encoders/x64                                   51s 962MB
Nov 13 00:13:33 Starting compiler/encoders/arm7
Nov 13 00:15:07 Finished compiler/encoders/arm7                                1m33s   1GB
Nov 13 00:15:07 Starting compiler/encoders/arm8
Nov 13 00:15:38 Finished compiler/encoders/arm8                                  30s 874MB
Nov 13 00:15:38 Starting compiler/encoders/mips
Nov 13 00:16:42 Finished compiler/encoders/mips                                1m04s   1GB
Nov 13 00:16:43 Starting compiler/encoders/riscv
Nov 13 00:17:55 Finished compiler/encoders/riscv                               1m12s 947MB
Nov 13 00:17:55 Starting compiler/encoders/ag32
Nov 13 00:18:10 Finished compiler/encoders/ag32                                  15s 787MB
Nov 13 00:18:10 Starting compiler/backend/x64
Nov 13 00:18:27 Finished compiler/backend/x64                                    16s   1GB
Nov 13 00:18:27 Starting compiler/backend/arm7
Nov 13 00:18:45 Finished compiler/backend/arm7                                   17s   1GB
Nov 13 00:18:45 Starting compiler/backend/arm8
Nov 13 00:19:01 Finished compiler/backend/arm8                                   16s   1GB
Nov 13 00:19:01 Starting compiler/backend/mips
Nov 13 00:19:18 Finished compiler/backend/mips                                   16s   1GB
Nov 13 00:19:18 Starting compiler/backend/riscv
Nov 13 00:19:35 Finished compiler/backend/riscv                                  17s   1GB
Nov 13 00:19:35 Starting compiler/backend/ag32
Nov 13 00:20:37 Finished compiler/backend/ag32                                 1m02s   1GB
Nov 13 00:20:37 Starting compiler/parsing/proofs
Nov 13 00:25:54 Finished compiler/parsing/proofs                               5m17s   1GB
Nov 13 00:25:54 Starting compiler/inference/proofs
Nov 13 00:28:34 Finished compiler/inference/proofs                             2m39s   1GB
Nov 13 00:28:34 Starting compiler/backend/semantics
Nov 13 00:34:05 Finished compiler/backend/semantics                            5m30s   2GB
Nov 13 00:34:05 Starting compiler/backend/reg_alloc/proofs
Nov 13 00:37:12 Finished compiler/backend/reg_alloc/proofs                     3m07s   1GB
Nov 13 00:37:12 Starting compiler/backend/proofs
Nov 13 01:14:04 Finished compiler/backend/proofs                              36m51s   5GB
Nov 13 01:14:04 Starting compiler/encoders/x64/proofs
Nov 13 01:22:35 Finished compiler/encoders/x64/proofs                          8m31s   4GB
Nov 13 01:22:35 Starting compiler/encoders/arm7/proofs
Nov 13 01:34:02 Finished compiler/encoders/arm7/proofs                        11m26s   3GB
Nov 13 01:34:02 Starting compiler/encoders/arm8/proofs
Nov 13 01:39:55 Finished compiler/encoders/arm8/proofs                         5m53s   1GB
Nov 13 01:39:55 Starting compiler/encoders/mips/proofs
Nov 13 01:48:35 Finished compiler/encoders/mips/proofs                         8m39s   2GB
Nov 13 01:48:35 Starting compiler/encoders/riscv/proofs
Nov 13 01:56:26 Finished compiler/encoders/riscv/proofs                        7m50s   1GB
Nov 13 01:56:26 Starting compiler/encoders/ag32/proofs
Nov 13 01:58:43 Finished compiler/encoders/ag32/proofs                         2m17s 758MB
Nov 13 01:58:43 Starting compiler/backend/x64/proofs
Nov 13 01:59:00 Finished compiler/backend/x64/proofs                             16s 986MB
Nov 13 01:59:00 Starting compiler/backend/arm7/proofs
Nov 13 01:59:18 Finished compiler/backend/arm7/proofs                            17s   1GB
Nov 13 01:59:18 Starting compiler/backend/arm8/proofs
Nov 13 01:59:35 Finished compiler/backend/arm8/proofs                            16s   1GB
Nov 13 01:59:35 Starting compiler/backend/mips/proofs
Nov 13 01:59:53 Finished compiler/backend/mips/proofs                            17s   1GB
Nov 13 01:59:53 Starting compiler/backend/riscv/proofs
Nov 13 02:00:09 Finished compiler/backend/riscv/proofs                           16s   1GB
Nov 13 02:00:10 Starting compiler/backend/ag32/proofs
Nov 13 02:08:30 Finished compiler/backend/ag32/proofs                          8m20s   2GB
Nov 13 02:08:30 Starting compiler/proofs
Nov 13 02:10:02 Finished compiler/proofs                                       1m31s   3GB
Nov 13 02:10:02 Starting candle/set-theory
Nov 13 02:10:28 Finished candle/set-theory                                       25s 678MB
Nov 13 02:10:28 Starting candle/syntax-lib
Nov 13 02:10:38 Finished candle/syntax-lib                                        9s 472MB
Nov 13 02:10:38 Starting candle/standard/syntax
Nov 13 02:12:16 Finished candle/standard/syntax                                1m37s 986MB
Nov 13 02:12:16 Starting candle/standard/semantics
Nov 13 02:13:48 Finished candle/standard/semantics                             1m32s   1GB
Nov 13 02:13:48 Starting candle/standard/monadic
Nov 13 02:15:16 Finished candle/standard/monadic                               1m27s   1GB
Nov 13 02:15:16 Starting candle/standard/ml_kernel
Nov 13 02:19:00 Finished candle/standard/ml_kernel                             3m44s   6GB
Nov 13 02:19:01 Starting candle/standard/opentheory
Nov 13 02:27:19 Finished candle/standard/opentheory                            8m18s   5GB
Nov 13 02:27:19 Starting candle/standard/opentheory/compilation
Nov 13 02:54:48 Finished candle/standard/opentheory/compilation               27m28s  23GB
Nov 13 02:54:48 Starting candle/standard/opentheory/compilation/proofs
Nov 13 02:55:22 Finished candle/standard/opentheory/compilation/proofs           33s   3GB
Nov 13 02:55:22 Starting characteristic/examples
Nov 13 02:56:45 Finished characteristic/examples                               1m22s   2GB
Nov 13 02:56:45 Starting tutorial/solutions
Nov 13 03:09:22 Finished tutorial/solutions                                   12m37s   6GB
Nov 13 03:09:22 Starting translator/monadic/examples
Nov 13 03:12:03 Finished translator/monadic/examples                           2m40s   2GB
Nov 13 03:12:03 Starting examples
Nov 13 03:20:06 Finished examples                                              8m03s   4GB
Nov 13 03:20:07 Starting examples/compilation/x64
Nov 13 05:17:49 Finished examples/compilation/x64                           1h57m42s  19GB
Nov 13 05:17:49 Starting examples/compilation/x64/proofs
Nov 13 05:19:49 Finished examples/compilation/x64/proofs                       1m59s   2GB
Nov 13 05:19:49 Starting examples/compilation/ag32
Nov 13 05:46:44 Finished examples/compilation/ag32                            26m54s   6GB
Nov 13 05:46:44 Starting examples/compilation/ag32/proofs
Nov 13 05:47:31 Finished examples/compilation/ag32/proofs                        46s   2GB
Nov 13 05:47:31 Starting translator/okasaki-examples
Nov 13 05:51:20 Finished translator/okasaki-examples                           3m48s   1GB
Nov 13 05:51:20 Starting translator/other-examples
Nov 13 05:53:00 Finished translator/other-examples                             1m40s   1GB
Nov 13 05:53:00 Starting compiler/parsing/tests
Nov 13 05:53:25 Finished compiler/parsing/tests                                  24s 618MB
Nov 13 05:53:25 Starting compiler/inference/tests
Nov 13 05:57:26 Finished compiler/inference/tests                              4m01s   4GB
Nov 13 05:57:26 Starting compiler/bootstrap/translation
Nov 13 08:20:44 Finished compiler/bootstrap/translation                     2h23m17s  40GB
Nov 13 08:20:44 Starting unverified/sexpr-bootstrap/x64/64
Nov 13 08:33:00 FAILED: unverified/sexpr-bootstrap/x64/64
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/developers/bin[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Starting work on README.md
Starting work on cake-sexpr-x64-64
README.md                                       real:    0s  user:    0s     OK
cake-sexpr-x64-64                               real:  110s  user:  106s     OK
Starting work on cake.S
cake.S                                          real:  614s  user:  587s     OK
Starting work on cake
cake                                            real:    5s  user:    4sFAIL<2>
 cake.S:(.text+0x1092331): undefined reference to `ffiget_arg_count'
 /tmp/cc2VOc4k.o: In function `windows_ffiwrite':
 cake.S:(.text+0x1092342): undefined reference to `ffiwrite'
 /tmp/cc2VOc4k.o: In function `windows_ffiread':
 cake.S:(.text+0x1092353): undefined reference to `ffiread'
 /tmp/cc2VOc4k.o: In function `windows_ffi':
 cake.S:(.text+0x1092364): undefined reference to `ffi'
 collect2: error: ld returned 1 exit status
 make: *** [/home/cur/sao/cakeml/regression/cakeml-1081/unverified/sexpr-bootstrap/x64/64/cake] Error 1
 <builtin>: recipe for target '/home/cur/sao/cakeml/regression/cakeml-1081/unverified/sexpr-bootstrap/x64/64/cake' failed