在Linux上构建Isabelle ARM

Question

有人试图在Linux ARM上构建Isabelle吗？
我在armv7hl上安装了Fedora 21。 我能够建立纯粹的，但不是HOL。这似乎是一个记忆的问题，但我不确定。 有没有一种方法可以一步一步地构建它？ heaps/polyml-5.5.2_armv7l-linux的内容仅包含构建后的Pure。

更新：

ARM板

联想IdeaPadA10搭配1GB RAM
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平台 - 近年来伊莎贝尔的所有系统集成工作正朝86/x86_64的标准化。请注意，Poly/ML仅在ARM上解释，所以会稍微慢一点。

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