在Linux ARM上构建Isabelle

Question

有人试图在Linux ARM上构建Isabelle吗？

我在armv7hl上有Fedora 21。我能造出纯粹，但不是HOL。这似乎是记忆的问题，但我不确定。有办法一步一步地建造它吗？堆/polyml-5.5.2_armv7l-Linux的内容只包含构建后的Pure。

更新：

臂板

联想1GB内存IdeaPadA10 Android版本4.2.2 内核3.0.36 Fedora 21使用chroot安装。

错误信息是：

* * * Failed to load theory "Inductive" (unresolved "Complete_Lattices")
* * * Failed to load theory "Product_Type" (unresolved "Inductive")
* * * Failed to load theory "Sum_Type" (unresolved "Inductive")
* * * Failed to load theory "Complete_Partial_Order" (unresolved "Product_Type")
* * * Failed to load theory "Nat" (unresolved "Inductive")
* * * Failed to load theory "Datatype" (unresolved "Nat", "Product_Type", "Sum_Type")
* * * Failed to load theory "Finite_Set" (unresolved "Nat", "Product_Type", "Sum_Type")
* * * Failed to load theory "Meson" (unresolved "Nat")
* * * Failed to load theory "ATP" (unresolved "Meson")
* * * Failed to load theory "Metis" (unresolved "ATP")
* * * Failed to load theory "Groups_Big" (unresolved "Finite_Set")
* * * Failed to load theory "Relation" (unresolved "Finite_Set")
* * * Failed to load theory "Transitive_Closure" (unresolved "Relation")
* * * Failed to load theory "Wellfounded" (unresolved "Transitive_Closure")
* * * Failed to load theory "Fun_Def_Base" (unresolved "Wellfounded")
* * * Failed to load theory "Wfrec" (unresolved "Wellfounded")
* * * Failed to load theory "Order_Relation" (unresolved "Wfrec")
* * * Failed to load theory "Equiv_Relations" (unresolved "Groups_Big", "Relation")
* * * Failed to load theory "Hilbert_Choice" (unresolved "Nat", "Wellfounded")
* * * Failed to load theory "BNF_Wellorder_Relation" (unresolved "Order_Relation")
* * * Failed to load theory "BNF_Wellorder_Embedding" (unresolved "BNF_Wellorder_Relation", "Hilbert_Choice")
* * * Failed to load theory "BNF_Constructions_on_Wellorders" (unresolved "BNF_Wellorder_Embedding")
* * * Failed to load theory "Zorn" (unresolved "Hilbert_Choice", "Order_Relation")
* * * Failed to load theory "BNF_Cardinal_Order_Relation" (unresolved "BNF_Constructions_on_Wellorders", "Zorn")
* * * Failed to load theory "BNF_Cardinal_Arithmetic" (unresolved "BNF_Cardinal_Order_Relation")
* * * Failed to load theory "BNF_Def" (unresolved "BNF_Cardinal_Arithmetic", "Fun_Def_Base")
* * * Failed to load theory "BNF_Comp" (unresolved "BNF_Def")
* * * Failed to load theory "Basic_BNFs" (unresolved "BNF_Def")
* * * Failed to load theory "BNF_FP_Base" (unresolved "BNF_Comp", "Basic_BNFs")
* * * Failed to load theory "BNF_LFP" (unresolved "BNF_FP_Base")
* * * Failed to load theory "Num" (unresolved "BNF_LFP", "Datatype")
* * * Failed to load theory "Power" (unresolved "Equiv_Relations", "Num")
* * * Failed to load theory "Option" (unresolved "BNF_LFP", "Datatype", "Finite_Set")
* * * Failed to load theory "Extraction" (unresolved "Datatype", "Option")
* * * Failed to load theory "Lattices_Big" (unresolved "Finite_Set", "Option")
* * * Failed to load theory "Partial_Function" (unresolved "Complete_Partial_Order", "Fun_Def_Base", "Option")
* * * Failed to load theory "Transfer" (unresolved "BNF_FP_Base", "Hilbert_Choice", "Metis", "Option")
* * * Failed to load theory "Fun_Def" (unresolved "Partial_Function")
* * * Failed to load theory "Lifting" (unresolved "Equiv_Relations", "Transfer")
* * * Failed to load theory "Lifting_Option" (unresolved "Lifting", "Option")
* * * Failed to load theory "Lifting_Product" (unresolved "Basic_BNFs", "Lifting")
* * * Failed to load theory "Lifting_Set" (unresolved "Lifting")
* * * Failed to load theory "Lifting_Sum" (unresolved "Basic_BNFs", "Lifting")
* * * Failed to load theory "Quotient" (unresolved "Lifting")
* * * Failed to load theory "Int" (unresolved "Equiv_Relations", "Fun_Def", "Power", "Quotient")
* * * Failed to load theory "Nat_Transfer" (unresolved "Int")
* * * Failed to load theory "Divides" (unresolved "Nat_Transfer")
* * * Failed to load theory "Set_Interval" (unresolved "Lattices_Big", "Nat_Transfer")
* * * Failed to load theory "Numeral_Simprocs" (unresolved "Divides")
* * * Failed to load theory "Code_Numeral" (unresolved "Divides", "Lifting", "Nat_Transfer")
* * * Failed to load theory "SMT2" (unresolved "Divides")
* * * Failed to load theory "Semiring_Normalization" (unresolved "Nat_Transfer", "Numeral_Simprocs")
* * * Failed to load theory "Groebner_Basis" (unresolved "Semiring_Normalization")
* * * Failed to load theory "Presburger" (unresolved "Groebner_Basis", "Set_Interval")
* * * Failed to load theory "Sledgehammer" (unresolved "Presburger", "SMT2")
* * * Failed to load theory "List" (unresolved "Code_Numeral", "Lifting_Option", "Lifting_Product", "Lifting_Set", "Sledgehammer")
* * * Failed to load theory "Map" (unresolved "List")
* * * Failed to load theory "Random" (unresolved "List")
* * * Failed to load theory "Enum" (unresolved "Map")
* * * Failed to load theory "String" (unresolved "Enum")
* * * Failed to load theory "BNF_GFP" (unresolved "BNF_FP_Base", "String")
* * * Failed to load theory "Predicate" (unresolved "String")
* * * Failed to load theory "Lazy_Sequence" (unresolved "Predicate")
* * * Failed to load theory "Typerep" (unresolved "String")
* * * Failed to load theory "Limited_Sequence" (unresolved "Lazy_Sequence")
* * * Failed to load theory "Code_Evaluation" (unresolved "Limited_Sequence", "Typerep")
* * * Failed to load theory "Quickcheck_Random" (unresolved "Code_Evaluation", "Enum", "Random")
* * * Failed to load theory "Quickcheck_Exhaustive" (unresolved "Quickcheck_Random")
* * * Failed to load theory "Quickcheck_Narrowing" (unresolved "Quickcheck_Random")
* * * Failed to load theory "Record" (unresolved "Quickcheck_Exhaustive")
* * * Failed to load theory "Random_Pred" (unresolved "Quickcheck_Random")
* * * Failed to load theory "Random_Sequence" (unresolved "Random_Pred")
* * * Failed to load theory "Nitpick" (unresolved "Record")
* * * Failed to load theory "SMT" (unresolved "Record")
* * * Failed to load theory "Predicate_Compile" (unresolved "Quickcheck_Exhaustive", "Random_Sequence")
* * * Failed to load theory "Main" (unresolved "BNF_GFP", "Extraction", "Lifting_Sum", "Nitpick", "Predicate_Compile", "Quickcheck_Narrowing", "SMT")
* * * Failed to load theory "Archimedean_Field" (unresolved "Main")
* * * Failed to load theory "Conditionally_Complete_Lattices" (unresolved "Main")
* * * Failed to load theory "Fact" (unresolved "Main")
* * * Failed to load theory "Parity" (unresolved "Main")
* * * Failed to load theory "GCD" (unresolved "Fact", "Parity")
* * * Failed to load theory "Topological_Spaces" (unresolved "Conditionally_Complete_Lattices", "Main")
* * * Failed to load theory "Rat" (unresolved "Archimedean_Field", "GCD")
* * * Failed to load theory "Real" (unresolved "Conditionally_Complete_Lattices", "Rat")
* * * Failed to load theory "Real_Vector_Spaces" (unresolved "Real", "Topological_Spaces")
* * * Failed to load theory "Limits" (unresolved "Real_Vector_Spaces")
* * * Failed to load theory "Deriv" (unresolved "Limits")
* * * Failed to load theory "Series" (unresolved "Limits")
* * * Failed to load theory "NthRoot" (unresolved "Deriv", "Parity")
* * * Failed to load theory "Transcendental" (unresolved "Deriv", "Fact", "NthRoot", "Series")
* * * Failed to load theory "Complex" (unresolved "Transcendental")
* * * Failed to load theory "MacLaurin" (unresolved "Transcendental")
* * * Failed to load theory "Taylor" (unresolved "MacLaurin")
* * * Failed to load theory "Complex_Main" (unresolved "Complex", "Deriv", "Main", "Real", "Taylor", "Transcendental")
* * * Outer syntax error (line 984 of "~~/src/HOL/Complete_Lattices.thy"): keyword ")" expected,
* * * but identifier output (line 984 of "~~/src/HOL/Complete_Lattices.thy") was found
* * * At command "<malformed>" (line 984 of "~~/src/HOL/Complete_Lattices.thy")

Answer 1

我对ARM平台知之甚少--近年来，Isabelle的所有系统集成工作都标准化为x86/x86_64。请注意，Poly只在ARM上解释，所以它会有点慢。

此外，对于完全的Isabelle/HOL来说，这是一件非常重要的事情，您需要的不仅仅是1GB。我通常以4GB作为底线，尽管2GB可能用于演示目的。