এটি হল coqchk কমান্ড যা আমাদের একাধিক বিনামূল্যের অনলাইন ওয়ার্কস্টেশন যেমন উবুন্টু অনলাইন, ফেডোরা অনলাইন, উইন্ডোজ অনলাইন এমুলেটর বা MAC OS অনলাইন এমুলেটর ব্যবহার করে OnWorks ফ্রি হোস্টিং প্রদানকারীতে চালানো যেতে পারে।
কার্যক্রম:
NAME এর
coqchk - Coq প্রুফ চেকার সংকলিত লাইব্রেরি যাচাইকারী
সাইনোপিসিস
coqchk [ অপশন ] মডিউল
বর্ণনাঃ
coqchk কম্পাইল করা লাইব্রেরির স্বতন্ত্র পরীক্ষক (coqc দ্বারা উত্পাদিত .vo ফাইল)
Coq প্রুফ সহকারী। আরও তথ্যের জন্য রেফারেন্স ম্যানুয়াল দেখুন। এর সাথে ফিরে আসে
প্রস্থান কোড 0 যদি অনুরোধ করা সমস্ত কাজ সফল হয়। একটি অ-শূন্য রিটার্ন কোড মানে যে
কিছু ভুল হয়েছে: কিছু লাইব্রেরি পাওয়া যায়নি, দূষিত বিষয়বস্তু, টাইপ-চেকিং
ব্যর্থতা, ইত্যাদি
মডিউল চেক করা মডিউল একটি তালিকা. মডিউল একটি সংক্ষিপ্ত বা দ্বারা উল্লেখ করা যেতে পারে
যোগ্য নাম।
বিকল্প
-I হয়, --অন্তর্ভুক্ত Dir
ডিরেক্টরি যোগ করুন Dir অন্তর্ভুক্ত পাথ মধ্যে
-R Dir coqdir
recursively ম্যাপ শারীরিক Dir যৌক্তিকভাবে coqdir
- নীরব
coqchk কম শব্দচয়ন করে তোলে।
- স্বীকার করুন মডিউল
নির্দিষ্ট মডিউল এবং এর সমস্ত নির্ভরতাকে বিশ্বস্ত হিসাবে ট্যাগ করুন এবং হবে না
পুনঃচেক করা হয়েছে, যদি না অন্য বিকল্পগুলির দ্বারা স্পষ্টভাবে অনুরোধ করা হয়।
-নোরেক মডিউল
নির্দিষ্ট করে যে প্রদত্ত মডিউলটি যাচাই করার অনুরোধ না করেই যাচাই করা হবে
নির্ভরতা
-মি, --স্মৃতি
চেকার দ্বারা ব্যবহৃত মেমরির একটি সারাংশ প্রদর্শন করে।
-ও, --আউটপুট-প্রসঙ্গ
যৌক্তিক বিষয়বস্তুর একটি সারসংক্ষেপ প্রদর্শন করে যা যাচাই করা হয়েছে: অনুমান এবং
impredicativity ব্যবহার.
- অনুমানমূলক - সেট
চেকারকে এই পতাকার সাথে সংকলিত লাইব্রেরিগুলি গ্রহণ করার অনুমতি দেয়৷
-v coqchk সংস্করণ প্রিন্ট করুন এবং প্রস্থান করুন।
-কোক্লিব Dir
স্ট্যান্ডার্ড লাইব্রেরির ডিফল্ট অবস্থান ওভাররাইড করে।
-কোথায় coqchk স্ট্যান্ডার্ড লাইব্রেরি অবস্থান প্রিন্ট করুন এবং প্রস্থান করুন।
-হ, --help
বিকল্পগুলির তালিকা মুদ্রণ করুন
onworks.net পরিষেবা ব্যবহার করে অনলাইনে coqchk ব্যবহার করুন
