मैंने लिनक्स में सफलतापूर्वक कोक 8.6 और कोक्वाइड स्थापित किया है (उबंटू 17.04)। हालांकि, मुझे इस स्थापना में SSReflect और MathComp जोड़ने के लिए आगे बढ़ना नहीं है। मेरे द्वारा चेक किए गए सभी संदर्भ मुझे बहुत भ्रमित लगते थे। क्या किसी के पास सीधी और सरल नुस्खा है? मेरे पास ओपेम स्थापित है।लिनक्स में एसएसआरफलेक्ट और मैथकंप स्थापित करने के लिए कैसे?
मैं उबंटू 16.04 पर हूं। के एक कदम पीछे जाएं और OPAM स्थापित करके शुरू करते हैं:
$ sudo apt update && sudo apt install opam
$ opam --version
1.2.2
$ opam init # agree to modify your dot-files
$ eval `opam config env`
$ ocamlc -version
4.02.3
इसके बाद, आप उबंटू बहुत पुराने OCaml संस्करण से अधिक नया एक के लिए स्विच कर सकते हैं। यह चरण वैकल्पिक है और इसमें लगभग 10 मिनट लगते हैं।
$ opam switch 4.04.1
$ eval `opam config env`
$ ocamlc -version
4.04.1
अब, चलो गणित कंप्यूटर अनुप्रयोग स्थापित करने के लिए सक्षम होने के लिए निम्नलिखित डेटा संग्रह स्थान जुड़ करते हैं:
$ opam repo add coq-released https://coq.inria.fr/opam/released
और अंत में, ssreflect स्थापित:
$ opam install coq-mathcomp-ssreflect
OPAM निर्भरता पता लगाना होगा (Coq सहित), हमने जो पूछा है उसे डाउनलोड और इंस्टॉल करें!
यह पूरी तरह से काम किया, बहुत बहुत धन्यवाद! अब मैं देख सकता हूं कि सब कुछ सही संस्करण के साथ स्थापित है। हालांकि, जब भी मैं अपनी स्क्रिप्ट में "आयात ssreflect की आवश्यकता है" लिखता हूं, तो मुझे अभी भी त्रुटि संदेश मिलते हैं: "लाइब्रेरी ssreflect का पता लगाने में असमर्थ"। कुछ अभी भी गायब है, यह क्या हो सकता है इसका कोई विचार? – Marcus
यह गणित नामस्थान के अंतर्गत है: उदा। 'Mathcomp.ssreflect.all_ssreflect. आयात करें' या 'मैथकंप से आयात करें ssreflect.all_ssreflect.' आयात करें या (अगर हम केवल कुछ मूलभूत सामग्री आयात करना चाहते हैं)' mathcomp.ssreflect से आयात करें ssreflect ssrnat ssrbool eqtype। –
धन्यवाद, लेकिन मुझे अभी भी संदेश मिल गया है "त्रुटि: तार्किक पथ मिलान प्रत्यय <> और mfcomp.ssreflect" के लिए भौतिक पथ नहीं मिला है, और तीसरे मामले में, और अन्य दो के लिए समान संदेश। – Marcus
पूर्णता के लिए, वैकल्पिक विकल्प the Nix package manager (ओपेम के बजाय) का उपयोग करके किया जाता है। यह (curl https://nixos.org/nix/install | sh) स्थापित करने के बाद, आप निम्न कमांड के साथ गणित-कॉम्प के साथ एक CoqIDE उपलब्ध शुरू कर सकते हैं:
nix-shell -p coqPackages_8_6.mathcomp --run coqide
तो फिर तुम सिर्फ अपनी फ़ाइल From mathcomp Require Import ssreflect.
वाह, इतना आसान! बीटीडब्ल्यू, निक्स को स्थापित करने के बाद मुझे 'रन' करना पड़ा। 'Nix-shell 'निष्पादित करने में सक्षम होने के लिए $ HOME/.nix-profile/etc/profile.d/nix.sh'। –
ऐसा लगता है कि इस मामले में निक्स ने कोक 8.4pl6 स्थापित किया, इसलिए 'से ...' काम नहीं करता है। क्या हालिया संस्करण स्थापित करने का कोई तरीका है?(आम तौर पर, मै मैकोज़ पर हूं यदि यह मायने रखता है)। 'nix-shell' संस्करण 1.11.9 है। –
@AntonTrunov क्षमा करें मैंने यह सुनिश्चित करने के लिए आदेश तय किया है कि Coq 8.6 स्थापित संस्करण है। –
साथ 'OPAM स्थापित करता है Coq-mathcomp-ssreflect शुरू कर सकते हैं काम नहीं करते? –
नहीं। मुझे त्रुटि संदेश मिलता है "कोई पैकेज नामक coq-mathcomp-ssreflect नहीं मिला"। वैसे, क्या मुझे इन पैकेजों को अपने आप डाउनलोड करना है? मैं उन्हें कहां प्राप्त कर सकता हूं? – Marcus
यदि मैं अलग से प्रयास करता हूं, तो ओपम कहता है कि coq पहले से स्थापित है और मैथकंप और ssreflect नहीं मिला था। – Marcus