CakeML:7f9f024bedaa89b1dd3bd371cf03ced2ab8310c1 Adjust data_to_word to fit syntactic criteria #366 (i2w_w2i_32bit)Merging into:c382040c6f947d8309996fbbb2d23912b8a00cf4 Fix riscv to_dataBootstrap - main prog renamedHOL:adf95fed567e76641363a906871d9110e3d12f71 Useful functions for dealing with terms up-to aconvMachine:cse-gmeza 4.13.10-200.fc26.x86_64 x86_64 GNU/Linux Claimed job Starting semantics/ffi Finished semantics/ffi 9s 0kB Starting semantics Finished semantics 1m09s 0kB Starting semantics/proofs Finished semantics/proofs 1m47s 0kB Starting basis/pure Finished basis/pure 34s 0kB Starting translator Finished translator 3m41s 0kB Starting compiler/parsing Finished compiler/parsing 1m25s 0kB Starting characteristic Finished characteristic 2m11s 0kB Starting basis Finished basis 15m03s 0kB Starting translator/monadic Finished translator/monadic 1m44s 0kB Starting compiler/inference Finished compiler/inference 1m13s 0kB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 24s 0kB Starting compiler/backend/gc Finished compiler/backend/gc 7m10s 0kB Starting compiler/backend Finished compiler/backend 3s 0kB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 0kB Starting compiler/encoders/x64 Finished compiler/encoders/x64 13s 0kB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 46s 0kB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 7s 0kB Starting compiler/encoders/mips Finished compiler/encoders/mips 9s 0kB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 8s 0kB Starting compiler/backend/x64 Finished compiler/backend/x64 24s 0kB Starting compiler/backend/arm6 Finished compiler/backend/arm6 24s 0kB Starting compiler/backend/arm8 Finished compiler/backend/arm8 24s 0kB Starting compiler/backend/mips Finished compiler/backend/mips 23s 0kB Starting compiler/backend/riscv Finished compiler/backend/riscv 25s 0kB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 5m57s 0kB Starting compiler/inference/proofs Finished compiler/inference/proofs 2m14s 0kB Starting compiler/backend/semantics FAILED: compiler/backend/semantics ]0;Holmake: ..Recursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/multiword ]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/multiwordRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/hoare-triple ]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/hoare-triple]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/hoare-triple ]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/multiword]0;Holmake: ~/PhD/cake/regression/HOL/examples/machine-code/multiwordFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/machine-code/multiword ]0;Holmake: ..Recursively calling Holmake in ../../../basis/pure ]0;Holmake: ../../../basis/pureRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/regular ]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/balanced_bst ]0;Holmake: ~/PhD/cake/regression/HOL/examples/balanced_bst]0;Holmake: ~/PhD/cake/regression/HOL/examples/balanced_bstFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/balanced_bst ]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages ]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languagesFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages ]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/context-free ]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/context-free]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/context-freeFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/context-free ]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regular]0;Holmake: ~/PhD/cake/regression/HOL/examples/formal-languages/regularStarting work on regexp2dfa regexp2dfa OK Finished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/formal-languages/regular ]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc ]0;Holmake: ../../../miscRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lub ]0;Holmake: ~/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/fun-op-sem/lprefix_lub ]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: ../../../basis/pure]0;Holmake: ../../../basis/pureFinished recursive invocation in ../../../basis/pure ]0;Holmake: ..Recursively calling Holmake in ../reg_alloc ]0;Holmake: ../reg_allocRecursively calling Holmake in ../../../unverified/reg_alloc ]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocFinished recursive invocation in ../../../unverified/reg_alloc ]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocFinished recursive invocation in ../reg_alloc ]0;Holmake: ..Recursively calling Holmake in ../../encoders ]0;Holmake: ../../encoders]0;Holmake: ../../encodersFinished recursive invocation in ../../encoders ]0;Holmake: ..Recursively calling Holmake in ../../encoders/asm ]0;Holmake: ../../encoders/asmRecursively calling Holmake in /home/agomezl/PhD/cake/regression/HOL/examples/l3-machine-code/common ]0;Holmake: ~/PhD/cake/regression/HOL/examples/l3-machine-code/common]0;Holmake: ~/PhD/cake/regression/HOL/examples/l3-machine-code/commonFinished recursive invocation in /home/agomezl/PhD/cake/regression/HOL/examples/l3-machine-code/common ]0;Holmake: ../../encoders/asmRecursively 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: ../../encoders/asm]0;Holmake: ../../encoders/asmFinished recursive invocation in ../../encoders/asm ]0;Holmake: ..]0;Holmake: ..Finished recursive invocation in .. ]0;Holmake: .Recursively calling Holmake in ../../../semantics/proofs ]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsFinished recursive invocation in ../../../semantics/proofs ]0;Holmake: .]0;Holmake: .Starting work on closSemTheory Starting work on conSemTheory Starting work on exhSemTheory Starting work on targetSemTheory targetSemTheory OK Starting work on wordSemTheory conSemTheory OK Starting work on conPropsTheory exhSemTheory OK Starting work on decSemTheory closSemTheory OK Starting work on bvlSemTheory decSemTheory OK Starting work on closPropsTheory wordSemTheory OK Starting work on labSemTheory bvlSemTheory OK Starting work on bviSemTheory labSemTheory FAILED! <1> pattern completion has added 2 clauses to the original specification.>> <<HOL message: mk_functional: pattern completion has added 4 clauses to the original specification.>> <<HOL message: mk_functional: pattern completion has added 3 clauses to the original specification.>> Saved definition __ "evaluate_def" Saved induction ___ "evaluate_ind" Saved definition __ "semantics_def" Exporting theory "labSem" ... done. Theory "labSem" took 9.4s to build conPropsTheory M-KILLED closPropsTheory M-KILLED bviSemTheory M-KILLED