CakeML:5117c497e17a2887fe508122ef05a30613be0e1d Add Runtime module to basis (contains fullGC()) #369 (force-gc)Merging into:c382040c6f947d8309996fbbb2d23912b8a00cf4 Fix riscv to_dataBootstrap - main prog renamedHOL:adf95fed567e76641363a906871d9110e3d12f71 Useful functions for dealing with terms up-to aconvMachine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux Claimed job Building HOL Starting semantics/ffi Finished semantics/ffi 20s 237MB Starting semantics Finished semantics 2m17s 1GB Starting semantics/proofs Finished semantics/proofs 3m31s 1GB Starting basis/pure Finished basis/pure 1m08s 585MB Starting translator Finished translator 7m19s 1GB Starting compiler/parsing Finished compiler/parsing 2m26s 1GB Starting characteristic Finished characteristic 4m38s 2GB Starting basis Finished basis 29m20s 2GB Starting translator/monadic Finished translator/monadic 3m46s 1GB Starting compiler/inference Finished compiler/inference 2m17s 1GB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 48s 839MB Starting compiler/backend/gc Finished compiler/backend/gc 14m26s 2GB Starting compiler/backend Finished compiler/backend 1s 14MB Starting compiler/encoders/asm Finished compiler/encoders/asm 0s 11MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 29s 384MB Starting compiler/encoders/arm6 Finished compiler/encoders/arm6 1m24s 447MB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 15s 371MB Starting compiler/encoders/mips Finished compiler/encoders/mips 18s 409MB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 16s 457MB Starting compiler/backend/x64 Finished compiler/backend/x64 43s 1GB Starting compiler/backend/arm6 Finished compiler/backend/arm6 44s 1GB Starting compiler/backend/arm8 Finished compiler/backend/arm8 40s 920MB Starting compiler/backend/mips Finished compiler/backend/mips 43s 1GB Starting compiler/backend/riscv Finished compiler/backend/riscv 45s 1GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 4m51s 692MB Starting compiler/inference/proofs Finished compiler/inference/proofs 4m23s 1GB Starting compiler/backend/semantics Finished compiler/backend/semantics 19m22s 3GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 1m11s 343MB Starting compiler/backend/proofs Finished compiler/backend/proofs 1h11m42s 4GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 9m52s 1GB Starting compiler/encoders/arm6/proofs Finished compiler/encoders/arm6/proofs 11m35s 1GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 9m06s 1GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 12m35s 1GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 14m06s 1GB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 52s 1GB Starting compiler/backend/arm6/proofs Finished compiler/backend/arm6/proofs 58s 1GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 50s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 54s 1GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 56s 1GB Starting compiler/proofs Finished compiler/proofs 1m44s 1GB Starting candle/set-theory Finished candle/set-theory 50s 558MB Starting candle/syntax-lib Finished candle/syntax-lib 19s 548MB Starting candle/standard/syntax Finished candle/standard/syntax 3m03s 550MB Starting candle/standard/semantics Finished candle/standard/semantics 2m28s 839MB Starting candle/standard/monadic Finished candle/standard/monadic 2m48s 845MB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 11m58s 2GB Starting candle/standard/opentheory Finished candle/standard/opentheory 29s 709MB Starting characteristic/examples Finished characteristic/examples 2m05s 1GB Starting tutorial/solutions Finished tutorial/solutions 32m27s 8GB Starting examples Finished examples 8m43s 2GB Starting examples/compilation Finished examples/compilation 4h12m20s 14GB Starting examples/compilation/proofs Finished examples/compilation/proofs 5m29s 3GB Starting compiler/benchmarks Finished compiler/benchmarks 1h42m41s 14GB Starting translator/okasaki-examples Finished translator/okasaki-examples 7m38s 1GB Starting translator/other-examples Finished translator/other-examples 1m02s 836MB Starting compiler/parsing/tests Finished compiler/parsing/tests 41s 341MB Starting compiler/bootstrap/translation FAILED: compiler/bootstrap/translation ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/formal-languages/context-free ]0;Holmake: .Recursively calling Holmake in ../../../basis ]0;Holmake: ../../../basisRecursively calling Holmake in ../../../basis/pure ]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/formal-languages/regular ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/balanced_bst ]0;Holmake: /scratch/cakeml/worker/HOL/examples/balanced_bst]0;Holmake: /scratch/cakeml/worker/HOL/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/balanced_bst ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/formal-languages ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/formal-languages ]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/formal-languages/regular ]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc ]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lub ]0;Holmake: /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lub ]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/machine-code/hoare-triple ]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/worker/HOL/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: ../../../basis/pure]0;Holmake: ../../../basis/pureFinished recursive invocation in ../../../basis/pure ]0;Holmake: ../../../basisRecursively 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: ../../../basis]0;Holmake: ../../../basisFinished recursive invocation in ../../../basis ]0;Holmake: .Recursively calling Holmake in ../.. ]0;Holmake: ../..Recursively calling Holmake in ../../backend ]0;Holmake: ../../backendRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/machine-code/multiword ]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/multiwordFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/machine-code/multiword ]0;Holmake: ../../backendRecursively calling Holmake in ../../backend/reg_alloc ]0;Holmake: ../../backend/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: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_allocFinished recursive invocation in ../../backend/reg_alloc ]0;Holmake: ../../backendRecursively calling Holmake in ../../encoders ]0;Holmake: ../../encoders]0;Holmake: ../../encodersFinished recursive invocation in ../../encoders ]0;Holmake: ../../backendRecursively calling Holmake in ../../encoders/asm ]0;Holmake: ../../encoders/asmRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/common ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/commonFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/common ]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmFinished recursive invocation in ../../encoders/asm ]0;Holmake: ../../backend]0;Holmake: ../../backendFinished recursive invocation in ../../backend ]0;Holmake: ../..Recursively calling Holmake in ../../backend/arm6 ]0;Holmake: ../../backend/arm6Recursively calling Holmake in ../../encoders/arm6 ]0;Holmake: ../../encoders/arm6Recursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/model ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/lib ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/libFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/lib ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/modelFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/model ]0;Holmake: ../../encoders/arm6Recursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/step ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/stepRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-codeRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/machine-code/decompiler ]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/decompilerFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/machine-code/decompiler ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-codeFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/stepFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm/step ]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6Finished recursive invocation in ../../encoders/arm6 ]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6Finished recursive invocation in ../../backend/arm6 ]0;Holmake: ../..Recursively calling Holmake in ../../backend/arm8 ]0;Holmake: ../../backend/arm8Recursively calling Holmake in ../../encoders/arm8 ]0;Holmake: ../../encoders/arm8Recursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm8/model ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm8/modelFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm8/model ]0;Holmake: ../../encoders/arm8Recursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm8/step ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm8/stepFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/arm8/step ]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8Finished recursive invocation in ../../encoders/arm8 ]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8Finished recursive invocation in ../../backend/arm8 ]0;Holmake: ../..Recursively calling Holmake in ../../backend/mips ]0;Holmake: ../../backend/mipsRecursively calling Holmake in ../../encoders/mips ]0;Holmake: ../../encoders/mipsRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/mips/model ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/mips/modelFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/mips/model ]0;Holmake: ../../encoders/mipsRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/mips/step ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/mips/stepFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/mips/step ]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mipsFinished recursive invocation in ../../encoders/mips ]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mipsFinished recursive invocation in ../../backend/mips ]0;Holmake: ../..Recursively calling Holmake in ../../backend/riscv ]0;Holmake: ../../backend/riscvRecursively calling Holmake in ../../encoders/riscv ]0;Holmake: ../../encoders/riscvRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/riscv/model ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/riscv/modelFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/riscv/model ]0;Holmake: ../../encoders/riscvRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/riscv/step ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/riscv/stepFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/riscv/step ]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscvFinished recursive invocation in ../../encoders/riscv ]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscvFinished recursive invocation in ../../backend/riscv ]0;Holmake: ../..Recursively calling Holmake in ../../backend/x64 ]0;Holmake: ../../backend/x64Recursively calling Holmake in ../../encoders/x64 ]0;Holmake: ../../encoders/x64Recursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/x64/model ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/x64/modelFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/x64/model ]0;Holmake: ../../encoders/x64Recursively calling Holmake in /scratch/cakeml/worker/HOL/examples/l3-machine-code/x64/step ]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/worker/HOL/examples/l3-machine-code/x64/stepFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/l3-machine-code/x64/step ]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64Finished recursive invocation in ../../encoders/x64 ]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64Finished recursive invocation in ../../backend/x64 ]0;Holmake: ../..Recursively calling Holmake in ../../inference ]0;Holmake: ../../inferenceRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/unification/triangular/first-order ]0;Holmake: /scratch/cakeml/worker/HOL/examples/unification/triangular/first-orderRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/unification/triangular ]0;Holmake: /scratch/cakeml/worker/HOL/examples/unification/triangular]0;Holmake: /scratch/cakeml/worker/HOL/examples/unification/triangularFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/unification/triangular ]0;Holmake: /scratch/cakeml/worker/HOL/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/worker/HOL/examples/unification/triangular/first-orderFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/unification/triangular/first-order ]0;Holmake: ../../inference]0;Holmake: ../../inferenceFinished recursive invocation in ../../inference ]0;Holmake: ../..]0;Holmake: ../..Finished recursive invocation in ../.. ]0;Holmake: .Recursively calling Holmake in ../../backend/reg_alloc/proofs ]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofsFinished recursive invocation in ../../backend/reg_alloc/proofs ]0;Holmake: .Recursively calling Holmake in ../../inference/proofs ]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofsFinished recursive invocation in ../../inference/proofs ]0;Holmake: .]0;Holmake: .Starting work on heap heap OK Starting work on to_dataProgTheory to_dataProgTheory OK Starting work on lexerProgTheory lexerProgTheory OK Starting work on parserProgTheory parserProgTheory OK Starting work on inferProgTheory inferProgTheory FAILED! <1> Saved theorem _____ "infer_type_subst_v_thm" Translating count_list_aux Saved theorem _____ "nsLookup_auto_env_24" Saved theorem _____ "count_list_aux_v_thm" Translating count_list Saved theorem _____ "nsLookup_auto_env_25" Saved theorem _____ "count_list_v_thm" error in quse /scratch/cakeml/worker/cakeml/compiler/bootstrap/translation/inferProgScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"} error in load inferProgScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"} Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}