coqide.byte - ক্লাউডে অনলাইন

এটি coqide.byte কমান্ড যা আমাদের একাধিক বিনামূল্যের অনলাইন ওয়ার্কস্টেশন যেমন উবুন্টু অনলাইন, ফেডোরা অনলাইন, উইন্ডোজ অনলাইন এমুলেটর বা MAC OS অনলাইন এমুলেটর ব্যবহার করে OnWorks ফ্রি হোস্টিং প্রদানকারীতে চালানো যেতে পারে।

কার্যক্রম:

NAME এর


coqide - Coq প্রুফ সহকারী গ্রাফিকাল ইন্টারফেস

সাইনোপিসিস


coqide [ অপশন ]

বর্ণনাঃ


coqide Coq প্রমাণ সহকারীর জন্য একটি gtk গ্রাফিকাল ইন্টারফেস।

Coq-এর কমান্ড-লাইন-ভিত্তিক ব্যবহারের জন্য, দেখুন কোকটপ(1); Coq এর ব্যাচ-ভিত্তিক ব্যবহারের জন্য, দেখুন
coqc(1).

বিকল্প


-h দ্বারা গৃহীত বিকল্পগুলির সম্পূর্ণ তালিকা দেখান coqide.

-I Dir, -অন্তর্ভুক্ত Dir
অন্তর্ভুক্ত পাথে ডিরেক্টরি dir যোগ করুন।

-R Dir coqdir
পুনরাবৃত্তিমূলকভাবে শারীরিক মানচিত্র Dir যৌক্তিকভাবে coqdir.

-src অন্তর্ভুক্ত পাথে উত্স ডিরেক্টরি যোগ করুন।

-আই f, -ইনপুট স্টেট f
থেকে রাজ্য পড়ুন f.coq

-কোলাহল একটি খালি অবস্থা দিয়ে শুরু করুন।

-আউটপুট স্টেট f
ফাইলে রাজ্য লিখুন f.coq

-লোড-এমএল-অবজেক্ট f
ML অবজেক্ট ফাইল লোড করুন f.

-লোড-এমএল-উৎস f
ML ফাইল লোড করুন f.

-l f, -লোড-ভেরনাক-উৎস f
Coq ফাইল লোড করুন f.v (লোড f.).

-lv f, -লোড-ভেরনাক-উৎস-ভার্বোস f
Coq ফাইল লোড করুন f.v (লোড ভার্বোস f.).

-লোড-ভেরনাক-বস্তু f
Coq অবজেক্ট ফাইল লোড করুন f.vo

-প্রয়োজন f
Coq অবজেক্ট ফাইল লোড করুন f.vo এবং এটি আমদানি করুন (প্রয়োজন f.).

- কম্পাইল f
Coq ফাইল কম্পাইল করুন f.v (উচিত -ব্যাচ).

-সংকলন-ভার্বোস f
শব্দগতভাবে Coq ফাইল কম্পাইল f.v (উচিত -ব্যাচ).

-ও Coq বা Coq_SearchIsos-এর নেটিভ-কোড সংস্করণ চালান।

-বাইট Coq বা Coq_SearchIsos এর বাইটকোড সংস্করণ চালান।

-কোথায় Coq এর স্ট্যান্ডার্ড লাইব্রেরি অবস্থান প্রিন্ট করুন এবং প্রস্থান করুন।

-v Coq সংস্করণ প্রিন্ট করুন এবং প্রস্থান করুন।

-q rcfile লোড করা এড়িয়ে যান।

-init-ফাইল f
rcfile সেট করুন f.

-ব্যাচ ব্যাচ মোড (আর্গুমেন্ট পার্সিংয়ের পরেই প্রস্থান করে)।

-বুট বুট মোড (উচিত -q এবং -ব্যাচ).

- emacs Coq কে বলে যে এটি Emacs এর অধীনে কার্যকর করা হয়।

-ডাম্প-গ্লোব f
ফাইলে বিশ্বায়ন ডাম্প করুন f (এর দ্বারা ব্যবহার করা হবে coqdoc(1))।

- অনুমানমূলক - সেট
সেট বাছাই সেট impredicative.

-প্রমাণ-লোড করবেন না
মেমরিতে অস্বচ্ছ প্রমাণ লোড করবেন না।

-xml XML ফাইলগুলিকে হয় ডিরেক্টরিতে রুট করা অনুক্রমে রপ্তানি করুন
COQ_XML_LIBRARY_ROOT (যদি সেট থাকে) অথবা stdout (যদি সেট না থাকে)।

onworks.net পরিষেবা ব্যবহার করে অনলাইনে coqide.byte ব্যবহার করুন



সর্বশেষ লিনাক্স এবং উইন্ডোজ অনলাইন প্রোগ্রাম