Overview

Job 1288

CakeML:7743179ad38f045d2fe295964a9c766e185bfca4
  Remove mentions of lcsymtacs (which no longer exists)
HOL:de873d08971c87bcfbbce86cdcd59909ef803929
  Remove some Unicode in src
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               0s  30MB
 Starting developers/bin
 Finished developers/bin                                           7s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                            8s 263MB
 Starting semantics
 FAILED: semantics
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Starting work on lem_list_extraTheory
Starting work on lem_set_extraTheory
Starting work on lem_stringTheory
Starting work on lem_string_extraTheory
lem_set_extraTheory                                                                                                                      real:    0s  user:    0s     OK
Starting work on byteTheory
lem_stringTheory                                                                                                                         real:    0s  user:    0s     OK
Starting work on addancs
addancs                                                                                                                                  real:    0s  user:    0s     OK
Starting work on astScript
astScript                                                                                                                                real:    0s  user:    0s     OK
Starting work on fpSemTheory
lem_string_extraTheory                                                                                                                   real:    2s  user:    2s     OK
Starting work on namespaceScript
namespaceScript                                                                                                                          real:    0s  user:    0s     OK
Starting work on namespaceTheory
lem_list_extraTheory                                                                                                                     real:    2s  user:    2s     OK
Starting work on tokensScript
tokensScript                                                                                                                             real:    0s  user:    0s     OK
Starting work on tokensTheory
byteTheory                                                                                                                               real:    2s  user:    2s     OK
Starting work on miscTheory
fpSemTheory                                                                                                                              real:    3s  user:    3s     OK
namespaceTheory                                                                                                                          real:    2s  user:    2s     OK
Starting work on astTheory
tokensTheory                                                                                                                             real:    4s  user:    3s     OK
Starting work on gramTheory
astTheory                                                                                                                                real:    8s  user:    8s     OK
Starting work on semanticPrimitivesTheory
gramTheory                                                                                                                               real:    9s  user:    9s     OK
miscTheory                                                                                                                               real:   15s  user:   14sFAIL<1>
      "num_to_hex_string_length_1",
      [
         QUOTE
         " (*#loc 1862 36*)\n   \226\136\128x. x < 16 \226\135\146 (LENGTH (num_to_hex_string x) = 1)"
         ],
      ... \\ ... \\ EVAL_TAC
      )
 error in quse /home/myreen/regression/cakeml-1288/misc/miscScript.sml : Fail "Static Errors"
 error in load /home/myreen/regression/cakeml-1288/misc/miscScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
semanticPrimitivesTheory                                                                                                                                         M-KILLED