এটি coq-tex কমান্ড যা আমাদের একাধিক বিনামূল্যের অনলাইন ওয়ার্কস্টেশন যেমন উবুন্টু অনলাইন, ফেডোরা অনলাইন, উইন্ডোজ অনলাইন এমুলেটর বা MAC OS অনলাইন এমুলেটর ব্যবহার করে OnWorks ফ্রি হোস্টিং প্রদানকারীতে চালানো যেতে পারে।
কার্যক্রম:
NAME এর
coq-tex - LaTeX ফাইলগুলিতে এম্বেড করা Coq বাক্যাংশগুলি প্রক্রিয়া করুন
সাইনোপিসিস
coq-tex [ -o আউটপুট ফাইল ] [ -n লাইন প্রস্থ ] [ -মেজ coq-ইমেজ ] [ -w ] [ -v ] [ -sl ] [
-হরুল ] [ -ছোট ] ইনপুট ফাইল ...
বর্ণনাঃ
সার্জারির coq-tex ফিল্টার LaTeX ফাইলে এম্বেড করা Coq বাক্যাংশের নির্যাস, তাদের মূল্যায়ন করে এবং
প্রতিটি বাক্যাংশের পরে মূল্যায়নের ফলাফল সন্নিবেশ করান।
ইনপুট ফাইলগুলিতে Coq কোড অন্তর্ভুক্ত করার জন্য তিনটি LaTeX পরিবেশ প্রদান করা হয়েছে:
coq_উদাহরণ
\begin{coq_example} এবং \end{coq_example}-এর মধ্যে বাক্যাংশগুলি মূল্যায়ন করা হয় এবং
আউটপুট ফাইলে অনুলিপি করা হয়েছে। প্রতিটি শব্দগুচ্ছ এর প্রতিক্রিয়া দ্বারা অনুসরণ করা হয়
শীর্ষ স্তরের লুপ।
coq_example*
\begin{coq_example*} এবং \end{coq_example*}-এর মধ্যে বাক্যাংশগুলি মূল্যায়ন করা হয় এবং
আউটপুট ফাইলে অনুলিপি করা হয়েছে। টপলেভেল লুপের প্রতিক্রিয়া বাতিল করা হয়।
coq_eval
\begin{coq_eval} এবং \end{coq_eval} এর মধ্যে বাক্যাংশগুলিকে নীরবে মূল্যায়ন করা হয়৷
তারা আউটপুট ফাইলে কপি করা হয় না, এবং টপলেভেল লুপের প্রতিক্রিয়া
বাতিল করা হয়
ফলস্বরূপ LaTeX কোড ফাইলটিতে সংরক্ষণ করা হয় ফাইল.v.tex যদি ইনপুট ফাইলের একটি নাম থাকে
ফর্ম ফাইল.tex, অন্যথায় আউটপুট ফাইলের নাম ইনপুট ফাইলের নাম
সঙ্গে `.v.tex' যুক্ত।
দ্বারা উত্পাদিত ফাইল coq-tex LaTeX দ্বারা সরাসরি প্রক্রিয়া করা যেতে পারে। উভয় Coq বাক্যাংশ
এবং টপলেভেল আউটপুট টাইপরাইটার ফন্টে টাইপসেট।
বিকল্প
-o আউটপুট ফাইল
একটি ফাইলের নাম উল্লেখ করুন যেখানে LaTeX আউটপুট সংরক্ষণ করা হবে। একটি ড্যাশ `-'
LaTeX আউটপুটকে স্ট্যান্ডার্ড আউটপুটে প্রিন্ট করতে দেয়।
-n লাইন প্রস্থ
লাইনের প্রস্থ সেট করুন। ডিফল্ট 72টি অক্ষর। শীর্ষ স্তরের প্রতিক্রিয়া
লুপগুলি ভাঁজ করা হয় যদি সেগুলি লাইনের প্রস্থের চেয়ে দীর্ঘ হয়। কোন ভাঁজ উপর সঞ্চালিত হয়
Coq ইনপুট পাঠ্য।
-মেজ coq-ইমেজ
ফাইলের কারণ coq-ইমেজ Coq বাক্যাংশ মূল্যায়ন করার জন্য কার্যকর করা হবে। গতানুগতিক,
এই আদেশ কোকটপ মূল্যায়ন করতে ব্যবহৃত হয় এমন কোনো পথ উল্লেখ না করে
Coq বাক্যাংশ।
-w শব্দ কাটা এড়িয়ে যখনই সম্ভব একটি স্পেস ক্যারেক্টারের উপর লাইনগুলি ভাঁজ করার কারণ করুন
আউটপুটে ডিফল্টরূপে, শব্দ নির্বিশেষে, ভাঁজ লাইনের প্রস্থে ঘটে
কাটা।
-v ভার্বোস মোড। স্ট্যান্ডার্ড আউটপুটে Coq উত্তর প্রিন্ট করে। সনাক্ত করতে দরকারী
Coq বাক্যাংশে ত্রুটি।
-sl তির্যক মোড। Coq উত্তরগুলি একটি তির্যক ফন্টে লেখা হয়।
-হরুল অনুভূমিক লাইন মোড। Coq অংশ দুটি অনুভূমিক রেখার মধ্যে লেখা হয়।
-ছোট ছোট ফন্ট মোড। Coq অংশগুলি একটি ছোট ফন্টে লেখা হয়।
সতর্কতা
\begin... এবং \ end... বাক্যাংশগুলোকে অবশ্যই একটি লাইনে বসতে হবে, কোনো অক্ষর ছাড়াই
ব্যাকস্ল্যাশের আগে বা ক্লোজিং ব্রেসের পরে। প্রতিটি Coq বাক্যাংশের দ্বারা সমাপ্ত করা আবশ্যক৷
`।' একটি লাইনের শেষে। এর মধ্যে ফাঁকা স্থান গ্রহণ করা হয়।' এবং নতুন লাইন, কিন্তু যে কোনো
অন্যান্য অক্ষর coq-tex শব্দগুচ্ছের শেষ উপেক্ষা করবে, যার ফলে একটি
বাক্যাংশগুলিতে প্রতিক্রিয়াগুলির ভুল পরিবর্তন। (প্রতিক্রিয়াগুলি ''পিছিয়ে''।)
onworks.net পরিষেবা ব্যবহার করে coq-tex অনলাইন ব্যবহার করুন
