Job 1086

CakeML:2680f32a69334bea368d0928d98b6f1fccd1f15d
  Fix translation of parserProg given new validAddSym constant [Nov 12 05:58:45]
#695 (ocaml-infixes)
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:oven3 4.19.67.1.amd64-smp

Nov 13 08:31:30 Claimed job
Nov 13 08:31:33 Reusing HOL
Nov 13 08:32:44 Starting developers
Nov 13 08:32:51 Finished developers                                               6s 124MB
Nov 13 08:32:51 Starting developers/bin
Nov 13 08:33:04 Finished developers/bin                                          13s 966MB
Nov 13 08:33:04 Starting semantics/ffi
Nov 13 08:33:27 Finished semantics/ffi                                           22s 274MB
Nov 13 08:33:27 Starting semantics
Nov 13 08:36:08 Finished semantics                                             2m40s   1GB
Nov 13 08:36:08 Starting semantics/proofs
Nov 13 08:42:57 Finished semantics/proofs                                      6m48s   1GB
Nov 13 08:42:57 Starting semantics/alt_semantics
Nov 13 08:43:14 Finished semantics/alt_semantics                                 16s 328MB
Nov 13 08:43:14 Starting semantics/alt_semantics/proofs
Nov 13 08:47:15 Finished semantics/alt_semantics/proofs                        4m00s 793MB
Nov 13 08:47:15 Starting basis/pure
Nov 13 08:48:52 Finished basis/pure                                            1m37s 700MB
Nov 13 08:48:52 Starting translator
Nov 13 08:52:31 Finished translator                                            3m38s   1GB
Nov 13 08:52:31 Starting compiler/parsing
Nov 13 08:54:51 Finished compiler/parsing                                      2m19s   1GB
Nov 13 08:54:51 Starting characteristic
Nov 13 09:06:19 Finished characteristic                                       11m28s   1GB
Nov 13 09:06:20 Starting translator/monadic
Nov 13 09:09:33 Finished translator/monadic                                    3m13s   1GB
Nov 13 09:09:33 Starting basis
Nov 13 09:50:56 Finished basis                                                41m22s   3GB
Nov 13 09:50:56 Starting compiler/inference
Nov 13 09:54:33 Finished compiler/inference                                    3m36s   1GB
Nov 13 09:54:33 Starting compiler/backend/reg_alloc
Nov 13 09:56:26 Finished compiler/backend/reg_alloc                            1m52s   1GB
Nov 13 09:56:26 Starting compiler/backend/gc
Nov 13 10:02:23 Finished compiler/backend/gc                                   5m56s   1GB
Nov 13 10:02:23 Starting compiler/backend
Nov 13 10:09:18 Finished compiler/backend                                      6m54s   2GB
Nov 13 10:09:18 Starting compiler/encoders/asm
Nov 13 10:10:03 Finished compiler/encoders/asm                                   44s 578MB
Nov 13 10:10:03 Starting compiler/encoders/x64
Nov 13 10:10:57 Finished compiler/encoders/x64                                   53s 724MB
Nov 13 10:10:57 Starting compiler/encoders/arm7
Nov 13 10:12:47 Finished compiler/encoders/arm7                                1m50s 770MB
Nov 13 10:12:48 Starting compiler/encoders/arm8
Nov 13 10:13:14 Finished compiler/encoders/arm8                                  25s 793MB
Nov 13 10:13:14 Starting compiler/encoders/mips
Nov 13 10:13:49 Finished compiler/encoders/mips                                  34s   1GB
Nov 13 10:13:49 Starting compiler/encoders/riscv
Nov 13 10:14:17 Finished compiler/encoders/riscv                                 27s 737MB
Nov 13 10:14:17 Starting compiler/encoders/ag32
Nov 13 10:14:55 Finished compiler/encoders/ag32                                  37s 548MB
Nov 13 10:14:55 Starting compiler/backend/x64
Nov 13 10:15:32 Finished compiler/backend/x64                                    37s   1GB
Nov 13 10:15:32 Starting compiler/backend/arm7
Nov 13 10:16:11 Finished compiler/backend/arm7                                   38s   1GB
Nov 13 10:16:12 Starting compiler/backend/arm8
Nov 13 10:16:49 Finished compiler/backend/arm8                                   37s   1GB
Nov 13 10:16:49 Starting compiler/backend/mips
Nov 13 10:17:27 Finished compiler/backend/mips                                   37s   1GB
Nov 13 10:17:27 Starting compiler/backend/riscv
Nov 13 10:18:06 Finished compiler/backend/riscv                                  38s   1GB
Nov 13 10:18:06 Starting compiler/backend/ag32
Nov 13 10:20:26 Finished compiler/backend/ag32                                 2m19s   1GB
Nov 13 10:20:26 Starting compiler/parsing/proofs
Nov 13 10:32:34 Finished compiler/parsing/proofs                              12m07s 988MB
Nov 13 10:32:34 Starting compiler/inference/proofs
Nov 13 10:38:47 Finished compiler/inference/proofs                             6m11s   1GB
Nov 13 10:38:47 Starting compiler/backend/semantics
Nov 13 10:50:20 Finished compiler/backend/semantics                           11m33s   1GB
Nov 13 10:50:21 Starting compiler/backend/reg_alloc/proofs
Nov 13 10:57:45 Finished compiler/backend/reg_alloc/proofs                     7m23s   1GB
Nov 13 10:57:45 Starting compiler/backend/proofs
Nov 13 12:14:08 Finished compiler/backend/proofs                            1h16m22s   4GB
Nov 13 12:14:08 Starting compiler/encoders/x64/proofs
Nov 13 12:34:50 Finished compiler/encoders/x64/proofs                         20m41s   4GB
Nov 13 12:34:50 Starting compiler/encoders/arm7/proofs
Nov 13 13:02:53 Finished compiler/encoders/arm7/proofs                        28m02s   3GB
Nov 13 13:02:53 Starting compiler/encoders/arm8/proofs
Nov 13 13:17:01 Finished compiler/encoders/arm8/proofs                        14m07s   1GB
Nov 13 13:17:01 Starting compiler/encoders/mips/proofs
Nov 13 13:38:39 Finished compiler/encoders/mips/proofs                        21m37s   2GB
Nov 13 13:38:39 Starting compiler/encoders/riscv/proofs
Nov 13 13:57:28 Finished compiler/encoders/riscv/proofs                       18m48s   1GB
Nov 13 13:57:28 Starting compiler/encoders/ag32/proofs
Nov 13 14:02:51 Finished compiler/encoders/ag32/proofs                         5m22s 886MB
Nov 13 14:02:51 Starting compiler/backend/x64/proofs
Nov 13 14:03:29 Finished compiler/backend/x64/proofs                             38s   1GB
Nov 13 14:03:30 Starting compiler/backend/arm7/proofs
Nov 13 14:04:20 Finished compiler/backend/arm7/proofs                            50s 880MB
Nov 13 14:04:20 Starting compiler/backend/arm8/proofs
Nov 13 14:04:59 Finished compiler/backend/arm8/proofs                            38s   1GB
Nov 13 14:04:59 Starting compiler/backend/mips/proofs
Nov 13 14:05:36 Finished compiler/backend/mips/proofs                            37s 994MB
Nov 13 14:05:37 Starting compiler/backend/riscv/proofs
Nov 13 14:06:15 Finished compiler/backend/riscv/proofs                           38s   1GB
Nov 13 14:06:15 Starting compiler/backend/ag32/proofs
Nov 13 14:25:59 Finished compiler/backend/ag32/proofs                         19m43s   2GB
Nov 13 14:26:00 Starting compiler/proofs
Nov 13 14:29:33 Finished compiler/proofs                                       3m33s   2GB
Nov 13 14:29:34 Starting candle/set-theory
Nov 13 14:30:28 Finished candle/set-theory                                       53s 898MB
Nov 13 14:30:28 Starting candle/syntax-lib
Nov 13 14:30:50 Finished candle/syntax-lib                                       22s 684MB
Nov 13 14:30:50 Starting candle/standard/syntax
Nov 13 14:34:33 Finished candle/standard/syntax                                3m42s   1GB
Nov 13 14:34:33 Starting candle/standard/semantics
Nov 13 14:38:14 Finished candle/standard/semantics                             3m40s   1GB
Nov 13 14:38:14 Starting candle/standard/monadic
Nov 13 14:41:37 Finished candle/standard/monadic                               3m22s   1GB
Nov 13 14:41:37 Starting candle/standard/ml_kernel
Nov 13 14:50:00 Finished candle/standard/ml_kernel                             8m22s   6GB
Nov 13 14:50:00 Starting candle/standard/opentheory
Nov 13 15:08:46 Finished candle/standard/opentheory                           18m45s   3GB
Nov 13 15:08:46 Starting candle/standard/opentheory/compilation
Nov 13 16:09:34 Finished candle/standard/opentheory/compilation             1h00m47s  13GB
Nov 13 16:09:34 Starting candle/standard/opentheory/compilation/proofs
Nov 13 16:11:04 Finished candle/standard/opentheory/compilation/proofs         1m30s   2GB
Nov 13 16:11:05 Starting characteristic/examples
Nov 13 16:14:04 Finished characteristic/examples                               2m59s   2GB
Nov 13 16:14:04 Starting tutorial/solutions
Nov 13 16:43:39 Finished tutorial/solutions                                   29m34s   6GB
Nov 13 16:43:39 Starting translator/monadic/examples
Nov 13 16:48:56 Finished translator/monadic/examples                           5m15s   2GB
Nov 13 16:48:56 Starting examples
Nov 13 17:04:38 Finished examples                                             15m42s   4GB
Nov 13 17:04:38 Starting examples/compilation/x64
Nov 13 21:35:29 Finished examples/compilation/x64                           4h30m50s  12GB
Nov 13 21:35:29 Starting examples/compilation/x64/proofs
Nov 13 21:39:11 Finished examples/compilation/x64/proofs                       3m41s   2GB
Nov 13 21:39:11 Starting examples/compilation/ag32
Nov 13 22:42:32 Finished examples/compilation/ag32                          1h03m20s   7GB
Nov 13 22:42:32 Starting examples/compilation/ag32/proofs
Nov 13 22:44:07 Finished examples/compilation/ag32/proofs                      1m34s   3GB
Nov 13 22:44:07 Starting translator/okasaki-examples
Nov 13 22:52:22 Finished translator/okasaki-examples                           8m14s   1GB
Nov 13 22:52:22 Starting translator/other-examples
Nov 13 22:55:54 Finished translator/other-examples                             3m31s   1GB
Nov 13 22:55:54 Starting compiler/parsing/tests
Nov 13 22:56:51 Finished compiler/parsing/tests                                  56s 546MB
Nov 13 22:56:51 Starting compiler/inference/tests
Nov 13 23:05:24 Finished compiler/inference/tests                              8m32s   6GB
Nov 13 23:05:24 Starting compiler/bootstrap/translation
Nov 14 04:36:01 Finished compiler/bootstrap/translation                     5h30m36s  70GB
Nov 14 04:36:01 Starting unverified/sexpr-bootstrap/x64/64
Nov 14 05:01:24 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:  175s  user:  166s     OK
Starting work on cake.S
cake.S                                                                                                                                                                             real: 1326s  user: 1268s     OK
Starting work on cake
cake                                                                                                                                                                               real:   12s  user:    9sFAIL<2>
 cake.S:(.text+0x108f4ed): undefined reference to `ffiget_arg_count'
 /tmp/ccjicP9b.o: In function `windows_ffiwrite':
 cake.S:(.text+0x108f4fe): undefined reference to `ffiwrite'
 /tmp/ccjicP9b.o: In function `windows_ffiread':
 cake.S:(.text+0x108f50f): undefined reference to `ffiread'
 /tmp/ccjicP9b.o: In function `windows_ffi':
 cake.S:(.text+0x108f520): undefined reference to `ffi'
 collect2: error: ld returned 1 exit status
 make: *** [/root/regression/cakeml-1086/unverified/sexpr-bootstrap/x64/64/cake] Error 1
 <builtin>: recipe for target '/root/regression/cakeml-1086/unverified/sexpr-bootstrap/x64/64/cake' failed