CakeML:a580584f6755d3b703b68a58783047045206ff81 Merge branch 'master' into term-not-eqtype #361 (term-not-eqtype)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 1m12s 0kB Starting semantics/proofs Finished semantics/proofs 1m56s 0kB Starting basis/pure Finished basis/pure 35s 0kB Starting translator Finished translator 3m53s 0kB Starting compiler/parsing Finished compiler/parsing 1m38s 0kB Starting characteristic Finished characteristic 2m14s 0kB Starting basis Finished basis 15m58s 0kB Starting translator/monadic Finished translator/monadic 2m00s 0kB Starting compiler/inference Finished compiler/inference 1m21s 0kB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 26s 0kB Starting compiler/backend/gc FAILED: compiler/backend/gc ]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/asmStarting work on asmTheory asmTheory OK Starting work on asmSemTheory asmSemTheory OK Starting work on asmPropsTheory asmPropsTheory OK Finished recursive invocation in ../../encoders/asm ]0;Holmake: ..]0;Holmake: ..Starting work on heap heap OK Starting work on backend_commonTheory Starting work on db_varsTheory Starting work on decLangTheory Starting work on jsonLangTheory decLangTheory OK Starting work on labLangTheory backend_commonTheory OK Starting work on closLangTheory jsonLangTheory OK Starting work on modLangTheory labLangTheory OK Starting work on stackLangTheory db_varsTheory OK Starting work on lab_filterTheory lab_filterTheory OK Starting work on lab_to_targetTheory closLangTheory OK Starting work on bviTheory modLangTheory OK Starting work on dataLangTheory stackLangTheory OK Starting work on bvlTheory bviTheory OK Starting work on bvi_letTheory dataLangTheory OK Starting work on data_liveTheory bvlTheory OK Starting work on data_simpTheory bvi_letTheory OK Starting work on data_spaceTheory data_simpTheory OK Starting work on bvi_tailrecTheory lab_to_targetTheory OK Starting work on bvl_constTheory data_liveTheory FAILED! <1> pattern completion has added 26 clauses to the original specification.>> Saved theorem _____ "is_pure_pmatch" <<HOL warning: GrammarDeltas.revise_data: Grammar-deltas: overload_on("compile_tupled") invalidated by DelConstant(data_live$compile_tupled)>> Saved definition __ "compile_def" Saved induction ___ "compile_ind" Exporting theory "data_live" ... done. Theory "data_live" took 5.3s to build data_spaceTheory M-KILLED bvi_tailrecTheory M-KILLED bvl_constTheory M-KILLED Finished recursive invocation in .. ]0;Holmake: .