在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可能用於演示目的。