Job 104

CakeML:d1468029c35ade0de3ab7e1dc536932c76d6ebb7
  Remove last cheats in new RatProg [Dec 21 23:13:38]
#413 (mlrat-as-real)
Merging into:5a615647a8e5d50d633b288acd22eb2e8b580f37
  Include stdlib explicitly in basis_ffi [Dec 14 00:19:23]
HOL:cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a
  Merge pull request #502 from marioxcc/master [Dec 21 04:20:24]
Machine:cakeml1853 4.4.0-22-generic x86_64 GNU/Linux

Dec 22 06:43:10 Claimed job
Dec 22 06:43:19 Building HOL
Dec 22 06:56:00 Starting semantics/ffi
Dec 22 06:57:09 Finished semantics/ffi                                         1m07s 366MB
Dec 22 06:57:11 Starting semantics
Dec 22 06:59:56 Finished semantics                                             2m43s   1GB
Dec 22 06:59:58 Starting semantics/proofs
Dec 22 07:03:35 Finished semantics/proofs                                      3m34s   1GB
Dec 22 07:03:37 Starting basis/pure
Dec 22 07:09:43 Finished basis/pure                                            6m04s 623MB
Dec 22 07:09:45 Starting translator
Dec 22 07:17:06 Finished translator                                            7m19s   1GB
Dec 22 07:17:08 Starting compiler/parsing
Dec 22 07:19:35 Finished compiler/parsing                                      2m24s   2GB
Dec 22 07:19:37 Starting characteristic
Dec 22 07:24:26 Finished characteristic                                        4m47s   1GB
Dec 22 07:24:28 Starting basis
Dec 22 07:32:16 FAILED: basis
]0;Holmake: pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/formal-languages/regular
]0;Holmake: pureRecursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a/examples/machine-code/hoare-triple
]0;Holmake: ../miscRecursively calling Holmake in ../developers
]0;Holmake: ../developers]0;Holmake: ../developersFinished recursive invocation in ../developers
]0;Holmake: ../miscRecursively calling Holmake in ../misc/lem_lib_stub
]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stubFinished recursive invocation in ../misc/lem_lib_stub
]0;Holmake: ../misc]0;Holmake: ../miscFinished recursive invocation in ../misc
]0;Holmake: pure]0;Holmake: pureFinished recursive invocation in pure
]0;Holmake: .Recursively calling Holmake in ../characteristic
]0;Holmake: ../characteristicRecursively calling Holmake in ../compiler/parsing
]0;Holmake: ../compiler/parsingRecursively calling Holmake in ../semantics
]0;Holmake: ../semanticsRecursively calling Holmake in ../semantics/ffi
]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffiFinished recursive invocation in ../semantics/ffi
]0;Holmake: ../semantics]0;Holmake: ../semanticsFinished recursive invocation in ../semantics
]0;Holmake: ../compiler/parsing]0;Holmake: ../compiler/parsingFinished recursive invocation in ../compiler/parsing
]0;Holmake: ../characteristicRecursively calling Holmake in ../semantics/alt_semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofsRecursively calling Holmake in ../semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semanticsFinished recursive invocation in ../semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics/proofsRecursively calling Holmake in ../semantics/proofs
]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsFinished recursive invocation in ../semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofsFinished recursive invocation in ../semantics/alt_semantics/proofs
]0;Holmake: ../characteristicRecursively calling Holmake in ../translator
]0;Holmake: ../translator]0;Holmake: ../translatorFinished recursive invocation in ../translator
]0;Holmake: ../characteristic]0;Holmake: ../characteristicFinished recursive invocation in ../characteristic
]0;Holmake: .]0;Holmake: .Starting work on RuntimeProgTheory
Starting work on clFFITheory
Starting work on fsFFITheory
Starting work on basis_ffi.o
basis_ffi.o                                                                  OK
clFFITheory                                                                  OK
fsFFITheory                                                                  OK
Starting work on fsFFIPropsTheory
RuntimeProgTheory                                                            OK
Starting work on OptionProgTheory
OptionProgTheory                                                             OK
Starting work on ListProgTheory
fsFFIPropsTheory                                                             OK
ListProgTheory                                                               OK
Starting work on VectorProgTheory
Starting work on ListProofTheory
ListProofTheory                                                              OK
VectorProgTheory                                                             OK
Starting work on StringProgTheory
StringProgTheory                                                             OK
Starting work on mlbasicsProgTheory
mlbasicsProgTheory                                                           OK
Starting work on IntProgTheory
IntProgTheory                                                                OK
Starting work on RatProgTheory
RatProgTheory                                                       FAILED! <1>
 /scratch/cakeml/regression/cakeml-104/basis/RatProgScript.sml:35: error: Value or constructor (real_of_int_le) has not been declared in structure intrealTheory
 Found near
   [
      GSYM intrealTheory.real_of_int_num,
      GSYM intrealTheory.real_of_int_mul,
      intrealTheory.real_of_int_le,
      GSYM rat_of_int_of_num,
      rat_of_int_MUL,
      ...
      ]