ssreflect

Question

के लिए Coqide loadpath त्रुटि मैं एक Coq नौसिखिया हूँ और इसलिए सबूत जांच की मेरी समझ में सुधार करने के लिए मैं Ssreflect पुस्तकालय का उपयोग करने की कोशिश कर रहा हूँ।

मैंने मैक ओएस बनाम 10.10.3 (योसमेट) पर Ssreflect v 1.5 स्थापित किया है जो टर्मिनल पर चलता है।

Cannot find library ssreflect in loadpath 

मैं का उपयोग कर की कोशिश की है:

Add LoadPath "/opt/local/lib/coq/user-contrib/Ssreflect/". 

जहां

Require Import ssreflect. 

मैं त्रुटि मिलती है:

लेकिन जब मैं का उपयोग कर CoqIDE 8.4p15 में पुस्तकालय लोड करने का प्रयास SSRCOQ_LIB वर्तमान में सेट है, लेकिन मुझे त्रुटि मिलती है:

The file /opt/local/lib/coq/user-contrib/Ssreflect/ssreflect.vo contains library Ssreflect.ssreflect and not library ssreflect 

Coqide के भीतर से ssreflect लाइब्रेरी को लोड करने में किसी भी मदद के लिए आभारी।

Answer 1

Coq-Club Forum पर लोगों के लिए एक बड़ा धन्यवाद जिन्होंने इस समस्या में मदद की, और विशेष रूप से पियरे बोउटिलियर जिन्होंने समस्या के कारण को ठहराया और समाधान प्रदान किया।

• /opt/स्थानीय/bin/coqtop में एक (जो जहाँ मेरे नकल में शायद तुम्हारा स्थापित किया गया है फ़ोल्डर है:

  समस्या यह है कि मैं coqtop की 2 प्रतियां और मानक पुस्तकालयों में से 2 प्रतियां था एक अलग फ़ोल्डर) और ssreflect संकलित करने के लिए प्रयोग किया जाता है (I कॉक स्थापित करने के लिए मैकपोर्ट्स का उपयोग किया जाता है)।

• ऐप पर डबल क्लिक किए जाने पर कोक्वाइड द्वारा लोड किया गया है (I/cpqids_CoqIDE_8.4pl5.app/Resources/bin/coqtop में से एक (मैंने इसे कोग वेबसाइट से डाउनलोड किया है)।

इसलिए जब मैं CoqIDE में था यह एक है कि मैं संकलन और Ssreflect पुस्तकालय स्थापित करने के लिए प्रयोग किया जाता है की तुलना में coqtop के एक अलग संस्करण बुला रहा था।

समाधान निम्नलिखित है:

• CoqIDE पर डबल क्लिक करें
• ओपन CoqIDE मेनू में वरीयताओं
• सेट रूपरेखा -> coqtop (या यह हो सकता है ऑटो) के लिए "/ opt/स्थानीय/बिन/coqtop "(या जहां भी आपका संस्करण स्थापित है) ठीक है लागू करें।
• बाहर निकलें और कोक्वाइड को पुनरारंभ करें।

मैं सफलतापूर्वक Ssreflect पुस्तकालय दोनों लोड टर्मिनल और CoqIDE में coqtop का उपयोग कर का उपयोग करते हुए:

Require Import ssreflect.