Job 2603

CakeML:e4a5d6253daf10340cbac340ac36006df28b43c9
  Add missing README.md [Sep 13 15:24:23]
#1053 (dafny)
Merging into:7b614da7b56c9d04e55ecc20f0c22bdd8d7866e7
  Fix a broken proof [Sep 11 11:01:55]
HOL:7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361
  Fix bug in reduceLib.NOT_CONV [Sep 09 04:53:02]
Machine:pavlova

Sep 13 17:11:04 Claimed job
Sep 13 17:11:08 Reusing HOL
Sep 13 17:11:20 Starting developers
Sep 13 17:11:24 Finished developers                                               2s 223MB
Sep 13 17:11:25 Starting developers/bin
Sep 13 17:11:47 Finished developers/bin                                          20s   1GB
Sep 13 17:11:48 Starting compiler/proofs
Sep 13 18:59:43 Finished compiler/proofs                                    1h47m53s  44GB
Sep 13 18:59:44 Starting compiler/bootstrap/translation
Sep 14 03:59:18 Finished compiler/bootstrap/translation                     8h59m32s  90GB
Sep 14 03:59:19 Starting semantics/ffi
Sep 14 03:59:28 Finished semantics/ffi                                            8s 735MB
Sep 14 03:59:29 Starting semantics
Sep 14 03:59:31 Finished semantics                                                0s  64MB
Sep 14 03:59:31 Starting semantics/proofs
Sep 14 03:59:55 Finished semantics/proofs                                        22s 814MB
Sep 14 03:59:56 Starting semantics/alt_semantics
Sep 14 04:00:22 Finished semantics/alt_semantics                                 25s 657MB
Sep 14 04:00:23 Starting semantics/alt_semantics/proofs
Sep 14 04:10:35 Finished semantics/alt_semantics/proofs                       10m10s   2GB
Sep 14 04:10:36 Starting basis/pure
Sep 14 04:10:37 Finished basis/pure                                               0s  70MB
Sep 14 04:10:38 Starting translator
Sep 14 04:12:18 Finished translator                                            1m39s   4GB
Sep 14 04:12:19 Starting compiler/parsing
Sep 14 04:12:21 Finished compiler/parsing                                         0s  72MB
Sep 14 04:12:22 Starting characteristic
Sep 14 04:12:23 Finished characteristic                                           0s  91MB
Sep 14 04:12:24 Starting translator/monadic
Sep 14 04:12:26 Finished translator/monadic                                       0s  98MB
Sep 14 04:12:27 Starting basis
Sep 14 04:14:52 Finished basis                                                 2m23s   4GB
Sep 14 04:14:53 Starting compiler/inference
Sep 14 04:14:54 Finished compiler/inference                                       0s  93MB
Sep 14 04:14:55 Starting compiler/backend/reg_alloc
Sep 14 04:14:57 Finished compiler/backend/reg_alloc                               0s  65MB
Sep 14 04:14:58 Starting compiler/backend/gc
Sep 14 04:15:00 Finished compiler/backend/gc                                      1s 142MB
Sep 14 04:15:01 Starting compiler/backend
Sep 14 04:15:06 Finished compiler/backend                                         4s 363MB
Sep 14 04:15:07 Starting compiler/encoders/asm
Sep 14 04:15:09 Finished compiler/encoders/asm                                    0s  90MB
Sep 14 04:15:09 Starting compiler/encoders/x64
Sep 14 04:15:11 Finished compiler/encoders/x64                                    0s  98MB
Sep 14 04:15:12 Starting compiler/encoders/arm7
Sep 14 04:15:14 Finished compiler/encoders/arm7                                   0s  99MB
Sep 14 04:15:15 Starting compiler/encoders/arm8
Sep 14 04:15:16 Finished compiler/encoders/arm8                                   0s  96MB
Sep 14 04:15:17 Starting compiler/encoders/arm8_asl
Sep 14 06:33:18 Finished compiler/encoders/arm8_asl                         2h17m59s  41GB
Sep 14 06:33:19 Starting compiler/encoders/mips
Sep 14 06:33:20 Finished compiler/encoders/mips                                   0s  99MB
Sep 14 06:33:21 Starting compiler/encoders/riscv
Sep 14 06:33:23 Finished compiler/encoders/riscv                                  0s  99MB
Sep 14 06:33:24 Starting compiler/encoders/ag32
Sep 14 06:33:26 Finished compiler/encoders/ag32                                   0s  98MB
Sep 14 06:33:26 Starting compiler/backend/x64
Sep 14 06:33:28 Finished compiler/backend/x64                                     1s 137MB
Sep 14 06:33:29 Starting compiler/backend/arm7
Sep 14 06:33:31 Finished compiler/backend/arm7                                    1s 137MB
Sep 14 06:33:32 Starting compiler/backend/arm8
Sep 14 06:33:34 Finished compiler/backend/arm8                                    1s 137MB
Sep 14 06:33:35 Starting compiler/backend/mips
Sep 14 06:33:37 Finished compiler/backend/mips                                    1s 137MB
Sep 14 06:33:38 Starting compiler/backend/riscv
Sep 14 06:33:40 Finished compiler/backend/riscv                                   1s 137MB
Sep 14 06:33:41 Starting compiler/backend/ag32
Sep 14 06:35:03 Finished compiler/backend/ag32                                 1m21s   2GB
Sep 14 06:35:04 Starting compiler/parsing/proofs
Sep 14 06:35:06 Finished compiler/parsing/proofs                                  0s  72MB
Sep 14 06:35:07 Starting compiler/inference/proofs
Sep 14 06:35:08 Finished compiler/inference/proofs                                0s 100MB
Sep 14 06:35:09 Starting compiler/backend/semantics
Sep 14 06:38:21 Finished compiler/backend/semantics                            3m10s   2GB
Sep 14 06:38:22 Starting compiler/backend/reg_alloc/proofs
Sep 14 06:38:24 Finished compiler/backend/reg_alloc/proofs                        0s  93MB
Sep 14 06:38:25 Starting compiler/backend/proofs
Sep 14 06:39:19 Finished compiler/backend/proofs                                 53s   2GB
Sep 14 06:39:20 Starting compiler/backend/serialiser
Sep 14 06:39:22 Finished compiler/backend/serialiser                              1s 140MB
Sep 14 06:39:23 Starting compiler/encoders/x64/proofs
Sep 14 06:49:14 Finished compiler/encoders/x64/proofs                          9m50s   6GB
Sep 14 06:49:15 Starting compiler/encoders/arm7/proofs
Sep 14 07:02:31 Finished compiler/encoders/arm7/proofs                        13m14s  13GB
Sep 14 07:02:32 Starting compiler/encoders/arm8/proofs
Sep 14 07:09:34 Finished compiler/encoders/arm8/proofs                         7m01s   6GB
Sep 14 07:09:35 Starting compiler/encoders/arm8_asl/proofs
Sep 14 08:00:33 Finished compiler/encoders/arm8_asl/proofs                    50m56s   9GB
Sep 14 08:00:34 Starting compiler/encoders/mips/proofs
Sep 14 08:11:10 Finished compiler/encoders/mips/proofs                        10m35s   6GB
Sep 14 08:11:11 Starting compiler/encoders/riscv/proofs
Sep 14 08:20:09 Finished compiler/encoders/riscv/proofs                        8m56s   4GB
Sep 14 08:20:10 Starting compiler/encoders/ag32/proofs
Sep 14 08:23:12 Finished compiler/encoders/ag32/proofs                         3m00s   2GB
Sep 14 08:23:13 Starting compiler/backend/x64/proofs
Sep 14 08:24:01 Finished compiler/backend/x64/proofs                             47s   3GB
Sep 14 08:24:02 Starting compiler/backend/arm7/proofs
Sep 14 08:24:50 Finished compiler/backend/arm7/proofs                            47s   2GB
Sep 14 08:24:51 Starting compiler/backend/arm8/proofs
Sep 14 08:25:35 Finished compiler/backend/arm8/proofs                            43s   3GB
Sep 14 08:25:36 Starting compiler/backend/arm8_asl
Sep 14 08:26:09 Finished compiler/backend/arm8_asl                               31s   2GB
Sep 14 08:26:10 Starting compiler/backend/mips/proofs
Sep 14 08:27:01 Finished compiler/backend/mips/proofs                            49s   3GB
Sep 14 08:27:02 Starting compiler/backend/riscv/proofs
Sep 14 08:28:00 Finished compiler/backend/riscv/proofs                           57s   4GB
Sep 14 08:28:01 Starting compiler/backend/ag32/proofs
Sep 14 08:42:46 Finished compiler/backend/ag32/proofs                         14m43s   6GB
Sep 14 08:42:47 Starting compiler/backend/cv_compute
Sep 14 08:44:43 Finished compiler/backend/cv_compute                           1m54s   3GB
Sep 14 08:44:43 Starting cv_translator
Sep 14 09:05:15 Finished cv_translator                                        20m30s  12GB
Sep 14 09:05:16 Starting candle/set-theory
Sep 14 09:06:09 Finished candle/set-theory                                       51s   1GB
Sep 14 09:06:10 Starting candle/syntax-lib
Sep 14 09:06:11 Finished candle/syntax-lib                                        0s  72MB
Sep 14 09:06:12 Starting candle/standard/syntax
Sep 14 09:06:32 Finished candle/standard/syntax                                  19s   1GB
Sep 14 09:06:33 Starting candle/standard/semantics
Sep 14 09:09:28 Finished candle/standard/semantics                             2m54s   3GB
Sep 14 09:09:29 Starting candle/standard/monadic
Sep 14 09:09:31 Finished candle/standard/monadic                                  0s  99MB
Sep 14 09:09:32 Starting candle/standard/ml_kernel
Sep 14 09:11:41 Finished candle/standard/ml_kernel                             2m07s   5GB
Sep 14 09:11:41 Starting candle/overloading/syntax
Sep 14 09:15:29 Finished candle/overloading/syntax                             3m46s   2GB
Sep 14 09:15:30 Starting candle/overloading/semantics
Sep 14 09:27:19 Finished candle/overloading/semantics                         11m47s   4GB
Sep 14 09:27:20 Starting candle/overloading/monadic
Sep 14 09:30:00 Finished candle/overloading/monadic                            2m39s   2GB
Sep 14 09:30:01 Starting candle/overloading/ml_kernel
Sep 14 09:38:16 Finished candle/overloading/ml_kernel                          8m13s   7GB
Sep 14 09:38:17 Starting candle/overloading/ml_checker
Sep 14 09:41:06 Finished candle/overloading/ml_checker                         2m48s   7GB
Sep 14 09:41:07 Starting candle/prover
Sep 14 09:51:57 Finished candle/prover                                        10m49s   5GB
Sep 14 09:51:58 Starting pancake
Sep 14 09:52:26 Finished pancake                                                 27s 944MB
Sep 14 09:52:27 Starting pancake/ffi
Sep 14 09:52:28 Finished pancake/ffi                                              0s  22MB
Sep 14 09:52:29 Starting pancake/semantics
Sep 14 09:54:45 Finished pancake/semantics                                     2m15s   2GB
Sep 14 09:54:46 Starting pancake/parser
Sep 14 09:55:09 Finished pancake/parser                                          22s 804MB
Sep 14 09:55:10 Starting pancake/proofs
Sep 14 10:11:24 Finished pancake/proofs                                       16m12s   7GB
Sep 14 10:11:25 Starting compiler/dafny
Sep 14 10:13:54 Finished compiler/dafny                                        2m28s   7GB
Sep 14 10:13:55 Starting compiler/dafny/translation
Sep 14 10:42:28 Finished compiler/dafny/translation                           28m31s  15GB
Sep 14 10:42:29 Starting compiler/dafny/compilation
Sep 14 10:46:02 FAILED: compiler/dafny/compilation
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/cv_translator
Scanned 88 directories
Starting work on README.md
Starting work on dafny_compilerCompileTheory
README.md                                                           (0s)     OK
dafny_compilerCompileTheory                                       (189s)     OK
Starting work on dafny_compiler
dafny_compiler                                                      (0s)FAIL<1>
 /usr/bin/ld: NOTE: This behaviour is deprecated and will be removed in a future version of the linker
 /usr/bin/ld: /tmp/cchuKf5c.o: in function `ffidouble_pow':
 basis_ffi.c:(.text+0x911): undefined reference to `pow'
 /usr/bin/ld: /tmp/cchuKf5c.o: in function `ffidouble_ln':
 basis_ffi.c:(.text+0x959): undefined reference to `log'
 /usr/bin/ld: /tmp/cchuKf5c.o: in function `ffidouble_exp':
 basis_ffi.c:(.text+0x9a1): undefined reference to `exp'
 /usr/bin/ld: /tmp/cchuKf5c.o: in function `ffidouble_floor':
 basis_ffi.c:(.text+0x9e9): undefined reference to `floor'
 collect2: error: ld returned 1 exit status