Overview

Job 104

CakeML:d1468029c35ade0de3ab7e1dc536932c76d6ebb7
  Remove last cheats in new RatProg
#413 (mlrat-as-real)
Merging into:5a615647a8e5d50d633b288acd22eb2e8b580f37
  Include stdlib explicitly in basis_ffi
HOL:cdc248766a858dd0feedabaf5fc7a0a8d8ddc83a
  Merge pull request #502 from marioxcc/master
Machine:cakeml1853 4.4.0-22-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting semantics/ffi
 Finished semantics/ffi                                         1m07s 366MB
 Starting semantics
 Finished semantics                                             2m43s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m34s   1GB
 Starting basis/pure
 Finished basis/pure                                            6m04s 623MB
 Starting translator
 Finished translator                                            7m19s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m24s   2GB
 Starting characteristic
 Finished characteristic                                        4m47s   1GB
 Starting basis
 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,
      ...
      ]